awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
is_surj : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
is_comm : IsMulCommutative M
a b : N
⊢ a * b = b * a
have have : ∀ (a' : M) (ha' : (f : (a : M) → N) a' = a), a * b = b * a
Tactic: have ⟨a', ha'⟩ := is_surj a
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
is_surj : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : (f : (a : M) → N) a' = a
⊢ a * b = b * a
have have : ∀ (b' : M) (hb' : (f : (a : M) → N) b' = b), a * b = b * a
Tactic: have ⟨b', hb'⟩ := is_surj b
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : MulOne M
n : ℕ
f : Monoid.End M
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M)
have zero : Eq (α := M → M) (⇑f : (a : M) → M)^[0] (⇑(npowRec 0 f) : (a : M) → M)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : MulOne M
n : ℕ
f : Monoid.End M
zero : Eq (α := M → M) (⇑f : (a : M) → M)^[0] (⇑(npowRec 0 f) : (a : M) → M)
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M)
have succ : ∀ (n : ℕ),
  Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M) →
    Eq (α := M → M) (⇑f : (a : M) → M)^[n + 1] (⇑(npowRec (n + 1) f) : (a : M) → M)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : MulOne M
f : Monoid.End M
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[0] (⇑(npowRec 0 f) : (a : M) → M)
have zero : Eq.{u_4 + 1} (α := M → M) id (⇑1 : (a : M) → M)
Tactic: simp [npowRec, *]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : MulOne M
f : Monoid.End M
n : ℕ
h : Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M)
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[n + 1] (⇑(npowRec (n + 1) f) : (a : M) → M)
have succ : Eq (α := M → M) (comp (β := M) (⇑(npowRec n f) : (a : M) → M) (⇑f : (a : M) → M)) (⇑(npowRec n f * f) : (a : M) → M)
Tactic: simp [npowRec, *]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : One M
inst_1 : One N
inst_2 : One P
f : OneHom N P
⊢ Eq (α := OneHom M P) (f.comp 1) 1
have h : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((f.comp 1 : (a : M) → P) x : P) ((1 : (a : M) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : MulOne M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : N →* P
⊢ Eq (α := M →* P) (f.comp 1) 1
have h : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((f.comp 1 : (a : M) → P) x : P) ((1 : (a : M) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Instances (goal)
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
⊢ Eq (α := (M →* N) →* M →* P) { toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } 1
have h : ∀ (f : M →* N),
  Eq (α := M →* P) (({ toFun := comp 1, map_one' := sorry, map_mul' := sorry } : (a : M →* N) → M →* P) f : M →* P)
    ((1 : (a : M →* N) → M →* P) f : M →* P)
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Instances (goal)
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
⊢ { 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 }
have h : ∀ (f : M →* N),
  Eq (α := M →* P) (({ toFun := (g₁ * g₂).comp, map_one' := sorry, map_mul' := sorry } : (a : M →* N) → M →* P) f : M →* P)
    ((HMul.hMul (α := (M →* N) →* M →* P) { toFun := g₁.comp, map_one' := sorry, map_mul' := sorry : (M →* N) →* M →* P }
            { toFun := g₂.comp, map_one' := sorry, map_mul' := sorry : (M →* N) →* M →* P } :
          (a : M →* N) → M →* P)
        f :
      M →* P)
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Algebra.Group.Ideal (goal)
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ (↑(closure s) : Set M) = s ∪ univ * s
have rw : (↑I : Set M) = s ∪ univ * s
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Group.Ideal (goal)
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
⊢ (↑(closure s) : Set M) = s ∪ univ * s
have suffices : closure s = I
Tactic: suffices closure s = I by rw [this]; rfl
-- Lean 4 proof step from Mathlib.Algebra.Group.Ideal (goal)
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
⊢ closure s = I
have refine : ∀ (x : M) (hx : x ∈ I), x ∈ univ * s → Membership.mem (γ := SubMulAction M M) (closure s) x
Tactic: refine (closure_le.2 fun x => Or.inl).antisymm fun x hx => hx.elim mem_closure_of_mem ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Ideal (goal)
Goal:
M : Type u_1
inst : Semigroup M
s : Set M
x : M
⊢ Membership.mem (γ := SemigroupIdeal M) (closure s) x ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y * z = x
have rw : x ∈ s ∪ univ * s ↔ x ∈ s ∨ ∃ (y : M), ∃ z ∈ s, y * z = x
Tactic: rw [← SetLike.mem_coe, coe_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Ideal (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
⊢ (↑(closure s) : Set M) = univ * s
have rw : s ⊆ univ * s
Tactic: rw [coe_closure, union_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Ideal (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
x : M
⊢ Membership.mem (γ := SemigroupIdeal M) (closure s) x ↔ ∃ (y : M), ∃ z ∈ s, y * z = x
have rw : x ∈ univ * s ↔ ∃ (y : M), ∃ z ∈ s, y * z = x
Tactic: rw [← SetLike.mem_coe, coe_closure']
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
S : Type u_3
inst : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a * b)
have rw : a * b * (a * b) = a * b
Tactic: rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ IsIdempotentElem (a * b)
have rw₁ : a * a * (b * b) = a * b
Tactic: rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ IsIdempotentElem (a * b)
have rw₂ : a * (b * b) = a * b
Tactic: rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ IsIdempotentElem (a * b)
have rw₃ : a * b = a * b
Tactic: rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
h_1 : IsIdempotentElem (a ^ n)
| a ^ n.succ
have rw : (a * a) ^ n.succ
Tactic: rw [← h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
h_1 : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = a ^ n.succ
have conv_rhs : a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
Tactic: conv_rhs => rw [← h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
h_1 : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
have rw : HPow.hPow (β := ℕ) (a ^ n.succ) 2 = (a * a) ^ n.succ
Tactic: rw [← sq, ← sq, ← pow_mul, ← pow_mul']
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
have rw₁ : HPow.hPow (β := ℕ) (a ^ n.succ) 2 = HPow.hPow (β := ℕ) a 2 ^ n.succ
Tactic: rw [← sq, ← sq, ← pow_mul, ← pow_mul']
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
have rw₂ : a ^ (n.succ * 2) = HPow.hPow (β := ℕ) a 2 ^ n.succ
Tactic: rw [← sq, ← sq, ← pow_mul, ← pow_mul']
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
have rw₃ : a ^ (n.succ * 2) = a ^ (n.succ * 2)
Tactic: rw [← sq, ← sq, ← pow_mul, ← pow_mul']
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
n_1 : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a ^ (n.succ + 1) = a
have rw : a ^ (n + 1) * a = a
Tactic: rw [pow_succ, ih, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a ^ (n.succ + 1) = a
have rw₁ : a * a = a
Tactic: rw [pow_succ, ih, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a ^ (n.succ + 1) = a
have rw₂ : a = a
Tactic: rw [pow_succ, ih, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsIdempotentElem a
n : ℕ
hn : n ≠ 0
⊢ a ^ n = a
have obtain : ∀ (i : ℕ) (hn : i + 1 ≠ 0), a ^ (i + 1) = a
Tactic: obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
⊢ a = 1
have have : ∀ (q : M) (eq : q * a = 1), a = 1
Tactic: have ⟨q, eq⟩ := h.exists_left_inv
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a = 1
have rw : a = q * a
Tactic: rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a = 1
have rw₁ : a * a = q * (a * a)
Tactic: rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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)
⊢ a = 1
have rw₂ : a * a = q * a * a
Tactic: rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a = 1
have rw₃ : a * a = 1 * a
Tactic: rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a = 1
have rw₄ : a * a = a
Tactic: rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ a = 1
have rw₅ : a = a
Tactic: rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ IsIdempotentElem.{u_5} (M := N) ((f : (a : M) → N) e : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) e : N) ((f : (a : M) → N) e : N) = (f : (a : M) → N) e
Tactic: rw [IsIdempotentElem, ← map_mul, he.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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
⊢ IsIdempotentElem.{u_5} (M := N) ((f : (a : M) → N) e : N)
have rw₁ : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) (e * e) : N) ((f : (a : M) → N) e : N)
Tactic: rw [IsIdempotentElem, ← map_mul, he.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Idempotent (goal)
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)
⊢ IsIdempotentElem.{u_5} (M := N) ((f : (a : M) → N) e : N)
have rw₂ : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) e : N) ((f : (a : M) → N) e : N)
Tactic: rw [IsIdempotentElem, ← map_mul, he.eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have pos : ∀ (hs : a ∈ s), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Tactic: by_cases hs : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
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
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have neg : ∀ (hs : ¬a ∈ s), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Tactic: by_cases hs : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have pos : ∀ (ht : a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Tactic: by_cases ht : a ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
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
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have neg : ∀ (ht : ¬a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Tactic: by_cases ht : a ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have pos : ∀ (ht : a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Tactic: by_cases ht : a ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
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
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have neg : ∀ (ht : ¬a ∈ t), (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
Tactic: by_cases ht : a ∈ t
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have rw : (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a
Tactic: rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_notMem h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
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
⊢ (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have rw₁ : (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * 1
Tactic: rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_notMem h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
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
⊢ (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
have rw₂ : (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a
Tactic: rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_notMem h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
⊢ Eq (α := (x : α) → M) (s.mulIndicator fun (a : α) ↦ f a * g a) fun (a : α) ↦ s.mulIndicator f a * s.mulIndicator g a
have h : ∀ (x : α), s.mulIndicator (fun (a : α) ↦ f a * g a) x = s.mulIndicator f x * s.mulIndicator g x
Tactic: funext
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
⊢ s.mulIndicator (fun (a : α) ↦ f a * g a) x = s.mulIndicator f x * s.mulIndicator g x
have 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
Tactic: simp only [mulIndicator]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
⊢ (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
have pos : x ∈ s → f x * g x = f x * g x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
pos : x ∈ s → f x * g x = f x * g x
⊢ (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
have neg : ¬x ∈ s → 1 = HMul.hMul (α := M) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
h : ¬x ∈ s
⊢ 1 = HMul.hMul (α := M) 1 1
have neg : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport f).mulIndicator (f * g) = f
have refine : ∀ (x : α) (hx : x ∈ mulSupport f), (f * g) x = f x
Tactic: refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (hypothesis)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
⊢ (f * g) x = f x
have this : g x = 1
Tactic: have : g x = 1 := notMem_mulSupport.1 (disjoint_left.1 h hx)
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ (f * g) x = f x
have rw : f x * g x = f x
Tactic: rw [Pi.mul_apply, this, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
rw : f x * g x = f x
⊢ (f * g) x = f x
have rw₁ : f x * 1 = f x
Tactic: rw [Pi.mul_apply, this, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
rw : f x * g x = f x
rw₁ : f x * 1 = f x
⊢ (f * g) x = f x
have rw₂ : f x = f x
Tactic: rw [Pi.mul_apply, this, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport g).mulIndicator (f * g) = g
have refine : ∀ (x : α) (hx : x ∈ mulSupport g), (f * g) x = g x
Tactic: refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (hypothesis)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x
have this : f x = 1
Tactic: have : f x = 1 := notMem_mulSupport.1 (disjoint_right.1 h hx)
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x
have rw : f x * g x = g x
Tactic: rw [Pi.mul_apply, this, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
rw : f x * g x = g x
⊢ (f * g) x = g x
have rw₁ : 1 * g x = g x
Tactic: rw [Pi.mul_apply, this, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
rw : f x * g x = g x
rw₁ : 1 * g x = g x
⊢ (f * g) x = g x
have rw₂ : g x = g x
Tactic: rw [Pi.mul_apply, this, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Indicator (goal)
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
⊢ s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise (β := fun (i : α) ↦ M) f g
have h : ∀ (x : α), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
Tactic: ext x