awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
x₁ x₂ : M
⊢ (((f : (a : M) → N →* P) (x₁ * x₂) : N →* P) : (a : N) → P) y =
    HMul.hMul (α := P) (β := P) ((((f : (a : M) → N →* P) x₁ : N →* P) : (a : N) → P) y : P)
      ((((f : (a : M) → N →* P) x₂ : N →* P) : (a : N) → P) y : P)

Tactic:
simp [f.map_mul, mul_apply]

Premises used: MonoidHom.map_mul, MonoidHom.mul_apply
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
x_1 : MulOneClass M
x_2 : MulOneClass N
x_3 : CommMonoid P
f : M →* N →* P
x : M
y : N
⊢ Eq.{uP + 1} (α := P) ((((f.flip : (a : N) → M →* P) y : M →* P) : (a : M) → P) x : P)
    ((((f : (a : M) → N →* P) x : N →* P) : (a : N) → P) y : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
x : MulOneClass M
x_1 : MulOneClass N
x_2 : CommMonoid P
f : M →* N →* P
n : N
⊢ Eq.{uP + 1} (α := P) (((f : (a : M) → N →* P) 1 : (a : N) → P) n : P) (1 : P)

Tactic:
(flip f n).map_one

Premises used: MonoidHom.map_one, MonoidHom.flip, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
x : MulOneClass M
x_1 : MulOneClass N
x_2 : CommMonoid P
f : M →* N →* P
m₁ m₂ : M
n : N
⊢ (((f : (a : M) → N →* P) (m₁ * m₂) : N →* P) : (a : N) → P) n =
    HMul.hMul (α := P) (β := P) ((((f : (a : M) → N →* P) m₁ : N →* P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →* P) m₂ : N →* P) : (a : N) → P) n : P)

Tactic:
(flip f n).map_mul _ _

Premises used: MonoidHom.flip, DFunLike.coe, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
x : Group M
x_1 : MulOneClass N
x_2 : CommGroup P
f : M →* N →* P
m : M
n : N
⊢ Eq.{uP + 1} (α := P) ((((f : (a : M) → N →* P) m⁻¹ : N →* P) : (a : N) → P) n : P)
    (((((f : (a : M) → N →* P) m : N →* P) : (a : N) → P) n)⁻¹ : P)

Tactic:
(flip f n).map_inv _

Premises used: MonoidHom.map_inv, MonoidHom.flip, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
x : Group M
x_1 : MulOneClass N
x_2 : CommGroup P
f : M →* N →* P
m₁ m₂ : M
n : N
⊢ (((f : (a : M) → N →* P) (m₁ / m₂) : N →* P) : (a : N) → P) n =
    HDiv.hDiv (α := P) (β := P) ((((f : (a : M) → N →* P) m₁ : N →* P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →* P) m₂ : N →* P) : (a : N) → P) n : P)

Tactic:
(flip f n).map_div _ _

Premises used: MonoidHom.map_div, MonoidHom.flip, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
h :
  ∀ (f : M →* N),
    Eq (α := M →* P) (({ toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } : (a : M →* N) → M →* P) f : M →* P)
      ((1 : (a : M →* N) → M →* P) f : M →* P)
⊢ Eq (α := (M →* N) →* M →* P) { toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } 1

Tactic:
ext1 f
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
f : M →* N
⊢ Eq (α := M →* P) (({ toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } : (a : M →* N) → M →* P) f : M →* P)
    ((1 : (a : M →* N) → M →* P) f : M →* P)

Tactic:
one_comp f

Premises used: MonoidHom.one_comp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
f : M →* N
⊢ Eq (α := M →* P) (({ toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } : (a : M →* N) → M →* P) f : M →* P)
    ((1 : (a : M →* N) → M →* P) f : M →* P)

Tactic:
exact one_comp f

Premises used: MonoidHom.one_comp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
g₁ g₂ : N →* P
h :
  ∀ (f : M →* N),
    Eq (α := M →* P) (({ toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } : (a : M →* N) → M →* P) f : M →* P)
      ((HMul.hMul (α := (M →* N) →* M →* P) { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P }
              { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P } :
            (a : M →* N) → M →* P)
          f :
        M →* P)
