awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
⊢ a * (↑(normUnit a) : α) * (↑u : α) * (↑u⁻¹ : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
have rw : a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
Tactic: rw [mul_right_comm a]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
⊢ a * (↑(normUnit a) : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
have a₁ : a * (↑(normUnit a) : α) * (↑u : α) * (↑u⁻¹ : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
Tactic: calc
    a * ↑(normUnit a) = a * ↑(normUnit a) * ↑u * ↑u⁻¹ := (Units.mul_inv_cancel_right _ _).symm
    _ = a * ↑u * ↑(normUnit a) * ↑u⁻¹ := by rw [mul_right_comm a]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
x y : α
⊢ Eq (α := α) ((normalize : (a : α) → α) x : α) ((normalize : (a : α) → α) y : α) ↔ Associated x y
have rw : x ∣ y ∧ y ∣ x ↔ Associated x y
Tactic: rw [normalize_eq_normalize_iff, dvd_dvd_iff_associated]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
x y : α
rw : x ∣ y ∧ y ∣ x ↔ Associated x y
⊢ Eq (α := α) ((normalize : (a : α) → α) x : α) ((normalize : (a : α) → α) y : α) ↔ Associated x y
have rw₁ : Associated x y ↔ Associated x y
Tactic: rw [normalize_eq_normalize_iff, dvd_dvd_iff_associated]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
⊢ a = 0 ∧ b = 0
have let : ∀ (ca : α) (ha : a = @gcd _ inst _ a b * ca), a = 0 ∧ b = 0
Tactic: let ⟨ca, ha⟩ := gcd_dvd_left a b
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
ca : α
ha : a = @gcd _ inst _ a b * ca
⊢ a = 0 ∧ b = 0
have let : ∀ (cb : α) (hb : b = @gcd _ inst _ a b * cb), a = 0 ∧ b = 0
Tactic: let ⟨cb, hb⟩ := gcd_dvd_right a b
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
ca : α
ha : a = @gcd _ inst _ a b * ca
cb : α
hb : b = @gcd _ inst _ a b * cb
⊢ a = 0 ∧ b = 0
have rw : ∀ (ha : a = 0) (cb : α) (hb : b = 0), a = 0 ∧ b = 0
Tactic: rw [h, zero_mul] at ha hb
Cleared hypotheses: ha, cb, hb
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ @gcd _ inst _ a b = 0
have rw : Dvd.dvd.{u_1} (α := α) 0 (@gcd _ inst _ 0 0)
Tactic: rw [ha, hb, ← zero_dvd_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ Dvd.dvd.{u_1} (α := α) 0 (@gcd _ inst _ 0 0)
have a₁ : Dvd.dvd.{u_1} (α := α) 0 0
Tactic: apply dvd_gcd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
have inl : Associated (@gcd _ inst _ (0 * b) (0 * c)) (0 * @gcd _ inst _ b c)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
inl : Associated (@gcd _ inst _ (0 * b) (0 * c)) (0 * @gcd _ inst _ b c)
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
have inr : ∀ (ha : a ≠ 0), Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
have inr : ∀ (d : α) (eq : @gcd _ inst _ (a * b) (a * c) = a * d),
  Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
Tactic: obtain ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
have inr : @gcd _ inst _ (a * b) (a * c) ∣ a * @gcd _ inst _ b c
Tactic: apply associated_of_dvd_dvd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
inr : @gcd _ inst _ (a * b) (a * c) ∣ a * @gcd _ inst _ b c
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
have inr₁ : a * @gcd _ inst _ b c ∣ @gcd _ inst _ (a * b) (a * c)
Tactic: apply associated_of_dvd_dvd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ @gcd _ inst _ (a * b) (a * c) ∣ a * @gcd _ inst _ b c
have inr : a * d ∣ a * @gcd _ inst _ b c
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ a * d ∣ a * @gcd _ inst _ b c
have inr : d ∣ @gcd _ inst _ b c
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ (k * m) n
have grw : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
Tactic: grw [← dvd_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ (m * k) n
have grw : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
Tactic: grw [← dvd_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ m (k * n)
have grw : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
Tactic: grw [← dvd_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ m (n * k)
have grw : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
Tactic: grw [← dvd_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ m * @gcd _ inst _ k n
have rw : ∀ (H : k ∣ n * m), k ∣ @gcd _ inst _ k n * m
Tactic: rw [mul_comm] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
h : Nonempty.{u_1 + 1} (GCDMonoid α)
k m n : α
H : k ∣ m * n
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have intro : ∀ (val : GCDMonoid α), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have pos : ∀ (h0 : @gcd _ inst _ k m = 0), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
Tactic: by_cases h0 : gcd k m = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
pos : ∀ (h0 : @gcd _ inst _ k m = 0), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have neg : ∀ (h0 : ¬@gcd _ inst _ k m = 0), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
Tactic: by_cases h0 : gcd k m = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : @gcd _ inst _ k m = 0
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have h0₁ : k = 0 ∧ m = 0
Tactic: rw [gcd_eq_zero_iff] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : k = 0 ∧ m = 0
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have pos : ∀ (H : 0 ∣ 0 * n), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ 0 ∧ a₂ ∣ n ∧ 0 = a₁ * a₂
Tactic: rcases h0 with ⟨rfl, rfl⟩
Cleared hypotheses: k, m, H, h0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have neg : ∀ (a : α) (ha : k = @gcd _ inst _ k m * a), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
Tactic: obtain ⟨a, ha⟩ := gcd_dvd_left k m
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
have neg : a ∣ n
Tactic: refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
⊢ a ∣ n
have neg : k ∣ @gcd _ inst _ k m * n
Tactic: rw [← mul_dvd_mul_iff_left h0, ← ha]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n : α
⊢ @gcd _ inst _ k (m * n) ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
have obtain : ∀ (m' n' : α) (hm' : m' ∣ m) (hn' : n' ∣ n) (h : @gcd _ inst _ k (m * n) = m' * n'),
  @gcd _ inst _ k (m * n) ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
Tactic: obtain ⟨m', n', hm', hn', h⟩ := exists_dvd_and_dvd_of_dvd_mul (gcd_dvd_right k (m * n))
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
⊢ @gcd _ inst _ k (m * n) ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
have rw : m' * n' ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
⊢ m' * n' ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
have hm'n' : m' * n' ∣ k
Tactic: have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' * n' ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
have a : m' ∣ @gcd _ inst _ k m
Tactic: apply mul_dvd_mul
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
a : m' ∣ @gcd _ inst _ k m
⊢ m' * n' ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
have a₁ : n' ∣ @gcd _ inst _ k n
Tactic: apply mul_dvd_mul
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' ∣ @gcd _ inst _ k m
have hm'k : m' ∣ k
Tactic: have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ @gcd _ inst _ k n
have hn'k : n' ∣ k
Tactic: have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
have pos : ∀ (hg : @gcd _ inst _ a b = 0), @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
Tactic: by_cases hg : gcd a b = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
pos : ∀ (hg : @gcd _ inst _ a b = 0), @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
have neg : ∀ (hg : ¬@gcd _ inst _ a b = 0), @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
Tactic: by_cases hg : gcd a b = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : @gcd _ inst _ a b = 0
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
have hg₁ : a = 0 ∧ b = 0
Tactic: rw [gcd_eq_zero_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : a = 0 ∧ b = 0
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
have pos : @gcd _ inst _ 0 (HPow.hPow (α := α) 0 k) ∣ HPow.hPow (α := α) (@gcd _ inst _ 0 0) k
Tactic: rcases hg with ⟨rfl, rfl⟩
Cleared hypotheses: a, b, hg
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
⊢ @gcd _ inst _ a (HPow.hPow (β := ℕ) b 0) ∣ HPow.hPow (β := ℕ) (@gcd _ inst _ a b) 0
have neg : @gcd _ inst _ a 1 ∣ 1
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b ^ (k + 1)) ∣ @gcd _ inst _ a b ^ (k + 1)
have neg : @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k
Tactic: rw [pow_succ', pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k
have trans : @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k)
Tactic: trans gcd a b * gcd a (b ^ k)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
trans : @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k)
⊢ @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k
have trans₁ : @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k
Tactic: trans gcd a b * gcd a (b ^ k)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : ¬@gcd _ inst _ a b = 0
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
have neg : @gcd _ inst _ a (HPow.hPow (β := ℕ) b 0) ∣ HPow.hPow (β := ℕ) (@gcd _ inst _ a b) 0
Tactic: induction k with
    | zero => rw [pow_zero, pow_zero]; exact (gcd_one_right' a).dvd
    | succ k hk =>
      rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : ¬@gcd _ inst _ a b = 0
neg : @gcd _ inst _ a (HPow.hPow (β := ℕ) b 0) ∣ HPow.hPow (β := ℕ) (@gcd _ inst _ a b) 0
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
have neg₁ : ∀ (k : ℕ) (hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k),
  @gcd _ inst _ a (b ^ (k + 1)) ∣ @gcd _ inst _ a b ^ (k + 1)
Tactic: induction k with
    | zero => rw [pow_zero, pow_zero]; exact (gcd_one_right' a).dvd
    | succ k hk =>
      rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (@gcd _ inst _ (d₁ ^ k) b)
have h₁ : @gcd _ inst _ (d₁ ^ k) b ∣ 1
Tactic: apply isUnit_of_dvd_one
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ @gcd _ inst _ (d₁ ^ k) b ∣ 1
have trans : @gcd _ inst _ (d₁ ^ k) b ∣ @gcd _ inst _ d₁ b ^ k
Tactic: trans gcd d₁ b ^ k
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
trans : @gcd _ inst _ (d₁ ^ k) b ∣ @gcd _ inst _ d₁ b ^ k
⊢ @gcd _ inst _ (d₁ ^ k) b ∣ 1
have trans₁ : @gcd _ inst _ d₁ b ^ k ∣ 1
Tactic: trans gcd d₁ b ^ k
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ @gcd _ inst _ d₁ b ^ k ∣ 1
have hu : IsUnit (@gcd _ inst _ d₁ b ^ k)
Tactic: apply IsUnit.dvd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (@gcd _ inst _ d₁ b ^ k)
have hu : IsUnit (@gcd _ inst _ d₁ b)
Tactic: apply IsUnit.pow
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (@gcd _ inst _ d₁ b)
have hu : @gcd _ inst _ d₁ b ∣ 1
Tactic: apply isUnit_of_dvd_one
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ @gcd _ inst _ d₁ b ∣ 1
have hu : @gcd _ inst _ a b ∣ 1
Tactic: grw [hd₁, hab.dvd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
hu : @gcd _ inst _ a b ∣ 1
⊢ @gcd _ inst _ d₁ b ∣ 1
have hu₁ : Dvd.dvd.{u_1} (α := α) 1 1
Tactic: grw [hd₁, hab.dvd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
have h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
Tactic: have h1 : IsUnit (gcd (d₁ ^ k) b) := by
    apply isUnit_of_dvd_one
    trans gcd d₁ b ^ k
    · exact gcd_pow_left_dvd_pow_gcd
    · apply IsUnit.dvd
      apply IsUnit.pow
      apply isUnit_of_dvd_one
      grw [hd₁, hab.dvd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
⊢ d₁ ^ k ∣ a * b
have h₁ : a * b = d₁ ^ k * d₂ ^ k
Tactic: use d₂ ^ k
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
⊢ a * b = d₁ ^ k * d₂ ^ k
have h₁ : (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k
Tactic: rw [h, hc]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
have h2 : d₁ ^ k ∣ a * b
Tactic: have h2 : d₁ ^ k ∣ a * b := by
    use d₂ ^ k
    rw [h, hc]
    exact mul_pow d₁ d₂ k
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ a * b
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
have h2₁ : d₁ ^ k ∣ b * a
Tactic: rw [mul_comm] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ∣ a
have apply : @gcd _ inst _ (d₁ ^ k) b * a ∣ a
Tactic: apply (dvd_gcd_mul_of_dvd_mul h2).trans
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ @gcd _ inst _ (d₁ ^ k) b * a ∣ a
have rw : a ∣ a
Tactic: rw [h1.mul_left_dvd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
have h3 : d₁ ^ k ∣ a
Tactic: have h3 : d₁ ^ k ∣ a := by
    apply (dvd_gcd_mul_of_dvd_mul h2).trans
    rw [h1.mul_left_dvd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
hdk : d₁ ^ k = 0
⊢ False
have h3₁ : 0 ∣ a
Tactic: rw [hdk] at h3
Cleared hypotheses: h3, hdk