awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b_1 c_1 : α
pab_1 : p a b_1
pbc_1 : p b_1 c_1
pac_1 : p a c_1
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
inr : f a b * (f b c * f c a * f a c) = f a b * f b c
inr₁ : f a b * (f b c * (f c a * f a c)) = f a b * f b c
inr₂ : f a b * (f b c * 1) = f a b * f b c
inr₃ inr₄ : f a b * f b c = f a b * f b c
⊢ f a b * (f b a * f a c) = f a b * f b c

Tactic:
rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c

Tactic:
have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c := by
    intro b c rbc pab pbc pac
    obtain rab | rba := total_of r a b
    · exact hmul rab rbc pab pbc pac
    rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
    obtain rac | rca := total_of r a c
    · rw [hmul rba rac (hsymm pab) pac pbc]
    · rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
inl : ∀ (rbc : r b c), f a c = f a b * f b c
inr : ∀ (rcb : r c b), f a c = f a b * f b c
⊢ f a c = f a b * f b c

Tactic:
obtain rbc | rcb := total_of r b c

Premises used: total_of
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c

Tactic:
hmul' rbc pab pbc pac
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c

Tactic:
exact hmul' rbc pab pbc pac
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
p r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
hsymm : Symmetric p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
inr : f a c = f a c * f c b * f b c
inr₁ : f a c = f a c * (f c b * f b c)
inr₂ : f a c = f a c * 1
inr₃ inr₄ : f a c = f a c
⊢ f a c = f a b * f b c

Tactic:
rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
hf_swap : ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1
hmul₁ : ∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c
pab : p a ∧ p b
pbc : p b ∧ p c
pac : p a ∧ p c
⊢ f a c = f a b * f b c

Tactic:
apply multiplicative_of_symmetric_of_total (fun a b => p a ∧ p b) r f fun _ _ => And.symm

Premises used: multiplicative_of_symmetric_of_total, And, And.symm
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
hf_swap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
⊢ ∀ {a b : α}, p a ∧ p b → f a b * f b a = 1

Tactic:
simp_rw [and_imp]

Premises used: and_imp
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b : α}, p a → p b → f a b * f b a = 1

Tactic:
@hswap
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b : α}, p a → p b → f a b * f b a = 1

Tactic:
exact @hswap
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
a_1 b_1 c_1 : α
⊢ r a_1 b_1 → r b_1 c_1 → p a_1 ∧ p b_1 → p b_1 ∧ p c_1 → p a_1 ∧ p c_1 → f a_1 c_1 = f a_1 b_1 * f b_1 c_1

Tactic:
fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ ∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c

Tactic:
exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p b

Tactic:
⟨pa, pb⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p b ∧ p c

Tactic:
⟨pb, pc⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p c

Tactic:
⟨pa, pc⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Monoid β
r : α → α → Prop
inst_1 : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ p a ∧ p b

Tactic:
exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
F : Type u_5
inst : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
rw : id = (c f)^[0]
⊢ c (HPow.hPow (β := ℕ) f 0) = (c f)^[0]

Tactic:
rw [pow_zero, h1]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
F : Type u_5
inst : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
M : Type u_4
F : Type u_5
inst : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
rw : c (f ^ n * f) = (c f)^[n + 1]
rw₁ : c (f ^ n * f) = (c f)^[n] ∘ c f
rw₂ : c (f ^ n) ∘ c f = (c f)^[n] ∘ c f
rw₃ rw₄ : (c f)^[n] ∘ c f = (c f)^[n] ∘ c f
⊢ c (f ^ (n + 1)) = (c f)^[n + 1]

Tactic:
rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]

Premises used: Function.iterate_succ, pow_succ
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α_1 : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
change : (n + 1) • a = n • a + a
⊢ (n + 1) • a = n • a + a

Tactic:
change (n + 1) • a = n • a + a

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α_1 : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
rw : n • a + HSMul.hSMul (α := ℕ) 1 a = n • a + a
rw₁ rw₂ : n • a + a = n • a + a
⊢ (n + 1) • a = n • a + a

Tactic:
rw [add_nsmul, one_nsmul]

Premises used: one_nsmul, add_nsmul
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α_1 : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommGroup α
n : ℕ
a : α
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) a = n • a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
z : M
h : IsMulCentral z
a c : M
rw : a * z * c = a * (c * z)
rw₁ : a * z * c = a * c * z
rw₂ : z * a * c = a * c * z
rw₃ : z * (a * c) = a * c * z
rw₄ rw₅ : a * c * z = a * c * z
⊢ a * z * c = a * (z * c)

