awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
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)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
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)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : One β
inst_1 : Nonempty α
⊢ Eq (α := Set β) (range.{u_5, u_4 + 1} (ι := α) 1) {1}

Tactic:
range_const

Premises used: Set.range_const
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : One β
s : Set β
inst_1 : Decidable (1 ∈ s)
⊢ Eq.{u_4 + 1} (α := Set α) (1 ⁻¹' s) (if 1 ∈ s then univ else ∅)

Tactic:
Set.preimage_const 1 s

Premises used: Set.preimage_const, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
i : I
inst : (i : ι) → Monoid (M i)
inst_1 : ∀ (i : ι), IsMulTorsionFree.{u_3} (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : Eq (α := (i : ι) → M i) ((fun (a : (i : ι) → M i) ↦ a ^ n) a) ((fun (a : (i : ι) → M i) ↦ a ^ n) b)
h : ∀ (i : ι), a i = b i
⊢ a = b

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
i_1 : I
inst : (i : ι) → Monoid (M i)
inst_1 : ∀ (i : ι), IsMulTorsionFree.{u_3} (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : Eq (α := (i : ι) → M i) ((fun (a : (i : ι) → M i) ↦ a ^ n) a) ((fun (a : (i : ι) → M i) ↦ a ^ n) b)
i : ι
⊢ a i = b i

Tactic:
pow_left_injective hn <| congr_fun hab i

Premises used: pow_left_injective, congr_fun
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
i_1 : I
inst : (i : ι) → Monoid (M i)
inst_1 : ∀ (i : ι), IsMulTorsionFree.{u_3} (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : Eq (α := (i : ι) → M i) ((fun (a : (i : ι) → M i) ↦ a ^ n) a) ((fun (a : (i : ι) → M i) ↦ a ^ n) b)
i : ι
⊢ a i = b i

Tactic:
exact pow_left_injective hn <| congr_fun hab i

Premises used: pow_left_injective, congr_fun
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : One β
⊢ Monotone.{u_4, u_5} (α := α) (β := β) 1

Tactic:
monotone_const

Premises used: monotone_const
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : One β
⊢ Antitone.{u_4, u_5} (α := α) (β := β) 1

Tactic:
antitone_const

Premises used: antitone_const
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
M : Type u_4
N : Type u_5
x : Mul M
x_1 : CommSemigroup N
f g : M →ₙ* N
⊢ HMul.hMul (α := (a : M) → N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) = fun (x_2 : M) ↦
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x_2 : N) ((g : (a : M) → N) x_2 : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
γ : Type w
inst : Nonempty I
inst_1 : (i : I) → Mul (f i)
inst_2 : Mul γ
g : (i : I) → MulHom.{w, v} γ (f i)
hg : ∀ (i : I), Function.Injective.{w + 1, v + 1} (α := γ) (β := f i) (⇑(g i) : (a : γ) → f i)
⊢ Function.Injective (α := γ) (β := (i : I) → f i) (⇑(mulHom (f := f) g) : (a : γ) → (i : I) → f i)

Tactic:
fun _ _ h =>
  let ⟨i⟩ := ‹Nonempty I›
  hg i ((funext_iff.mp h :) i)

Premises used: funext_iff, _private.0.Pi.mulHom_injective.match_1, Iff.mp, Function.Injective, Eq
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
γ : Type w
inst : Nonempty I
inst_1 : (i : I) → MulOneClass (f i)
inst_2 : MulOneClass γ
g : (i : I) → MonoidHom.{w, v} γ (f i)
hg : ∀ (i : I), Function.Injective.{w + 1, v + 1} (α := γ) (β := f i) (⇑(g i) : (a : γ) → f i)
⊢ Function.Injective (α := γ) (β := (i : I) → f i) (⇑(monoidHom (f := f) g) : (a : γ) → (i : I) → f i)

Tactic:
Pi.mulHom_injective (fun i => (g i).toMulHom) hg

Premises used: MonoidHom.toMulHom, Pi.mulHom_injective
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → Mul (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : Mul α
inst_2 : Mul β
f : α →ₙ* β
I : Type u_6
x x_1 : I → α
h :
  ∀ (x_2 : I),
    ((⇑f : (a : α) → β) ∘ (x * x_1)) x_2 =
      HMul.hMul (α := I → β) (β := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1) x_2
⊢ (⇑f : (a : α) → β) ∘ (x * x_1) = HMul.hMul (α := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → Mul (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : Mul α
inst_2 : Mul β
f : α →ₙ* β
I : Type u_6
x x_1 : I → α
x_2 : I
⊢ ((⇑f : (a : α) → β) ∘ (x * x_1)) x_2 =
    HMul.hMul (α := I → β) (β := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1) x_2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → MulOneClass (f i)
i : I
⊢ Eq (α := (a : (i : I) → f i) → f i) (⇑(evalMonoidHom f i) : (a : (i : I) → f i) → f i) (Function.eval (β := f) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → MulOneClass (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : MulOneClass α
inst_2 : MulOneClass β
f : α →* β
I : Type u_6
h : ∀ (x : I), Eq.{u_5 + 1} (α := β) (Function.comp.{u_6 + 1, u_4 + 1, u_5 + 1} (β := α) (⇑f : (a : α) → β) 1 x) (1 x)
⊢ Eq (α := I → β) (Function.comp.{u_6 + 1, u_4 + 1, u_5 + 1} (β := α) (⇑f : (a : α) → β) 1) 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → MulOneClass (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : MulOneClass α
inst_2 : MulOneClass β
f : α →* β
I : Type u_6
x : I
⊢ Eq.{u_5 + 1} (α := β) (Function.comp.{u_6 + 1, u_4 + 1, u_5 + 1} (β := α) (⇑f : (a : α) → β) 1 x) (1 x)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → MulOneClass (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : MulOneClass α
inst_2 : MulOneClass β
f : α →* β
I : Type u_6
x x_1 : I → α
h :
  ∀ (x_2 : I),
    ((⇑f : (a : α) → β) ∘ (x * x_1)) x_2 =
      HMul.hMul (α := I → β) (β := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1) x_2
⊢ (⇑f : (a : α) → β) ∘ (x * x_1) = HMul.hMul (α := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → MulOneClass (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : MulOneClass α
inst_2 : MulOneClass β
f : α →* β
I : Type u_6
x x_1 : I → α
x_2 : I
⊢ ((⇑f : (a : α) → β) ∘ (x * x_1)) x_2 =
    HMul.hMul (α := I → β) (β := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1) x_2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → One (f i)
i : I
x : f i
⊢ (mulSingle f i : (a : f i) → (i : I) → f i) x = Pi.mulSingle (M := f) i x

Tactic:
rfl

Premises used: Function.update, dite, Pi.mulSingle, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → One (f i)
i : I
⊢ Eq (α := (a : f i) → (i : I) → f i) (⇑(mulSingle f i) : (a : f i) → (i : I) → f i) (Pi.mulSingle (M := f) i)

Tactic:
rfl

Premises used: Function.update, dite, Pi.mulSingle, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i : I
x : f i
⊢ (mulSingle f i : (a : f i) → (i : I) → f i) x = Pi.mulSingle (M := f) i x

Tactic:
rfl

Premises used: Function.update, dite, Pi.mulSingle, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i : I
⊢ Eq (α := (a : f i) → (i : I) → f i) (⇑(mulSingle f i) : (a : f i) → (i : I) → f i) (Pi.mulSingle (M := f) i)

Tactic:
rfl

Premises used: Function.update, dite, Pi.mulSingle, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → SemilatticeSup (f i)
inst_2 : (i : I) → One (f i)
i : I
x y : f i
⊢ mulSingle (M := f) i (x ⊔ y) = mulSingle (M := f) i x ⊔ mulSingle (M := f) i y

Tactic:
Function.update_sup _ _ _ _

Premises used: Pi.mulSingle, Function.update_sup
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → SemilatticeInf (f i)
inst_2 : (i : I) → One (f i)
i : I
x y : f i
⊢ mulSingle (M := f) i (x ⊓ y) = mulSingle (M := f) i x ⊓ mulSingle (M := f) i y

Tactic:
Function.update_inf _ _ _ _

Premises used: Function.update_inf, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i : I
x y : f i
⊢ mulSingle (M := f) i (x * y) = mulSingle (M := f) i x * mulSingle (M := f) i y

Tactic:
(MonoidHom.mulSingle f i).map_mul x y

Premises used: Function.update, MonoidHom.mulSingle, dite, MonoidHom.map_mul, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
i : I
x : f i
⊢ mulSingle (M := f) i x⁻¹ = (mulSingle (M := f) i x)⁻¹

Tactic:
(MonoidHom.mulSingle f i).map_inv x

Premises used: Function.update, MonoidHom.mulSingle, dite, MonoidHom.map_inv, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
i : I
x y : f i
⊢ mulSingle (M := f) i (x / y) = mulSingle (M := f) i x / mulSingle (M := f) i y

Tactic:
(MonoidHom.mulSingle f i).map_div x y

Premises used: Function.update, MonoidHom.mulSingle, dite, MonoidHom.map_div, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → Monoid (f i)
i : I
x : f i
n : ℕ
⊢ mulSingle (M := f) i (x ^ n) = mulSingle (M := f) i x ^ n

Tactic:
(MonoidHom.mulSingle f i).map_pow x n

Premises used: Function.update, MonoidHom.mulSingle, dite, Pi.mulSingle, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
i : I
x : f i
n : ℤ
⊢ mulSingle (M := f) i (x ^ n) = mulSingle (M := f) i x ^ n

Tactic:
(MonoidHom.mulSingle f i).map_zpow x n

Premises used: Function.update, MonoidHom.mulSingle, dite, Pi.mulSingle, MonoidHom.map_zpow
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
h : ∀ (k : I), (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
⊢ Commute (mulSingle (M := f) i x) (mulSingle (M := f) j y)

Tactic:
ext k
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
pos : i = k → (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
neg : ¬i = k → (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
⊢ (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k

Tactic:
by_cases i = k
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h : i = k
⊢ (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h : ¬i = k
⊢ (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
inl : Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) i (x i))
inr : ∀ (hij : i ≠ j), Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))
⊢ Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) i (x i))

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))

Tactic:
Pi.mulSingle_commute hij _ _

Premises used: Pi.mulSingle_commute
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))

Tactic:
exact Pi.mulSingle_commute hij _ _

Premises used: Pi.mulSingle_commute
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
h : ∀ (j : I), Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j
⊢ Function.update (β := f) g i x = g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x

Tactic:
ext j
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : Function.update (β := f) g i x i = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) i
h₁ : ∀ (h : i ≠ j), Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j
⊢ Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update (β := f) g i x i = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) i

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j

Tactic:
simp [h, eqComm]

Premises used: eqComm
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
refine_1 :
  ∀
    (h :
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
        HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)),
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
refine_2 :
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
⊢ HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
⊢ HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k

Tactic:
have hk := congr_fun h k
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
⊢ HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) l =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) l

Tactic:
have hl := congr_fun h l
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
hl :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) l =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) l
⊢ HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) m =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) m

Tactic:
have hm := congr_fun h m
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
hl :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) l =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) l
hm :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) m =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) m
⊢ HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) n =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) n

Tactic:
have hn := congr_fun h n
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
hl :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) l =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) l
hm :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) m =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) m
hn :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) n =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
grind [mul_one, one_mul, mul_apply]

Premises used: Pi.mul_apply, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : 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 →
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)

Tactic:
aesop (add simp [mulSingle_apply])

Premises used: Pi.mulSingle_apply
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Mul (f i)
x y z : (i : I) → f i
h : ∀ (i : I), SemiconjBy (x i) (y i) (z i)
⊢ SemiconjBy x y z

Tactic:
funext h

Premises used: SemiconjBy, funext
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Mul (f i)
x y z : (i : I) → f i
⊢ SemiconjBy x y z ↔ ∀ (i : I), SemiconjBy (x i) (y i) (z i)

Tactic:
funext_iff

Premises used: SemiconjBy, funext_iff
-- Module: Mathlib.Algebra.Group.Pi.Lemmas
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Mul (f i)
x y : (i : I) → f i
h : ∀ (i : I), Commute (x i) (y i)
⊢ Commute x y

Tactic:
SemiconjBy.pi h

Premises used: Commute, SemiconjBy.pi