awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
inst_3 : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ generator (ϕ.submoduleImage N) ∣ (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯)
have rw : ∃ (y : M) (yN : y ∈ N),
  Eq.{u + 1} (α := R) ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y sorry) : R)
    ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x sorry) : R)
Tactic: rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y
have rw : ∀ (hx : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z}))
  (hy : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})),
  LE.le (α := Ideal R) (Ideal.span {gcd x y}) (Ideal.span {z})
Tactic: rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
hx : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z})
hy : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})
⊢ LE.le (α := Ideal R) (Ideal.span {gcd x y}) (Ideal.span {z})
have rw : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z}) ∧ LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})
Tactic: rw [span_gcd, Ideal.span_insert, sup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
⊢ Membership.mem (γ := Ideal R) (Ideal.span {x, y}) (gcd x y)
have rw : Membership.mem (γ := Ideal R) (Ideal.span {gcd x y}) (gcd x y)
Tactic: rw [← span_gcd]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
⊢ Membership.mem (γ := Ideal R) (Ideal.span {gcd x y}) (gcd x y)
have a : Membership.mem (γ := Set R) {gcd x y} (gcd x y)
Tactic: apply Ideal.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsCoprime x y
have rw : IsUnit (gcd x y)
Tactic: rw [← Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_sup_eq, ← Ideal.span_union,
    Set.singleton_union, ← span_gcd, Ideal.span_singleton_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
have insert : ∀ (x y : R) (hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)),
  ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Tactic: obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
⊢ ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
have insert : ∀ (u : Rˣ)
  (hu : IsBezout.gcd (f a) (s.gcd f) * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)),
  ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Tactic: obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : IsBezout.gcd (f a) (s.gcd f) * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
⊢ ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
have hu₁ : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
Tactic: rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
⊢ ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
have insert : ∀ (g : α → R) (hg : s.gcd f = ∑ a ∈ s, f a * g a), ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Tactic: obtain ⟨g, hg⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
have insert : (insert a s).gcd f =
  ∑ a_1 ∈ insert a s,
    HMul.hMul (β := R) (f a_1)
      (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a_1 : R)
Tactic: refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ (insert a s).gcd f =
    ∑ a_1 ∈ insert a s,
      HMul.hMul (β := R) (f a_1)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a_1 : R)
have insert : f a * x * (↑u : R) + (∑ a ∈ s, f a * g a) * y * (↑u : R) =
  HMul.hMul (β := R) (f a) (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a : R) +
    ∑ x_1 ∈ s,
      HMul.hMul (β := R) (f x_1)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R)
Tactic: rw [gcd_insert, sum_insert ha, ← hu, hg]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ f a * x * (↑u : R) + (∑ a ∈ s, f a * g a) * y * (↑u : R) =
    HMul.hMul (β := R) (f a)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a : R) +
      ∑ x_1 ∈ s,
        HMul.hMul (β := R) (f x_1)
          (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R)
have insert : Eq.{u + 1} (α := R) (∑ x ∈ s, f x * (g x * (y * (↑u : R))))
  (∑ x_1 ∈ s,
    HMul.hMul (β := R) (f x_1)
      (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R))
Tactic: simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
s : Finset α
f : α → R
⊢ ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
have empty : ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
s : Finset α
f : α → R
empty : ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a
⊢ ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a),
  ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
s : Finset α
f : α → R
⊢ ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
have empty : ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
s : Finset α
f : α → R
empty : ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a
⊢ ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a),
  ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
⊢ 1 ∈ T
have obtain : ∀ (z : R) (hz : generator S = generator T * z), 1 ∈ T
Tactic: obtain ⟨z, hz⟩ := (mem_iff_generator_dvd _).1 (hST <| generator_mem S)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ T ≤ S
have rwa : Ideal.span {generator T} ≤ S
Tactic: rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
rwa : Ideal.span {generator T} ≤ S
⊢ T ≤ S
have rwa₁ : {generator T} ⊆ (↑S : Set R)
Tactic: rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
rwa : Ideal.span {generator T} ≤ S
rwa₁ : {generator T} ⊆ (↑S : Set R)
⊢ T ≤ S
have rwa₂ : generator T ∈ (↑S : Set R)
Tactic: rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ 1 ∈ T
have hTS : T ≤ S
Tactic: have hTS : T ≤ S := by
          rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