Tactic:
rw [h.comm, ← h.right_assoc, ← h.comm, ← h.left_assoc, h.comm]

Premises used: IsMulCentral.comm, IsMulCentral.left_assoc, IsMulCentral.right_assoc
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
a : M
inst : Mul M
h : IsMulCentral a
b c : M
⊢ a * (b * c) = b * (a * c)

Tactic:
simp only [(h.comm _).eq, h.right_assoc]

Premises used: IsMulCentral.comm, IsMulCentral.right_assoc, Commute.eq
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
c : M
inst : Mul M
h : IsMulCentral c
a b : M
⊢ a * b * c = a * c * b

Tactic:
simp only [h.right_assoc, h.mid_assoc, (h.comm _).eq]

Premises used: IsMulCentral.comm, IsMulCentral.mid_assoc, IsMulCentral.right_assoc, Commute.eq
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
z : M
⊢ z ∈ center M ↔ IsMulCentral z

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.center
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : Mul M
c : M
⊢ c ∈ S.centralizer ↔ ∀ m ∈ S, m * c = c * m

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
simp :
  ∀
    (hz₁ :
      (∀ (a : M), z₁ * a = a * z₁) ∧ (∀ (b c : M), z₁ * (b * c) = z₁ * b * c) ∧ ∀ (a b : M), a * b * z₁ = a * (b * z₁))
    (hz₂ :
      (∀ (a : M), z₂ * a = a * z₂) ∧ (∀ (b c : M), z₂ * (b * c) = z₂ * b * c) ∧ ∀ (a b : M), a * b * z₂ = a * (b * z₂)),
    (∀ (a : M), z₁ * z₂ * a = a * (z₁ * z₂)) ∧
      (∀ (b c : M), z₁ * z₂ * (b * c) = z₁ * z₂ * b * c) ∧ ∀ (a b : M), a * b * (z₁ * z₂) = a * (b * (z₁ * z₂))
⊢ z₁ * z₂ ∈ center M

Tactic:
simp only [commute_iff_eq, mem_center_iff, isMulCentral_iff] at *

Premises used: commute_iff_eq, isMulCentral_iff, Set.mem_center_iff
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
z₁ z₂ : M
hz₁ : (∀ (a : M), z₁ * a = a * z₁) ∧ (∀ (b c : M), z₁ * (b * c) = z₁ * b * c) ∧ ∀ (a b : M), a * b * z₁ = a * (b * z₁)
hz₂ : (∀ (a : M), z₂ * a = a * z₂) ∧ (∀ (b c : M), z₂ * (b * c) = z₂ * b * c) ∧ ∀ (a b : M), a * b * z₂ = a * (b * z₂)
⊢ (∀ (a : M), z₁ * z₂ * a = a * (z₁ * z₂)) ∧
    (∀ (b c : M), z₁ * z₂ * (b * c) = z₁ * z₂ * b * c) ∧ ∀ (a b : M), a * b * (z₁ * z₂) = a * (b * (z₁ * z₂))

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
S : Set M
⊢ center M ⊆ S.centralizer

Tactic:
fun _ hx m _ ↦ (hx.comm m).symm

Premises used: Set.Mem, setOf, SemiconjBy, Commute, IsMulCentral.comm, Set.centralizer, Set.Subset, Commute.symm
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S T : Set M
inst : Mul M
⊢ (S ∪ T).centralizer = S.centralizer ∩ T.centralizer

Tactic:
simp [centralizer, or_imp, forall_and, setOf_and]

Premises used: Set.setOf_and, or_imp, Set.centralizer, forall_and
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S T : Set M
inst : Mul M
h : S ⊆ T
⊢ T.centralizer ⊆ S.centralizer

Tactic:
fun _ ht s hs ↦ ht s (h hs)

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : Mul M
⊢ S ⊆ S.centralizer.centralizer

Tactic:
fun x hx _ hy ↦ (hy x hx).symm

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Eq.symm
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer = S.centralizer

Tactic:
Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer

Premises used: Set.Subset.antisymm, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
S : Set M
refine : S.centralizer.centralizer.centralizer ⊆ S.centralizer
⊢ S.centralizer.centralizer.centralizer = S.centralizer

Tactic:
refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer

