awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
rw : a * c = a * (b * d) ↔ c = b * d
rw₁ rw₂ : c = b * d ↔ c = b * d
⊢ a * c = a * b * d ↔ c = b * d

Tactic:
rw [mul_assoc, mul_right_inj' ha]

Premises used: mul_assoc, mul_right_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
rw : b * c = a * d * c ↔ b = a * d
rw₁ rw₂ : b = a * d ↔ b = a * d
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
rw [mul_right_comm, mul_left_inj' hc]

Premises used: mul_right_comm, mul_left_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
left : a ≠ 0
right : ∃ (x : α), ¬IsUnit x ∧ b = a * x
⊢ DvdNotUnit a b

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False

Tactic:
hnd (dvd_zero _)

Premises used: dvd_zero
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False

Tactic:
exact hnd (dvd_zero _)

Premises used: dvd_zero
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
right : ∀ (c : α) (hnd : ¬a * c ∣ a), ∃ (x : α), ¬IsUnit x ∧ a * c = a * x
⊢ ∃ (x : α), ¬IsUnit x ∧ b = a * x

Tactic:
rcases hd with ⟨c, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ (x : α), ¬IsUnit x ∧ a * c = a * x

Tactic:
⟨c, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
right : ¬IsUnit c
⊢ ∃ (x : α), ¬IsUnit x ∧ a * c = a * x

Tactic:
refine ⟨c, ?_, rfl⟩
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * (↑u : α) ∣ a
⊢ False

Tactic:
simp at hnd
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
x : α
⊢ IsRelPrime 0 x ↔ IsUnit x

Tactic:
⟨(· (dvd_zero _) dvd_rfl), IsUnit.isRelPrime_right⟩

Premises used: dvd_zero, IsUnit.isRelPrime_right, Iff.intro, dvd_rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
x : α
⊢ IsRelPrime x 0 ↔ IsUnit x

Tactic:
isRelPrime_comm.trans isRelPrime_zero_left

Premises used: isRelPrime_comm, Iff.trans, isRelPrime_zero_left
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Nontrivial α
⊢ ¬IsRelPrime.{u_1} (α := α) 0 0

Tactic:
mt isRelPrime_zero_right.mp not_isUnit_zero

Premises used: mt, not_isUnit_zero, isRelPrime_zero_right, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Nontrivial α
h : IsRelPrime.{u_1} (α := α) 0 0
⊢ False

Tactic:
not_isRelPrime_zero_zero h

Premises used: not_isRelPrime_zero_zero
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Nontrivial α
h : IsRelPrime.{u_1} (α := α) 0 0
⊢ False

Tactic:
exact not_isRelPrime_zero_zero h

Premises used: not_isRelPrime_zero_zero
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsRelPrime x y

Tactic:
fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy

Premises used: IsRelPrime, by_contra
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
refine : ∀ (z : α) (hx : z ∣ x) (hy : z ∣ y) (h : ¬IsUnit z), z ≠ 0
⊢ IsRelPrime x y

Tactic:
refine fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy

Premises used: by_contra
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit.{u_1} (M := α) 0
⊢ False

Tactic:
nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩

Premises used: zero_dvd_iff, And.intro, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit.{u_1} (M := α) 0
⊢ False

Tactic:
exact nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩

Premises used: zero_dvd_iff, And.intro, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False

Tactic:
simp [hx0] at hyx
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
h_1 : d ∣ 1
e : α
he : 1 = d * e
rw : x = x * d * e
rw₁ : x = x * (d * e)
rw₂ : x = x * 1
rw₃ rw₄ : x = x
⊢ x = y * e

Tactic:
rw [hd, mul_assoc, ← he, mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
lhs : x * 1
| x * 1 = x * (d * e)

Tactic:
lhs
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
rw : x * d * e * 1
| x * 1

Tactic:
rw [he, hdx]
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
simp : x * (d * e)
| x * d * e * 1

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
rw : x * (d * e)
| x * 1 = x * (d * e)

Tactic:
lhs
            rw [he, hdx]
            simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
conv : x * 1 = x * (d * e)
conv₁ : x * (d * e) = x * (d * e)
⊢ x * 1 = x * (d * e)

Tactic:
conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
rcases : ∀ (u : α) (h₁ : p * u ≠ 0), p ≠ 0
⊢ p ≠ 0

Tactic:
rcases h₂ with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0

Tactic:
left_ne_zero_of_mul h₁

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0

Tactic:
exact left_ne_zero_of_mul h₁

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : MonoidWithZero α
⊢ IsPrimal.{u_1} (α := α) 0

Tactic:
fun a b h ↦ ⟨a, b, dvd_rfl, dvd_rfl, (zero_dvd_iff.mp h).symm⟩

Premises used: IsPrimal, zero_dvd_iff, And.intro, Exists.intro, Iff.mp, dvd_rfl, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
inl : ∀ (hm : IsPrimal.{u_2} (α := α) 0), IsPrimal (0 * n)
inr : ∀ (h0 : m ≠ 0), IsPrimal (m * n)
⊢ IsPrimal (m * n)

Tactic:
obtain rfl | h0 := eq_or_ne m 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
n : α
hn : IsPrimal n
hm inl inl₁ inl₂ inl₃ : IsPrimal.{u_2} (α := α) 0
⊢ IsPrimal (0 * n)

Tactic:
rwa [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
h : m * n ∣ b * c
inr :
  ∀ (a₁ a₂ b c : α) (hm : IsPrimal (a₁ * a₂)) (h0 : a₁ * a₂ ≠ 0) (h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)),
    ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂

Tactic:
obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)

Premises used: dvd_of_mul_right_dvd, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)
⊢ n ∣ b * c

Tactic:
rw [mul_mul_mul_comm, mul_dvd_mul_iff_left h0] at h

Premises used: mul_mul_mul_comm, mul_dvd_mul_iff_left
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : n ∣ b * c
inr :
  ∀ (a₁' a₂' : α) (h₁ : a₁' ∣ b) (h₂ : a₂' ∣ c) (hn : IsPrimal (a₁' * a₂')) (h : a₁' * a₂' ∣ b * c),
    ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1
⊢ ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Tactic:
obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
a₁' a₂' : α
h₁ : a₁' ∣ b
h₂ : a₂' ∣ c
hn : IsPrimal (a₁' * a₂')
h : a₁' * a₂' ∣ b * c
⊢ ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1

Tactic:
⟨a₁ * a₁', a₂ * a₂', mul_dvd_mul_left _ h₁, mul_dvd_mul_left _ h₂, mul_mul_mul_comm _ _ _ _⟩

Premises used: HMul.hMul, mul_mul_mul_comm, mul_dvd_mul_left, And.intro, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
a₁' a₂' : α
h₁ : a₁' ∣ b
h₂ : a₂' ∣ c
hn : IsPrimal (a₁' * a₂')
h : a₁' * a₂' ∣ b * c
⊢ ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1

Tactic:
exact ⟨a₁ * a₁', a₂ * a₂', mul_dvd_mul_left _ h₁, mul_dvd_mul_left _ h₂, mul_mul_mul_comm _ _ _ _⟩
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
c d : α
hcd : a = a * c * d
⊢ c = 1 ∧ d = 1 ∨ a = 0

Tactic:
rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd

Premises used: mul_assoc, eq_comm, mul_eq_one, mul_right_eq_self₀
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
inl : a = a * 1
inr : 0 = 0 * c
⊢ a = a * c

Tactic:
obtain ⟨rfl, -⟩ | rfl := hcd

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
d : α
⊢ a = a * 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Subsingleton.{u_1 + 1} αˣ
c d : α
⊢ 0 = 0 * c

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a b : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
⊢ a ∣ b → b ∣ a → b = a

Tactic:
flip dvd_antisymm

Premises used: dvd_antisymm, flip
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a b : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
h : ∀ (c : α), a ∣ c ↔ b ∣ c
⊢ a = b

Tactic:
((h _).2 dvd_rfl).antisymm <| (h _).1 dvd_rfl

Premises used: Iff.mpr, Iff.mp, dvd_rfl, Dvd.dvd.antisymm
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a b : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
h : ∀ (c : α), c ∣ a ↔ c ∣ b
⊢ a = b

Tactic:
((h _).1 dvd_rfl).antisymm <| (h _).2 dvd_rfl

Premises used: Iff.mpr, Iff.mp, dvd_rfl, Dvd.dvd.antisymm
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
mp : a ^ n ∣ a ^ m → n ≤ m
mpr : n ≤ m → a ^ n ∣ a ^ m
⊢ a ^ n ∣ a ^ m ↔ n ≤ m

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
mp : ¬m < n
⊢ n ≤ m

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
mp : IsUnit a
⊢ False

Tactic:
apply ha
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
rw : a ^ (m + 1) ∣ a ^ m
⊢ a ^ m * a ∣ a ^ m * 1

Tactic:
rw [← pow_succ, mul_one]

Premises used: pow_succ, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ (m + 1) ∣ a ^ m

Tactic:
(pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h

Premises used: Nat.succ_le_of_lt, pow_dvd_pow, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ (m + 1) ∣ a ^ m

Tactic:
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h

Premises used: Nat.succ_le_of_lt, pow_dvd_pow, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ m * a ∣ a ^ m * 1

Tactic:
have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
mp : a ^ m ≠ 0
⊢ IsUnit a

Tactic:
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this

Premises used: mul_dvd_mul_iff_left, isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ a ^ m ≠ 0

Tactic:
apply pow_ne_zero m ha₀

Premises used: pow_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m

Tactic:
apply pow_dvd_pow

Premises used: pow_dvd_pow
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
⊢ m ∣ n ↔ m = 0 → n = 0

Tactic:
⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩

Premises used: _private.0.GroupWithZero.dvd_iff.match_1, Iff.intro, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
refine_1 : m ∣ n → ∀ (hm : m = 0) (a : α) (ha : n = m * a), n = 0
refine_2 : ∀ (h : m = 0 → n = 0), m ∣ n
⊢ m ∣ n ↔ m = 0 → n = 0

Tactic:
refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0

Tactic:
simp [hm, ha]
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Tactic:
⟨m⁻¹ * n, ?_⟩

Premises used: HMul.hMul, Inv.inv, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
refine_2 : n = m * (m⁻¹ * n)
⊢ m ∣ n

Tactic:
refine ⟨m⁻¹ * n, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
refine_2 : ∀ (h : m = 0 → Eq.{u_1 + 1} (α := α) 0 0), 0 = m * (m⁻¹ * 0)
refine_2₁ : ∀ (hn : n ≠ 0), n = m * (m⁻¹ * n)
⊢ n = m * (m⁻¹ * n)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m : α
h : m = 0 → Eq.{u_1 + 1} (α := α) 0 0
⊢ 0 = m * (m⁻¹ * 0)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
refine_2 refine_2₁ : n = n
⊢ n = m * (m⁻¹ * n)

Tactic:
rw [mul_inv_cancel_left₀ (mt h hn)]

Premises used: mul_inv_cancel_left₀, mt
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
neZero : NeZero.{u_3} (R := β) ((f : (a : α) → β) a : β)
h : a = 0
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
neZero : NeZero.{u_3} (R := β) ((f : (a : α) → β) a : β)
h : a = 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
ZeroHomClass.map_zero f

Premises used: ZeroHomClass.map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
neZero : NeZero.{u_3} (R := β) ((f : (a : α) → β) a : β)
h : a = 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
exact ZeroHomClass.map_zero f

Premises used: ZeroHomClass.map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : NeZero a
rw : Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 0 : β)
⊢ Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
rw [← ZeroHomClass.map_zero f]

Premises used: ZeroHomClass.map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : NeZero a
⊢ Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 0 : β)

Tactic:
hf.ne NeZero.out

Premises used: Function.Injective.ne, NeZero.out
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : NeZero a
⊢ Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 0 : β)

Tactic:
exact hf.ne NeZero.out

Premises used: Function.Injective.ne, NeZero.out
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
f g : α →*₀ β
h : Eq (α := (a : α) → β) ((fun (f : α →*₀ β) ↦ f.toFun) f) ((fun (f : α →*₀ β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (map_zero' : toFun 0 = 0)
    (map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1)
    (map_mul' :
      ∀ (x y : α),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
          { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
            { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →*₀ β) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' })
        ((fun (f : α →*₀ β) ↦ f.toFun) g)),
    { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
g : α →*₀ β
toFun : α → β
map_zero' : toFun 0 = 0
map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1
map_mul' :
  ∀ (x y : α),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →*₀ β) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : α →*₀ β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_zero'_1 : toFun_1 0 = 0)
    (map_one'_1 : { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun 1 = 1)
    (map_mul'_1 :
      ∀ (x y : α),
        { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun (x * y) =
          { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun x *
            { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun y)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →*₀ β) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' })
        ((fun (f : α →*₀ β) ↦ f.toFun)
          { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
    { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } =
      { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }
⊢ { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g