⊢ 1 ∈ T
have inr : ∀ (y : R) (hy : z = generator S * y), 1 ∈ T
Tactic: obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
⊢ 1 ∈ T
have this : generator S ≠ 0
Tactic: have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T
have inr : ∀ (h : z ∈ S) (y : R) (hz : 1 = generator T * y) (hy : z = generator S * y) (this : generator S ≠ 0), 1 ∈ T
Tactic: rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
Cleared hypotheses: hz, h, y, hy, this
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
⊢ 1 ∈ T
have x₁ : generator T ∈ S ∨ z ∈ S
Tactic: cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with
      | inl h =>
        have hTS : T ≤ S := by
          rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
        exact (hxS <| hTS hxT).elim
      | inr h =>
        obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
        have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
        rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
        exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
wf : WellFounded.{u + 1} (α := R) EuclideanDomain.r
hmin :
  wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧
    wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
⊢ wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∣
    x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h
have this : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0}
Tactic: have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∉
                    { x : R | x ∈ S ∧ x ≠ 0 } :=
                  fun h₁ => WellFounded.not_lt_min wf _ h₁ (mod_lt x hmin.2)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
wf : WellFounded.{u + 1} (α := R) EuclideanDomain.r
hmin :
  wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧
    wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0}
⊢ x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0
have this₁ : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ S ∨
  x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0
Tactic: simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
wf : WellFounded.{u + 1} (α := R) EuclideanDomain.r
hmin :
  wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧
    wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0}
⊢ wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∣
    x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h
have this₁ : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0
Tactic: have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h = 0 := by
                  simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
                  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : ¬Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
a : R
⊢ a ∈ S ↔ Membership.mem (γ := Submodule R R) (R ∙ 0) a
have rw : a ∈ S ↔ a = 0
Tactic: rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : R ∙ p < I
⊢ I = ⊤
have rcases : ∀ (a : R) (hI : LT.lt (α := Ideal R) (R ∙ p) (R ∙ a)), Eq (α := Ideal R) (R ∙ a) ⊤
Tactic: rcases principal I with ⟨a, rfl⟩
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : LT.lt (α := Ideal R) (R ∙ p) (R ∙ a)
⊢ Eq (α := Ideal R) (R ∙ a) ⊤
have rw : IsUnit a
Tactic: rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : LT.lt (α := Ideal R) (R ∙ p) (R ∙ a)
⊢ IsUnit a
have rcases : ∀ (b : R) (hp : Irreducible (a * b)) (hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)), IsUnit a
Tactic: rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
Cleared hypotheses: p, hp, hI
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
⊢ IsUnit a
have refine : ∀ (hb : IsUnit b), LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)
Tactic: refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_gt hI))
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
hb : IsUnit b
⊢ LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)
have rw : LE.le (α := Ideal R) (Ideal.span {a}) (R ∙ a * b)
Tactic: rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
hb : IsUnit b
rw : LE.le (α := Ideal R) (Ideal.span {a}) (R ∙ a * b)
⊢ LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)
have rw₁ : LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {a * b})
Tactic: rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
hb : IsUnit b
rw : LE.le (α := Ideal R) (Ideal.span {a}) (R ∙ a * b)
rw₁ : LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {a * b})
⊢ LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)
have rw₂ : a * b ∣ a
Tactic: rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
hb : IsUnit b
rw : LE.le (α := Ideal R) (Ideal.span {a}) (R ∙ a * b)
rw₁ : LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {a * b})
rw₂ : a * b ∣ a
⊢ LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)
have rw₃ : a ∣ a
Tactic: rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]