awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
refine_1 :
  ∀ (x : L),
    Membership.mem (γ := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 1) x →
      Membership.mem (γ := Submodule B L)
        ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x
refine_2 :
  ∀ (x : L)
    (hx :
      Membership.mem (γ := Submodule B L)
        ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x)
    (x : L) (h : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑1 : Set K)) x),
    Membership.mem (γ := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 1) x
⊢ Eq (α := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1) 1

Tactic:
refine coeToSubmodule_injective <| Submodule.ext fun x ↦ ⟨fun hx ↦ span_induction
    ?_ (zero_mem _) (fun y z _ _ hy hz ↦ add_mem hy hz) (fun b y _ hy ↦ smul_mem _ b hy) hx, ?_⟩

Premises used: Submodule.span_induction, Iff.intro, FractionalIdeal.coeToSubmodule_injective, Submodule.ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
b : B
left : b ∈ (↑⊤ : Set B)
refine_1 :
  Membership.mem (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1))
    (HSMul.hSMul (β := L) b 1)
⊢ Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1))
    ((Algebra.linearMap B L : (a : B) → L) b : L)

Tactic:
rw [Algebra.linearMap_apply, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.linearMap_apply, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
b : B
left : b ∈ (↑⊤ : Set B)
⊢ 1 ∈ (↑1 : Set K) ∧ Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) 1 : L) (1 : L)

Tactic:
simpa using one_mem_one

Premises used: FractionalIdeal.one_mem_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
b : B
left : b ∈ (↑⊤ : Set B)
⊢ Membership.mem (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1))
    (HSMul.hSMul (β := L) b 1)

Tactic:
exact smul_mem _ _ <| subset_span ⟨1, by simpa using one_mem_one⟩

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x : L
hx :
  Membership.mem (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x
a : A
ha : a ∈ (↑⊤ : Set A)
rw :
  Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((IsLocalization.map L f hf : (a : K) → L) ((Algebra.linearMap A K : (a : A) → K) a : K) : L)
rw₁ :
  Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((IsLocalization.map L f hf : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
⊢ Eq.{u_4 + 1} (α := L) ((Algebra.linearMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((IsLocalization.map L f hf : (a : K) → L) ((Algebra.linearMap A K : (a : A) → K) a : K) : L)

Tactic:
rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]

Premises used: Algebra.linearMap_apply, IsLocalization.map_eq
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x : L
hx :
  Membership.mem (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x
a : A
ha : a ∈ (↑⊤ : Set A)
⊢ Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 1)
    ((IsLocalization.map L f hf : (a : K) → L) ((Algebra.linearMap A K : (a : A) → K) a : K) : L)

Tactic:
exact ⟨f a, ha, by rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : I ≤ 1
obtain :
  ∀ (J : Ideal A) (hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1),
    LE.le (α := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf (↑J : FractionalIdeal M K)) 1
⊢ LE.le (α := FractionalIdeal N L) (extended L hf I) 1

Tactic:
obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp hI

Premises used: FractionalIdeal.le_one_iff_exists_coeIdeal, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
x : L
hx :
  Membership.mem (γ := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf (↑J : FractionalIdeal M K)) x
⊢ ∃ (t : Finset K),
    (↑t : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K) ∧
      ∃ (c : ↥t → B), ∑ i : ↥t, HSMul.hSMul (β := L) (c i) ((IsLocalization.map L f hf : (a : K) → L) (↑i : K) : L) = x

Tactic:
simp only [mem_extended_iff, mem_span_image_iff_exists_fun] at hx

Premises used: Submodule.mem_span_image_iff_exists_fun, FractionalIdeal.mem_extended_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
x : L
hx :
  ∃ (t : Finset K),
    (↑t : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K) ∧
      ∃ (c : ↥t → B), ∑ i : ↥t, HSMul.hSMul (β := L) (c i) ((IsLocalization.map L f hf : (a : K) → L) (↑i : K) : L) = x
obtain :
  ∀ (s : Finset K) (hs : (↑s : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K)) (c : ↥s → B),
    Membership.mem (γ := FractionalIdeal N L) 1
      (∑ i : ↥s, HSMul.hSMul (β := L) (c i) ((IsLocalization.map L f hf : (a : K) → L) (↑i : K) : L))
⊢ Membership.mem (γ := FractionalIdeal N L) 1 x

Tactic:
obtain ⟨s, hs, c, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
s : Finset K
hs : (↑s : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K)
c : ↥s → B
⊢ Membership.mem (γ := FractionalIdeal N L) 1
    (∑ i : ↥s, HSMul.hSMul (β := L) (c i) ((IsLocalization.map L f hf : (a : K) → L) (↑i : K) : L))

Tactic:
Submodule.sum_smul_mem _ _ fun ⟨x, hx⟩ h ↦ ?_

Premises used: IsLocalization.map, Submodule.sum_smul_mem, _private.0.FractionalIdeal.extended_le_one_of_le_one.match_1, Set.Mem, Membership.mem, FractionalIdeal.coeToSubmodule, OfNat.ofNat, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
s : Finset K
hs : (↑s : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K)
c : ↥s → B
refine :
  ∀ (x : ↥s) (x : K) (hx : x ∈ s)
    (h : Membership.mem (γ := Finset ↥s) Finset.univ (Subtype.mk (p := fun (x : K) ↦ x ∈ s) x hx)),
    Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) (↑1 : Submodule B L)
      ((IsLocalization.map L f hf : (a : K) → L) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ s) x hx) : K) : L)
