awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.NonAssoc.LieAdmissible.Defs (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : Ring L
⊢ ∀ (x y z : L),
    associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
have suffices : ∀ (a b c : L), associator a b c = 0
Tactic: suffices ∀ a b c : L, associator a b c = 0 by simp
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : α
b : P → α
c : ¬P → α
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h
have isTrue : ∀ (h : P), a * b h = a * b h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : α
b : P → α
c : ¬P → α
isTrue : ∀ (h : P), a * b h = a * b h
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h
have isFalse : ∀ (h : ¬P), a * c h = a * c h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c
have isTrue : ∀ (h : P), a h * c = a h * c
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : α
isTrue : ∀ (h : P), a h * c = a h * c
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c
have isFalse : ∀ (h : ¬P), b h * c = b h * c
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ HMul.hMul (α := α) (if h : P then a h else b h) (if h : P then c h else d h) = if h : P then a h * c h else b h * d h
have isTrue : ∀ (h : P), a h * c h = a h * c h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
isTrue : ∀ (h : P), a h * c h = a h * c h
⊢ HMul.hMul (α := α) (if h : P then a h else b h) (if h : P then c h else d h) = if h : P then a h * c h else b h * d h
have isFalse : ∀ (h : ¬P), b h * d h = b h * d h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c d : α
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d
have isTrue : P → a * c = a * c
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c d : α
isTrue : P → a * c = a * c
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d
have isFalse : ¬P → b * d = b * d
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : α
b : P → α
c : ¬P → α
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h
have isTrue : ∀ (h : P), a / b h = a / b h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : α
b : P → α
c : ¬P → α
isTrue : ∀ (h : P), a / b h = a / b h
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h
have isFalse : ∀ (h : ¬P), a / c h = a / c h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c
have isTrue : ∀ (h : P), a h / c = a h / c
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : α
isTrue : ∀ (h : P), a h / c = a h / c
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c
have isFalse : ∀ (h : ¬P), b h / c = b h / c
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ HDiv.hDiv (α := α) (if h : P then a h else b h) (if h : P then c h else d h) = if h : P then a h / c h else b h / d h
have isTrue : ∀ (h : P), a h / c h = a h / c h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Defs (goal)
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
isTrue : ∀ (h : P), a h / c h = a h / c h
⊢ HDiv.hDiv (α := α) (if h : P then a h else b h) (if h : P then c h else d h) = if h : P then a h / c h else b h / d h
have isFalse : ∀ (h : ¬P), b h / d h = b h / d h
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ if p then a else b
have isTrue : p → 1 ≤ a
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 1 ≤ a
hb : 1 ≤ b
isTrue : p → 1 ≤ a
⊢ 1 ≤ if p then a else b
have isFalse : ¬p → 1 ≤ b
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : a ≤ 1
hb : b ≤ 1
⊢ (if p then a else b) ≤ 1
have isTrue : p → a ≤ 1
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : a ≤ 1
hb : b ≤ 1
isTrue : p → a ≤ 1
⊢ (if p then a else b) ≤ 1
have isFalse : ¬p → b ≤ 1
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 1 < a
hb : 1 < b
⊢ 1 < if p then a else b
have isTrue : p → 1 < a
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 1 < a
hb : 1 < b
isTrue : p → 1 < a
⊢ 1 < if p then a else b
have isFalse : ¬p → 1 < b
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : a < 1
hb : b < 1
⊢ (if p then a else b) < 1
have isTrue : p → a < 1
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Lemmas (goal)
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : a < 1
hb : b < 1
isTrue : p → a < 1
⊢ (if p then a else b) < 1
have isFalse : ¬p → b < 1
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
⊢ mulSingle (M := M) i x = 1 ↔ x = 1
have refine : ∀ (h : mulSingle (M := M) i x = 1), x = 1
Tactic: refine ⟨fun h => ?_, fun h => h.symm ▸ mulSingle_one i⟩
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
h : mulSingle (M := M) i x = 1
⊢ x = 1
have rw : mulSingle (M := M) i x i = 1
Tactic: rw [← mulSingle_eq_same i x, h, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
h : mulSingle (M := M) i x = 1
rw : mulSingle (M := M) i x i = 1
⊢ x = 1
have rw₁ : Eq.{u_6 + 1} (α := M i) (1 i) 1
Tactic: rw [← mulSingle_eq_same i x, h, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
h : mulSingle (M := M) i x = 1
rw : mulSingle (M := M) i x i = 1
rw₁ : Eq.{u_6 + 1} (α := M i) (1 i) 1
⊢ x = 1
have rw₂ : Eq.{u_6 + 1} (α := M i) 1 1
Tactic: rw [← mulSingle_eq_same i x, h, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
⊢ f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
have pos : ∀ (h : j = i), f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
pos : ∀ (h : j = i), f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
⊢ f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
have neg : ∀ (h : ¬j = i), f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Notation.Pi.Basic (goal)
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : j = i
⊢ f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
have pos : ∀ (x : M j) (y : N j), f' j (mulSingle (M := M) j x j) (mulSingle (M := N) j y j) = mulSingle (M := O) j (f' j x y) j
Tactic: subst h
Cleared hypotheses: i, x, y, h
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
⊢ f x = g x
have rw : 1 = g x
Tactic: rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
rw : 1 = g x
⊢ f x = g x
have rw₁ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
⊢ f x = g x
have if : ∀ (hx : x ∈ mulSupport f), f x = g x
Tactic: if hx : x ∈ f.mulSupport then exact h₂ x hx
    else rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
if : ∀ (hx : x ∈ mulSupport f), f x = g x
⊢ f x = g x
have if₁ : ∀ (hx : ¬x ∈ mulSupport f), f x = g x
Tactic: if hx : x ∈ f.mulSupport then exact h₂ x hx
    else rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x y) = insert x (mulSupport f)
have h : ∀ (a : ι), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)
have h : a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a y) ↔ a ∈ insert a (mulSupport f)
Tactic: obtain rfl | hne := eq_or_ne a x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
h : a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a y) ↔ a ∈ insert a (mulSupport f)
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)
have h₁ : ∀ (hne : a ≠ x), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)
Tactic: obtain rfl | hne := eq_or_ne a x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) = mulSupport f \ {x}
have h : ∀ (a : ι), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x a : ι
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}
have h : a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a 1) ↔ a ∈ mulSupport f \ {a}
Tactic: obtain rfl | hne := eq_or_ne a x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x a : ι
h : a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a 1) ↔ a ∈ mulSupport f \ {a}
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}
have h₁ : ∀ (hne : a ≠ x), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}
Tactic: obtain rfl | hne := eq_or_ne a x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
inst_2 : DecidableEq M
f : ι → M
x : ι
y : M
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
have inl : mulSupport (update (β := fun (a : ι) ↦ M) f x 1) =
  if Eq.{u_3 + 1} (α := M) 1 1 then mulSupport f \ {x} else insert x (mulSupport f)
