-- Mathlib/RingTheory/FractionalIdeal/Extended.lean
theorem extended_one : extended L hf (1 : FractionalIdeal M K) = 1

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
b : B
left✝ : b ∈ ↑⊤
⊢ 1 ∈ ↑1 ∧ (IsLocalization.map L f hf) 1 = 1

Tactic:
simp [one_mem_one]

Result:
no goals

Proof state:
case 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
x : L
⊢ x ∈ (fun I => ↑I) 1 → x ∈ (fun I => ↑I) (extended L hf 1)

Tactic:
rintro ⟨b, _, rfl⟩

Result:
case 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
b : B
left✝ : b ∈ ↑⊤
⊢ (Algebra.linearMap B L) b ∈ (fun I => ↑I) (extended L hf 1)

Proof state:
case 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
x : L
hx : x ∈ (fun I => ↑I) (extended L hf 1)
⊢ ∀ x ∈ ⇑(IsLocalization.map L f hf) '' ↑1, x ∈ (fun I => ↑I) 1

Tactic:
rintro _ ⟨_, ⟨a, ha, rfl⟩, rfl⟩

Result:
case refine_2.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
x : L
hx : x ∈ (fun I => ↑I) (extended L hf 1)
a : A
ha : a ∈ ↑⊤
⊢ (IsLocalization.map L f hf) ((Algebra.linearMap A K) a) ∈ (fun I => ↑I) 1

Proof state:
case 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
b : B
left✝ : b ∈ ↑⊤
⊢ b • 1 ∈ (fun I => ↑I) (extended L hf 1)

Tactic:
exact smul_mem _ _ <| subset_span ⟨1, by simp [one_mem_one]⟩

Result:
no goals

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
⊢ extended 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, ?_⟩

Result:
case 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
x : L
⊢ x ∈ (fun I => ↑I) 1 → x ∈ (fun I => ↑I) (extended L hf 1)

case 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
x : L
hx : x ∈ (fun I => ↑I) (extended L hf 1)
⊢ ∀ x ∈ ⇑(IsLocalization.map L f hf) '' ↑1, x ∈ (fun I => ↑I) 1

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
x : L
hx : x ∈ (fun I => ↑I) (extended L hf 1)
a : A
ha : a ∈ ↑⊤
⊢ (Algebra.linearMap B L) (f a) = (IsLocalization.map L f hf) ((Algebra.linearMap A K) a)

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

Result:
no goals

Proof state:
case 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
b : B
left✝ : b ∈ ↑⊤
⊢ (Algebra.linearMap B L) b ∈ (fun I => ↑I) (extended L hf 1)

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

Result:
case 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
b : B
left✝ : b ∈ ↑⊤
⊢ b • 1 ∈ (fun I => ↑I) (extended L hf 1)

Proof state:
case refine_2.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
x : L
hx : x ∈ (fun I => ↑I) (extended L hf 1)
a : A
ha : a ∈ ↑⊤
⊢ (IsLocalization.map L f hf) ((Algebra.linearMap A K) a) ∈ (fun I => ↑I) 1

Tactic:
exact ⟨f a, ha, by rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]⟩

Result:
no goals