awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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
have neg : ¬x ∈ s → 0 = HMul.hMul (α := M₀) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
h : ¬x ∈ s
⊢ 0 = HMul.hMul (α := M₀) 0 0
have neg : Eq.{u_4 + 1} (α := M₀) 0 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun (j : ι) ↦ f j * g j) i = s.indicator f i * g i
have simp : (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i
Tactic: simp only [indicator]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i
have pos : i ∈ s → f i * g i = f i * g i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i
have neg : ¬i ∈ s → 0 = 0 * g i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h : ¬i ∈ s
⊢ 0 = 0 * g i
have neg : Eq.{u_4 + 1} (α := M₀) 0 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun (j : ι) ↦ f j * g j) i = f i * s.indicator g i
have simp : (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0
Tactic: simp only [indicator]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0
have pos : i ∈ s → f i * g i = f i * g i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0
have neg : ¬i ∈ s → 0 = f i * 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h : ¬i ∈ s
⊢ 0 = f i * 0
have neg : Eq.{u_4 + 1} (α := M₀) 0 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun (x : ι) ↦ f x * a) i = s.indicator f i * a
have rw : s.indicator f i * a = s.indicator f i * a
Tactic: rw [indicator_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun (x : ι) ↦ a * f x) i = a * s.indicator f i
have rw : a * s.indicator f i = a * s.indicator f i
Tactic: rw [indicator_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (s ∩ t).indicator (fun (j : ι) ↦ f j * g j) i = s.indicator f i * t.indicator g i
have rw : s.indicator (t.indicator fun (j : ι) ↦ f j * g j) i = s.indicator f i * t.indicator g i
Tactic: rw [← Set.indicator_indicator]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun (j : ι) ↦ f j * g j) i = s.indicator f i * t.indicator g i
have 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
Tactic: simp_rw [indicator]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (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
have pos : i ∈ s → i ∈ t → f i * g i = f i * g i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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
have neg : i ∈ s → ¬i ∈ t → 0 = f i * 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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
have pos₁ : ¬i ∈ s → i ∈ t → 0 = 0 * g i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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
have neg₁ : ¬i ∈ s → ¬i ∈ t → 0 = HMul.hMul (α := M₀) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroOneClass M₀
s t : Set ι
x : ι
⊢ (s ∩ t).indicator 1 x = HMul.hMul (α := (x : ι) → M₀) (β := (x : ι) → M₀) (s.indicator 1) (t.indicator 1) x
have simp : Eq.{u_4 + 1} (α := M₀) ((s ∩ t).indicator 1 x) ((s ∩ t).indicator (fun (j : ι) ↦ 1) x)
Tactic: simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = HMul.hMul (α := M₀) (s.indicator 1 i) (t.indicator 1 j)
have 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)
Tactic: simp_rw [indicator, mem_prod_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (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)
have pos : ∀ (h₀ : i ∈ s ∧ j ∈ t), i ∈ s → j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) (1 i) (1 j)
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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)
⊢ (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)
have neg : ∀ (h₀ : i ∈ s ∧ j ∈ t), i ∈ s → ¬j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) (1 i) 0
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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)
have pos₁ : ∀ (h₀ : i ∈ s ∧ j ∈ t), ¬i ∈ s → j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) 0 (1 j)
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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)
⊢ (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)
have neg₁ : ∀ (h₀ : i ∈ s ∧ j ∈ t), ¬i ∈ s → ¬j ∈ t → 1 (i, j) = HMul.hMul (α := M₀) 0 0
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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)
have pos₂ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), i ∈ s → j ∈ t → 0 = HMul.hMul (α := M₀) (1 i) (1 j)
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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)
⊢ (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)
have neg₂ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), i ∈ s → ¬j ∈ t → 0 = HMul.hMul (α := M₀) (1 i) 0
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ (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)
have pos₃ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), ¬i ∈ s → j ∈ t → 0 = HMul.hMul (α := M₀) 0 (1 j)
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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)
⊢ (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)
have neg₃ : ∀ (h₀ : ¬(i ∈ s ∧ j ∈ t)), ¬i ∈ s → ¬j ∈ t → 0 = HMul.hMul (α := M₀) 0 0
Tactic: split_ifs with h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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) 0
have neg : Eq.{u_4 + 1} (α := M₀) 1 0
Tactic: simp only [Pi.one_apply, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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₀) 0 (1 j)
have pos : Eq.{u_4 + 1} (α := M₀) 1 0
Tactic: simp only [Pi.one_apply, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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₀) 0 0
have neg : Eq.{u_4 + 1} (α := M₀) 1 0
Tactic: simp only [Pi.one_apply, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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) (1 j)
have pos : Eq.{u_4 + 1} (α := M₀) 0 1
Tactic: simp only [Pi.one_apply, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := M₀) 1 0
have right : j ∈ t
Tactic: tauto
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := M₀) 1 0
have left : i ∈ s
Tactic: tauto
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := M₀) 1 0
have left : i ∈ s
Tactic: tauto
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := M₀) 1 0
have right : j ∈ t
Tactic: tauto
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) 0 1
have pos : i ∈ s → j ∈ t → ∀ (h₀ : ¬i ∈ s), Eq.{u_4 + 1} (α := M₀) 0 1
Tactic: tauto
Cleared hypotheses: h₀, h, h_1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ Eq.{u_4 + 1} (α := M₀) 0 1
have pos₁ : i ∈ s → j ∈ t → ∀ (h₀ : ¬j ∈ t), Eq.{u_4 + 1} (α := M₀) 0 1
Tactic: tauto
Cleared hypotheses: h₀, h, h_1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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)
⊢ s = t
have h₁ : ∀ (x : ι), x ∈ s ↔ x ∈ t
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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 : ι
⊢ x ∈ s ↔ x ∈ t
have h₁ : Eq.{u_4 + 1} (α := M₀) (s.indicator 1 x) 1 ↔ Eq.{u_4 + 1} (α := M₀) (t.indicator 1 x) 1
Tactic: simp_rw [← indicator_eq_one_iff_mem M₀, h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
⊢ (support.{u_1, u_4} (M := M₀) fun (a : ι) ↦ f a ^ n) = support f
have h : ∀ (x : ι), Membership.mem (γ := Set ι) (support.{u_1, u_4} (M := M₀) fun (a : ι) ↦ f a ^ n) x ↔ x ∈ support f
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddGroup R
f : ι → R
⊢ mulSupport (1 - f) = support f
have rw : mulSupport (1 + -f) = support f
Tactic: rw [sub_eq_add_neg, mulSupport_one_add', support_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : One R
inst_1 : AddGroup R
f : ι → R
rw : mulSupport (1 + -f) = support f
⊢ mulSupport (1 - f) = support f
have rw₁ : support (-f) = support f
Tactic: rw [sub_eq_add_neg, mulSupport_one_add', support_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
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
⊢ mulSupport (1 - f) = support f
have rw₂ : support f = support f
Tactic: rw [sub_eq_add_neg, mulSupport_one_add', support_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f a * f b = 0
have rw : f (a * b) = 0
Tactic: rw [← mul, H, zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f a * f b = 0
have rw₂ : Eq.{u_3 + 1} (α := M₀') 0 0
Tactic: rw [← mul, H, zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (hypothesis)
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 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
⊢ x = x_1
have this : f ((fun (x : M₀) ↦ a * x) x) = f ((fun (x : M₀) ↦ a * x) x_1)
Tactic: have := congr_arg f He
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (hypothesis)
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 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
this : f ((fun (x : M₀) ↦ a * x) x) = f ((fun (x : M₀) ↦ a * x) x_1)
⊢ x = x_1
have this₁ : f a * f x = f a * f x_1
Tactic: rw [mul, mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
this : f a * f x = f a * f x_1
Hfa : f a = 0
⊢ f a = f 0
have rw : 0 = f 0
Tactic: rw [Hfa, zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
this : f a * f x = f a * f x_1
Hfa : f a = 0
rw : 0 = f 0
⊢ f a = f 0
have rw₁ : Eq.{u_3 + 1} (α := M₀') 0 0
Tactic: rw [Hfa, zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (hypothesis)
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 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
⊢ x = x_1
have this : f ((fun (x : M₀) ↦ x * a) x) = f ((fun (x : M₀) ↦ x * a) x_1)
Tactic: have := congr_arg f He
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (hypothesis)
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 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
this : f ((fun (x : M₀) ↦ x * a) x) = f ((fun (x : M₀) ↦ x * a) x_1)
⊢ x = x_1
have this₁ : f x * f a = f x_1 * f a
Tactic: rw [mul, mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
this : f x * f a = f x_1 * f a
Hfa : f a = 0
⊢ f a = f 0
have rw : 0 = f 0
Tactic: rw [Hfa, zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
this : f x * f a = f x_1 * f a
Hfa : f a = 0
rw : 0 = f 0
⊢ f a = f 0
have rw₁ : Eq.{u_3 + 1} (α := M₀') 0 0
Tactic: rw [Hfa, zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : GroupWithZero G₀
inst_1 : Zero G₀'
inst_2 : Mul G₀'
inst_3 : One G₀'
inst_4 : Inv G₀'
inst_5 : Div G₀'
inst_6 : Pow G₀' ℕ
inst_7 : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
⊢ f 0⁻¹ = f 0
have rw : (f 0)⁻¹ = f 0
Tactic: rw [inv, zero, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : GroupWithZero G₀
inst_1 : Zero G₀'
inst_2 : Mul G₀'
inst_3 : One G₀'
inst_4 : Inv G₀'
inst_5 : Div G₀'
inst_6 : Pow G₀' ℕ
inst_7 : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
rw : (f 0)⁻¹ = f 0
⊢ f 0⁻¹ = f 0
have rw₁ : Eq.{u_2 + 1} (α := G₀) 0⁻¹ 0
Tactic: rw [inv, zero, inv_zero]