⊢ { toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } =
    HMul.hMul (α := (M →* N) →* M →* P) { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P }
      { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P }

Tactic:
ext1 f
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
g₁ g₂ : N →* P
f : M →* N
⊢ Eq (α := M →* P) (({ toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } : (a : M →* N) → M →* P) f : M →* P)
    ((HMul.hMul (α := (M →* N) →* M →* P) { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P }
            { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P } :
          (a : M →* N) → M →* P)
        f :
      M →* P)

Tactic:
mul_comp g₁ g₂ f

Premises used: MonoidHom.mul_comp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
g₁ g₂ : N →* P
f : M →* N
⊢ Eq (α := M →* P) (({ toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } : (a : M →* N) → M →* P) f : M →* P)
    ((HMul.hMul (α := (M →* N) →* M →* P) { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P }
            { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ : (M →* N) →* M →* P } :
          (a : M →* N) → M →* P)
        f :
      M →* P)

Tactic:
exact mul_comp g₁ g₂ f

Premises used: MonoidHom.mul_comp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
inst_3 : MulOneClass Q
f : M →* N →* P
g : Q →* N
m : M
q : Q
⊢ Eq.{uP + 1} (α := P) ((((f.compl₂ g : (a : M) → Q →* P) m : Q →* P) : (a : Q) → P) q : P)
    ((((f : (a : M) → N →* P) m : N →* P) : (a : N) → P) ((g : (a : Q) → N) q : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommMonoid P
inst_3 : CommMonoid Q
f : M →* N →* P
g : P →* Q
m : M
n : N
⊢ Eq.{uQ + 1} (α := Q) ((((f.compr₂ g : (a : M) → N →* Q) m : N →* Q) : (a : N) → Q) n : Q)
    ((g : (a : P) → Q) ((((f : (a : M) → N →* P) m : N →* P) : (a : N) → P) n : P) : Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
I : SemigroupIdeal M
x y : M
⊢ y ∈ I → x * y ∈ I

Tactic:
SubMulAction.smul_mem I x

Premises used: Set.Mem, SubMulAction.smul_mem
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
s : Set M
x : M
⊢ Membership.mem (γ := SemigroupIdeal M) (closure s) x ↔ ∀ (p : SemigroupIdeal M), s ⊆ (↑p : Set M) → x ∈ p

Tactic:
SubMulAction.mem_closure

Premises used: Set.Mem, SubMulAction.mem_closure
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
s : Set M
⊢ s ⊆ (↑(closure s) : Set M)

Tactic:
SubMulAction.subset_closure

Premises used: SubMulAction.subset_closure
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
s : Set M
x : M
hx : x ∈ s
⊢ Membership.mem (γ := SemigroupIdeal M) (closure s) x

Tactic:
SubMulAction.mem_closure_of_mem hx

Premises used: SubMulAction.mem_closure_of_mem, Set.Mem
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
s : Set M
I : SemigroupIdeal M
⊢ closure s ≤ I ↔ s ⊆ (↑I : Set M)

Tactic:
SubMulAction.closure_le

Premises used: SubMulAction.closure_le, Set.Mem
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
s t : Set M
h : s ⊆ t
⊢ LE.le (α := SemigroupIdeal M) (closure s) (closure t)

Tactic:
SubMulAction.closure_mono h

Premises used: Set.Mem, SubMulAction.closure_mono
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
x y : M
hy : y ∈ s
⊢ x • y ∈ s ∪ univ * s

Tactic:
.inr <| mul_mem_mul (mem_univ _) hy

Premises used: Set.union, Set.Mem, setOf, Set.mem_univ, Set.mul_mem_mul, Or.inr
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
x y : M
hy : y ∈ s
⊢ x • y ∈ s ∪ univ * s

Tactic:
exact .inr <| mul_mem_mul (mem_univ _) hy

Premises used: Set.mem_univ, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
x y z : M
hz : z ∈ s
⊢ HSMul.hSMul (β := M) x ((fun (x1 x2 : M) ↦ x1 * x2) y z) ∈ s ∪ univ * s

Tactic:
simpa [← mul_assoc] using .inr <| mul_mem_mul (mem_univ _) hz

Premises used: mul_assoc, Set.mem_univ, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
rw : (↑I : Set M) = s ∪ univ * s
⊢ (↑(closure s) : Set M) = s ∪ univ * s

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ (↑I : Set M) = s ∪ univ * s

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
suffices : closure s = I
⊢ (↑(closure s) : Set M) = s ∪ univ * s

Tactic:
suffices closure s = I by rw [this]; rfl
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
⊢ closure s = I

Tactic:
(closure_le.2 fun x => Or.inl).antisymm fun x hx => hx.elim mem_closure_of_mem ?_

Premises used: Iff.mpr, LE.le.antisymm, SemigroupIdeal.closure_le, SemigroupIdeal.mem_closure_of_mem, Or.elim
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
refine : ∀ (x : M) (hx : x ∈ I), x ∈ univ * s → Membership.mem (γ := SubMulAction M M) (closure s) x
⊢ closure s = I

Tactic:
refine (closure_le.2 fun x => Or.inl).antisymm fun x hx => hx.elim mem_closure_of_mem ?_
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
y z : M
hz : z ∈ s
hx : (fun (x1 x2 : M) ↦ x1 * x2) y z ∈ I
⊢ Membership.mem (γ := SubMulAction M M) (closure s) ((fun (x1 x2 : M) ↦ x1 * x2) y z)

Tactic:
SemigroupIdeal.mul_mem _ _ (mem_closure_of_mem hz)

Premises used: Set.Mem, SemigroupIdeal.mem_closure_of_mem, SemigroupIdeal.mul_mem
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
y z : M
hz : z ∈ s
hx : (fun (x1 x2 : M) ↦ x1 * x2) y z ∈ I
⊢ Membership.mem (γ := SubMulAction M M) (closure s) ((fun (x1 x2 : M) ↦ x1 * x2) y z)

Tactic:
exact SemigroupIdeal.mul_mem _ _ (mem_closure_of_mem hz)

Premises used: SemigroupIdeal.mem_closure_of_mem, SemigroupIdeal.mul_mem
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
x : M
rw : x ∈ s ∪ univ * s ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y * z = x
⊢ Membership.mem (γ := SemigroupIdeal M) (closure s) x ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y * z = x

Tactic:
rw [← SetLike.mem_coe, coe_closure]

Premises used: SemigroupIdeal.coe_closure, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
x : M
⊢ x ∈ s ∪ univ * s ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y * z = x

Tactic:
simp [mem_mul]

Premises used: Set.mem_mul
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Monoid M
s : Set M
rw : s ⊆ univ * s
⊢ (↑(closure s) : Set M) = univ * s

Tactic:
rw [coe_closure, union_eq_right]

Premises used: SemigroupIdeal.coe_closure, Set.union_eq_right
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
hx : x ∈ s
⊢ (fun (x1 x2 : M) ↦ x1 * x2) 1 x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ s ⊆ univ * s

Tactic:
exact fun x hx => ⟨1, mem_univ 1, x, hx, by simp⟩
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
rw : x ∈ univ * s ↔ ∃ (y : M), ∃ z ∈ s, y * z = x
⊢ Membership.mem (γ := SemigroupIdeal M) (closure s) x ↔ ∃ (y : M), ∃ z ∈ s, y * z = x

Tactic:
rw [← SetLike.mem_coe, coe_closure']

Premises used: SetLike.mem_coe, SemigroupIdeal.coe_closure'
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
⊢ x ∈ univ * s ↔ ∃ (y : M), ∃ z ∈ s, y * z = x

Tactic:
simp [mem_mul]

Premises used: Set.mem_mul
-- Module: Mathlib.Algebra.Group.Ideal
Goal:
M : Type u_1
inst : Mul M
I : SemigroupIdeal M
⊢ I.FG ↔ ∃ (s : Finset M), I = closure (↑s : Set M)

Tactic:
SubMulAction.fg_iff

Premises used: SubMulAction.FG, SubMulAction.fg_iff, SemigroupIdeal.FG
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Mul M
a : M
⊢ IsIdempotentElem a ↔ a * a = a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsIdempotentElem
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Mul M
inst_1 : Std.IdempotentOp fun (x1 x2 : M) ↦ x1 * x2
a : M
⊢ IsIdempotentElem a

Tactic:
Std.IdempotentOp.idempotent a

Premises used: Std.IdempotentOp.idempotent, IsIdempotentElem
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Mul M
a : M
ha : IsIdempotentElem a
⊢ a * a = a

Tactic:
ha

Premises used: IsIdempotentElem
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
S : Type u_3
inst : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
rw : a * b * (a * b) = a * b
rw₁ : a * a * (b * b) = a * b
rw₂ : a * (b * b) = a * b
rw₃ rw₄ : a * b = a * b
⊢ IsIdempotentElem (a * b)

Tactic:
rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]

Premises used: Commute.mul_mul_mul_comm, Commute.symm, IsIdempotentElem, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
S : Type u_3
inst : CommSemigroup S
a b : S
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a * b)

Tactic:
ha.mul_of_commute (.all ..) hb

Premises used: IsIdempotentElem.mul_of_commute, Commute.all
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : MulOneClass M
⊢ IsIdempotentElem.{u_1} (M := M) 1

Tactic:
mul_one _

Premises used: IsIdempotentElem, mul_one
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq.{u_1 + 1} (α := M) (↑1 : M) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
h_1 : IsIdempotentElem (a ^ n)
rw : (a * a) ^ n.succ
| a ^ n.succ

Tactic:
rw [← h.eq]

Premises used: IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
h_1 : IsIdempotentElem (a ^ n)
conv_rhs : a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
⊢ a ^ n.succ * a ^ n.succ = a ^ n.succ

Tactic:
conv_rhs => rw [← h.eq]

Premises used: IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
h_1 : IsIdempotentElem (a ^ n)
rw : HPow.hPow (β := ℕ) (a ^ n.succ) 2 = (a * a) ^ n.succ
rw₁ : HPow.hPow (β := ℕ) (a ^ n.succ) 2 = HPow.hPow (β := ℕ) a 2 ^ n.succ
rw₂ : a ^ (n.succ * 2) = HPow.hPow (β := ℕ) a 2 ^ n.succ
rw₃ rw₄ : a ^ (n.succ * 2) = a ^ (n.succ * 2)
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ

Tactic:
rw [← sq, ← sq, ← pow_mul, ← pow_mul']

Premises used: sq, pow_mul, pow_mul'
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
rw : a ^ (n + 1) * a = a
rw₁ : a * a = a
rw₂ rw₃ : a = a
⊢ a ^ (n.succ + 1) = a

Tactic:
rw [pow_succ, ih, h.eq]

Premises used: pow_succ, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsIdempotentElem a
n : ℕ
hn : n ≠ 0
obtain : ∀ (i : ℕ) (hn : i + 1 ≠ 0), a ^ (i + 1) = a
⊢ a ^ n = a

Tactic:
obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsIdempotentElem a
i : ℕ
hn : i + 1 ≠ 0
⊢ a ^ (i + 1) = a

Tactic:
h.pow_succ_eq _

Premises used: IsIdempotentElem.pow_succ_eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsIdempotentElem a
i : ℕ
hn : i + 1 ≠ 0
⊢ a ^ (i + 1) = a

Tactic:
exact h.pow_succ_eq _

Premises used: IsIdempotentElem.pow_succ_eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
have : ∀ (q : M) (eq : q * a = 1), a = 1
⊢ a = 1

Tactic:
have ⟨q, eq⟩ := h.exists_left_inv
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
rw : a = q * a
rw₁ : a * a = q * (a * a)
rw₂ : a * a = q * a * a
rw₃ : a * a = 1 * a
rw₄ : a * a = a
rw₅ rw₆ : a = a
⊢ a = 1

Tactic:
rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]

Premises used: mul_assoc, IsIdempotentElem.eq, one_mul
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
h : IsUnit.{u_1} (M := M) 1
⊢ IsIdempotentElem.{u_1} (M := M) 1

Tactic:
.one

Premises used: IsIdempotentElem.one
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : Monoid M
h : IsUnit.{u_1} (M := M) 1
⊢ IsIdempotentElem.{u_1} (M := M) 1

Tactic:
exact .one
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_1
inst : CancelMonoid M
a : M
⊢ IsIdempotentElem a ↔ a = 1

Tactic:
simp [IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_4
N : Type u_5
F : Type u_6
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) e : N) ((f : (a : M) → N) e : N) = (f : (a : M) → N) e
rw₁ : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) (e * e) : N) ((f : (a : M) → N) e : N)
rw₂ rw₃ : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) e : N) ((f : (a : M) → N) e : N)
⊢ IsIdempotentElem.{u_5} (M := N) ((f : (a : M) → N) e : N)

