awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)

Tactic:
fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
refine_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
refine_2 :
  ¬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
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)

Tactic:
refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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 : IsUnit ((↑u : M) * A) ∨ IsUnit B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u.isUnit_units_mul]

Premises used: Units.isUnit_units_mul
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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
⊢ IsUnit ((↑u : M) * A) ∨ IsUnit B

Tactic:
apply h
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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)
refine_1₁ refine_1₂ : (↑u : M) * y = (↑u : M) * y
⊢ (↑u : M) * y = (↑u : M) * A * B

Tactic:
rw [mul_assoc, ← HAB]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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 : IsUnit ((↑u⁻¹ : M) * A) ∨ IsUnit B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u⁻¹.isUnit_units_mul]

Premises used: Inv.inv, Units.isUnit_units_mul
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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
⊢ IsUnit ((↑u⁻¹ : M) * A) ∨ IsUnit B

Tactic:
apply h
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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)
refine_2₂ refine_2₃ : y = y
⊢ y = (↑u⁻¹ : M) * A * B

Tactic:
rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]

Premises used: mul_assoc, Units.inv_mul_cancel_left
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
h : IsUnit x
⊢ Irreducible (x * y) ↔ Irreducible y

Tactic:
let ⟨x, ha⟩ := h
  ha ▸ irreducible_units_mul x

Premises used: HMul.hMul, _private.0.irreducible_isUnit_mul.match_1, Eq.rec, Irreducible, Iff, irreducible_units_mul
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
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)
⊢ Irreducible (y * (↑u : M)) ↔ Irreducible y

Tactic:
simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]

Premises used: and_congr_right_iff, Units.isUnit_mul_units, irreducible_iff
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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)

Tactic:
fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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
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
⊢ ¬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:
refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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 : IsUnit A ∨ IsUnit (B * (↑u : M))
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u.isUnit_mul_units B]

Premises used: Units.isUnit_mul_units
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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))
⊢ IsUnit A ∨ IsUnit (B * (↑u : M))

Tactic:
apply h
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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)
refine_1₁ refine_1₂ : y * (↑u : M) = y * (↑u : M)
⊢ y * (↑u : M) = A * (B * (↑u : M))

Tactic:
rw [← mul_assoc, ← HAB]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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 : IsUnit A ∨ IsUnit (B * (↑u⁻¹ : M))
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u⁻¹.isUnit_mul_units B]

Premises used: Inv.inv, Units.isUnit_mul_units
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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))
⊢ IsUnit A ∨ IsUnit (B * (↑u⁻¹ : M))

Tactic:
apply h
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
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)
refine_2₂ refine_2₃ : y = y
⊢ y = A * (B * (↑u⁻¹ : M))

Tactic:
rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

Premises used: mul_assoc, Units.mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
h : IsUnit x
⊢ Irreducible (y * x) ↔ Irreducible y

Tactic:
let ⟨x, hx⟩ := h
  hx ▸ irreducible_mul_units x

Premises used: HMul.hMul, irreducible_mul_units, _private.0.irreducible_isUnit_mul.match_1, Eq.rec, Irreducible, Iff
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
mp : Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
mpr : Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x → Irreducible (x * y)
⊢ Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
⊢ Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

Tactic:
fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm

