awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : ¬IsUnit a
inr : ¬IsUnit.{u_2} (M := M₀) 0
⊢ ¬IsUnit a⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ h]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit.{u_2} (M := M₀) 0

Tactic:
not_isUnit_zero

Premises used: not_isUnit_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit.{u_2} (M := M₀) 0

Tactic:
exact not_isUnit_zero

Premises used: not_isUnit_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
⊢ IsUnit a ∧ ¬IsUnit b ∨ ¬IsUnit a ∧ IsUnit b ∨ IsUnit a ∧ IsUnit b

Tactic:
grind
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
inl : ∀ (ha : IsUnit a) (hb : ¬IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
inr : ∀ (ha : ¬IsUnit a) (hb : IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
inr₁ : ∀ (ha : IsUnit a) (hb : IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind

Premises used: IsUnit, And, Not
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
⊢ ¬IsUnit (a * b)

Tactic:
simpa [ha.mul_left_iff]

Premises used: IsUnit.mul_left_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
⊢ ¬IsUnit (a * b)

Tactic:
have : ¬ IsUnit (a * b) := by simpa [ha.mul_left_iff]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
this : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
simp [Ring.inverse_non_unit, hb, this]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬IsUnit (a * b)

Tactic:
simpa [hb.mul_right_iff]

Premises used: IsUnit.mul_right_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬IsUnit (a * b)

Tactic:
have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
this : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
simp [Ring.inverse_non_unit, ha, this]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
inr : a * b = (↑(ha.unit * hb.unit) : M₀)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
simp [Ring.inverse_of_isUnit, ha, hb, ha.mul hb, ← Units.val_mul, ← mul_inv_rev]

Premises used: IsUnit.mul, mul_inv_rev, Ring.inverse_of_isUnit, Units.val_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a * b = (↑(ha.unit * hb.unit) : M₀)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
x : M₀
⊢ x⁻¹ʳ ≠ 0 → IsUnit x

Tactic:
simpa using mt <| Ring.inverse_non_unit (x := x)

Premises used: mt, Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
x : M₀
⊢ ¬IsUnit x ↔ x⁻¹ʳ = 0

Tactic:
grind
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
⊢ Nontrivial M₀

Tactic:
nontriviality M₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ IsUnit x ↔ x * x⁻¹ʳ = 1

Tactic:
⟨mul_inverse_cancel _, ?_⟩

Premises used: Ring.mul_inverse_cancel, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
refine : x * x⁻¹ʳ = 1 → IsUnit x
⊢ IsUnit x ↔ x * x⁻¹ʳ = 1

Tactic:
refine ⟨mul_inverse_cancel _, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
contrapose : ¬IsUnit x → ¬x * x⁻¹ʳ = 1
⊢ x * x⁻¹ʳ = 1 → IsUnit x

Tactic:
contrapose
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ ¬IsUnit x → ¬x * x⁻¹ʳ = 1

Tactic:
simp +contextual [not_isUnit_iff_inverse_eq_zero]

Premises used: Ring.not_isUnit_iff_inverse_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ IsUnit x ↔ x⁻¹ʳ * x = 1

Tactic:
⟨Ring.inverse_mul_cancel x, ?_⟩

Premises used: Ring.inverse_mul_cancel, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
refine : x⁻¹ʳ * x = 1 → IsUnit x
⊢ IsUnit x ↔ x⁻¹ʳ * x = 1

Tactic:
refine ⟨Ring.inverse_mul_cancel x, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
contrapose : ¬IsUnit x → ¬x⁻¹ʳ * x = 1
⊢ x⁻¹ʳ * x = 1 → IsUnit x

Tactic:
contrapose
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ ¬IsUnit x → ¬x⁻¹ʳ * x = 1

Tactic:
simp +contextual [not_isUnit_iff_inverse_eq_zero]

Premises used: Ring.not_isUnit_iff_inverse_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
⊢ Nontrivial M₀

Tactic:
nontriviality M₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : Nontrivial M₀
pos : ∀ (h : IsUnit a), a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
neg : ∀ (h : ¬IsUnit a), a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
by_cases h : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : IsUnit a
pos pos₁ : a⁻¹ʳ = a⁻¹ʳ
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
rw [Ring.inverse_inverse h]

Premises used: Ring.inverse_inverse
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
simp [Ring.not_isUnit_iff_inverse_eq_zero.mp h]

Premises used: Iff.mp, Ring.not_isUnit_iff_inverse_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
h : Ne.{u_3 + 1} (α := G₀) 1 0
huv : (↑(mk0 1 h) : G₀) = (↑1 : G₀)
⊢ mk0 1 h = 1

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
h : Ne.{u_3 + 1} (α := G₀) 1 0
⊢ (↑(mk0 1 h) : G₀) = (↑1 : G₀)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ (↑(mk0 a h) : G₀) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
u : G₀ˣ
h : (↑u : G₀) ≠ 0
⊢ mk0 (↑u : G₀) h = u

Tactic:
Units.ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
u : G₀ˣ
⊢ (↑u : G₀) * (↑u : G₀)⁻¹ = 1

Tactic:
mul_inv_cancel₀ u.ne_zero

Premises used: mul_inv_cancel₀, Units.ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
u : G₀ˣ
⊢ (↑u : G₀)⁻¹ * (↑u : G₀) = 1

Tactic:
inv_mul_cancel₀ u.ne_zero

Premises used: Units.ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
h : mk0 a ha = mk0 b hb
⊢ a = b

Tactic:
injection h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
p : G₀ˣ → Prop
⊢ (∃ (g : G₀ˣ), p g) ↔ ∃ (g : G₀), ∃ (hg : g ≠ 0), p (mk0 g hg)

Tactic:
⟨fun ⟨g, pg⟩ => ⟨g, g.ne_zero, (g.mk0_val g.ne_zero).symm ▸ pg⟩,
  fun ⟨g, hg, pg⟩ => ⟨Units.mk0 g hg, pg⟩⟩

Premises used: Units.val, Exists, Eq.rec, Units.ne_zero, Units.mk0, _private.0.Units.exists0.match_2, Iff.intro, Exists.intro, _private.0.Units.exists0.match_1, Eq.symm, Units.mk0_val
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ (g : G₀), ∃ (hg : g ≠ 0), p g hg) ↔ ∃ (g : G₀), ∃ (hg : g ≠ 0), p (↑(mk0 g hg) : G₀) ⋯

Tactic:
simp_rw [val_mk0]

Premises used: Units.val_mk0
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
p : G₀ → Prop
⊢ (∃ (u : G₀ˣ), p (↑u : G₀)) ↔ ∃ (x : G₀), x ≠ 0 ∧ p x

Tactic:
simp [exists0]

Premises used: Units.exists0
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
⊢ a = 0 ∨ ∃ (u : G₀ˣ), a = (↑u : G₀)

Tactic:
simpa using em _

Premises used: em
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
x : G₀
hx : x ≠ 0
⊢ IsUnit x

Tactic:
(Units.mk0 x hx).isUnit

Premises used: Units.mk0, Units.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
⊢ (∃ (x : G₀), x ≠ 0 ∧ x = a) ↔ a ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
inst_1 : GroupWithZero G₀
a_1 b_1 c : G₀
m n : ℕ
a b : G₀
h : a * b = 0
contrapose! : ∀ (h : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
inst_1 : GroupWithZero G₀
a_1 b_1 c : G₀
m n : ℕ
a b : G₀
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0

Tactic:
(Units.mk0 a h.1 * Units.mk0 b h.2).ne_zero

Premises used: HMul.hMul, Units.ne_zero, Units.mk0, And.right, And.left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
inst_1 : GroupWithZero G₀
a_1 b_1 c : G₀
m n : ℕ
a b : G₀
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0

Tactic:
exact (Units.mk0 a h.1 * Units.mk0 b h.2).ne_zero

Premises used: HMul.hMul, Units.ne_zero, Units.mk0, And.right, And.left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
huv : (↑(mk0 (x * y) hxy) : G₀) = (↑(mk0 x ⋯ * mk0 y ⋯) : G₀)
⊢ mk0 (x * y) hxy = mk0 x ⋯ * mk0 y ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ (↑(mk0 (x * y) hxy) : G₀) = (↑(mk0 x ⋯ * mk0 y ⋯) : G₀)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
rw : a * b⁻¹ ≠ 0
⊢ a / b ≠ 0

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0

Tactic:
mul_ne_zero ha (inv_ne_zero hb)

Premises used: inv_ne_zero, mul_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0

Tactic:
exact mul_ne_zero ha (inv_ne_zero hb)

Premises used: inv_ne_zero, mul_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
⊢ a / b = 0 ↔ a = 0 ∨ b = 0

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Tactic:
div_eq_zero_iff.not.trans not_or

Premises used: Iff.not, not_or, Iff.trans, div_eq_zero_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a / a = 1

Tactic:
h.isUnit.div_self

Premises used: IsUnit.div_self, Ne.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
contrapose! : a = 0 → a / a ≠ 1
⊢ a / a = 1 → a ≠ 0

Tactic:
contrapose!
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
⊢ a = 0 → a / a ≠ 1

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
⊢ a = b * c⁻¹ ↔ a * c = b

Tactic:
hc.isUnit.eq_mul_inv_iff_mul_eq

Premises used: Ne.isUnit, IsUnit.eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a = b⁻¹ * c ↔ b * a = c

Tactic:
hb.isUnit.eq_inv_mul_iff_mul_eq

Premises used: Ne.isUnit, IsUnit.eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
⊢ a⁻¹ * b = c ↔ b = a * c

Tactic:
ha.isUnit.inv_mul_eq_iff_eq_mul

Premises used: Ne.isUnit, IsUnit.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a * b⁻¹ = c ↔ a = c * b

Tactic:
hb.isUnit.mul_inv_eq_iff_eq_mul

Premises used: Ne.isUnit, IsUnit.mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
hb : b ≠ 0
⊢ a * b⁻¹ = 1 ↔ a = b

Tactic:
hb.isUnit.mul_inv_eq_one

Premises used: Ne.isUnit, IsUnit.mul_inv_eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
ha.isUnit.inv_mul_eq_one

Premises used: Ne.isUnit, IsUnit.inv_mul_eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
hb : b ≠ 0
⊢ a * b = 1 ↔ a = b⁻¹

Tactic:
hb.isUnit.mul_eq_one_iff_eq_inv

Premises used: Ne.isUnit, IsUnit.mul_eq_one_iff_eq_inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a * b = 1 ↔ a⁻¹ = b

Tactic:
ha.isUnit.mul_eq_one_iff_inv_eq

Premises used: Ne.isUnit, IsUnit.mul_eq_one_iff_inv_eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
rwa : b ≠ 0
⊢ a * b = c

Tactic:
rwa [← eq_mul_inv_iff_mul_eq₀]

Premises used: eq_mul_inv_iff_mul_eq₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a c : G₀
ha : a ≠ 0
h : a = c * 0⁻¹
⊢ False

Tactic:
simp [ha] at h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
rwa : a ≠ 0
⊢ a * b = c

Tactic:
rwa [← eq_inv_mul_iff_mul_eq₀]

Premises used: eq_inv_mul_iff_mul_eq₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False

Tactic:
simp [hb] at h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
h : b⁻¹ * a = c
⊢ a = b * c

Tactic:
(mul_eq_of_eq_inv_mul₀ hc h.symm).symm

Premises used: mul_eq_of_eq_inv_mul₀, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : a * c⁻¹ = b
⊢ a = b * c

Tactic:
(mul_eq_of_eq_mul_inv₀ hb h.symm).symm

Premises used: mul_eq_of_eq_mul_inv₀, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
b a : G₀
h : b ≠ 0
⊢ a / b * b = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a * (1 / a) = 1

Tactic:
h.isUnit.mul_one_div_cancel

Premises used: Ne.isUnit, IsUnit.mul_one_div_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ 1 / a * a = 1

Tactic:
h.isUnit.one_div_mul_cancel

Premises used: Ne.isUnit, IsUnit.one_div_mul_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
⊢ a / c = b / c ↔ a = b

Tactic:
hc.isUnit.div_left_inj

Premises used: Ne.isUnit, IsUnit.div_left_inj
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a / b = c ↔ a = c * b

Tactic:
hb.isUnit.div_eq_iff

Premises used: Ne.isUnit, IsUnit.div_eq_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ c = a / b ↔ c * b = a

Tactic:
hb.isUnit.eq_div_iff

Premises used: Ne.isUnit, IsUnit.eq_div_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a / b = c ↔ c * b = a

Tactic:
hb.isUnit.div_eq_iff.trans eq_comm

Premises used: Ne.isUnit, IsUnit.div_eq_iff, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
⊢ a = b / c ↔ a * c = b

Tactic:
hc.isUnit.eq_div_iff

Premises used: Ne.isUnit, IsUnit.eq_div_iff
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a = c * b → a / b = c

Tactic:
hb.isUnit.div_eq_of_eq_mul

Premises used: Ne.isUnit, IsUnit.div_eq_of_eq_mul
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
⊢ a * c = b → a = b / c

Tactic:
hc.isUnit.eq_div_of_mul_eq

Premises used: Ne.isUnit, IsUnit.eq_div_of_mul_eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
hb : b ≠ 0
⊢ a / b = 1 ↔ a = b

Tactic:
hb.isUnit.div_eq_one_iff_eq

Premises used: Ne.isUnit, IsUnit.div_eq_one_iff_eq
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
b : G₀
hb : b ≠ 0
a : G₀
⊢ b / (a * b) = a⁻¹

Tactic:
hb.isUnit.div_mul_cancel_right _

Premises used: Ne.isUnit, IsUnit.div_mul_cancel_right
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ a * c / (b * c) = a / b

Tactic:
hc.isUnit.mul_div_mul_right _ _

Premises used: Ne.isUnit, IsUnit.mul_div_mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
b a : G₀
hb : b ≠ 0
⊢ a = a * b * (1 / b)

Tactic:
(hb.isUnit.mul_mul_div _).symm

Premises used: Ne.isUnit, IsUnit.mul_mul_div, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
c : G₀
hc : c ≠ 0
a b : G₀
rw : a / c * c / b = a / b
rw₁ rw₂ : a / b = a / b
⊢ a / c / (b / c) = a / b

Tactic:
rw [div_div_eq_mul_div, div_mul_cancel₀ _ hc]

Premises used: div_mul_cancel₀, div_div_eq_mul_div
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
rw : a / b * b / c = a / c
rw₁ rw₂ : a / c = a / c
⊢ a / b * (b / c) = a / c

Tactic:
rw [← mul_div_assoc, div_mul_cancel₀ _ hb]

Premises used: div_mul_cancel₀, mul_div_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
inl : ∀ (h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0), a / 0 * 0 = a
inr : ∀ (hb : b ≠ 0), a / b * b = a
⊢ a / b * b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0
⊢ a / 0 * 0 = a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a / b * b = a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
inl : ∀ (h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0), a * 0 / 0 = a
inr : ∀ (hb : b ≠ 0), a * b / b = a
⊢ a * b / b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0
⊢ a * 0 / 0 = a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
b a : G₀
hb : b ≠ 0
⊢ a /ₚ Units.mk0 b hb = a / b

Tactic:
divp_eq_div _ _

Premises used: divp_eq_div
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
⊢ m - n + n = m

Tactic:
have h1 : m - n + n = m := Nat.sub_add_cancel h
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
rw : a ^ (m - n + n) = a ^ m
rw₁ rw₂ : a ^ m = a ^ m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
rw [← pow_add, h1]

Premises used: pow_add
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2

Premises used: eq_div_of_mul_eq, pow_ne_zero, div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
inl : HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
inr : ∀ (ha : a ≠ 0), a ^ (m - n) = a ^ m * (a ^ n)⁻¹
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ m ≠ 0

Tactic:
lia
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
h : n < m
inl : 0 = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹
inl₁ : 0 = 0 * (HPow.hPow (α := G₀) 0 n)⁻¹
inl₂ inl₃ : Eq.{u_3 + 1} (α := G₀) 0 0
⊢ HPow.hPow (α := G₀) 0 (m - n) = HPow.hPow (α := G₀) 0 m * (HPow.hPow (α := G₀) 0 n)⁻¹

Tactic:
rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by lia), zero_mul]

Premises used: Nat.sub_pos_of_lt, MulZeroClass.zero_mul, zero_pow, Nat.ne_of_gt
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
pow_sub₀ _ ha <| Nat.le_of_lt h

Premises used: Nat.le_of_lt, pow_sub₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Basic
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
exact pow_sub₀ _ ha <| Nat.le_of_lt h

Premises used: Nat.le_of_lt, pow_sub₀