Tactic: rcases eq_or_ne y 1 with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
inst_2 : DecidableEq M
f : ι → M
x : ι
y : M
inl :
  mulSupport (update (β := fun (a : ι) ↦ M) f x 1) =
    if Eq.{u_3 + 1} (α := M) 1 1 then mulSupport f \ {x} else insert x (mulSupport f)
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
have inr : ∀ (hy : y ≠ 1),
  mulSupport (update (β := fun (a : ι) ↦ M) f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
Tactic: rcases eq_or_ne y 1 with rfl | hy
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
⊢ extend f g 1 x = 1
have pos : ∀ (hf : ∃ (a : ι), f a = x), extend f g 1 x = 1
Tactic: by_cases hf : ∃ a, f a = x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
pos : ∀ (hf : ∃ (a : ι), f a = x), extend f g 1 x = 1
⊢ extend f g 1 x = 1
have neg : ∀ (hf : ¬∃ (a : ι), f a = x), extend f g 1 x = 1
Tactic: by_cases hf : ∃ a, f a = x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ (a : ι), f a = x
⊢ extend f g 1 x = 1
have pos : ¬Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf ∈ mulSupport g
Tactic: rw [extend, dif_pos hf, ← notMem_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ (a : ι), f a = x
⊢ ¬Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf ∈ mulSupport g
have hfg₁ : ¬f (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf) ∈ f '' mulSupport g
Tactic: rw [← Classical.choose_spec hf] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ (a : ι), f a = x
⊢ extend f g 1 x = 1
have neg : Eq.{u_4 + 1} (α := N) (1 x) 1
Tactic: rw [extend_apply' _ _ _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
⊢ f x ∈ mulSupport (extend f g 1)
have rwa : extend f g 1 (f x) ≠ 1
Tactic: rwa [mem_mulSupport, hf.extend_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
rwa : extend f g 1 (f x) ≠ 1
⊢ f x ∈ mulSupport (extend f g 1)
have rwa₁ : g x ≠ 1
Tactic: rwa [mem_mulSupport, hf.extend_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
have simp_rw : mulSupport f ⊆ sᶜ ↔ EqOn f 1 s
Tactic: simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
simp_rw : mulSupport f ⊆ sᶜ ↔ EqOn f 1 s
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
have simp_rw₁ : (∀ (x : ι), ¬x ∈ sᶜ → f x = 1) ↔ EqOn f 1 s
Tactic: simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
simp_rw : mulSupport f ⊆ sᶜ ↔ EqOn f 1 s
simp_rw₁ : (∀ (x : ι), ¬x ∈ sᶜ → f x = 1) ↔ EqOn f 1 s
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
have simp_rw₂ : (∀ (x : ι), x ∈ s → f x = 1) ↔ EqOn f 1 s
Tactic: simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
simp_rw : mulSupport f ⊆ sᶜ ↔ EqOn f 1 s
simp_rw₁ : (∀ (x : ι), ¬x ∈ sᶜ → f x = 1) ↔ EqOn f 1 s
simp_rw₂ : (∀ (x : ι), x ∈ s → f x = 1) ↔ EqOn f 1 s
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
have simp_rw₃ : (∀ (x : ι), x ∈ s → f x = 1) ↔ ∀ ⦃x : ι⦄, x ∈ s → f x = 1 x
Tactic: simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s
have rw : Disjoint (mulSupport f) s ↔ EqOn f 1 s
Tactic: rw [disjoint_comm, mulSupport_disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
rw : Disjoint (mulSupport f) s ↔ EqOn f 1 s
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s
have rw₁ : EqOn f 1 s ↔ EqOn f 1 s
Tactic: rw [disjoint_comm, mulSupport_disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
⊢ mulSupport f = ∅ ↔ f = 1
have rw : (∀ (x : ι), ¬Membership.mem (γ := Set ι) ∅ x → f x = 1) ↔ ∀ (x : ι), f x = 1 x
Tactic: rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
⊢ (mulSupport f).Nonempty ↔ f ≠ 1
have rw : mulSupport f ≠ ∅ ↔ f ≠ 1
Tactic: rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
rw : mulSupport f ≠ ∅ ↔ f ≠ 1
⊢ (mulSupport f).Nonempty ↔ f ≠ 1
have rw₁ : ¬mulSupport f = ∅ ↔ f ≠ 1
Tactic: rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
rw : mulSupport f ≠ ∅ ↔ f ≠ 1
rw₁ : ¬mulSupport f = ∅ ↔ f ≠ 1
⊢ (mulSupport f).Nonempty ↔ f ≠ 1
have rw₂ : ¬f = 1 ↔ f ≠ 1
Tactic: rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)
have this : range f ⊆ insert 1 (f '' k)
Tactic: have : range f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_mono h))
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : One M
c : M
hc : c ≠ 1
⊢ Eq.{u_1 + 1} (α := Set ι) (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ c) univ
have h : ∀ (x : ι),
  Membership.mem (γ := Set ι) (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ c) x ↔ Membership.mem (γ := Set ι) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
g : M → N
f : ι → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : ι
⊢ (g ∘ f) x = 1 ↔ f x = 1
have rw : g (f x) = 1 ↔ f x = 1
Tactic: rw [Function.comp, hg (mem_range_self x)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
g : M → N
f : ι → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : ι
rw : g (f x) = 1 ↔ f x = 1
⊢ (g ∘ f) x = 1 ↔ f x = 1
have rw₁ : f x = 1 ↔ f x = 1
Tactic: rw [Function.comp, hg (mem_range_self x)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
f : ι → M
s : Set κ
g : κ → ι
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))
have rw : g '' s ∩ mulSupport f = g '' (s ∩ g ⁻¹' mulSupport f)
Tactic: rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
f : ι → M
s : Set κ
g : κ → ι
rw : g '' s ∩ mulSupport f = g '' (s ∩ g ⁻¹' mulSupport f)
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))
have rw₁ : g '' s ∩ mulSupport f = g '' s ∩ mulSupport f
Tactic: rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : Membership.mem (γ := Set ι) {i} x
⊢ x ∈ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)
have rwa : Ne.{u_3 + 1} (α := M) (mulSingle (M := fun (a : ι) ↦ M) i a x : M) (1 : M)
Tactic: rwa [mem_mulSupport, hx, mulSingle_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : Membership.mem (γ := Set ι) {i} x
rwa : Ne.{u_3 + 1} (α := M) (mulSingle (M := fun (a : ι) ↦ M) i a x : M) (1 : M)
⊢ x ∈ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)
have rwa₁ : Ne.{u_3 + 1} (α := M) (mulSingle (M := fun (a : ι) ↦ M) i a i : M) (1 : M)
Tactic: rwa [mem_mulSupport, hx, mulSingle_eq_same]