awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ LE.le (α := FractionalIdeal N L) (extended L hf I) 1
have 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
Tactic: obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp hI
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (hypothesis)
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
⊢ Membership.mem (γ := FractionalIdeal N L) 1 x
have 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
Tactic: simp only [mem_extended_iff, mem_span_image_iff_exists_fun] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ Membership.mem (γ := FractionalIdeal N L) 1 x
have 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))
Tactic: obtain ⟨s, hs, c, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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))
have 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)
Tactic: refine Submodule.sum_smul_mem _ _ fun ⟨x, hx⟩ h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨a, ha, rfl⟩ := hI (hs hx)
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ LE.le (α := FractionalIdeal N L) 1 (extended L hf I)
have rw : ∀ (hI : 1 ∈ I), Membership.mem (γ := FractionalIdeal N L) (extended L hf I) 1
Tactic: rw [one_le] at hI ⊢
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) 1 : L) (1 : L)
have rw : Eq.{u_4 + 1} (α := L) 1 1
Tactic: rw [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ extended L hf (I + J) = HAdd.hAdd (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)
have 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)))
Tactic: apply coeToSubmodule_injective
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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.{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)))
have 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))))
Tactic: simp only [coe_extended_eq_span, coe_add, Submodule.add_eq_sup, ← span_union, ← Set.image_union]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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.{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))))
have 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)
Tactic: apply Submodule.span_eq_span
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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))))
have 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)
Tactic: apply Submodule.span_eq_span
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨i, hi, j, hj, rfl⟩ := (mem_add I J y).mp <| SetLike.mem_coe.mp hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have a : y ∈ I + J
Tactic: suffices y ∈ I + J from SetLike.mem_coe.mpr <| Submodule.subset_span ⟨y, by simp [this]⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ extended L hf (I * J) = HMul.hMul (α := FractionalIdeal N L) (extended L hf I) (extended L hf J)
have 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)))
Tactic: apply coeToSubmodule_injective
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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.{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)))
have 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))))
Tactic: simp only [coe_extended_eq_span, coe_mul, span_mul_span]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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))))
have 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)
Tactic: refine Submodule.span_eq_span (fun _ h ↦ ?_) (fun _ h ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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))))
have 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)
Tactic: refine Submodule.span_eq_span (fun _ h ↦ ?_) (fun _ h ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ 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)
have 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)
Tactic: rcases h with ⟨x, hx, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (hypothesis)
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)
⊢ 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)
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (hypothesis)
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 (α := 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)
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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) x : L)
have a : ∀ (y : K) (hy : y ∈ (↑(↑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) y : L)
Tactic: refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_)
      (fun a y _ hy ↦ ?_) hx