⊢ Membership.mem (γ := FractionalIdeal N L) 1
    (∑ i : ↥s, HSMul.hSMul (β := L) (c i) ((IsLocalization.map L f hf : (a : K) → L) (↑i : K) : L))

Tactic:
refine Submodule.sum_smul_mem _ _ fun ⟨x, hx⟩ h ↦ ?_

Premises used: Submodule.sum_smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
s : Finset K
hs : (↑s : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K)
c : ↥s → B
x_1 : ↥s
x : K
hx : x ∈ s
h : Membership.mem (γ := Finset ↥s) Finset.univ (Subtype.mk (p := fun (x : K) ↦ x ∈ s) x hx)
obtain :
  ∀ (a : A) (ha : a ∈ (↑⊤ : Set A)) (hx : Membership.mem (α := K) s ((Algebra.linearMap A K : (a : A) → K) a : K))
    (h :
      Membership.mem.{u_3, u_3} (α := ↥s) (γ := Finset ↥s) Finset.univ
        (Subtype.mk (p := fun (x : K) ↦ x ∈ s) ((Algebra.linearMap A K : (a : A) → K) a) hx : ↥s)),
    Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) (↑1 : Submodule B L)
      ((IsLocalization.map L f hf : (a : K) → L)
          ((↑(Subtype.mk (p := fun (x : K) ↦ x ∈ s) ((Algebra.linearMap A K : (a : A) → K) a) hx) : K) : K) :
        L)
⊢ Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) (↑1 : Submodule B L)
    ((IsLocalization.map L f hf : (a : K) → L) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ s) x hx) : K) : L)

Tactic:
obtain ⟨a, ha, rfl⟩ := hI (hs hx)

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
s : Finset K
hs : (↑s : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K)
c : ↥s → B
x : ↥s
a : A
ha : a ∈ (↑⊤ : Set A)
hx : Membership.mem (α := K) s ((Algebra.linearMap A K : (a : A) → K) a : K)
h :
  Membership.mem.{u_3, u_3} (α := ↥s) (γ := Finset ↥s) Finset.univ
    (Subtype.mk (p := fun (x : K) ↦ x ∈ s) ((Algebra.linearMap A K : (a : A) → K) a) hx : ↥s)
⊢ Membership.mem (α := B) (↑⊤ : Set B) ((f : (a : A) → B) a : B) ∧
    Eq.{u_4 + 1} (α := L) ((Algebra.linearMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
      ((IsLocalization.map L f hf : (a : K) → L)
          ((↑(Subtype.mk (p := fun (x : K) ↦ x ∈ s) ((Algebra.linearMap A K : (a : A) → K) a) hx) : K) : K) :
        L)

Tactic:
simp [map_eq]

Premises used: IsLocalization.map_eq
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : LE.le.{u_3} (α := FractionalIdeal M K) (↑J : FractionalIdeal M K) 1
s : Finset K
hs : (↑s : Set K) ⊆ (↑(↑J : FractionalIdeal M K) : Set K)
c : ↥s → B
x : ↥s
a : A
ha : a ∈ (↑⊤ : Set A)
hx : Membership.mem (α := K) s ((Algebra.linearMap A K : (a : A) → K) a : K)
h :
  Membership.mem.{u_3, u_3} (α := ↥s) (γ := Finset ↥s) Finset.univ
    (Subtype.mk (p := fun (x : K) ↦ x ∈ s) ((Algebra.linearMap A K : (a : A) → K) a) hx : ↥s)
⊢ Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) (↑1 : Submodule B L)
    ((IsLocalization.map L f hf : (a : K) → L)
        ((↑(Subtype.mk (p := fun (x : K) ↦ x ∈ s) ((Algebra.linearMap A K : (a : A) → K) a) hx) : K) : K) :
      L)

Tactic:
exact ⟨f a, by simp [map_eq]⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ≤ I
rw : ∀ (hI : 1 ∈ I), Membership.mem (γ := FractionalIdeal N L) (extended L hf I) 1
⊢ LE.le (α := FractionalIdeal N L) 1 (extended L hf I)

Tactic:
rw [one_le] at hI ⊢

Premises used: FractionalIdeal.one_le
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ∈ I
rw rw₁ : Eq.{u_4 + 1} (α := L) 1 1
⊢ Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) 1 : L) (1 : L)

