α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ (_ : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a) ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ↑(piCongr h₁ h₂) f (↑h₁ a) = ↑(h₂ a) (f a)
change Eq.ndrec _ _ = _
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
hZa : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a
⊢ hZa ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ (_ : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a) ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
generalize_proofs hZa
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ∀ (hZa : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a), hZa ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
hZa : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a
⊢ hZa ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
revert hZa
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ∀ (hZa : ↑h₁.symm.symm a = ↑h₁ a), hZa ▸ ↑(piCongrRight h₂) f a = ↑(h₂ a) (f a)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ∀ (hZa : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a), hZa ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
rw [h₁.symm_apply_apply a]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ↑(piCongrRight h₂) f a = ↑(h₂ a) (f a)
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ∀ (hZa : ↑h₁.symm.symm a = ↑h₁ a), hZa ▸ ↑(piCongrRight h₂) f a = ↑(h₂ a) (f a)
simp
no goals
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ↑(piCongrRight h₂) f a = ↑(h₂ a) (f a)
rfl