awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
M₀ : Type u_6
inst : CommMonoidWithZero M₀
n : ℕ
hn : n ≠ 0
⊢ Eq.{u_6 + 1} (α := (a : M₀) → M₀) (⇑(powMonoidWithZeroHom hn) : (a : M₀) → M₀) fun (x : M₀) ↦ x ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
M₀ : Type u_6
inst : CommMonoidWithZero M₀
n : ℕ
hn : n ≠ 0
a : M₀
⊢ (powMonoidWithZeroHom hn : (a : M₀) → M₀) a = a ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Idempotent
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ IsIdempotentElem.{u_1} (M := M₀) 0

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_zero, IsIdempotentElem
-- Module: Mathlib.Algebra.GroupWithZero.Idempotent
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ Eq.{u_1 + 1} (α := M₀) (↑0 : M₀) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
h : ∀ (x : ι), s.indicator (fun (i : ι) ↦ f i * g i) x = s.indicator f x * s.indicator g x
⊢ Eq (α := (x : ι) → M₀) (s.indicator fun (i : ι) ↦ f i * g i) fun (i : ι) ↦ s.indicator f i * s.indicator g i

Tactic:
funext
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
h : (if x ∈ s then f x * g x else 0) = (if x ∈ s then f x else 0) * if x ∈ s then g x else 0
⊢ s.indicator (fun (i : ι) ↦ f i * g i) x = s.indicator f x * s.indicator g x

Tactic:
simp only [indicator]

