awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∣ HMul.hMul (α := R) ((normalize : (a : R) → R) b : R) g
have h : ∀ b_1 ∈ T, x ∣ b * id b_1
Tactic: rw [← Finset.gcd_mul_left, Finset.dvd_gcd_iff]
-- 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)
c : R
hc : c ∈ T
⊢ x ∣ b * id c
have h : b * id c ∈ J * K
Tactic: rw [← mem_span_singleton, span, ← 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ Submodule.IsPrincipal I
have obtain : ∀ (a : R) (K : Ideal R) (ha0 : a ≠ 0)
  (h :
    (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))),
  Submodule.IsPrincipal I
Tactic: obtain ⟨a, K, ha0, h⟩ := exists_eq_spanSingleton_mul (I : FractionalIdeal R⁰ (FractionRing R))⁻¹
-- 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ Eq (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑(I * K) : FractionalIdeal R⁰ (FractionRing R))
    (↑(span {a}) : FractionalIdeal R⁰ (FractionRing R))
have rw : HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
    (↑K : FractionalIdeal R⁰ (FractionRing R)) =
  spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
Tactic: rw [coeIdeal_mul, coeIdeal_span_singleton]
-- 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
have rw : ∀
  (hI :
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
        (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
      1)
  (a : R) (K : Ideal R) (ha0 : a ≠ 0)
  (h :
    (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))),
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
Tactic: rw [← mul_inv_cancel_iff_isUnit] at hI
Cleared hypotheses: hI, a, K, ha0, h
-- 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)
I : Ideal R
hI :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    1
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
have ha0' : HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    ((spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a))⁻¹ :
      FractionalIdeal (R := R) R⁰ (FractionRing R)) =
  1
Tactic: have ha0' := spanSingleton_mul_inv (R₁ := R) (FractionRing R)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
          (mem_nonZeroDivisors_iff_ne_zero.mpr ha0))
-- 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)
I : Ideal R
hI :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    1
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
ha0' :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a))⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) =
    1
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
have h₁ : Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
  ((fun (t : FractionalIdeal (R := R) R⁰ (FractionRing R)) ↦
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
          (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
            FractionalIdeal (R := R) R⁰ (FractionRing R))
          ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
        t)
    (HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))))
  ((fun (t : FractionalIdeal (R := R) R⁰ (FractionRing R)) ↦
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
          (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
            FractionalIdeal (R := R) R⁰ (FractionRing R))
          ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
        t)
    (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹)
Tactic: replace h :=
        congrArg
          (fun t =>
            spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * I * t)
          h.symm
Cleared hypotheses: h
-- 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ Submodule.IsPrincipal I
have hIK : I * K = span {a}
Tactic: have hIK : I * K = Ideal.span ({a} : Set R) :=
    (coeIdeal_inj (K := FractionRing R)).mp <| by
      rw [coeIdeal_mul, coeIdeal_span_singleton]
      rw [← mul_inv_cancel_iff_isUnit] at hI
      have ha0' := spanSingleton_mul_inv (R₁ := R) (FractionRing R)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
          (mem_nonZeroDivisors_iff_ne_zero.mpr ha0))
      replace h :=
        congrArg
          (fun t =>
            spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * I * t)
          h.symm
      dsimp only at h
      rwa [mul_mul_mul_comm, ← spanSingleton_inv, ha0', one_mul, mul_assoc, hI, mul_one] at h
-- 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
⊢ Submodule.IsPrincipal I
have refine : ∃ (K : Ideal R), I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)
Tactic: refine isPrincipal_of_exists_mul_ne_zero_isPrincipal (J := I) ?_
-- 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
⊢ ∃ (K : Ideal R), I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)
have refine_1 : I * K ≠ 0
Tactic: refine ⟨K, ?_, ?_⟩
-- 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)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
refine_1 : I * K ≠ 0
⊢ ∃ (K : Ideal R), I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)
have refine_2 : Submodule.IsPrincipal (I * K)
Tactic: refine ⟨K, ?_, ?_⟩
-- 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)
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I : FractionalIdeal R⁰ (FractionRing R)).num
⊢ (↑(↑I : FractionalIdeal R⁰ (FractionRing R)) : Submodule R (FractionRing R)).IsPrincipal
have hJunit : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑J : FractionalIdeal R⁰ (FractionRing R))
Tactic: have hJunit : IsUnit (J : FractionalIdeal R⁰ (FractionRing R)) :=
    FractionalIdeal.isUnit_num.mpr ⟨I, rfl⟩
