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
I J : FractionalIdeal M K
y : K
hy : y ∈ (↑I : Set K) ∪ (↑J : Set K)
a : y ∈ I + J
⊢ Membership.mem (α := L) (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I + J) : Set K))) : Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)

Tactic:
suffices y ∈ I + J from SetLike.mem_coe.mpr <| Submodule.subset_span ⟨y, by simp [this]⟩
-- 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)
⊢ y ∈ I + J

Tactic:
hy.elim (fun h ↦ (mem_add I J y).mpr ⟨y, h, 0, zero_mem J, add_zero y⟩)
      (fun h ↦ (mem_add I J y).mpr ⟨0, zero_mem I, y, h, zero_add y⟩)

Premises used: Iff.mpr, FractionalIdeal.mem_add, zero_add, FractionalIdeal.zero_mem, And.intro, Exists.intro, add_zero, Or.elim, OfNat.ofNat
-- 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)
⊢ y ∈ I + J

Tactic:
exact hy.elim (fun h ↦ (mem_add I J y).mpr ⟨y, h, 0, zero_mem J, add_zero y⟩)
      (fun h ↦ (mem_add I J y).mpr ⟨0, zero_mem I, y, h, zero_add y⟩)

Premises used: Iff.mpr, FractionalIdeal.mem_add, zero_add, FractionalIdeal.zero_mem, And.intro, Exists.intro, add_zero, Or.elim, OfNat.ofNat
-- 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))
      (HMul.hMul (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)))
⊢ extended L hf (I * J) = HMul.hMul (α := 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 (α := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K)))
    (span B
      (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
        ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑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))
      (HMul.hMul (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)))

Tactic:
simp only [coe_extended_eq_span, coe_mul, span_mul_span]

Premises used: Submodule.span_mul_span, FractionalIdeal.coe_mul, 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
⊢ Eq (α := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K)))
    (span B
      (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
        ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))))

Tactic:
Submodule.span_eq_span (fun _ h ↦ ?_) (fun _ h ↦ ?_)

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
a :
  ∀ (x : L) (h : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K)) x),
    x ∈
      (↑(span B
            (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
              ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
        Set L)
a₁ :
  ∀ (x : L)
    (h :
      x ∈
        HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
          ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))),
    x ∈ (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K))) : Set L)
⊢ Eq (α := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K)))
    (span B
      (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
        ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))))

Tactic:
refine Submodule.span_eq_span (fun _ h ↦ ?_) (fun _ h ↦ ?_)

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
x : L
h : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K)) x
a :
  ∀ (x : K) (hx : x ∈ (↑(I * J) : Set K)),
    Membership.mem (α := L)
      (↑(span B
            (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
              ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
        Set L)
      ((IsLocalization.map L f hf : (a : K) → L) x : L)
⊢ x ∈
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)

Tactic:
rcases h with ⟨x, hx, rfl⟩

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
I J : FractionalIdeal M K
x : K
hx : x ∈ (↑(I * J) : Set K)
⊢ x ∈ (↑I : Submodule A K) * (↑J : Submodule A K)

Tactic:
replace hx : x ∈ (I : Submodule A K) * (J : Submodule A K) := coe_mul I J ▸ hx
-- 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
x : K
hx : x ∈ (↑I : Submodule A K) * (↑J : Submodule A K)
⊢ Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x

Tactic:
rw [Submodule.mul_eq_span_mul_set] at hx

Premises used: Submodule.mul_eq_span_mul_set
-- 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) 0 : 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
y : K
hy : y ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)
a :
  ∀ (i : K) (hi : i ∈ (↑(↑I : Submodule A K) : Set K)) (j : K) (hj : j ∈ (↑(↑J : Submodule A K) : Set K))
    (hy : i * j ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)),
    Membership.mem (α := L)
      (↑(span B
            (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
              ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
        Set L)
      ((IsLocalization.map L f hf : (a : K) → L) (i * j) : L)
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)

Tactic:
rcases Set.mem_mul.mp hy with ⟨i, hi, j, hj, rfl⟩

Premises used: Iff.mp, rfl, Set.mem_mul
-- 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
i : K
hi : i ∈ (↑(↑I : Submodule A K) : Set K)
j : K
hj : j ∈ (↑(↑J : Submodule A K) : Set K)
hy : i * j ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
i : K
hi : i ∈ (↑(↑I : Submodule A K) : Set K)
j : K
hj : j ∈ (↑(↑J : Submodule A K) : Set K)
hy : i * j ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
i : K
hi : i ∈ (↑(↑I : Submodule A K) : Set K)
j : K
hj : j ∈ (↑(↑J : Submodule A K) : Set K)
hy : i * j ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)
⊢ HMul.hMul (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L) =
    (IsLocalization.map L f hf : (a : K) → L) (i * j)

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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
i : K
hi : i ∈ (↑(↑I : Submodule A K) : Set K)
j : K
hj : j ∈ (↑(↑J : Submodule A K) : Set K)
hy : i * j ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (i * j) : L)

Tactic:
exact subset_span <| Set.mem_mul.mpr
        ⟨map_f i, ⟨i, hi, by simp⟩, map_f j, ⟨j, hj, by simp⟩, by simp⟩

Premises used: Submodule.subset_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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
y z : K
h : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y
h_1 : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) z
hy :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
hz :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) z : L)
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (y + z) : L)

Tactic:
map_add map_f y z ▸ Submodule.add_mem _ hy hz

Premises used: IsLocalization.map, Set.Mem, Eq.rec, map_add, Eq.symm, Submodule.add_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
I J : FractionalIdeal M K
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
y z : K
h : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y
h_1 : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) z
hy :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
hz :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) z : L)
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (y + z) : L)

Tactic:
exact map_add map_f y z ▸ Submodule.add_mem _ hy hz
-- 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
a : A
y : K
h : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y
hy :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
a₁ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
      ((IsLocalization.map L f hf : (a : K) → L) y : L) ∈
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
⊢ Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (a • y) : L)

Tactic:
rw [Algebra.smul_def, map_mul, map_eq, ← Algebra.smul_def]

Premises used: IsLocalization.map_eq, map_mul, Algebra.smul_def
-- 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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
a : A
y : K
h : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y
hy :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
      ((IsLocalization.map L f hf : (a : K) → L) y : L) ∈
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)

Tactic:
smul_mem _ (f a) hy

Premises used: Set.Mem, DFunLike.coe, 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
I J : FractionalIdeal M K
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
a : A
y : K
h : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y
hy :
  Membership.mem (α := L)
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
      ((IsLocalization.map L f hf : (a : K) → L) y : L) ∈
    (↑(span B
          (HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
            ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K)))) :
      Set L)

Tactic:
exact smul_mem _ (f a) hy

Premises used: DFunLike.coe, 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
I J : FractionalIdeal M K
x : L
h :
  x ∈
    HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
      ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))
a :
  ∀ (i : K) (hi : i ∈ (↑I : Set K)) (j : K) (hj : j ∈ (↑J : Set K))
    (h :
      HMul.hMul (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
          ((IsLocalization.map L f hf : (a : K) → L) j : L) ∈
        HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
          ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))),
    HMul.hMul (α := 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 * J) : Set K))) : Set L)
⊢ x ∈ (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K))) : Set L)

Tactic:
rcases Set.mem_mul.mp h with ⟨y, ⟨i, hi, rfl⟩, z, ⟨j, hj, rfl⟩, rfl⟩

Premises used: Iff.mp, rfl, Set.mem_mul