awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
have h4 : d₁ ^ k ≠ 0
Tactic: have h4 : d₁ ^ k ≠ 0 := by
    intro hdk
    rw [hdk] at h3
    apply absurd (zero_dvd_iff.mp h3) ha
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
⊢ ∃ (d : α), Associated (d ^ k) a
have inl : Subsingleton α → ∃ (d : α), Associated (d ^ k) a
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
inl : Subsingleton α → ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a
have inr : Nontrivial α → ∃ (d : α), Associated (d ^ k) a
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Subsingleton α
⊢ ∃ (d : α), Associated (d ^ k) a
have h₁ : Associated (HPow.hPow (α := α) 0 k) a
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Subsingleton α
⊢ Associated (HPow.hPow (α := α) 0 k) a
have h₁ : Associated (HPow.hPow (α := α) 0 k) (HPow.hPow (α := α) 0 k)
Tactic: rw [Subsingleton.elim a (0 ^ k)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
⊢ ∃ (d : α), Associated (d ^ k) a
have pos : ∀ (ha : a = 0), ∃ (d : α), Associated (d ^ k) a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
pos : ∀ (ha : a = 0), ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a
have neg : ∀ (ha : ¬a = 0), ∃ (d : α), Associated (d ^ k) a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
⊢ ∃ (d : α), Associated (d ^ k) a
have h₁ : Associated (HPow.hPow (α := α) 0 k) a
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
⊢ Associated (HPow.hPow (α := α) 0 k) a
have h₁ : ∀ (h : a * b = HPow.hPow (β := ℕ) c 0), Associated (HPow.hPow (α := α) (β := ℕ) 0 0) a
Tactic: obtain rfl | hk := eq_or_ne k 0
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
h₁ : ∀ (h : a * b = HPow.hPow (β := ℕ) c 0), Associated (HPow.hPow (α := α) (β := ℕ) 0 0) a
⊢ Associated (HPow.hPow (α := α) 0 k) a
have h₂ : ∀ (hk : k ≠ 0), Associated (HPow.hPow (α := α) 0 k) a
Tactic: obtain rfl | hk := eq_or_ne k 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
hk : k ≠ 0
⊢ Associated (HPow.hPow (α := α) 0 k) a
have h₁ : Associated (HPow.hPow (α := α) 0 k) 0
Tactic: rw [ha, zero_pow hk]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
hk : k ≠ 0
h₁ : Associated (HPow.hPow (α := α) 0 k) 0
⊢ Associated (HPow.hPow (α := α) 0 k) a
have h₂ : Associated.{u_1} (M := α) 0 0
Tactic: rw [ha, zero_pow hk]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
⊢ ∃ (d : α), Associated (d ^ k) a
have pos : ∀ (hb : b = 0), ∃ (d : α), Associated (d ^ k) a
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
pos : ∀ (hb : b = 0), ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a
have neg : ∀ (hb : ¬b = 0), ∃ (d : α), Associated (d ^ k) a
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ ∃ (d : α), Associated (d ^ k) a
have h₁ : Associated (HPow.hPow (α := α) 1 k) a
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated (HPow.hPow (α := α) 1 k) a
have h₁ : Associated 1 a
Tactic: rw [one_pow]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated 1 a
have h₁ : Associated (@gcd _ inst _ a b) a
Tactic: apply (associated_one_iff_isUnit.mpr hab).symm.trans
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated (@gcd _ inst _ a b) a
have h₁ : Associated (@gcd _ inst _ a 0) a
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
⊢ ∃ (d : α), Associated (d ^ k) a
have neg : ∀ (h : a * b = HPow.hPow (β := ℕ) c 0), ∃ (d : α), Associated (HPow.hPow (β := ℕ) d 0) a
Tactic: obtain rfl | hk := k.eq_zero_or_pos
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (h : a * b = HPow.hPow (β := ℕ) c 0), ∃ (d : α), Associated (HPow.hPow (β := ℕ) d 0) a
⊢ ∃ (d : α), Associated (d ^ k) a
have neg₁ : ∀ (hk : k > 0), ∃ (d : α), Associated (d ^ k) a
Tactic: obtain rfl | hk := k.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = HPow.hPow (β := ℕ) c 0
⊢ ∃ (d : α), Associated (HPow.hPow (β := ℕ) d 0) a
have h₁ : Associated (HPow.hPow (α := α) (β := ℕ) 1 0) a
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = HPow.hPow (β := ℕ) c 0
⊢ Associated (HPow.hPow (α := α) (β := ℕ) 1 0) a
have h₁ : ∀ (h : a * b = 1), Associated 1 a
Tactic: rw [pow_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
⊢ Associated 1 a
have h₁ : 1 * (↑(Units.mkOfMulEqOne a b h) : α) = a
Tactic: use Units.mkOfMulEqOne _ _ h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
⊢ 1 * (↑(Units.mkOfMulEqOne a b h) : α) = a
have h₁ : 1 * a = a
Tactic: rw [Units.val_mkOfMulEqOne, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
h₁ : 1 * a = a
⊢ 1 * (↑(Units.mkOfMulEqOne a b h) : α) = a
have h₂ : a = a
Tactic: rw [Units.val_mkOfMulEqOne, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ c ∣ a * b
have rw : c ∣ c ^ k
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ ∃ (d : α), Associated (d ^ k) a
have hc : c ∣ a * b
Tactic: have hc : c ∣ a * b := by
    rw [h]
    exact dvd_pow_self _ hk.ne'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc : c ∣ a * b
⊢ ∃ (d : α), Associated (d ^ k) a
have neg : ∀ (d₁ d₂ : α) (hd₁ : d₁ ∣ a) (hd₂ : d₂ ∣ b) (hc : c = d₁ * d₂), ∃ (d : α), Associated (d ^ k) a
Tactic: obtain ⟨d₁, d₂, hd₁, hd₂, hc⟩ := exists_dvd_and_dvd_of_dvd_mul hc
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
⊢ ∃ (d : α), Associated (d ^ k) a
have h₁ : Associated (d₁ ^ k) a
Tactic: use d₁
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
⊢ Associated (d₁ ^ k) a
have h₁ : ∀ (h0₁ : d₁ ^ k ≠ 0) (a' : α) (ha' : a = d₁ ^ k * a'), Associated (d₁ ^ k) a
Tactic: obtain ⟨h0₁, ⟨a', ha'⟩⟩ := pow_dvd_of_mul_eq_pow ha hab h hc hd₁
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a
have h₁ : ∀ (h : b * a = c ^ k),
  Nontrivial α →
    ∀ (ha : ¬a = 0) (hb : ¬b = 0) (hk : k > 0) (hc : c ∣ a * b) (d₁ d₂ : α) (hd₁ : d₁ ∣ a) (hd₂ : d₂ ∣ b)
      (hc : c = d₂ * d₁) (h0₁ : d₁ ^ k ≠ 0) (a' : α) (ha' : a = d₁ ^ k * a'), Associated (d₁ ^ k) a
Tactic: rw [mul_comm] at h hc
Cleared hypotheses: h, h_1, ha, hb, hk, hc_1, d₁, d₂, hd₁, hd₂, hc, h0₁, a', ha'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : b * a = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a
have h₁ : ∀ (hab : IsUnit (@gcd _ inst _ b a)) {k : ℕ} (h : b * a = c ^ k),
  Nontrivial α →
    ∀ (ha : ¬a = 0) (hb : ¬b = 0) (hk : k > 0) (hc : c ∣ a * b) (d₁ d₂ : α) (hd₁ : d₁ ∣ a) (hd₂ : d₂ ∣ b)
      (hc : c = d₂ * d₁) (h0₁ : d₁ ^ k ≠ 0) (a' : α) (ha' : a = d₁ ^ k * a'), Associated (d₁ ^ k) a
Tactic: rw [(gcd_comm' a b).isUnit_iff] at hab
Cleared hypotheses: hab, k, h, h_1, ha, hb, hk, hc_1, d₁, d₂, hd₁, hd₂, hc, h0₁, a', ha'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h : b * a = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a
have h₁ : ∀ (h0₂ : d₂ ^ k ≠ 0) (b' : α) (hb' : b = d₂ ^ k * b'), Associated (d₁ ^ k) a
Tactic: obtain ⟨h0₂, ⟨b', hb'⟩⟩ := pow_dvd_of_mul_eq_pow hb hab h hc hd₂
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h : b * a = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a
have h₁ : ∀ (ha' : a = d₁ ^ k * a') (h0₂ : d₂ ^ k ≠ 0) (b' : α) (h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k)
  (hb' : b = d₂ ^ k * b'), Associated (d₁ ^ k) a
Tactic: rw [ha', hb', hc, mul_pow] at h
Cleared hypotheses: h, ha', h0₂, b', hb'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ a' * b' = 1
have apply : d₁ ^ k * (a' * b') = d₁ ^ k * 1
Tactic: apply (mul_right_inj' h0₁).mp
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₁ ^ k * (a' * b') = d₁ ^ k * 1
have rw : d₁ ^ k * (a' * b') = d₁ ^ k
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₁ ^ k * (a' * b') = d₁ ^ k
have apply : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * d₁ ^ k
Tactic: apply (mul_right_inj' h0₂).mp
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * d₁ ^ k
have rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
have rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
Tactic: rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
have rw₁ : d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
Tactic: rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₁ : d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
have rw₂ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * (d₁ ^ k * a'))
Tactic: rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₁ : d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₂ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * (d₁ ^ k * a'))
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
have rw₃ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * d₁ ^ k * a')
Tactic: rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₁ : d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₂ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₃ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * d₁ ^ k * a')
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
have rw₄ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (d₁ ^ k * b' * a')
Tactic: rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a
have h' : a' * b' = 1
Tactic: have h' : a' * b' = 1 := by
    apply (mul_right_inj' h0₁).mp
    rw [mul_one]
    apply (mul_right_inj' h0₂).mp
    rw [← h]
    rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
⊢ Associated (d₁ ^ k) a
have h₁ : d₁ ^ k * (↑(Units.mkOfMulEqOne a' b' h') : α) = a
Tactic: use Units.mkOfMulEqOne _ _ h'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
⊢ d₁ ^ k * (↑(Units.mkOfMulEqOne a' b' h') : α) = a
have h₁ : d₁ ^ k * a' = a
Tactic: rw [Units.val_mkOfMulEqOne, ha']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
h₁ : d₁ ^ k * a' = a
⊢ d₁ ^ k * (↑(Units.mkOfMulEqOne a' b' h') : α) = a
have h₂ : d₁ ^ k * a' = d₁ ^ k * a'
Tactic: rw [Units.val_mkOfMulEqOne, ha']
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
⊢ IsUnit (@gcd _ inst _ x' y')
have rw : Associated (@gcd _ inst _ x' y') 1
Tactic: rw [← associated_one_iff_isUnit]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
⊢ Associated (@gcd _ inst _ x' y') 1
have refine : Associated (@gcd _ inst _ x y * @gcd _ inst _ x' y') (@gcd _ inst _ x y * 1)
Tactic: refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
⊢ Associated (@gcd _ inst _ x y * @gcd _ inst _ x' y') (@gcd _ inst _ x y * 1)
have h₁ : @gcd _ inst _ x y * 1 = @gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y')
Tactic: convert! (gcd_mul_left' (gcd x y) x' y').symm using 1