Premises used: Set.indicator
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
pos : x ∈ s → f x * g x = f x * g x
neg : ¬x ∈ s → 0 = HMul.hMul (α := M₀) 0 0
⊢ (if x ∈ s then f x * g x else 0) = (if x ∈ s then f x else 0) * if x ∈ s then g x else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
h : x ∈ s
⊢ f x * g x = f x * g x

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
h : ¬x ∈ s
neg neg₁ : Eq.{u_4 + 1} (α := M₀) 0 0
⊢ 0 = HMul.hMul (α := M₀) 0 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
simp : (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i
⊢ s.indicator (fun (j : ι) ↦ f j * g j) i = s.indicator f i * g i

Tactic:
simp only [indicator]

Premises used: Set.indicator
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
pos : i ∈ s → f i * g i = f i * g i
neg : ¬i ∈ s → 0 = 0 * g i
⊢ (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h : i ∈ s
⊢ f i * g i = f i * g i

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h : ¬i ∈ s
neg neg₁ : Eq.{u_4 + 1} (α := M₀) 0 0
⊢ 0 = 0 * g i

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
simp : (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0
⊢ s.indicator (fun (j : ι) ↦ f j * g j) i = f i * s.indicator g i

Tactic:
simp only [indicator]

Premises used: Set.indicator
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
pos : i ∈ s → f i * g i = f i * g i
neg : ¬i ∈ s → 0 = f i * 0
⊢ (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h : ¬i ∈ s
neg neg₁ : Eq.{u_4 + 1} (α := M₀) 0 0
⊢ 0 = f i * 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
rw rw₁ : s.indicator f i * a = s.indicator f i * a
⊢ s.indicator (fun (x : ι) ↦ f x * a) i = s.indicator f i * a

Tactic:
rw [indicator_mul_left]

Premises used: Set.indicator_mul_left
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
rw rw₁ : a * s.indicator f i = a * s.indicator f i
⊢ s.indicator (fun (x : ι) ↦ a * f x) i = a * s.indicator f i

Tactic:
rw [indicator_mul_right]

Premises used: Set.indicator_mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
rw : s.indicator (t.indicator fun (j : ι) ↦ f j * g j) i = s.indicator f i * t.indicator g i
⊢ (s ∩ t).indicator (fun (j : ι) ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
rw [← Set.indicator_indicator]

Premises used: Set.indicator_indicator
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
simp_rw : (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0
⊢ s.indicator (t.indicator fun (j : ι) ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
simp_rw [indicator]

Premises used: Set.indicator
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
pos : i ∈ s → i ∈ t → f i * g i = f i * g i
neg : i ∈ s → ¬i ∈ t → 0 = f i * 0
pos₁ : ¬i ∈ s → i ∈ t → 0 = 0 * g i
neg₁ : ¬i ∈ s → ¬i ∈ t → 0 = HMul.hMul (α := M₀) 0 0
⊢ (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h : i ∈ s
h_1 : i ∈ t
⊢ f i * g i = f i * g i

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h : i ∈ s
h_1 : ¬i ∈ t
⊢ 0 = f i * 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h : ¬i ∈ s
h_1 : i ∈ t
⊢ 0 = 0 * g i

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h : ¬i ∈ s
h_1 : ¬i ∈ t
⊢ 0 = HMul.hMul (α := M₀) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s t : Set ι
x : ι
simp : Eq.{u_4 + 1} (α := M₀) ((s ∩ t).indicator 1 x) ((s ∩ t).indicator (fun (j : ι) ↦ 1) x)
⊢ (s ∩ t).indicator 1 x = HMul.hMul (α := (x : ι) → M₀) (β := (x : ι) → M₀) (s.indicator 1) (t.indicator 1) x

Tactic:
simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]

Premises used: Pi.mul_apply, Pi.one_apply, Set.inter_indicator_mul, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s t : Set ι
x : ι
⊢ Eq.{u_4 + 1} (α := M₀) ((s ∩ t).indicator 1 x) ((s ∩ t).indicator (fun (j : ι) ↦ 1) x)

Tactic:
congr
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
simp_rw :
  (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = HMul.hMul (α := M₀) (if i ∈ s then 1 i else 0) (if j ∈ t then 1 j else 0)
⊢ (s ×ˢ t).indicator 1 (i, j) = HMul.hMul (α := M₀) (s.indicator 1 i) (t.indicator 1 j)

Tactic:
simp_rw [indicator, mem_prod_eq]

Premises used: Set.mem_prod_eq, Set.indicator
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
pos : ∀ (h₀ : i ∈ s ∧ j ∈ t), i ∈ s → j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) (1 i) (1 j)
neg : ∀ (h₀ : i ∈ s ∧ j ∈ t), i ∈ s → ¬j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) (1 i) 0
pos₁ : ∀ (h₀ : i ∈ s ∧ j ∈ t), ¬i ∈ s → j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) 0 (1 j)
neg₁ : ∀ (h₀ : i ∈ s ∧ j ∈ t), ¬i ∈ s → ¬j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) 0 0
pos₂ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), i ∈ s → j ∈ t → 0 = HMul.hMul (α := M₀) (1 i) (1 j)
neg₂ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), i ∈ s → ¬j ∈ t → 0 = HMul.hMul (α := M₀) (1 i) 0
pos₃ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), ¬i ∈ s → j ∈ t → 0 = HMul.hMul (α := M₀) 0 (1 j)
neg₃ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), ¬i ∈ s → ¬j ∈ t → 0 = HMul.hMul (α := M₀) 0 0
⊢ (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = HMul.hMul (α := M₀) (if i ∈ s then 1 i else 0) (if j ∈ t then 1 j else 0)

Tactic:
split_ifs with h₀
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : i ∈ s
h_1 : j ∈ t
⊢ 1 (i, j) = HMul.hMul (α := M₀) (1 i) (1 j)

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : i ∈ s
h_1 : ¬j ∈ t
neg : Eq.{u_4 + 1} (α := M₀) 1 0
⊢ 1 (i, j) = HMul.hMul (α := M₀) (1 i) 0

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : ¬i ∈ s
h_1 : j ∈ t
pos : Eq.{u_4 + 1} (α := M₀) 1 0
⊢ 1 (i, j) = HMul.hMul (α := M₀) 0 (1 j)

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : ¬i ∈ s
h_1 : ¬j ∈ t
neg : Eq.{u_4 + 1} (α := M₀) 1 0
⊢ 1 (i, j) = HMul.hMul (α := M₀) 0 0

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h : i ∈ s
h_1 : j ∈ t
pos : Eq.{u_4 + 1} (α := M₀) 0 1
⊢ 0 = HMul.hMul (α := M₀) (1 i) (1 j)

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h : i ∈ s
h_1 : ¬j ∈ t
⊢ 0 = HMul.hMul (α := M₀) (1 i) 0

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h : ¬i ∈ s
h_1 : j ∈ t
⊢ 0 = HMul.hMul (α := M₀) 0 (1 j)

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h : ¬i ∈ s
h_1 : ¬j ∈ t
⊢ 0 = HMul.hMul (α := M₀) 0 0

Tactic:
simp only [Pi.one_apply, mul_one, mul_zero]

Premises used: Pi.one_apply, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : i ∈ s
h_1 : ¬j ∈ t
⊢ i ∈ s

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : i ∈ s
h_1 : ¬j ∈ t
left : i ∈ s
⊢ j ∈ t

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : ¬i ∈ s
h_1 : j ∈ t
⊢ i ∈ s

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : ¬i ∈ s
h_1 : j ∈ t
left : i ∈ s
⊢ j ∈ t

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : ¬i ∈ s
h_1 : ¬j ∈ t
⊢ i ∈ s

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h : ¬i ∈ s
h_1 : ¬j ∈ t
left : i ∈ s
⊢ j ∈ t

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h : i ∈ s
h_1 : j ∈ t
pos : i ∈ s → j ∈ t → ∀ (h₀ : ¬i ∈ s), Eq.{u_4 + 1} (α := M₀) 0 1
pos₁ : i ∈ s → j ∈ t → ∀ (h₀ : ¬j ∈ t), Eq.{u_4 + 1} (α := M₀) 0 1
⊢ Eq.{u_4 + 1} (α := M₀) 0 1

Tactic:
tauto
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
inst_1 : Nontrivial M₀
⊢ Eq.{u_4 + 1} (α := M₀) (s.indicator 1 i) 0 ↔ ¬i ∈ s

Tactic:
simp [indicator_apply, imp_false]

Premises used: Set.indicator_apply, imp_false
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
inst_1 : Nontrivial M₀
⊢ Eq.{u_4 + 1} (α := M₀) (s.indicator 1 i) 0 ↔ ¬i ∈ s

Tactic:
classical simp [indicator_apply, imp_false]

Premises used: Set.indicator_apply, imp_false
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
inst_1 : Nontrivial M₀
⊢ Eq.{u_4 + 1} (α := M₀) (s.indicator 1 i) 1 ↔ i ∈ s

Tactic:
simp [indicator_apply, imp_false]

Premises used: Set.indicator_apply, imp_false
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
inst_1 : Nontrivial M₀
⊢ Eq.{u_4 + 1} (α := M₀) (s.indicator 1 i) 1 ↔ i ∈ s

Tactic:
classical simp [indicator_apply, imp_false]

Premises used: Set.indicator_apply, imp_false
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s t : Set ι
inst_1 : Nontrivial M₀
h : Eq (α := (x : ι) → M₀) (s.indicator 1) (t.indicator 1)
h₁ : ∀ (x : ι), x ∈ s ↔ x ∈ t
⊢ s = t

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s t : Set ι
inst_1 : Nontrivial M₀
h : Eq (α := (x : ι) → M₀) (s.indicator 1) (t.indicator 1)
x : ι
h₁ : Eq.{u_4 + 1} (α := M₀) (s.indicator 1 x) 1 ↔ Eq.{u_4 + 1} (α := M₀) (t.indicator 1 x) 1
⊢ x ∈ s ↔ x ∈ t

Tactic:
simp_rw [← indicator_eq_one_iff_mem M₀, h]

Premises used: Set.indicator_eq_one_iff_mem
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : Zero R
inst_1 : One R
inst_2 : NeZero.{u_5} (R := R) 1
⊢ Eq.{u_1 + 1} (α := Set ι) (support.{u_1, u_5} (M := R) 1) univ

Tactic:
support_const one_ne_zero

Premises used: Function.support_const, one_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : Zero R
inst_1 : One R
inst_2 : NeZero.{u_5} (R := R) 1
⊢ Eq.{u_1 + 1} (α := Set ι) (mulSupport.{u_1, u_5} (M := R) 0) univ

Tactic:
mulSupport_const zero_ne_one

Premises used: zero_ne_one, Function.mulSupport_const
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (x : ι) ↦ f x * g x) x
hf : f x = 0
⊢ Eq.{u_4 + 1} (α := M₀) ((fun (x : ι) ↦ f x * g x) x) 0

