awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
rw : ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i : HeightOneSpectrum R).asIdeal
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal

Tactic:
rw [← this, Finset.inf_eq_iInf, iInf_subtype', Ideal.mul_iInf, Ideal.mem_iInf]

Premises used: iInf_subtype', Ideal.mem_iInf, Finset.inf_eq_iInf, Ideal.mul_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
pos : ∀ (hqp : q = p'), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
neg : ∀ (hqp : ¬q = p'), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal

Tactic:
by_cases hqp : q = p'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : q = p'
pos : ∀ (hq : p' ∈ s), a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) p' hq) : HeightOneSpectrum R).asIdeal
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal

Tactic:
subst hqp
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
hq : p' ∈ s
⊢ HSub.hSub (α := R) (∑ p ∈ s, a p) (∑ q ∈ s \ {p'}, a q) ∈ J * p

Tactic:
sub_mem H₁ H₂

Premises used: sub_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
hq : p' ∈ s
h₁ : a p' = HSub.hSub (α := R) (∑ p ∈ s, a p) (∑ q ∈ s \ {p'}, a q)
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) p' hq) : HeightOneSpectrum R).asIdeal

Tactic:
convert! sub_mem H₁ H₂

Premises used: sub_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
hq : p' ∈ s
h₁ : a p' = a p' + ∑ x ∈ s \ {p'}, a x - ∑ q ∈ s \ {p'}, a q
h₂ h₃ : a p' = a p'
⊢ a p' = HSub.hSub (α := R) (∑ p ∈ s, a p) (∑ q ∈ s \ {p'}, a q)

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hp's, add_sub_cancel_right]

Premises used: add_sub_cancel_right, Finset.sum_eq_add_sum_diff_singleton_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal

Tactic:
Ideal.mul_mono_right ?_ (ha p' hp's)