Premises used: Or.symm, Irreducible.isUnit_or_isUnit, And.intro, Or.imp, rfl
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
mp : ∀ (h : Irreducible (x * y)) (h' : IsUnit y), Irreducible x
mp₁ : ∀ (h : Irreducible (x * y)) (h' : IsUnit x), Irreducible y
⊢ Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

Tactic:
refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm

Premises used: Or.imp
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
mp mp₁ mp₂ mp₃ : ∀ (h : Irreducible x) (h' : IsUnit y), Irreducible x
⊢ Irreducible x

Tactic:
rwa [irreducible_mul_isUnit h'] at h

Premises used: irreducible_mul_isUnit
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
mp mp₁ mp₂ mp₃ : ∀ (h : Irreducible y) (h' : IsUnit x), Irreducible y
⊢ Irreducible y

Tactic:
rwa [irreducible_isUnit_mul h'] at h

Premises used: irreducible_isUnit_mul
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
ha : Irreducible x
hb : IsUnit y
mpr mpr₁ mpr₂ mpr₃ : Irreducible x
⊢ Irreducible (x * y)

Tactic:
rwa [irreducible_mul_isUnit hb]

Premises used: irreducible_mul_isUnit
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x y : M
hb : Irreducible y
ha : IsUnit x
mpr mpr₁ mpr₂ mpr₃ : Irreducible y
⊢ Irreducible (x * y)

Tactic:
rwa [irreducible_isUnit_mul ha]

Premises used: irreducible_isUnit_mul
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
x : M
inst_2 : EquivLike F M N
inst_3 : MulEquivClass F M N
f : F
⊢ Irreducible.{u_3} (M := N) ((f : (a : M) → N) x : N) ↔ Irreducible x

Tactic:
simp [_root_.irreducible_iff, (EquivLike.surjective f).forall, ← map_mul, -isUnit_map_iff]

Premises used: Function.Surjective.forall, isUnit_map_iff, map_mul, irreducible_iff, EquivLike.surjective
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
f : F
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
inst_4 : IsLocalHom.{u_2, u_3, u_1} (R := M) (S := N) f
p q : M
hfx : Irreducible.{u_3} (M := N) ((f : (a : M) → N) (p * q) : N)
⊢ IsUnit p ∨ IsUnit q

Tactic:
(hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)

Premises used: IsUnit.of_map, map_mul, Irreducible.isUnit_or_isUnit, Or.imp
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
f : F
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
inst_4 : IsLocalHom.{u_2, u_3, u_1} (R := M) (S := N) f
p q : M
hfx : Irreducible.{u_3} (M := N) ((f : (a : M) → N) (p * q) : N)
⊢ IsUnit p ∨ IsUnit q

Tactic:
exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)

Premises used: map_mul, Irreducible.isUnit_or_isUnit, Or.imp
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
ha : Irreducible x
rw : ¬∃ (r : M), x = HPow.hPow (β := ℕ) r 2
⊢ ¬IsSquare x

Tactic:
rw [isSquare_iff_exists_sq]

Premises used: isSquare_iff_exists_sq
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
y : M
ha : Irreducible (HPow.hPow (β := ℕ) y 2)
⊢ Ne (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
y : M
ha : Irreducible (HPow.hPow (β := ℕ) y 2)
⊢ False

Tactic:
exact not_irreducible_pow (by decide) ha

Premises used: not_irreducible_pow
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
ha : IsSquare x
⊢ ¬Irreducible x

Tactic:
fun h => h.not_isSquare ha

Premises used: Irreducible.not_isSquare, Not
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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 rw₁ : 1 * (a * a⁻¹) = 1 * (a * a⁻¹)
⊢ 1 * (a * a⁻¹) = (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹)

Tactic:
rw [inv_mul_cancel]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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⁻¹) = (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹))

Tactic:
simp only [assoc]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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
rw₂ rw₃ : Eq.{u + 1} (α := G) 1 1
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1

Tactic:
rw [inv_mul_cancel, one_mul, inv_mul_cancel]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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 : 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]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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
rw₃ rw₄ : a = a
⊢ a * 1 = a

Tactic:
rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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 rw₁ : a⁻¹ * a * 1 = a⁻¹ * a * 1
⊢ a⁻¹ * a * 1 = a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹)

Tactic:
rw [mul_inv_cancel]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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)⁻¹) = a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹

Tactic:
simp only [assoc]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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
rw₂ rw₃ : Eq.{u + 1} (α := G) 1 1
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1

Tactic:
rw [mul_inv_cancel, mul_one, mul_inv_cancel]
-- Module: Mathlib.Algebra.Group.MinimalAxioms
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
rw₃ rw₄ : a = a
⊢ 1 * a = a

Tactic:
rw [← mul_inv_cancel a, assoc, inv_mul_cancel, mul_one]
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
⊢ a ≡ b [PMOD p] ↔ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
p a : M
⊢ HSMul.hSMul (α := ℕ) 0 p + a = HSMul.hSMul (α := ℕ) 0 p + a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a p : M
⊢ a ≡ a [PMOD p]

Tactic:
modEq_refl _

Premises used: AddCommGroup.modEq_refl
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
⊢ Std.Refl (ModEq p)

Tactic:
⟨modEq_refl⟩

Premises used: AddCommGroup.modEq_refl, Std.Refl.mk
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
h : a ≡ b [PMOD p]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
rcases : ∀ (m n : ℕ) (h : m • p + a = n • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + a
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + a

Tactic:
rcases h with ⟨m, n, h⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + a

Tactic:
⟨n, m, h.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + a

Tactic:
exact ⟨n, m, h.symm⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
⊢ Std.Symm (ModEq p)

Tactic:
⟨fun _ _ ↦ .symm⟩

Premises used: Std.Symm.mk, AddCommGroup.ModEq.symm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
⊢ a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]