Tactic:
simp only [hf, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (x : ι) ↦ f x * g x) x
hg : g x = 0
⊢ Eq.{u_4 + 1} (α := M₀) ((fun (x : ι) ↦ f x * g x) x) 0

Tactic:
simp only [hg, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
f g : ι → M₀
x : ι
⊢ Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (x : ι) ↦ f x * g x) x ↔ x ∈ support f ∩ support g

Tactic:
simp [not_or]

Premises used: not_or
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
f g : ι → M₀
⊢ support (f * g) = support f ∩ support g

Tactic:
support_mul _ _

Premises used: Function.support_mul
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
f : ι → M₀
hf : ∀ (x : ι), f x ≠ 0
g : ι → M₀
⊢ (support.{u_1, u_4} (M := M₀) fun (x : ι) ↦ f x * g x) = support g

Tactic:
simp [support_eq_univ hf]

Premises used: Function.support_eq_univ
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
f g : ι → M₀
hg : ∀ (x : ι), g x ≠ 0
⊢ (support.{u_1, u_4} (M := M₀) fun (x : ι) ↦ f x * g x) = support f

Tactic:
simp [support_eq_univ hg]

Premises used: Function.support_eq_univ
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
h : ∀ (x : ι), Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (a : ι) ↦ f a ^ n) x ↔ x ∈ support f
⊢ (support.{u_1, u_4} (M := M₀) fun (a : ι) ↦ f a ^ n) = support f

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x : ι
⊢ Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (a : ι) ↦ f a ^ n) x ↔ x ∈ support f