Tactic:
rw [IsIdempotentElem, ← map_mul, he.eq]

Premises used: map_mul, IsIdempotentElem, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_4
inst : Semigroup M
x : M
hx : IsIdempotentElem x
y : M
⊢ y * x * x = y * x

Tactic:
mul_assoc y x x ▸ congrArg (y * ·) hx.eq

Premises used: HMul.hMul, congrArg, mul_assoc, Eq.rec, IsIdempotentElem.eq, Eq.symm
-- Module: Mathlib.Algebra.Group.Idempotent
Goal:
M : Type u_4
inst : Semigroup M
x : M
hx : IsIdempotentElem x
y : M
⊢ x * (x * y) = x * y

Tactic:
mul_assoc x x y ▸ congrArg (· * y) hx.eq

Premises used: HMul.hMul, congrArg, mul_assoc, Eq.rec, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
pos : ∀ (hs : a ∈ s), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
neg : ∀ (hs : ¬a ∈ s), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
by_cases hs : a ∈ s
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
pos : ∀ (ht : a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
neg : ∀ (ht : ¬a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
by_cases ht : a ∈ t
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
pos : ∀ (ht : a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
neg : ∀ (ht : ¬a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
by_cases ht : a ∈ t
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
⊢ (s ∪ t).mulIndicator f * (s ∩ t).mulIndicator f = s.mulIndicator f * t.mulIndicator f

Tactic:
funext <| mulIndicator_union_mul_inter_apply f s t

Premises used: funext, Set.mulIndicator_union_mul_inter_apply
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
rw : (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a
rw₁ : (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * 1
rw₂ rw₃ : (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a
⊢ (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_notMem h, mul_one]

Premises used: Set.mulIndicator_of_notMem, Set.mulIndicator_union_mul_inter_apply, mul_one
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s t : Set α
h : Disjoint s t
f : α → M
⊢ (s ∪ t).mulIndicator f = fun (a : α) ↦ s.mulIndicator f a * t.mulIndicator f a

Tactic:
funext fun _ => mulIndicator_union_of_notMem_inter (fun ha => h.le_bot ha) _

Premises used: Disjoint.le_bot, Set.mulIndicator_union_of_notMem_inter, funext
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s t : Set α
f : α → M
⊢ (s ∆ t).mulIndicator f = (s \ t).mulIndicator f * (t \ s).mulIndicator f

Tactic:
mulIndicator_union_of_disjoint (disjoint_sdiff_self_right.mono_left sdiff_le) _

Premises used: disjoint_sdiff_self_right, sdiff_le, Disjoint.mono_left, Set.mulIndicator_union_of_disjoint, symmDiff
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
h : ∀ (x : α), s.mulIndicator (fun (a : α) ↦ f a * g a) x = s.mulIndicator f x * s.mulIndicator g x
⊢ Eq (α := (x : α) → M) (s.mulIndicator fun (a : α) ↦ f a * g a) fun (a : α) ↦ s.mulIndicator f a * s.mulIndicator g a

Tactic:
funext
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
h : (if x ∈ s then f x * g x else 1) = (if x ∈ s then f x else 1) * if x ∈ s then g x else 1
⊢ s.mulIndicator (fun (a : α) ↦ f a * g a) x = s.mulIndicator f x * s.mulIndicator g x

Tactic:
simp only [mulIndicator]

Premises used: Set.mulIndicator