awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x y : A
rw : r • (x + -y) = r • x - r • y
rw₁ : r • (x + -y) = r • x + -(r • y)
⊢ r • (x - y) = r • x - r • y
have rw₂ : r • x + r • -y = r • x + -(r • y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x y : A
rw : r • (x + -y) = r • x - r • y
rw₁ : r • (x + -y) = r • x + -(r • y)
rw₂ : r • x + r • -y = r • x + -(r • y)
⊢ r • (x - y) = r • x - r • y
have rw₃ : r • x + -(r • y) = r • x + -(r • y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0
have rw : a⁻¹ • a • x = 0
Tactic: rw [← inv_smul_smul a x, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
a : α
x : β
h : a • x = 0
rw : a⁻¹ • a • x = 0
⊢ x = 0
have rw₁ : HSMul.hSMul (β := β) a⁻¹ 0 = 0
Tactic: rw [← inv_smul_smul a x, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
a : α
x : β
h : a • x = 0
rw : a⁻¹ • a • x = 0
rw₁ : HSMul.hSMul (β := β) a⁻¹ 0 = 0
⊢ x = 0
have rw₂ : Eq.{u_11 + 1} (α := β) 0 0
Tactic: rw [← inv_smul_smul a x, h, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
⊢ ¬HSMul.hSMul (β := β) g 0 * (HSMul.hSMul (β := β) g 0)⁻¹ = 1
have rw : ¬Eq.{u_11 + 1} (α := β) 0 1
Tactic: rw [← smul_one g, ← inv_smul_eq_iff, smul_mul', inv_smul_smul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
⊢ g • x⁻¹ = (g • x)⁻¹
have pos : ∀ (hx : x = 0), g • x⁻¹ = (g • x)⁻¹
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
pos : ∀ (hx : x = 0), g • x⁻¹ = (g • x)⁻¹
⊢ g • x⁻¹ = (g • x)⁻¹
have neg : ∀ (hx : ¬x = 0), g • x⁻¹ = (g • x)⁻¹
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ g • x⁻¹ = (g • x)⁻¹
have pos : HSMul.hSMul (β := β) g 0⁻¹ = (HSMul.hSMul (β := β) g 0)⁻¹
Tactic: rw [hx, inv_zero, smul_zero, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : x = 0
pos : HSMul.hSMul (β := β) g 0⁻¹ = (HSMul.hSMul (β := β) g 0)⁻¹
⊢ g • x⁻¹ = (g • x)⁻¹
have pos₁ : HSMul.hSMul (β := β) g 0 = (HSMul.hSMul (β := β) g 0)⁻¹
Tactic: rw [hx, inv_zero, smul_zero, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : x = 0
pos : HSMul.hSMul (β := β) g 0⁻¹ = (HSMul.hSMul (β := β) g 0)⁻¹
pos₁ : HSMul.hSMul (β := β) g 0 = (HSMul.hSMul (β := β) g 0)⁻¹
⊢ g • x⁻¹ = (g • x)⁻¹
have pos₂ : Eq.{u_11 + 1} (α := β) 0 0⁻¹
Tactic: rw [hx, inv_zero, smul_zero, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : x = 0
pos : HSMul.hSMul (β := β) g 0⁻¹ = (HSMul.hSMul (β := β) g 0)⁻¹
pos₁ : HSMul.hSMul (β := β) g 0 = (HSMul.hSMul (β := β) g 0)⁻¹
pos₂ : Eq.{u_11 + 1} (α := β) 0 0⁻¹
⊢ g • x⁻¹ = (g • x)⁻¹
have pos₃ : Eq.{u_11 + 1} (α := β) 0 0
Tactic: rw [hx, inv_zero, smul_zero, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x⁻¹ = (g • x)⁻¹
have neg : g • x * g • x⁻¹ = 1
Tactic: apply eq_inv_of_mul_eq_one_right
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x * g • x⁻¹ = 1
have neg : g • (x * x⁻¹) = 1
Tactic: rw [← smul_mul', mul_inv_cancel₀ hx, smul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
neg : g • (x * x⁻¹) = 1
⊢ g • x * g • x⁻¹ = 1
have neg₁ : HSMul.hSMul (β := β) g 1 = 1
Tactic: rw [← smul_mul', mul_inv_cancel₀ hx, smul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
neg : g • (x * x⁻¹) = 1
neg₁ : HSMul.hSMul (β := β) g 1 = 1
⊢ g • x * g • x⁻¹ = 1
have neg₂ : Eq.{u_11 + 1} (α := β) 1 1
Tactic: rw [← smul_mul', mul_inv_cancel₀ hx, smul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x y : β
⊢ g • (x / y) = g • x / g • y
have rw : g • (x * y⁻¹) = g • x / g • y
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x y : β
rw : g • (x * y⁻¹) = g • x / g • y
⊢ g • (x / y) = g • x / g • y
have rw₁ : g • (x * y⁻¹) = g • x * (g • y)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x y : β
rw : g • (x * y⁻¹) = g • x / g • y
rw₁ : g • (x * y⁻¹) = g • x * (g • y)⁻¹
⊢ g • (x / y) = g • x / g • y
have rw₂ : g • x * g • y⁻¹ = g • x * (g • y)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x y : β
rw : g • (x * y⁻¹) = g • x / g • y
rw₁ : g • (x * y⁻¹) = g • x * (g • y)⁻¹
rw₂ : g • x * g • y⁻¹ = g • x * (g • y)⁻¹
⊢ g • (x / y) = g • x / g • y
have rw₃ : g • x * (g • y)⁻¹ = g • x * (g • y)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Opposite (goal)
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
⊢ m₁ = m₂
have inl : Subsingleton α → m₁ = m₂
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Opposite (goal)
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
inl : Subsingleton α → m₁ = m₂
⊢ m₁ = m₂
have inr : Nontrivial α → m₁ = m₂
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst : (i : I) → SMulZeroClass.{v, u_1} (f i) (g i)
a : (i : I) → f i
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 = 0
have h : ∀ (x : I), HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 = 0
have h : ∀ (x : I), HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
x y : (i : I) → g i
⊢ a • (x + y) = a • x + a • y
have h : ∀ (x_1 : I), (a • (x + y)) x_1 = (a • x + a • y) x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst : (i : I) → MulDistribMulAction.{v, u_1} (f i) (g i)
r : (i : I) → f i
⊢ HSMul.hSMul (β := (i : I) → g i) r 1 = 1
have h : ∀ (x : I), HSMul.hSMul (β := (i : I) → g i) r 1 x = 1 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst : (i : I) → MulDistribMulAction.{v, u_1} (f i) (g i)
r : (i : I) → f i
x y : (i : I) → g i
⊢ r • (x * y) = r • x * r • y
have h : ∀ (x_1 : I), (r • (x * y)) x_1 = (r • x * r • y) x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (Set.PairwiseDisjoint.{u_2, u_1} (α := Finset β) s fun (x : α) ↦ x • t) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
have simp_rw : (Set.PairwiseDisjoint.{u_2, u_1} (α := Set β) s fun (i : α) ↦ i • (↑t : Set β)) ↔
  Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
Tactic: simp_rw [← pairwiseDisjoint_coe, coe_smul_finset]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
a : α
inst_3 : Fintype β
ha : a ≠ 0
⊢ (↑(HSMul.hSMul (β := Finset β) a univ) : Set β) = (↑univ : Set β)
have push_cast : HSMul.hSMul (β := Set β) a Set.univ = Set.univ
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)
have hs₁ : ¬(↑s : Set α) ⊆ (↑0 : Set α)
Tactic: rw [← coe_subset] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : ¬(↑s : Set α) ⊆ (↑0 : Set α)
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)
have push_cast : ∀ (hs : ¬(↑s : Set α) ⊆ 0), HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ
Tactic: push_cast at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)
have push_cast : HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
have inl : (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
inl : (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
have inr : ∀ (ha : a ≠ 0), (a •> s)⁻¹ = s⁻¹ <• a⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
have inl : (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
inl : (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
have inl₁ : ∀ (hs : s.Nonempty), (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
have inr : ∀ (a_1 : α), a_1 ∈ (a •> s)⁻¹ ↔ a_1 ∈ s⁻¹ <• a⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
have inl : (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
inl : (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
have inr : ∀ (ha : a ≠ 0), (s <• a)⁻¹ = a⁻¹ •> s⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
have inl : (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
inl : (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
have inl₁ : ∀ (hs : s.Nonempty), (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
have inr : ∀ (a_1 : α), a_1 ∈ (s <• a)⁻¹ ↔ a_1 ∈ a⁻¹ •> s⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : SMulZeroClass α β
s : Set α
t : Set β
a x : α
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 0} 0
have rw : Eq (α := Set β) {0} 0
Tactic: rw [smul_zero, singleton_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : SMulZeroClass α β
s : Set α
t : Set β
a x : α
rw : Eq (α := Set β) {0} 0
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 0} 0
have rw₁ : Eq.{u_2 + 1} (α := Set β) 0 0
Tactic: rw [smul_zero, singleton_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
inst_2 : MulDistribMulAction α β
x : α
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 1} 1
have rw : Eq (α := Set β) {1} 1
Tactic: rw [smul_one, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
inst_2 : MulDistribMulAction α β
x : α
rw : Eq (α := Set β) {1} 1
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 1} 1
have rw₁ : Eq.{u_2 + 1} (α := Set β) 1 1
Tactic: rw [smul_one, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
⊢ s = 0 ∨ t = 0
have by_contra! : ∀ (H : s ≠ 0 ∧ t ≠ 0), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
⊢ False
have hst : (s * t).Nonempty
Tactic: have hst : (s * t).Nonempty := h.symm.subst zero_nonempty
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
hst : (s * t).Nonempty
⊢ False
have H₁ : ¬s ⊆ 0 ∧ ¬t ⊆ 0
Tactic: rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H
Cleared hypotheses: H, hst
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
hst : (s * t).Nonempty
⊢ False
have H₁ : (∃ a ∈ s, ¬a = 0) ∧ ∃ a ∈ t, ¬a = 0
Tactic: simp only [not_subset, mem_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
H : (∃ a ∈ s, ¬a = 0) ∧ ∃ a ∈ t, ¬a = 0
⊢ False
have obtain : ∀ (a : α) (hs : a ∈ s) (ha : ¬a = 0) (b : α) (ht : b ∈ t) (hb : ¬b = 0), False
Tactic: obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
have inl : (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
inl : (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
have inr : ∀ (ha : a ≠ 0), (a •> s)⁻¹ = s⁻¹ <• a⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
have inl : (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
inl : (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
have inl₁ : ∀ (hs : s.Nonempty), (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
have inr : ∀ (x : α), x ∈ (a •> s)⁻¹ ↔ x ∈ s⁻¹ <• a⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
have inl : (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
inl : (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
have inr : ∀ (ha : a ≠ 0), (s <• a)⁻¹ = a⁻¹ •> s⁻¹
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
have inl : (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
inl : (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
have inl₁ : ∀ (hs : s.Nonempty), (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
have inr : ∀ (x : α), x ∈ (s <• a)⁻¹ ↔ x ∈ a⁻¹ •> s⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
β : Type u_4
inst : SMul M β
α : Type u_5
inst_1 : Monoid M
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
a : M
c : β
⊢ HSMul.hSMul (β := α × β) a (0, c) = (0, a • c)
have rw : (HSMul.hSMul (β := α) a 0, a • c) = (0, a • c)
Tactic: rw [Prod.smul_mk, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
β : Type u_4
inst : SMul M β
α : Type u_5
inst_1 : Monoid M
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
a : M
c : β
rw : (HSMul.hSMul (β := α) a 0, a • c) = (0, a • c)
⊢ HSMul.hSMul (β := α × β) a (0, c) = (0, a • c)
have rw₁ : Eq (α := α × β) (0, a • c) (0, a • c)
Tactic: rw [Prod.smul_mk, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
β : Type u_5
inst_1 : Monoid M
inst_2 : AddMonoid β
inst_3 : DistribMulAction M β
a : M
b : α
⊢ HSMul.hSMul (β := α × β) a (b, 0) = (a • b, 0)
have rw : (a • b, HSMul.hSMul (β := β) a 0) = (a • b, 0)
Tactic: rw [Prod.smul_mk, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
β : Type u_5
inst_1 : Monoid M
inst_2 : AddMonoid β
inst_3 : DistribMulAction M β
a : M
b : α
rw : (a • b, HSMul.hSMul (β := β) a 0) = (a • b, 0)
⊢ HSMul.hSMul (β := α × β) a (b, 0) = (a • b, 0)
have rw₁ : Eq (α := α × β) (a • b, 0) (a • b, 0)
Tactic: rw [Prod.smul_mk, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
⊢ HSMul.hSMul (β := M × N) x 0 = 0
have fst : (HSMul.hSMul (β := M × N) x 0).1 = 0.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : Zero N
inst_2 : SMulZeroClass R M
inst_3 : SMulZeroClass R N
x : R
fst : (HSMul.hSMul (β := M × N) x 0).1 = 0.1
⊢ HSMul.hSMul (β := M × N) x 0 = 0
have snd : (HSMul.hSMul (β := M × N) x 0).2 = 0.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2
have fst : (x • (x_1 + x_2)).1 = (x • x_1 + x • x_2).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : DistribSMul R M
inst_3 : DistribSMul R N
x : R
x_1 x_2 : M × N
fst : (x • (x_1 + x_2)).1 = (x • x_1 + x • x_2).1
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2
have snd : (x • (x_1 + x_2)).2 = (x • x_1 + x • x_2).2
Tactic: ext