no goals
I : Type u
α : Type u_3
β : Type u_2
γ : Type u_1
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
classical
funext x
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]
case h
I : Type u
α : Type u_3
β : Type u_2
γ : Type u_1
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
I : Type u
α : Type u_3
β : Type u_2
γ : Type u_1
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
funext x
no goals
case h
I : Type u
α : Type u_3
β : Type u_2
γ : Type u_1
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]