awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
have pos : p * c' * a' = p * a
Tactic: refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
pos : p * c' * a' = p * a
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
have pos₁ : p * c' * b' = p * b
Tactic: refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a
have pos : p * (c' * a') = p * a
Tactic: rw [mul_assoc, ha']
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
pos : p * (c' * a') = p * a
⊢ p * c' * a' = p * a
have pos₁ : p * a = p * a
Tactic: rw [mul_assoc, ha']
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b
have pos : p * (c' * b') = p * b
Tactic: rw [mul_assoc, hb']
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
pos : p * (c' * b') = p * b
⊢ p * c' * b' = p * b
have pos₁ : p * b = p * b
Tactic: rw [mul_assoc, hb']
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
have neg : ∀ (a' b' c' : R) (coprime : IsRelPrime a' b') (a_ne_zero : c' * a' ≠ 0)
  (ih_a :
    c' * a' ≠ 0 →
      ∀ (b : R), ∃ (a'_1 : R) (b' : R) (c'_1 : R), IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b)
  (pa_ne_zero : p * (c' * a') ≠ 0) (h : ¬p ∣ c' * b'),
  ∃ (a'_1 : R) (b'_1 : R) (c'_1 : R), IsRelPrime a'_1 b'_1 ∧ c'_1 * a'_1 = p * (c' * a') ∧ c'_1 * b'_1 = c' * b'
Tactic: obtain ⟨a', b', c', coprime, rfl, rfl⟩ := ih_a a_ne_zero b
Cleared hypotheses: a, a_ne_zero, ih_a, pa_ne_zero, b, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 → ∀ (b : R), ∃ (a'_1 : R) (b' : R) (c'_1 : R), IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
⊢ ∃ (a'_1 : R) (b'_1 : R) (c'_1 : R), IsRelPrime a'_1 b'_1 ∧ c'_1 * a'_1 = p * (c' * a') ∧ c'_1 * b'_1 = c' * b'
have neg : IsRelPrime (p * a') b'
Tactic: refine ⟨p * a', b', c', ?_, mul_left_comm _ _ _, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 → ∀ (b : R), ∃ (a'_1 : R) (b' : R) (c'_1 : R), IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
⊢ IsUnit q
have neg : ∀ (p_dvd_q : p ∣ q), IsUnit q
Tactic: rcases p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q | q_dvd_a'
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 → ∀ (b : R), ∃ (a'_1 : R) (b' : R) (c'_1 : R), IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
neg : ∀ (p_dvd_q : p ∣ q), IsUnit q
⊢ IsUnit q
have neg₁ : ∀ (q_dvd_a' : q ∣ a'), IsUnit q
Tactic: rcases p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q | q_dvd_a'
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 → ∀ (b : R), ∃ (a'_1 : R) (b' : R) (c'_1 : R), IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
⊢ IsUnit q
have this : p ∣ c' * b'
Tactic: have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
hJ : ∃ (K : Ideal R), J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)
this : NormalizedGCDMonoid R := Classical.choice ⋯
⊢ Submodule.IsPrincipal J
have obtain : ∀ (K : Ideal R) (hJK0 : J * K ≠ 0) (hK : Submodule.IsPrincipal (J * K)), Submodule.IsPrincipal J
Tactic: obtain ⟨K, hJK0, hK⟩ := hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
⊢ Submodule.IsPrincipal J
have rcases : ∀ (x : R) (hJK : J * K = R ∙ x), Submodule.IsPrincipal J
Tactic: rcases hK.principal with ⟨x, hJK⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
⊢ Submodule.IsPrincipal J
have hxmemJK : x ∈ J * K
Tactic: have hxmemJK : x ∈ J * K := by simp [hJK]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
⊢ ∃ (T : Finset R), (↑T : Set R) ⊆ (↑K : Set R) ∧ x ∈ J * span (↑T : Set R)
have obtain : ∀ (S T : Finset R) (hSJ : (↑S : Set R) ⊆ (↑J : Set R)) (hTK : (↑T : Set R) ⊆ (↑K : Set R))
  (hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((↑S : Set R) * (↑T : Set R))) x),
  ∃ (T : Finset R), (↑T : Set R) ⊆ (↑K : Set R) ∧ x ∈ J * span (↑T : Set R)
Tactic: obtain ⟨S, T, hSJ, hTK, hx⟩ := Submodule.mem_span_mul_finite_of_mem_mul hxmemJK
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
S T : Finset R
hSJ : (↑S : Set R) ⊆ (↑J : Set R)
hTK : (↑T : Set R) ⊆ (↑K : Set R)
hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((↑S : Set R) * (↑T : Set R))) x
⊢ ∃ (T : Finset R), (↑T : Set R) ⊆ (↑K : Set R) ∧ x ∈ J * span (↑T : Set R)
have refine : x ∈ J * span (↑T : Set R)
Tactic: refine ⟨T, hTK, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
S T : Finset R
hSJ : (↑S : Set R) ⊆ (↑J : Set R)
hTK : (↑T : Set R) ⊆ (↑K : Set R)
hx : Membership.mem (γ := Submodule R R) (Submodule.span R ((↑S : Set R) * (↑T : Set R))) x
⊢ x ∈ J * span (↑T : Set R)
have rw : Membership.mem (γ := Ideal R) (span ((↑J : Set R) * (↑T : Set R))) x
Tactic: rw [← J.span_eq, span_mul_span]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
⊢ Submodule.IsPrincipal J
have this₁ : ∃ (T : Finset R), (↑T : Set R) ⊆ (↑K : Set R) ∧ x ∈ J * span (↑T : Set R)
Tactic: have : ∃ T : Finset R, (T : Set R) ⊆ K ∧ x ∈ J * span T := by
    obtain ⟨S, T, hSJ, hTK, hx⟩ := Submodule.mem_span_mul_finite_of_mem_mul hxmemJK
    refine ⟨T, hTK, ?_⟩
    rw [← J.span_eq, span_mul_span]
    exact span_mono (Set.mul_subset_mul_right hSJ) hx
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
this : ∃ (T : Finset R), (↑T : Set R) ⊆ (↑K : Set R) ∧ x ∈ J * span (↑T : Set R)
⊢ Submodule.IsPrincipal J
have obtain : ∀ (T : Finset R) (hTK : (↑T : Set R) ⊆ (↑K : Set R)) (hxT : x ∈ J * span (↑T : Set R)), Submodule.IsPrincipal J
Tactic: obtain ⟨T, hTK, hxT⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
⊢ Submodule.IsPrincipal J
have hK' : K' ≤ span {g}
Tactic: have hK' : K' ≤ span {g} :=
    span_le.mpr fun z hz ↦ mem_span_singleton.mpr (Finset.gcd_dvd hz)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
⊢ Submodule.IsPrincipal J
have hxJg : x ∈ J * span {g}
Tactic: have hxJg : x ∈ J * span {g} := mul_mono_right hK' hxT
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx : x = 0
⊢ False
have apply : J * K = 0
Tactic: apply hJK0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
⊢ Submodule.IsPrincipal J
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := by
    intro hx
    apply hJK0
    simpa [hJK]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
this : J * span {g} = span {x}
⊢ Submodule.IsPrincipal J
have obtain : ∀ (y : R) (hyJ : y ∈ J) (hJK : J * K = R ∙ y * g) (hxmemJK : y * g ∈ J * K) (hxT : y * g ∈ J * K')
  (hxJg : y * g ∈ J * span {g}) (hx0 : y * g ≠ 0) (this : J * span {g} = span {y * g}), Submodule.IsPrincipal J
Tactic: obtain ⟨y, hyJ, rfl⟩ := (Ideal.mem_mul_span_singleton).1 hxJg
Cleared hypotheses: x, hJK, hxmemJK, hxT, hxJg, hx0, this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J * span {g} = span {y * g}
⊢ Submodule.IsPrincipal J
have rw : ∀ (this : J = span {y}), Submodule.IsPrincipal J
Tactic: rw [← span_singleton_mul_span_singleton, span_singleton_mul_left_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J * span {g} = span {y * g}
rw : ∀ (this : J = span {y}), Submodule.IsPrincipal J
⊢ Submodule.IsPrincipal J
have rw₁ : ∀ (this : J * span {g} = HMul.hMul (α := Ideal R) (span {y}) (span {g})), g ≠ 0
Tactic: rw [← span_singleton_mul_span_singleton, span_singleton_mul_left_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J * span {g} = HMul.hMul (α := Ideal R) (span {y}) (span {g})
⊢ g ≠ 0
have contrapose : ∀ (hx0 : g = 0), y * g = 0
Tactic: contrapose hx0
Cleared hypotheses: hx0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
this : J * span {g} = HMul.hMul (α := Ideal R) (span {y}) (span {g})
hx0 : g = 0
⊢ y * g = 0
have rw : y * 0 = 0
Tactic: rw [hx0, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this_1 : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
this : J * span {g} = HMul.hMul (α := Ideal R) (span {y}) (span {g})
hx0 : g = 0
rw : y * 0 = 0
⊢ y * g = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [hx0, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
⊢ Submodule.IsPrincipal J
have suffices : J * span {g} = span {x}
Tactic: suffices J * span {g} = span {x} by
    obtain ⟨y, hyJ, rfl⟩ := (Ideal.mem_mul_span_singleton).1 hxJg
    rw [← span_singleton_mul_span_singleton, span_singleton_mul_left_inj] at this
    · exact ⟨y, this⟩
    · contrapose hx0
      rw [hx0, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
⊢ J * span {g} = span {x}
have refine : ∀ (b : R) (hb : b ∈ J) (z : R) (hz : Membership.mem (γ := Ideal R) (span {g}) z),
  Membership.mem (γ := Ideal R) (span {x}) (b * z)
Tactic: refine le_antisymm
      (mul_le.mpr fun b hb z hz ↦ ?_)
      ((span_singleton_le_iff_mem _).mpr hxJg)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) z
⊢ Membership.mem (γ := Ideal R) (span {x}) (b * z)
have obtain : ∀ (z : R) (hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)),
  Membership.mem (γ := Ideal R) (span {x}) (b * (g * z))
Tactic: obtain ⟨z, rfl⟩ := mem_span_singleton.mp hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
⊢ Membership.mem (γ := Ideal R) (span {x}) (b * (g * z))
have rw : x ∣ b * g * z
Tactic: rw [mem_span_singleton, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
⊢ x ∣ b * g * z
have h : x ∣ b * g
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
⊢ x ∣ b * g
have h : x ∣ HMul.hMul (α := R) ((normalize : (a : R) → R) b : R) g
Tactic: suffices x ∣ normalize b * g from this.trans ((associated_normalize b).mul_right g).dvd'