Tactic:
(pow_eq_zero_iff hn).not

Premises used: pow_eq_zero_iff, Set.Mem, setOf, Iff.not, Function.support, Not
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x : ι
⊢ Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (a : ι) ↦ f a ^ n) x ↔ x ∈ support f

Tactic:
exact (pow_eq_zero_iff hn).not

Premises used: pow_eq_zero_iff, Iff.not
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
⊢ support (f ^ n) = support f

Tactic:
support_pow _ hn

Premises used: Function.support_pow
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
f : ι → G₀
⊢ (support.{u_1, u_3} (M := G₀) fun (a : ι) ↦ (f a)⁻¹) = support f

Tactic:
Set.ext fun _ ↦ not_congr inv_eq_zero

Premises used: Set.ext, inv_eq_zero, not_congr
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
f : ι → G₀
⊢ support f⁻¹ = support f

Tactic:
support_inv _

Premises used: Function.support_inv
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
f g : ι → G₀
⊢ (support.{u_1, u_3} (M := G₀) fun (a : ι) ↦ f a / g a) = support f ∩ support g

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
f g : ι → G₀
⊢ support (f / g) = support f ∩ support g

Tactic:
support_div _ _

Premises used: Function.support_div
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddLeftCancelMonoid R
f : ι → R
⊢ (mulSupport.{u_1, u_5} (M := R) fun (x : ι) ↦ 1 + f x) = support f

Tactic:
Set.ext fun _ ↦ not_congr add_eq_left

Premises used: Set.ext, add_eq_left, not_congr
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddLeftCancelMonoid R
f : ι → R
⊢ mulSupport (1 + f) = support f

Tactic:
mulSupport_one_add f

Premises used: Function.mulSupport_one_add
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddRightCancelMonoid R
f : ι → R
⊢ (mulSupport.{u_1, u_5} (M := R) fun (x : ι) ↦ f x + 1) = support f

Tactic:
Set.ext fun _ ↦ not_congr add_eq_right

Premises used: Set.ext, add_eq_right, not_congr
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddRightCancelMonoid R
f : ι → R
⊢ mulSupport (f + 1) = support f

Tactic:
mulSupport_add_one f

Premises used: Function.mulSupport_add_one
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddGroup R
f : ι → R
rw : mulSupport (1 + -f) = support f
rw₁ : support (-f) = support f
rw₂ rw₃ : support f = support f
⊢ mulSupport (1 - f) = support f

Tactic:
rw [sub_eq_add_neg, mulSupport_one_add', support_neg]

Premises used: Function.mulSupport_one_add', sub_eq_add_neg, Function.support_neg
-- Module: Mathlib.Algebra.GroupWithZero.Indicator
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddGroup R
f : ι → R
⊢ (mulSupport.{u_1, u_5} (M := R) fun (x : ι) ↦ 1 - f x) = support f

Tactic:
mulSupport_one_sub' f

Premises used: Function.mulSupport_one_sub'
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : MulZeroClass M₀
inst_1 : Mul M₀'
inst_2 : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (0 * a) = f 0

Tactic:
simp only [mul, zero, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : MulZeroClass M₀
inst_1 : Mul M₀'
inst_2 : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (a * 0) = f 0

Tactic:
simp only [mul, zero, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : MulZeroClass M₀
inst_1 : Mul M₀'
inst_2 : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ 0 * f x = 0

Tactic:
simp only [← zero, ← mul, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : MulZeroClass M₀
inst_1 : Mul M₀'
inst_2 : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ f x * 0 = 0

Tactic:
simp only [← zero, ← mul, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
rw : f (a * b) = 0
rw₁ : f 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M₀') 0 0
⊢ f a * f b = 0

Tactic:
rw [← mul, H, zero]