[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → One (f i)
inst✝² : (i : I) → One (g i)
inst✝¹ : (i : I) → One (h i)
inst✝ : One β
i : I
x : β
i' : I
⊢ mulSingle i x i' = mulSingle i' x i
[PROOFSTEP]
simp [mulSingle_apply, eq_comm]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i
hf' : ∀ (i : I), f' i 1 = 1
i : I
x : f i
j : I
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j
[PROOFSTEP]
simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y✝ : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
x✝ y✝ : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
[PROOFSTEP]
subst h
[GOAL]
case pos
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y✝ : (i : I) → f i
i : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
j : I
x : f j
y : g j
⊢ f' j (mulSingle j x j) (mulSingle j y j) = mulSingle j (f' j x y) j
[PROOFSTEP]
simp only [mulSingle_eq_same]
[GOAL]
case neg
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
x✝ y✝ : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
[PROOFSTEP]
simp only [mulSingle_eq_of_ne h, hf']
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : One γ
f : α → β
x✝ : β
⊢ extend f 1 1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
apply ite_self
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
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₂
[PROOFSTEP]
classical
funext x
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (*) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· * ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
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₂
[PROOFSTEP]
funext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (*) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· * ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
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)⁻¹
[PROOFSTEP]
classical
funext x
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite has_inv.inv _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite Inv.inv _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
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)⁻¹
[PROOFSTEP]
funext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite has_inv.inv _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite Inv.inv _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
[PROOFSTEP]
classical
funext x
simp [Function.extend_def, apply_dite₂]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (/) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· / ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
[PROOFSTEP]
funext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f✝ i
i : I
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x
[PROOFSTEP]
simp [Function.extend_def, apply_dite₂]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (/) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· / ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α✝ : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
α : Type u_4
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ Pi.mulSingle i x j = x
[PROOFSTEP]
rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i✝ : I
a a' : α → γ
b b' : β → γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : α
c : γ
⊢ Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (inl i) c
[PROOFSTEP]
simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i✝ : I
a a' : α → γ
b b' : β → γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : β
c : γ
⊢ Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (inr i) c
[PROOFSTEP]
simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : α
⊢ Sum.elim (a * a') (b * b') (inl val✝) = (Sum.elim a b * Sum.elim a' b') (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : β
⊢ Sum.elim (a * a') (b * b') (inr val✝) = (Sum.elim a b * Sum.elim a' b') (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : α
⊢ Sum.elim (a / a') (b / b') (inl val✝) = (Sum.elim a b / Sum.elim a' b') (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : β
⊢ Sum.elim (a / a') (b / b') (inr val✝) = (Sum.elim a b / Sum.elim a' b') (inr val✝)
[PROOFSTEP]
rfl
