α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ (_ : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b) ▸
      ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) =
    ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ↑(piCongr' h₁ h₂).symm f (↑h₁.symm b) = ↑(h₂ b).symm (f b)
change Eq.ndrec _ _ = _
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
hWb : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b
⊢ hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) = ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ (_ : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b) ▸
      ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) =
    ↑(h₂ b).symm (f b)
generalize_proofs hWb
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ∀ (hWb : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b),
    hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) = ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
hWb : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b
⊢ hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) = ↑(h₂ b).symm (f b)
revert hWb
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b b' : β
hb : ↑h₁ (↑h₁.symm b) = b'
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b' = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b' = ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ∀ (hWb : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b),
    hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) = ↑(h₂ b).symm (f b)
generalize hb : h₁ (h₁.symm b) = b'
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b b' : β
hb : b = b'
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b' = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b' = ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b b' : β
hb : ↑h₁ (↑h₁.symm b) = b'
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b' = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b' = ↑(h₂ b).symm (f b)
rw [h₁.apply_symm_apply b] at hb
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b = ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b b' : β
hb : b = b'
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b' = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b' = ↑(h₂ b).symm (f b)
subst hb
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ↑(piCongrRight fun b => (h₂ b).symm) f b = ↑(h₂ b).symm (f b)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b = ↑(h₂ b).symm (f b)
simp
no goals
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ↑(piCongrRight fun b => (h₂ b).symm) f b = ↑(h₂ b).symm (f b)
rfl