awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B
have refine_1 : IsUnit ((↑u : M) * A) ∨ IsUnit B
Tactic: rw [← u.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit ((↑u : M) * A) ∨ IsUnit B
have refine_1 : (↑u : M) * y = (↑u : M) * A * B
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ (↑u : M) * y = (↑u : M) * A * B
have refine_1 : (↑u : M) * y = (↑u : M) * (A * B)
Tactic: rw [mul_assoc, ← HAB]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
refine_1 : (↑u : M) * y = (↑u : M) * (A * B)
⊢ (↑u : M) * y = (↑u : M) * A * B
have refine_1₁ : (↑u : M) * y = (↑u : M) * y
Tactic: rw [mul_assoc, ← HAB]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : (↑u : M) * y = A * B
⊢ IsUnit A ∨ IsUnit B
have refine_2 : IsUnit ((↑u⁻¹ : M) * A) ∨ IsUnit B
Tactic: rw [← u⁻¹.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : (↑u : M) * y = A * B
⊢ IsUnit ((↑u⁻¹ : M) * A) ∨ IsUnit B
have refine_2 : y = (↑u⁻¹ : M) * A * B
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : (↑u : M) * y = A * B
⊢ y = (↑u⁻¹ : M) * A * B
have refine_2 : y = (↑u⁻¹ : M) * (A * B)
Tactic: rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : (↑u : M) * y = A * B
refine_2 : y = (↑u⁻¹ : M) * (A * B)
⊢ y = (↑u⁻¹ : M) * A * B
have refine_2₁ : y = (↑u⁻¹ : M) * ((↑u : M) * y)
Tactic: rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : (↑u : M) * y = A * B
refine_2 : y = (↑u⁻¹ : M) * (A * B)
refine_2₁ : y = (↑u⁻¹ : M) * ((↑u : M) * y)
⊢ y = (↑u⁻¹ : M) * A * B
have refine_2₂ : y = y
Tactic: rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
⊢ Irreducible (y * (↑u : M)) ↔ Irreducible y
have simp : ¬IsUnit y → ((∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
Tactic: simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
have refine_1 : ¬IsUnit y →
  ∀ (h : ∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b) (A B : M) (HAB : y = A * B), IsUnit A ∨ IsUnit B
Tactic: refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
refine_1 :
  ¬IsUnit y →
    ∀ (h : ∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b) (A B : M) (HAB : y = A * B), IsUnit A ∨ IsUnit B
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
have refine_2 : ¬IsUnit y →
  ∀ (h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b) (A B : M) (HAB : y * (↑u : M) = A * B), IsUnit A ∨ IsUnit B
Tactic: refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B
have refine_1 : IsUnit A ∨ IsUnit (B * (↑u : M))
Tactic: rw [← u.isUnit_mul_units B]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit (B * (↑u : M))
have refine_1 : y * (↑u : M) = A * (B * (↑u : M))
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ y * (↑u : M) = A * (B * (↑u : M))
have refine_1 : y * (↑u : M) = A * B * (↑u : M)
Tactic: rw [← mul_assoc, ← HAB]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
refine_1 : y * (↑u : M) = A * B * (↑u : M)
⊢ y * (↑u : M) = A * (B * (↑u : M))
have refine_1₁ : y * (↑u : M) = y * (↑u : M)
Tactic: rw [← mul_assoc, ← HAB]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * (↑u : M) = A * B
⊢ IsUnit A ∨ IsUnit B
have refine_2 : IsUnit A ∨ IsUnit (B * (↑u⁻¹ : M))
Tactic: rw [← u⁻¹.isUnit_mul_units B]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * (↑u : M) = A * B
⊢ IsUnit A ∨ IsUnit (B * (↑u⁻¹ : M))
have refine_2 : y = A * (B * (↑u⁻¹ : M))
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * (↑u : M) = A * B
⊢ y = A * (B * (↑u⁻¹ : M))
have refine_2 : y = A * B * (↑u⁻¹ : M)
Tactic: rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * (↑u : M) = A * B
refine_2 : y = A * B * (↑u⁻¹ : M)
⊢ y = A * (B * (↑u⁻¹ : M))
have refine_2₁ : y = y * (↑u : M) * (↑u⁻¹ : M)
Tactic: rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
h_1 : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * (↑u : M) = A * B
refine_2 : y = A * B * (↑u⁻¹ : M)
refine_2₁ : y = y * (↑u : M) * (↑u⁻¹ : M)
⊢ y = A * (B * (↑u⁻¹ : M))
have refine_2₂ : y = y
Tactic: rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x y : M
⊢ Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
have mp : Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x y : M
mp : Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
⊢ Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
have mpr : Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x → Irreducible (x * y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x y : M
⊢ Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
have mp : ∀ (h : Irreducible (x * y)) (h' : IsUnit y), Irreducible x
Tactic: refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x y : M
mp : ∀ (h : Irreducible (x * y)) (h' : IsUnit y), Irreducible x
⊢ Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
have mp₁ : ∀ (h : Irreducible (x * y)) (h' : IsUnit x), Irreducible y
Tactic: refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
⊢ Irreducible x
have mp : ∀ (h : Irreducible x) (h' : IsUnit y), Irreducible x
Tactic: rwa [irreducible_mul_isUnit h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y
have mp : ∀ (h : Irreducible y) (h' : IsUnit x), Irreducible y
Tactic: rwa [irreducible_isUnit_mul h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
x : M
ha : Irreducible x
⊢ ¬IsSquare x
have rw : ¬∃ (r : M), x = HPow.hPow (β := ℕ) r 2
Tactic: rw [isSquare_iff_exists_sq]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a_1 a : G
⊢ 1 * (a * a⁻¹) = (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹)
have rw : 1 * (a * a⁻¹) = 1 * (a * a⁻¹)
Tactic: rw [inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a_1 a : G
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1
have rw : (a * a⁻¹)⁻¹ * (a * (1 * a⁻¹)) = 1
Tactic: rw [inv_mul_cancel, one_mul, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a_1 a : G
rw : (a * a⁻¹)⁻¹ * (a * (1 * a⁻¹)) = 1
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1
have rw₁ : (a * a⁻¹)⁻¹ * (a * a⁻¹) = 1
Tactic: rw [inv_mul_cancel, one_mul, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a_1 a : G
rw : (a * a⁻¹)⁻¹ * (a * (1 * a⁻¹)) = 1
rw₁ : (a * a⁻¹)⁻¹ * (a * a⁻¹) = 1
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1
have rw₂ : Eq.{u + 1} (α := G) 1 1
Tactic: rw [inv_mul_cancel, one_mul, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (hypothesis)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * 1 = a
have mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
Tactic: have mul_inv_cancel : ∀ a : G, a * a⁻¹ = 1 := fun a =>
        calc a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
          _ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by
            rw [inv_mul_cancel]
          _ = (a * a⁻¹)⁻¹ * (a * ((a⁻¹ * a) * a⁻¹)) := by
            simp only [assoc]
          _ = 1 := by
            rw [inv_mul_cancel, one_mul, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
⊢ a * 1 = a
have rw : a * (a⁻¹ * a) = a
Tactic: rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
rw : a * (a⁻¹ * a) = a
⊢ a * 1 = a
have rw₁ : a * a⁻¹ * a = a
Tactic: rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
rw : a * (a⁻¹ * a) = a
rw₁ : a * a⁻¹ * a = a
⊢ a * 1 = a
have rw₂ : 1 * a = a
Tactic: rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
rw : a * (a⁻¹ * a) = a
rw₁ : a * a⁻¹ * a = a
rw₂ : 1 * a = a
⊢ a * 1 = a
have rw₃ : a = a
Tactic: rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * 1 = a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹)
have rw : a⁻¹ * a * 1 = a⁻¹ * a * 1
Tactic: rw [mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1
have rw : a⁻¹ * 1 * a * (a⁻¹ * a)⁻¹ = 1
Tactic: rw [mul_inv_cancel, mul_one, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
rw : a⁻¹ * 1 * a * (a⁻¹ * a)⁻¹ = 1
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1
have rw₁ : a⁻¹ * a * (a⁻¹ * a)⁻¹ = 1
Tactic: rw [mul_inv_cancel, mul_one, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
rw : a⁻¹ * 1 * a * (a⁻¹ * a)⁻¹ = 1
rw₁ : a⁻¹ * a * (a⁻¹ * a)⁻¹ = 1
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1
have rw₂ : Eq.{u + 1} (α := G) 1 1
Tactic: rw [mul_inv_cancel, mul_one, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ 1 * a = a
have rw : a * a⁻¹ * a = a
Tactic: rw [← mul_inv_cancel a, assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
rw : a * a⁻¹ * a = a
⊢ 1 * a = a
have rw₁ : a * (a⁻¹ * a) = a
Tactic: rw [← mul_inv_cancel a, assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
rw : a * a⁻¹ * a = a
rw₁ : a * (a⁻¹ * a) = a
⊢ 1 * a = a
have rw₂ : a * 1 = a
Tactic: rw [← mul_inv_cancel a, assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.MinimalAxioms (goal)
Goal:
G : Type u
inst : Mul G
inst_1 : Inv G
inst_2 : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
rw : a * a⁻¹ * a = a
rw₁ : a * (a⁻¹ * a) = a
rw₂ : a * 1 = a
⊢ 1 * a = a
have rw₃ : a = a
Tactic: rw [← mul_inv_cancel a, assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
h : a ≡ b [PMOD p]
⊢ b ≡ a [PMOD p]
have h₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + a
have rcases : ∀ (m n : ℕ) (h : m • p + a = n • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + a
Tactic: rcases h with ⟨m, n, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
⊢ a ≡ c [PMOD p]
have hab₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
hab₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ a ≡ c [PMOD p]
have hbc₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + c
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
hab : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
hbc : ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + c
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
have rcases : ∀ (m n : ℕ) (hab : m • p + a = n • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
Tactic: rcases hab with ⟨m, n, hab⟩
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
hbc : ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + c
m n : ℕ
hab : m • p + a = n • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
have rcases : ∀ (k l : ℕ) (hbc : k • p + b = l • p + c), ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
Tactic: rcases hbc with ⟨k, l, hbc⟩
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
have h : (k + m) • p + a = (n + l) • p + c
Tactic: use k + m, n + l
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ (k + m) • p + a = (n + l) • p + c
have h : k • p + m • p + a = (n + l) • p + c
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
h : k • p + m • p + a = (n + l) • p + c
⊢ (k + m) • p + a = (n + l) • p + c
have h₁ : k • p + (m • p + a) = (n + l) • p + c
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
h : k • p + m • p + a = (n + l) • p + c
h₁ : k • p + (m • p + a) = (n + l) • p + c
⊢ (k + m) • p + a = (n + l) • p + c
have h₂ : k • p + (n • p + b) = (n + l) • p + c
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
h : k • p + m • p + a = (n + l) • p + c
h₁ : k • p + (m • p + a) = (n + l) • p + c
h₂ : k • p + (n • p + b) = (n + l) • p + c
⊢ (k + m) • p + a = (n + l) • p + c
have h₃ : k • p + (n • p + b) = n • p + l • p + c
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
h : k • p + m • p + a = (n + l) • p + c
h₁ : k • p + (m • p + a) = (n + l) • p + c
h₂ : k • p + (n • p + b) = (n + l) • p + c
h₃ : k • p + (n • p + b) = n • p + l • p + c
⊢ (k + m) • p + a = (n + l) • p + c
have h₄ : k • p + (n • p + b) = n • p + (l • p + c)
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
h : k • p + m • p + a = (n + l) • p + c
h₁ : k • p + (m • p + a) = (n + l) • p + c
h₂ : k • p + (n • p + b) = (n + l) • p + c
h₃ : k • p + (n • p + b) = n • p + l • p + c
h₄ : k • p + (n • p + b) = n • p + (l • p + c)
⊢ (k + m) • p + a = (n + l) • p + c
have h₅ : k • p + (n • p + b) = n • p + (k • p + b)
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
h : k • p + m • p + a = (n + l) • p + c
h₁ : k • p + (m • p + a) = (n + l) • p + c
h₂ : k • p + (n • p + b) = (n + l) • p + c
h₃ : k • p + (n • p + b) = n • p + l • p + c
h₄ : k • p + (n • p + b) = n • p + (l • p + c)
h₅ : k • p + (n • p + b) = n • p + (k • p + b)
⊢ (k + m) • p + a = (n + l) • p + c
have h₆ : n • p + (k • p + b) = n • p + (k • p + b)
Tactic: rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
hab : a ≡ b [PMOD p]
hcd : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p]
have hab₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: hab, hcd
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
hab : a ≡ b [PMOD p]
hcd : c ≡ d [PMOD p]
hab₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ a + c ≡ b + d [PMOD p]
have hcd₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: hab, hcd
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
hab : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
hcd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
have rcases : ∀ (k l : ℕ) (hab : k • p + a = l • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
Tactic: rcases hab with ⟨k, l, hab⟩
Cleared hypotheses: hab