Premises used: Set.Subset.antisymm, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer ⊆ S.centralizer

Tactic:
fun x hx y hy ↦ hx y <| Set.subset_centralizer_centralizer hy

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer ⊆ S.centralizer

Tactic:
exact fun x hx y hy ↦ hx y <| Set.subset_centralizer_centralizer hy
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : Mul M
h_comm : ∀ x ∈ S, ∀ y ∈ S, x * y = y * x
⊢ ∀ x ∈ S.centralizer.centralizer, ∀ y ∈ S.centralizer.centralizer, x * y = y * x

Tactic:
fun _ h₁ _ h₂ ↦ h₂ _ fun _ h₃ ↦ h₁ _ fun _ h₄ ↦ h_comm _ h₄ _ h₃
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
⊢ Eq.{u_1 + 1} (α := Set M) (centralizer ∅) ⊤

Tactic:
simp [centralizer]

Premises used: Set.centralizer
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
h : ∀ (x : M × N), x ∈ (S ×ˢ T).centralizer ↔ x ∈ S.centralizer ×ˢ T.centralizer
⊢ (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
x : M × N
h :
  (∀ (a : M) (b : N), a ∈ S ∧ b ∈ T → (a * x.1, b * x.2) = (x.1 * a, x.2 * b)) ↔
    (∀ m ∈ S, m * x.1 = x.1 * m) ∧ ∀ m ∈ T, m * x.2 = x.2 * m
⊢ x ∈ (S ×ˢ T).centralizer ↔ x ∈ S.centralizer ×ˢ T.centralizer

Tactic:
simp only [mem_prod, mem_centralizer_iff, Prod.forall, Prod.mul_def]

Premises used: Prod.mul_def, Set.mem_centralizer_iff, Set.mem_prod, Prod.forall
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
x : M × N
⊢ (∀ (a : M) (b : N), a ∈ S ∧ b ∈ T → (a * x.1, b * x.2) = (x.1 * a, x.2 * b)) ↔
    (∀ m ∈ S, m * x.1 = x.1 * m) ∧ ∀ m ∈ T, m * x.2 = x.2 * m

Tactic:
grind [Set.Nonempty]

Premises used: Set.Nonempty
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
S : Set M
T : Set N
⊢ S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer

Tactic:
simp_all [subset_def, mem_centralizer_iff]

Premises used: Set.subset_def, Set.mem_centralizer_iff
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
⊢ center (M × N) = center M ×ˢ center N

Tactic:
aesop (add simp [Prod.forall, forall_and, commute_iff_eq, isMulCentral_iff, mem_center_iff])

Premises used: commute_iff_eq, isMulCentral_iff, Set.mem_center_iff, Prod.forall, forall_and
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
h :
  ∀ (x : (i : ι) → A i),
    Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
      Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x
⊢ Eq (α := Set ((i : ι) → A i)) (center ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i))

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
h :
  ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
    ∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
⊢ Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
    Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x

Tactic:
simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]

Premises used: forall_true_left, funext_iff, commute_iff_eq, isMulCentral_iff, Set.mem_pi, Set.mem_center_iff, Set.mem_univ, Pi.mul_def
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ (∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)) →
    (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
h :
  ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) →
    ∀ (i : ι) (h1 : ∀ (a : (i : ι) → A i) (x_2 : ι), x x_2 * a x_2 = a x_2 * x x_2)
      (h2 : ∀ (b c : (i : ι) → A i) (x_2 : ι), x x_2 * (b x_2 * c x_2) = x x_2 * b x_2 * c x_2)
      (h3 : ∀ (a b : (i : ι) → A i) (x_2 : ι), a x_2 * b x_2 * x x_2 = a x_2 * (b x_2 * x x_2)),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
⊢ ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
    ∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)

Tactic:
refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
h :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a : A i
⊢ x i * a = a * x i

Tactic:
simpa using h1 (update x i a) i

Premises used: Function.update
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
h :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
b c : A i
⊢ x i * (b * c) = x i * b * c

Tactic:
simpa using h2 (update x i b) (update x i c) i

Premises used: Function.update
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
h :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a b : A i
⊢ a * b * x i = a * (b * x i)

Tactic:
simpa using h3 (update x i a) (update x i b) i

Premises used: Function.update
-- Module: Mathlib.Algebra.Group.Center
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
h :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
⊢ (∀ (a : A i), x i * a = a * x i) ∧
    (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)

Tactic:
exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