Tactic:
⟨.symm, .symm⟩

Premises used: Iff.intro, AddCommGroup.ModEq.symm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
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
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + b = n • p + c

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
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
rcases : ∀ (m n : ℕ) (hab : m • p + a = n • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c

Tactic:
rcases hab with ⟨m, n, hab⟩
-- Module: Mathlib.Algebra.Group.ModEq
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
rcases : ∀ (k l : ℕ) (hbc : k • p + b = l • p + c), ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c

Tactic:
rcases hbc with ⟨k, l, hbc⟩
-- Module: Mathlib.Algebra.Group.ModEq
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 + m) • p + a = (n + l) • p + c
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + c

Tactic:
use k + m, n + l
-- Module: Mathlib.Algebra.Group.ModEq
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)
h₆ h₇ : n • p + (k • p + b) = n • p + (k • p + b)
⊢ (k + m) • p + a = (n + l) • p + c

Tactic:
rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]

Premises used: add_left_comm, add_assoc, add_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
⊢ IsTrans M (ModEq p)

Tactic:
⟨fun _ _ _ ↦ .trans⟩

Premises used: AddCommGroup.ModEq.trans, IsTrans.mk
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b : M
⊢ a ≡ b [PMOD 0] ↔ a = b

Tactic:
simp [modEq_iff_nsmul]

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
p : M
⊢ HSMul.hSMul (α := ℕ) 0 p + p = HSMul.hSMul (α := ℕ) 1 p + 0

Tactic:
simp [one_nsmul]

Premises used: one_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a p : M
n : ℕ
⊢ HSMul.hSMul (α := ℕ) 0 p + (a + n • p) = n • p + a

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a p : M
n : ℕ
⊢ HSMul.hSMul (α := ℕ) 0 p + (n • p + a) = n • p + a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
hab : a ≡ b [PMOD p]
hcd : c ≡ d [PMOD p]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
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
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
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
rcases : ∀ (k l : ℕ) (hab : k • p + a = l • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)

Tactic:
rcases hab with ⟨k, l, hab⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
hcd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
k l : ℕ
hab : k • p + a = l • p + b
rcases : ∀ (m n : ℕ) (hcd : m • p + c = n • p + d), ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)

Tactic:
rcases hcd with ⟨m, n, hcd⟩
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : (k + m) • p + (a + c) = (l + n) • p + (b + d)
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)

Tactic:
use k + m, l + n
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
h₁ : k • p + a + (m • p + c) = (l + n) • p + (b + d)
h₂ : l • p + b + (m • p + c) = (l + n) • p + (b + d)
h₃ : l • p + b + (n • p + d) = (l + n) • p + (b + d)
h₄ : l • p + b + (n • p + d) = l • p + n • p + (b + d)
h₅ h₆ : l • p + n • p + (b + d) = l • p + n • p + (b + d)
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)

Tactic:
rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]

Premises used: add_add_add_comm, add_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p c : M
h : a ≡ b [PMOD p]
⊢ c + a ≡ c + b [PMOD p]

Tactic:
modEq_rfl.add h

Premises used: AddCommGroup.modEq_rfl, AddCommGroup.ModEq.add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p c : M
h : a ≡ b [PMOD p]
⊢ a + c ≡ b + c [PMOD p]

Tactic:
h.add modEq_rfl

Premises used: AddCommGroup.modEq_rfl, AddCommGroup.ModEq.add
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
h_1 : a ≡ b [PMOD n • p]
k l : ℕ
h : k • n • p + a = l • n • p + b
⊢ (k * n) • p + a = (l * n) • p + b

Tactic:
simpa [mul_nsmul']

Premises used: mul_nsmul'
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
h : a ≡ b [PMOD p]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b

Tactic:
rw [modEq_iff_nsmul] at *

Premises used: AddCommGroup.modEq_iff_nsmul
-- Module: Mathlib.Algebra.Group.ModEq
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
rcases : ∀ (k l : ℕ) (h : k • p + a = l • p + b), ∃ (m : ℕ), ∃ (n_1 : ℕ), m • n • p + n • a = n_1 • n • p + n • b
⊢ ∃ (m : ℕ), ∃ (n_1 : ℕ), m • n • p + n • a = n_1 • n • p + n • b

Tactic:
rcases h with ⟨k, l, h⟩