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✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂
classical
funext x
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]
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✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * 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✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * 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✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]