[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Semigroup (f i)
⊢ ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝ * c✝) x✝ = (a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
exact mul_assoc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → CommSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
⊢ ∀ (a b : (i : I) → f i), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → CommSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ : (i : I) → f i
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → CommSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝) x✝ = (b✝ * a✝) x✝
[PROOFSTEP]
exact mul_comm _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (1 * a✝) x✝ = a✝ x✝
[PROOFSTEP]
exact one_mul _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * 1) x✝ = a✝ x✝
[PROOFSTEP]
exact mul_one _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvOneClass (f i)
⊢ 1⁻¹ = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvOneClass (f i)
⊢ 1⁻¹ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvOneClass (f i)
x✝ : I
⊢ 1⁻¹ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact inv_one
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
⊢ ∀ (x : (i : I) → f i), (fun n x i => x i ^ n) 0 x = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
x✝ : (i : I) → f i
⊢ (fun n x i => x i ^ n) 0 x✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
x✝¹ : (i : I) → f i
x✝ : I
⊢ (fun n x i => x i ^ n) 0 x✝¹ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact Monoid.npow_zero _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
⊢ ∀ (n : ℕ) (x : (i : I) → f i), (fun n x i => x i ^ n) (n + 1) x = x * (fun n x i => x i ^ n) n x
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
n✝ : ℕ
x✝ : (i : I) → f i
⊢ (fun n x i => x i ^ n) (n✝ + 1) x✝ = x✝ * (fun n x i => x i ^ n) n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Monoid (f i)
src✝¹ : Semigroup ((i : I) → f i) := semigroup
src✝ : MulOneClass ((i : I) → f i) := mulOneClass
n✝ : ℕ
x✝¹ : (i : I) → f i
x✝ : I
⊢ (fun n x i => x i ^ n) (n✝ + 1) x✝¹ x✝ = (x✝¹ * (fun n x i => x i ^ n) n✝ x✝¹) x✝
[PROOFSTEP]
exact Monoid.npow_succ _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (a b : (i : I) → f i), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ b✝ : (i : I) → f i
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ / b✝) x✝ = (a✝ * b✝⁻¹) x✝
[PROOFSTEP]
exact div_eq_mul_inv _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (a : (i : I) → f i), (fun z x i => x i ^ z) 0 a = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ : (i : I) → f i
⊢ (fun z x i => x i ^ z) 0 a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
a✝ : (i : I) → f i
x✝ : I
⊢ (fun z x i => x i ^ z) 0 a✝ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact DivInvMonoid.zpow_zero' _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (n : ℕ) (a : (i : I) → f i),
    (fun z x i => x i ^ z) (Int.ofNat (Nat.succ n)) a = a * (fun z x i => x i ^ z) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