-- 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)
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I : FractionalIdeal R⁰ (FractionRing R)).num
hJunit : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑J : FractionalIdeal R⁰ (FractionRing R))
⊢ (↑(↑I : FractionalIdeal R⁰ (FractionRing R)) : Submodule R (FractionRing R)).IsPrincipal
have hJprin : Submodule.IsPrincipal J
Tactic: have hJprin : J.IsPrincipal := isPrincipal_of_isUnit_fractionalIdeal J hJunit
-- 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)
⊢ Subsingleton.{u_1 + 1} (ClassGroup R)
have refine : ∀ (y : ClassGroup R), y = 1
Tactic: refine subsingleton_of_forall_eq 1 ?_
-- 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)
x : ClassGroup R
⊢ x = 1
have refine : ∀ (I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
  Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)
Tactic: refine ClassGroup.induction (FractionRing R) ?_ x
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a_1 a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
h : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ (i ::ₘ s).prod ~ᵤ i * a
have rw : i * s.prod ~ᵤ i * a
Tactic: rw [s.prod_cons i]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a : α
hn0 : a ≠ 0
hnu : ¬IsUnit a
⊢ ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅
have obtain : ∀ (f : Multiset α) (hi : ∀ b ∈ f, Irreducible b) (u : αˣ) (hn0 : f.prod * (↑u : α) ≠ 0)
  (hnu : ¬IsUnit (f.prod * (↑u : α))),
  ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
Tactic: obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0
Cleared hypotheses: a, hn0, hnu
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
have obtain : ∀ (b : α) (h : b ∈ f), ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
Tactic: obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
have refine_1 : ∀ (a : α) (ha : a ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible a
Tactic: refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_1 : ∀ (a : α) (ha : a ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible a
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
have refine_2 : (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
Tactic: refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
a : α
ha : a ∈ b * (↑u : α) ::ₘ f.erase b
⊢ Irreducible a
have refine_1 : ∀ (ha : b * (↑u : α) ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible (b * (↑u : α))
Tactic: obtain rfl | ha := Multiset.mem_cons.1 ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
a : α
ha : a ∈ b * (↑u : α) ::ₘ f.erase b
refine_1 : ∀ (ha : b * (↑u : α) ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible (b * (↑u : α))
⊢ Irreducible a
have refine_1₁ : ∀ (ha : a ∈ f.erase b), Irreducible a
Tactic: obtain rfl | ha := Multiset.mem_cons.1 ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
⊢ (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
have refine_2 : b * (↑u : α) * (f.erase b).prod = f.prod * (↑u : α)
Tactic: rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_2 : b * (↑u : α) * (f.erase b).prod = f.prod * (↑u : α)
⊢ (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
have refine_2₁ : (↑u : α) * b * (f.erase b).prod = f.prod * (↑u : α)
Tactic: rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_2 : b * (↑u : α) * (f.erase b).prod = f.prod * (↑u : α)
refine_2₁ : (↑u : α) * b * (f.erase b).prod = f.prod * (↑u : α)
⊢ (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
have refine_2₂ : (↑u : α) * (b * (f.erase b).prod) = f.prod * (↑u : α)
Tactic: rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_2 : b * (↑u : α) * (f.erase b).prod = f.prod * (↑u : α)
refine_2₁ : (↑u : α) * b * (f.erase b).prod = f.prod * (↑u : α)
refine_2₂ : (↑u : α) * (b * (f.erase b).prod) = f.prod * (↑u : α)
⊢ (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
have refine_2₃ : (↑u : α) * f.prod = f.prod * (↑u : α)
Tactic: rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_2 : b * (↑u : α) * (f.erase b).prod = f.prod * (↑u : α)
refine_2₁ : (↑u : α) * b * (f.erase b).prod = f.prod * (↑u : α)
refine_2₂ : (↑u : α) * (b * (f.erase b).prod) = f.prod * (↑u : α)
refine_2₃ : (↑u : α) * f.prod = f.prod * (↑u : α)
⊢ (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
have refine_2₄ : f.prod * (↑u : α) = f.prod * (↑u : α)
Tactic: rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]