Tactic:
rw [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : 1 ∈ I
⊢ Membership.mem (γ := FractionalIdeal N L) (extended L hf I) 1

Tactic:
exact (mem_extended_iff _ _ _ _).mpr <| subset_span ⟨1, hI, by rw [map_one]⟩

Premises used: Iff.mpr, FractionalIdeal.mem_extended_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
a :
  Eq.{u_4 + 1} (α := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended L hf (I + J)))
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L))
      (HAdd.hAdd (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)))
⊢ extended L hf (I + J) = HAdd.hAdd (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)

Tactic:
apply coeToSubmodule_injective

Premises used: FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
a :
  Eq.{u_4 + 1} (α := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I + J) : Set K)))
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K))))
⊢ Eq.{u_4 + 1} (α := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended L hf (I + J)))
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L))
      (HAdd.hAdd (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)))

Tactic:
simp only [coe_extended_eq_span, coe_add, Submodule.add_eq_sup, ← span_union, ← Set.image_union]

Premises used: FractionalIdeal.coe_add, Submodule.span_union, Submodule.add_eq_sup, Set.image_union, FractionalIdeal.coe_extended_eq_span
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
a :
  (⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I + J) : Set K) ⊆
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)))) : Set L)
a₁ :
  (⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)) ⊆
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I + J) : Set K))) : Set L)
⊢ Eq.{u_4 + 1} (α := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I + J) : Set K)))
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K))))

Tactic:
apply Submodule.span_eq_span

Premises used: Submodule.span_eq_span
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
y : K
hy : y ∈ (↑(I + J) : Set K)
a :
  ∀ (i : K) (hi : i ∈ I) (j : K) (hj : j ∈ J) (hy : i + j ∈ (↑(I + J) : Set K)),
    Membership.mem (α := L)
      (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)))) : Set L)
      ((IsLocalization.map L f hf : (a : K) → L) (i + j) : L)
⊢ Membership.mem (α := L)
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)))) : Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)

Tactic:
obtain ⟨i, hi, j, hj, rfl⟩ := (mem_add I J y).mp <| SetLike.mem_coe.mp hy

Premises used: FractionalIdeal.mem_add, SetLike.mem_coe, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ (↑(I + J) : Set K)
a :
  HAdd.hAdd (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L) ∈
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)))) : Set L)
⊢ Membership.mem (α := L)
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)))) : Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (i + j) : L)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ (↑(I + J) : Set K)
⊢ Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
    ((IsLocalization.map L f hf : (a : K) → L) i : L)

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ (↑(I + J) : Set K)
⊢ Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) j : L)
    ((IsLocalization.map L f hf : (a : K) → L) j : L)

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ (↑(I + J) : Set K)
⊢ HAdd.hAdd (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L) ∈
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' ((↑I : Set K) ∪ (↑J : Set K)))) : Set L)

Tactic:
exact add_mem (Submodule.subset_span ⟨i, Set.mem_union_left _ hi, by simp⟩)
      (Submodule.subset_span ⟨j, Set.mem_union_right _ hj, by simp⟩)
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
y : K
hy : y ∈ (↑I : Set K) ∪ (↑J : Set K)
this : y ∈ I + J
⊢ y ∈ (↑(I + J) : Set K) ∧
    Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) y : L)
      ((IsLocalization.map L f hf : (a : K) → L) y : L)

Tactic:
simp [this]