⊢ (fun z x i => x i ^ z) (Int.ofNat (Nat.succ n✝)) a✝ = a✝ * (fun z x i => x i ^ z) (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
x✝ : I
⊢ (fun z x i => x i ^ z) (Int.ofNat (Nat.succ n✝)) a✝ x✝ = (a✝ * (fun z x i => x i ^ z) (Int.ofNat n✝) a✝) x✝
[PROOFSTEP]
exact DivInvMonoid.zpow_succ' _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
⊢ ∀ (n : ℕ) (a : (i : I) → f i), (fun z x i => x i ^ z) (Int.negSucc n) a = ((fun z x i => x i ^ z) (↑(Nat.succ n)) a)⁻¹
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
⊢ (fun z x i => x i ^ z) (Int.negSucc n✝) a✝ = ((fun z x i => x i ^ z) (↑(Nat.succ n✝)) a✝)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvMonoid (f i)
src✝ : Monoid ((i : I) → f i) := monoid
n✝ : ℕ
a✝ : (i : I) → f i
x✝ : I
⊢ (fun z x i => x i ^ z) (Int.negSucc n✝) a✝ x✝ = ((fun z x i => x i ^ z) (↑(Nat.succ n✝)) a✝)⁻¹ x✝
[PROOFSTEP]
exact DivInvMonoid.zpow_neg' _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvOneMonoid (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
⊢ 1⁻¹ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivInvOneMonoid (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
x✝ : I
⊢ 1⁻¹ x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact inv_one
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvolutiveInv (f i)
⊢ ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvolutiveInv (f i)
x✝ : (i : I) → f i
⊢ x✝⁻¹⁻¹ = x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → InvolutiveInv (f i)
x✝¹ : (i : I) → f i
x✝ : I
⊢ x✝¹⁻¹⁻¹ x✝ = x✝¹ x✝
[PROOFSTEP]
exact inv_inv _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
⊢ ∀ (a b : (i : I) → f i), (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
⊢ (a✝ * b✝)⁻¹ = b✝⁻¹ * a✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝)⁻¹ x✝ = (b✝⁻¹ * a✝⁻¹) x✝
[PROOFSTEP]
exact mul_inv_rev _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
⊢ ∀ (a b : (i : I) → f i), a * b = 1 → a⁻¹ = b
[PROOFSTEP]
intros _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
⊢ a✝⁻¹ = b✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → DivisionMonoid (f i)
src✝¹ : DivInvMonoid ((i : I) → f i) := divInvMonoid
src✝ : InvolutiveInv ((i : I) → f i) := involutiveInv
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
x✝ : I
⊢ a✝⁻¹ x✝ = b✝ x✝
[PROOFSTEP]
exact DivisionMonoid.inv_eq_of_mul _ _ (congrFun h _)
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Group (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
⊢ ∀ (a : (i : I) → f i), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Group (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
a✝ : (i : I) → f i
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → Group (f i)
src✝ : DivInvMonoid ((i : I) → f i) := divInvMonoid
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝⁻¹ * a✝) x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact mul_left_inv _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → LeftCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
⊢ ∀ (a b c : (i : I) → f i), a * b = a * c → b = c
[PROOFSTEP]
intros _ _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → LeftCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → LeftCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = a✝ * c✝
x✝ : I
⊢ b✝ x✝ = c✝ x✝
[PROOFSTEP]
exact LeftCancelSemigroup.mul_left_cancel _ _ _ (congr_fun h _)
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → RightCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
⊢ ∀ (a b c : (i : I) → f i), a * b = c * b → a = c
[PROOFSTEP]
intros _ _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → RightCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → RightCancelSemigroup (f i)
src✝ : Semigroup ((i : I) → f i) := semigroup
a✝ b✝ c✝ : (i : I) → f i
h : a✝ * b✝ = c✝ * b✝
x✝ : I
⊢ a✝ x✝ = c✝ x✝
[PROOFSTEP]
exact RightCancelSemigroup.mul_right_cancel _ _ _ (congr_fun h _)
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
⊢ ∀ (a : (i : I) → f i), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
⊢ 0 * a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (0 * a✝) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
exact zero_mul _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
⊢ a✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝ : (i : I) → MulZeroClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * 0) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
exact mul_zero _
[GOAL]
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_5
x✝¹ x✝ : I → α
⊢ (fun h => ↑f ∘ h) (x✝¹ * x✝) = (fun h => ↑f ∘ h) x✝¹ * (fun h => ↑f ∘ h) x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_5
x✝² x✝¹ : I → α
x✝ : I
⊢ (fun h => ↑f ∘ h) (x✝² * x✝¹) x✝ = ((fun h => ↑f ∘ h) x✝² * (fun h => ↑f ∘ h) x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
⊢ (fun h => ↑f ∘ h) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝ : I
⊢ (fun h => ↑f ∘ h) 1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝ : I
⊢ ↑f 1 = 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝¹ x✝ : I → α
⊢ OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } (x✝¹ * x✝) =
    OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝¹ *
      OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
x y : (i : I✝) → f✝ i
i j : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_3
β : Type u_4
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_5
x✝² x✝¹ : I → α
x✝ : I
⊢ OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } (x✝² * x✝¹) x✝ =
    (OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝² *
        OneHom.toFun { toFun := fun h => ↑f ∘ h, map_one' := (_ : (fun h => ↑f ∘ h) 1 = 1) } x✝¹)
      x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)
[PROOFSTEP]
intro i j hij x y
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)
[PROOFSTEP]
ext k
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
by_cases h1 : i = k
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
subst h1
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ (mulSingle i x * mulSingle j y) i = (mulSingle j y * mulSingle i x) i
[PROOFSTEP]
simp [hij]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : ¬i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
by_cases h2 : j = k
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : ¬i = k
h2 : j = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
subst h2
[GOAL]
case pos
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
h1 : ¬i = j
⊢ (mulSingle i x * mulSingle j y) j = (mulSingle j y * mulSingle i x) j
[PROOFSTEP]
simp [hij]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y✝ : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h1 : ¬i = k
h2 : ¬j = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
[PROOFSTEP]
simp [h1, h2]
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i✝ j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i✝ j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
[PROOFSTEP]
exact Pi.mulSingle_commute hij _ _
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x = g / mulSingle i (g i) * mulSingle i x
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | h)
[GOAL]
case h.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i
[PROOFSTEP]
simp
[GOAL]
case h.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x✝ y : (i : I) → f i
i j✝ : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
[PROOFSTEP]
simp [Function.update_noteq h.symm, h]
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hk := congr_fun h k
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hl := congr_fun h l
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hm := (congr_fun h m).symm
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle m u * mulSingle n v) m = (mulSingle k u * mulSingle l v) m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
have hn := (congr_fun h n).symm
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle m u * mulSingle n v) m = (mulSingle k u * mulSingle l v) m
hn : (mulSingle m u * mulSingle n v) n = (mulSingle k u * mulSingle l v) n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
simp only [mul_apply, mulSingle_apply, if_pos rfl] at hk hl hm hn 
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if m = n then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
rcases eq_or_ne k m with (rfl | hkm)
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
⊢ k = k ∧ l = n ∨ u = v ∧ k = n ∧ l = k ∨ u * v = 1 ∧ k = l ∧ k = n
[PROOFSTEP]
refine' Or.inl ⟨rfl, not_ne_iff.mp fun hln => (hv _).elim⟩
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
⊢ v = 1
[PROOFSTEP]
rcases eq_or_ne k l with (rfl | hkl)
[GOAL]
case refine'_1.inl.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle k v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = k then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = k then v else 1
hln : k ≠ n
⊢ v = 1
[PROOFSTEP]
rwa [if_neg hln.symm, if_neg hln.symm, one_mul, one_mul] at hn 
[GOAL]
case refine'_1.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
hkl : k ≠ l
⊢ v = 1
[PROOFSTEP]
rwa [if_neg hkl.symm, if_neg hln, one_mul, one_mul] at hl 
[GOAL]
case refine'_1.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if m = n then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
rcases eq_or_ne m n with (rfl | hmn)
[GOAL]
case refine'_1.inr.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
rcases eq_or_ne k l with (rfl | hkl)
[GOAL]
case refine'_1.inr.inl.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = k then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = k then v else 1
⊢ k = m ∧ k = m ∨ u = v ∧ k = m ∧ k = m ∨ u * v = 1 ∧ k = k ∧ m = m
[PROOFSTEP]
rw [if_neg hkm.symm, if_neg hkm.symm, one_mul, if_pos rfl] at hm 
[GOAL]
case refine'_1.inr.inl.inl
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hm : (if True then u else 1) * v = 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = k then v else 1
⊢ k = m ∧ k = m ∨ u = v ∧ k = m ∧ k = m ∨ u * v = 1 ∧ k = k ∧ m = m
[PROOFSTEP]
exact Or.inr (Or.inr ⟨hm, rfl, rfl⟩)
[GOAL]
case refine'_1.inr.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
simp only [if_neg hkm, if_neg hkl, mul_one] at hk 
[GOAL]
case refine'_1.inr.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
hk : (if True then u else 1) = 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
dsimp at hk 
[GOAL]
case refine'_1.inr.inl.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
hk : u = 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m
[PROOFSTEP]
contradiction
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if m = n then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
hmn : m ≠ n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
rw [if_neg hkm.symm, if_neg hmn, one_mul, mul_one] at hm 
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : (if True then u else 1) = if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
hmn : m ≠ n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
[PROOFSTEP]
obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hm.symm hu)).1
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hmn : m ≠ n
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = m then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = n then v else 1
hm : (if True then u else 1) = if m = m then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = m then v else 1
⊢ k = m ∧ m = n ∨ u = v ∧ k = n ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = n
[PROOFSTEP]
rw [if_neg hkm, if_neg hkm, one_mul, mul_one] at hk 
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hmn : m ≠ n
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle n v
hk : (if True then u else 1) = if k = n then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = n then v else 1
hm : (if True then u else 1) = if m = m then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = m then v else 1
⊢ k = m ∧ m = n ∨ u = v ∧ k = n ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = n
[PROOFSTEP]
obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hk.symm hu)).1
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hm : (if True then u else 1) = if m = m then v else 1
hmn : m ≠ k
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle k v
hk : (if True then u else 1) = if k = k then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = k then v else 1
hn : ((if k = m then u else 1) * if True then v else 1) = (if k = k then u else 1) * if k = m then v else 1
⊢ k = m ∧ m = k ∨ u = v ∧ k = k ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = k
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hk.trans (if_pos rfl), rfl, rfl⟩)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ | ⟨h, rfl, rfl⟩)
[GOAL]
case refine'_2.inl.intro
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ mulSingle k u * mulSingle l v = mulSingle k u * mulSingle l v
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr.inl.intro.intro
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l : I
u : M
hu hv : u ≠ 1
⊢ mulSingle k u * mulSingle l u = mulSingle l u * mulSingle k u
[PROOFSTEP]
apply mul_comm
[GOAL]
case refine'_2.inr.inr.intro.intro
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
x y : (i : I) → f i
i j : I
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : u * v = 1
⊢ mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
[PROOFSTEP]
simp_rw [← Pi.mulSingle_mul, h, mulSingle_one]
[GOAL]
ι : Type u_1
α : Type u_2
I : Type u
f✝ : I → Type v
x y : (i : I) → f✝ i
i j : I
η : Type v
R : Type w
s : ι → η
inst✝ : MulOneClass R
f g : ι → R
⊢ OneHom.toFun { toFun := fun f => extend s f 1, map_one' := (_ : extend s 1 1 = 1) } (f * g) =
    OneHom.toFun { toFun := fun f => extend s f 1, map_one' := (_ : extend s 1 1 = 1) } f *
      OneHom.toFun { toFun := fun f => extend s f 1, map_one' := (_ : extend s 1 1 = 1) } g
[PROOFSTEP]
simpa using Function.extend_mul s f g 1 1
