-- Mathlib/RingTheory/FractionalIdeal/Extended.lean
theorem extended_mul : (I * J).extended L hf = (I.extended L hf) * (J.extended L hf)

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ ↑I
j : K
hj : j ∈ ↑J
h :
  (IsLocalization.map L f hf) i * (IsLocalization.map L f hf) j ∈
    ⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J
⊢ (IsLocalization.map L f hf) (i * j) = (IsLocalization.map L f hf) i * (IsLocalization.map L f hf) j

Tactic:
simp

Result:
no goals

Proof state:
case a.refine_1.intro.intro
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ ↑I * ↑J
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
rw [Submodule.mul_eq_span_mul_set] at hx

Result:
case a.refine_1.intro.intro
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Proof state:
case a.refine_1.intro.intro.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

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

Result:
case a.refine_1.intro.intro.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ f a • (IsLocalization.map L f hf) y ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Proof state:
case a.refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑(I * J)
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

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

Result:
case a.refine_1.intro.intro
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ ↑(I * J)
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Proof state:
case a
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ (fun I => ↑I) (extended L hf (I * J)) = (fun I => ↑I) (extended L hf I * extended L hf J)

Tactic:
simp only [coe_extended_eq_span, coe_mul, span_mul_span]

Result:
case a
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ span B (⇑(IsLocalization.map L f hf) '' ↑(I * J)) =
    span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J)

Proof state:
case a.refine_1.intro.intro.refine_1.intro.intro.intro.intro
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
i : K
hi : i ∈ ↑↑I
j : K
hj : j ∈ ↑↑J
hy : i * j ∈ ↑↑I * ↑↑J
⊢ (IsLocalization.map L f hf) (i * j) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

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

Result:
no goals

Proof state:
case a.refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I * J)))

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

Result:
case a.refine_2.intro.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ ↑I
j : K
hj : j ∈ ↑J
h :
  (IsLocalization.map L f hf) i * (IsLocalization.map L f hf) j ∈
    ⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J
⊢ (IsLocalization.map L f hf) i * (IsLocalization.map L f hf) j ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I * J)))

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
i : K
hi : i ∈ ↑↑I
j : K
hj : j ∈ ↑↑J
hy : i * j ∈ ↑↑I * ↑↑J
⊢ (IsLocalization.map L f hf) i = (IsLocalization.map L f hf) i

Tactic:
simp [hi]

Result:
no goals