Premises used: Set.Mem, Ideal.mul_mono_right
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
neg : ∏ q ∈ s \ {p'}, q.asIdeal ≤ (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal
⊢ a p' ∈ J * (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal

Tactic:
refine Ideal.mul_mono_right ?_ (ha p' hp's)

Premises used: Ideal.mul_mono_right
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ q ∈ s \ {p'}

Tactic:
simpa [hq] using hqp
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset (s := {v : HeightOneSpectrum R | v.asIdeal ∣ I})
this_1 : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : (p : HeightOneSpectrum R) → R
ha : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ (p : HeightOneSpectrum R) (hps : p ∈ s), a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : Eq (α := Ideal R) (s.inf fun (i : HeightOneSpectrum R) ↦ i.asIdeal) (∏ i ∈ s, i.asIdeal)
inst : Nonempty.{max 1 (u_1 + 1)} ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ ∏ q ∈ s \ {p'}, q.asIdeal ≤ (↑(Subtype.mk (p := Membership.mem s) q hq) : HeightOneSpectrum R).asIdeal

Tactic:
exact Ideal.prod_le_inf.trans (Finset.inf_le (b := q) (by simpa [hq] using hqp))

Premises used: Ideal.prod_le_inf, LE.le.trans, Finset.inf_le
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
x : R
hxI : x ∈ I
hx : x ≠ 0
⊢ Ne (α := Ideal R) (Ideal.span {x}) 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
x : R
hxI : x ∈ I
hx : x ≠ 0
obtain :
  ∀ (y : R) (hxI : Membership.mem (γ := Ideal R) (Ideal.span {x} ⊔ Ideal.span {y}) x),
    ∃ (y_1 : R), Eq (α := Ideal R) (Ideal.span {x} ⊔ Ideal.span {y}) (Ideal.span {x, y_1})
⊢ ∃ (y : R), I = Ideal.span {x, y}

Tactic:
obtain ⟨y, rfl⟩ := exists_sup_span_eq (I.span_singleton_le_iff_mem.mpr hxI) (by simpa)

Premises used: Iff.mpr, Ideal.span_singleton_le_iff_mem, IsDedekindDomain.exists_sup_span_eq, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : Membership.mem (γ := Ideal R) (Ideal.span {x} ⊔ Ideal.span {y}) x
simp_rw : ∃ (y_1 : R), Eq (α := Ideal R) (Ideal.span {y, x}) (Ideal.span {y_1, x})
⊢ ∃ (y_1 : R), Eq (α := Ideal R) (Ideal.span {x} ⊔ Ideal.span {y}) (Ideal.span {x, y_1})

Tactic:
simp_rw [← Ideal.span_union, Set.union_singleton, Set.pair_comm x]

Premises used: Ideal.span_union, Set.union_singleton, Set.pair_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : Membership.mem (γ := Ideal R) (Ideal.span {x} ⊔ Ideal.span {y}) x
w : R
h : Eq (α := Ideal R) (Ideal.span {y, x}) (Ideal.span {y, x})
⊢ ∃ (y_1 : R), Eq (α := Ideal R) (Ideal.span {y, x}) (Ideal.span {y_1, x})

Tactic:
use y
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
inr :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
        [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
        (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c)
    (hb' : ¬b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
    [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
    (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
⊢ ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
wlog hb' : b = 1
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
    [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
    (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
⊢ b⁻¹ * a ≤ b⁻¹ * c

Tactic:
gcongr
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
    [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
    (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
⊢ b⁻¹ * a ≠ 0

Tactic:
simp [ha, hb]
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
    [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
    (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
inr :
  ∀ (x : K)
    (e :
      b⁻¹ * a + HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.spanSingleton R⁰ x) 1 =
        b⁻¹ * c),
    ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
⊢ ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
obtain ⟨x, e⟩ := this (a := b⁻¹ * a) (b := 1) (c := b⁻¹ * c) (by gcongr) (by simp [ha, hb])
      one_ne_zero rfl

Premises used: one_ne_zero, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
    [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
    (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
x : K
e : b⁻¹ * a + HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.spanSingleton R⁰ x) 1 = b⁻¹ * c
h : a + FractionalIdeal.spanSingleton R⁰ x * b = c
⊢ ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
use x
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_5 : Field K] [inst_6 : Algebra R K]
    [inst_7 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0)
    (hb : b ≠ 0) (hb' : b = 1), ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
x : K
e : b⁻¹ * a + HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.spanSingleton R⁰ x) 1 = b⁻¹ * c
⊢ a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
simpa [hb, ← mul_assoc, mul_add, mul_comm b (.spanSingleton _ _)] using congr(b * $e)

Premises used: FractionalIdeal.spanSingleton, mul_assoc, mul_comm, mul_add
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a b c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
hb' : b = 1
subst :
  ∀ (hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0),
    ∃ (x : K), a + HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.spanSingleton R⁰ x) 1 = c
⊢ ∃ (x : K), a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
subst hb'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
rw :
  LE.le.{u_2} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑(Ideal.span {(↑c.den : R)} * a.num) : FractionalIdeal R⁰ K)
    (↑(c.num * Ideal.span {(↑a.den : R)}) : FractionalIdeal R⁰ K)
⊢ Ideal.span {(↑c.den : R)} * a.num ≤ c.num * Ideal.span {(↑a.den : R)}

Tactic:
rw [← FractionalIdeal.coeIdeal_le_coeIdeal K]

Premises used: FractionalIdeal.coeIdeal_le_coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
simp :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        a) ≤
    HMul.hMul (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        c)
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ LE.le.{u_2} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑(Ideal.span {(↑c.den : R)} * a.num) : FractionalIdeal R⁰ K)
    (↑(c.num * Ideal.span {(↑a.den : R)}) : FractionalIdeal R⁰ K)

Tactic:
simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton, ←
      FractionalIdeal.den_mul_self_eq_num']

Premises used: FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_mul, FractionalIdeal.den_mul_self_eq_num'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R_1 : Type u_1
inst : CommRing R_1
K_1 : Type u_2
inst_1 : Field K_1
inst_2 : Algebra R_1 K_1
inst_3 : IsFractionRing R_1 K_1
R : Type u_1
inst_4 : CommRing R
K : Type u_2
inst_5 : Field K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : IsDedekindDomain R
a c : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 0
ring_nf :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      a ≤
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      c
⊢ HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        a) ≤
    HMul.hMul (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑c.den : R)) :
          FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        c)
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (↑a.den : R)) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
ring_nf