awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I⁻¹ ≤ J ↔ J⁻¹ ≤ I

Tactic:
simpa using le_inv_comm (A := A) (K := K) (inv_ne_zero hI) (inv_ne_zero hJ)

Premises used: FractionalIdeal.le_inv_comm, inv_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : J ≤ I⁻¹⁻¹ ↔ J ≤ I
rw₁ rw₂ : J ≤ I ↔ J ≤ I
⊢ I⁻¹ ≤ J⁻¹ ↔ J ≤ I

Tactic:
rw [le_inv_comm (inv_ne_zero hI) hJ, inv_inv]

Premises used: FractionalIdeal.le_inv_comm, inv_inv, inv_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
⊢ I ≠ 0

Tactic:
have hI0 : I ≠ 0 := spanFinset_ne_zero.mpr ⟨j, hjs, hjf⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
obtain :
  (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹ →
    ∀ (a : K) (hI : a ∈ I⁻¹) (hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I),
      ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)

Tactic:
obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this

Premises used: SetLike.lt_iff_le_and_exists, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : a ∈ I⁻¹
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
⊢ ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)

Tactic:
rw [mem_inv_iff hI0] at hI

Premises used: FractionalIdeal.mem_inv_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : a ∈ I⁻¹
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
hI₁ : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
⊢ a ∉ (↑J : FractionalIdeal A⁰ K) / I

Tactic:
rw [mem_inv_iff hI0] at hI

Premises used: FractionalIdeal.mem_inv_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)

Tactic:
⟨a, fun i hi => ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
refine_1 : ∀ (i : ι) (hi : i ∈ s), IsLocalization.IsInteger A (a * f i)
refine_2 : ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)

Tactic:
refine ⟨a, fun i hi => ?_, ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
i : ι
hi : i ∈ s
⊢ IsLocalization.IsInteger A (a * f i)

Tactic:
(mem_one_iff _).mp (hI (f i) (Submodule.subset_span (Set.mem_image_of_mem f hi)))

Premises used: IsLocalization.IsInteger, Set.Mem, setOf, FractionalIdeal.mem_one_iff, Set.mem_image_of_mem, Iff.mp, Submodule.subset_span, Set.range
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
i : ι
hi : i ∈ s
⊢ IsLocalization.IsInteger A (a * f i)

Tactic:
exact (mem_one_iff _).mp (hI (f i) (Submodule.subset_span (Set.mem_image_of_mem f hi)))

Premises used: FractionalIdeal.mem_one_iff, Set.mem_image_of_mem, Iff.mp, Submodule.subset_span
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
refine_2 :
  ∀
    (hpI :
      ∀ (i : ι) (_ : i ∈ s),
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)),
    a ∈ (↑J : FractionalIdeal A⁰ K) / I
⊢ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)

Tactic:
contrapose! hpI
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
⊢ a ∈ (↑J : FractionalIdeal A⁰ K) / I

Tactic:
(mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy

Premises used: Iff.mpr, Submodule.span_induction, FractionalIdeal.mem_div_iff_of_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
refine_2 :
  ∀ (y : K) (hy : y ∈ I) (x : K) (h : x ∈ f '' (↑s : Set ι)),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
refine_2₁ :
  ∀ (y : K) (hy : y ∈ I),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * 0)
refine_2₂ :
  ∀ (y : K) (hy : y ∈ I) (x y : K) (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x)
    (hy : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y) →
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))
refine_2₃ :
  ∀ (y : K) (hy : y ∈ I) (a_1 : A) (x : K)
    (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * a_1 • x)
⊢ a ∈ (↑J : FractionalIdeal A⁰ K) / I

Tactic:
refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy

Premises used: Iff.mpr, Submodule.span_induction, FractionalIdeal.mem_div_iff_of_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
i : ι
hi : i ∈ (↑s : Set ι)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)

Tactic:
hpI i hi
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
i : ι
hi : i ∈ (↑s : Set ι)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)

Tactic:
exact hpI i hi
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
refine_2 : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 0
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * 0)

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 0

Tactic:
Submodule.zero_mem _

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y_1 : K
hy : y_1 ∈ I
x y : K
refine_2 :
  Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x →
    ∀ (hy : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y),
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y) →
          Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))
⊢ ∀ (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x)
    (hy : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y) →
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))

Tactic:
_
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y_1 : K
hy : y_1 ∈ I
x y : K
hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
refine_2 :
  Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y →
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y) →
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))
⊢ ∀ (hy : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y) →
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))

Tactic:
_
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y_1 : K
hy_1 : y_1 ∈ I
x y : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hy_2 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
hy : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y)
refine_2 : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x + a * y)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y_1 : K
hy_1 : y_1 ∈ I
x y : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hy_2 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
hy : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x + a * y)

Tactic:
Submodule.add_mem _ hx hy

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y_1 : K
hy_1 : y_1 ∈ I
x y : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hy_2 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
hy : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x + a * y)

Tactic:
exact Submodule.add_mem _ hx hy

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
b : A
x : K
refine_2 :
  Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x →
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * b • x)
⊢ ∀ (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * b • x)

Tactic:
_