[GOAL]
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Injective R Q
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.mk Q
f : X✝ ⟶ Y✝
mn : CategoryTheory.Mono f
⊢ ∃ h, CategoryTheory.CategoryStruct.comp f h = g
[PROOFSTEP]
rcases Module.Injective.out _ _ f ((ModuleCat.mono_iff_injective f).mp mn) g with ⟨h, eq1⟩
[GOAL]
case intro
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Injective R Q
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.mk Q
f : X✝ ⟶ Y✝
mn : CategoryTheory.Mono f
h : ↑Y✝ →ₗ[R] ↑(ModuleCat.mk Q)
eq1 : ∀ (x : ↑X✝), ↑h (↑f x) = ↑g x
⊢ ∃ h, CategoryTheory.CategoryStruct.comp f h = g
[PROOFSTEP]
exact ⟨h, LinearMap.ext eq1⟩
[GOAL]
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
g : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), ↑h (↑f x) = ↑g x
[PROOFSTEP]
skip
[GOAL]
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
g : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), ↑h (↑f x) = ↑g x
[PROOFSTEP]
rcases@CategoryTheory.Injective.factors (ModuleCat R) _ ⟨Q⟩ _ ⟨X⟩ ⟨Y⟩ g f ((ModuleCat.mono_iff_injective _).mpr hf) with
  ⟨h, rfl⟩
[GOAL]
case intro
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
h : ModuleCat.mk Y ⟶ ModuleCat.mk Q
⊢ ∃ h_1, ∀ (x : X), ↑h_1 (↑f x) = ↑(CategoryTheory.CategoryStruct.comp f h) x
[PROOFSTEP]
exact ⟨h, fun x => rfl⟩
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq : ∀ ⦃x : { x // x ∈ a.domain }⦄ ⦃y : { x // x ∈ b.domain }⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y
⊢ a = b
[PROOFSTEP]
rcases a with ⟨a, a_le, e1⟩
[GOAL]
case mk
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain = b.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ b.domain }⦄,
    ↑x = ↑y → ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x = ↑b.toLinearPMap y
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b
[PROOFSTEP]
rcases b with ⟨b, b_le, e2⟩
[GOAL]
case mk.mk
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), ↑f m = ↑b { val := ↑i m, property := (_ : ↑i m ∈ b.domain) }
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain }⦄,
    ↑x = ↑y →
      ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x =
        ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap y
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = { toLinearPMap := b, le := b_le, is_extension := e2 }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toLinearPMap
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), ↑f m = ↑b { val := ↑i m, property := (_ : ↑i m ∈ b.domain) }
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain }⦄,
    ↑x = ↑y →
      ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x =
        ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap y
⊢ a = b
[PROOFSTEP]
exact LinearPMap.ext domain_eq to_fun_eq
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
r : a = b
x y : { x // x ∈ a.domain }
h : ↑x = ↑y
⊢ x = y
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
src✝ : N →ₗ.[R] Q := X1.toLinearPMap ⊓ X2.toLinearPMap
x : N
hx : x ∈ LinearMap.range i
⊢ x ∈ LinearPMap.eqLocus X1.toLinearPMap X2.toLinearPMap
[PROOFSTEP]
rcases hx with ⟨x, rfl⟩
[GOAL]
case intro
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
src✝ : N →ₗ.[R] Q := X1.toLinearPMap ⊓ X2.toLinearPMap
x : M
⊢ ↑i x ∈ LinearPMap.eqLocus X1.toLinearPMap X2.toLinearPMap
[PROOFSTEP]
refine' ⟨X1.le (Set.mem_range_self _), X2.le (Set.mem_range_self _), _⟩
[GOAL]
case intro
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
src✝ : N →ₗ.[R] Q := X1.toLinearPMap ⊓ X2.toLinearPMap
x : M
⊢ ↑X1.toLinearPMap { val := ↑i x, property := (_ : ↑i x ∈ X1.domain) } =
    ↑X2.toLinearPMap { val := ↑i x, property := (_ : ↑i x ∈ X2.domain) }
[PROOFSTEP]
rw [← X1.is_extension x, ← X2.is_extension x]
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
h : X.toLinearPMap = Y.toLinearPMap
⊢ X.domain = Y.domain
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
h : X.toLinearPMap = Y.toLinearPMap
x : { x // x ∈ X.domain }
y : { x // x ∈ Y.domain }
h' : ↑x = ↑y
⊢ ↑X.toLinearPMap x = ↑Y.toLinearPMap y
[PROOFSTEP]
have :
  {x y : N} →
    (h'' : x = y) →
      (hx : x ∈ X.toLinearPMap.domain) →
        (hy : y ∈ Y.toLinearPMap.domain) → X.toLinearPMap ⟨x, hx⟩ = Y.toLinearPMap ⟨y, hy⟩ :=
  by
  rw [h]
  intro _ _ h _ _
  congr
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
h : X.toLinearPMap = Y.toLinearPMap
x : { x // x ∈ X.domain }
y : { x // x ∈ Y.domain }
h' : ↑x = ↑y
⊢ ∀ {x y : N},
    x = y →
      ∀ (hx : x ∈ X.domain) (hy : y ∈ Y.domain),
        ↑X.toLinearPMap { val := x, property := hx } = ↑Y.toLinearPMap { val := y, property := hy }
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
h : X.toLinearPMap = Y.toLinearPMap
x : { x // x ∈ X.domain }
y : { x // x ∈ Y.domain }
h' : ↑x = ↑y
⊢ ∀ {x y : N},
    x = y →
      ∀ (hx : x ∈ Y.domain) (hy : y ∈ Y.domain),
        ↑Y.toLinearPMap { val := x, property := hx } = ↑Y.toLinearPMap { val := y, property := hy }
[PROOFSTEP]
intro _ _ h _ _
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
h✝ : X.toLinearPMap = Y.toLinearPMap
x : { x // x ∈ X.domain }
y : { x // x ∈ Y.domain }
h' : ↑x = ↑y
x✝ y✝ : N
h : x✝ = y✝
hx✝ : x✝ ∈ Y.domain
hy✝ : y✝ ∈ Y.domain
⊢ ↑Y.toLinearPMap { val := x✝, property := hx✝ } = ↑Y.toLinearPMap { val := y✝, property := hy✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
h : X.toLinearPMap = Y.toLinearPMap
x : { x // x ∈ X.domain }
y : { x // x ∈ Y.domain }
h' : ↑x = ↑y
this :
  ∀ {x y : N},
    x = y →
      ∀ (hx : x ∈ X.domain) (hy : y ∈ Y.domain),
        ↑X.toLinearPMap { val := x, property := hx } = ↑Y.toLinearPMap { val := y, property := hy }
⊢ ↑X.toLinearPMap x = ↑Y.toLinearPMap y
[PROOFSTEP]
apply this h' _ _
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
x : { x // x ∈ (X ⊓ Y).domain }
y : { x // x ∈ (X.toLinearPMap ⊓ Y.toLinearPMap).domain }
h : ↑x = ↑y
⊢ ↑(X ⊓ Y).toLinearPMap x = ↑(X.toLinearPMap ⊓ Y.toLinearPMap) y
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X Y : ExtensionOf i f
x : { x // x ∈ (X ⊓ Y).domain }
y : { x // x ∈ (X.toLinearPMap ⊓ Y.toLinearPMap).domain }
h : ↑x = ↑y
⊢ x = y
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
⊢ IsChain (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c)
[PROOFSTEP]
rintro _ ⟨a, a_mem, rfl⟩ _ ⟨b, b_mem, rfl⟩ neq
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
a : ExtensionOf i f
a_mem : a ∈ c
b : ExtensionOf i f
b_mem : b ∈ c
neq : (fun x => x.toLinearPMap) a ≠ (fun x => x.toLinearPMap) b
⊢ (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) a) ((fun x => x.toLinearPMap) b) ∨
    (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) b) ((fun x => x.toLinearPMap) a)
[PROOFSTEP]
exact hchain a_mem b_mem (ne_of_apply_ne _ neq)
[GOAL]
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
hnonempty : Set.Nonempty c
src✝ : N →ₗ.[R] Q :=
  LinearPMap.sSup ((fun x => x.toLinearPMap) '' c)
    (_ : DirectedOn (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c))
m : M
⊢ ↑f m =
    ↑{ domain := src✝.domain, toFun := src✝.toFun }
      { val := ↑i m, property := (_ : ↑i m ∈ { domain := src✝.domain, toFun := src✝.toFun }.domain) }
[PROOFSTEP]
refine' Eq.trans (hnonempty.some.is_extension m) _
[GOAL]
case refine'_1
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
⊢ ∀ {c : Set (ExtensionOf i f)} (hchain : IsChain (fun x x_1 => x ≤ x_1) c),
    Set.Nonempty c →
      let src :=
        LinearPMap.sSup ((fun x => x.toLinearPMap) '' c)
          (_ : DirectedOn (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c));
      DirectedOn (fun x x_1 => x ≤ x_1) (toLinearPMap '' c)
[PROOFSTEP]
intros c hchain _
[GOAL]
case refine'_1
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
hnonempty✝ : Set.Nonempty c
⊢ let src :=
    LinearPMap.sSup ((fun x => x.toLinearPMap) '' c)
      (_ : DirectedOn (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c));
  DirectedOn (fun x x_1 => x ≤ x_1) (toLinearPMap '' c)
[PROOFSTEP]
exact (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
[GOAL]
case refine'_2
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
hnonempty : Set.Nonempty c
src✝ : N →ₗ.[R] Q :=
  LinearPMap.sSup ((fun x => x.toLinearPMap) '' c)
    (_ : DirectedOn (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c))
m : M
⊢ ↑(Set.Nonempty.some hnonempty).toLinearPMap
      { val := ↑i m, property := (_ : ↑i m ∈ (Set.Nonempty.some hnonempty).toLinearPMap.domain) } =
    ↑{ domain := src✝.domain, toFun := src✝.toFun }
      { val := ↑i m, property := (_ : ↑i m ∈ { domain := src✝.domain, toFun := src✝.toFun }.domain) }
[PROOFSTEP]
symm
[GOAL]
case refine'_2
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
hnonempty : Set.Nonempty c
src✝ : N →ₗ.[R] Q :=
  LinearPMap.sSup ((fun x => x.toLinearPMap) '' c)
    (_ : DirectedOn (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c))
m : M
⊢ ↑{ domain := src✝.domain, toFun := src✝.toFun }
      { val := ↑i m, property := (_ : ↑i m ∈ { domain := src✝.domain, toFun := src✝.toFun }.domain) } =
    ↑(Set.Nonempty.some hnonempty).toLinearPMap
      { val := ↑i m, property := (_ : ↑i m ∈ (Set.Nonempty.some hnonempty).toLinearPMap.domain) }
[PROOFSTEP]
generalize_proofs _ h1
[GOAL]
case refine'_2
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
hnonempty : Set.Nonempty c
src✝ : N →ₗ.[R] Q :=
  LinearPMap.sSup ((fun x => x.toLinearPMap) '' c)
    (_ : DirectedOn (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c))
m : M
h✝ : ↑i m ∈ { domain := src✝.domain, toFun := src✝.toFun }.domain
h1 : ↑i m ∈ (Set.Nonempty.some hnonempty).toLinearPMap.domain
⊢ ↑{ domain := src✝.domain, toFun := src✝.toFun } { val := ↑i m, property := h✝ } =
    ↑(Set.Nonempty.some hnonempty).toLinearPMap { val := ↑i m, property := h1 }
[PROOFSTEP]
exact
  LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
    ((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
x y : { x // x ∈ LinearMap.range i }
⊢ (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
      (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y
[PROOFSTEP]
have eq1 : _ + _ = (x + y).1 := congr_arg₂ (· + ·) x.2.choose_spec y.2.choose_spec
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
x y : { x // x ∈ LinearMap.range i }
eq1 : ↑i (Exists.choose (_ : ↑x ∈ LinearMap.range i)) + ↑i (Exists.choose (_ : ↑y ∈ LinearMap.range i)) = ↑(x + y)
⊢ (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
      (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y
[PROOFSTEP]
rw [← map_add, ← (x + y).2.choose_spec] at eq1 
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
x y : { x // x ∈ LinearMap.range i }
eq1 :
  ↑i (Exists.choose (_ : ↑x ∈ LinearMap.range i) + Exists.choose (_ : ↑y ∈ LinearMap.range i)) =
    ↑i (Exists.choose (_ : ↑(x + y) ∈ LinearMap.range i))
⊢ (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
      (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
x y : { x // x ∈ LinearMap.range i }
eq1 :
  ↑i (Exists.choose (_ : ↑x ∈ LinearMap.range i) + Exists.choose (_ : ↑y ∈ LinearMap.range i)) =
    ↑i (Exists.choose (_ : ↑(x + y) ∈ LinearMap.range i))
⊢ ↑f (Exists.choose (_ : ↑(x + y) ∈ LinearMap.range i)) =
    ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)) + ↑f (Exists.choose (_ : ↑y ∈ LinearMap.range i))
[PROOFSTEP]
rw [← Fact.out (p := Function.Injective i) eq1, map_add]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
r : R
x : { x // x ∈ LinearMap.range i }
⊢ AddHom.toFun
      { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
        map_add' :=
          (_ :
            ∀ (x y : { x // x ∈ LinearMap.range i }),
              (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ LinearMap.range i }),
                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
        x
[PROOFSTEP]
have eq1 : r • _ = (r • x).1 := congr_arg ((· • ·) r) x.2.choose_spec
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
r : R
x : { x // x ∈ LinearMap.range i }
eq1 : r • ↑i (Exists.choose (_ : ↑x ∈ LinearMap.range i)) = ↑(r • x)
⊢ AddHom.toFun
      { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
        map_add' :=
          (_ :
            ∀ (x y : { x // x ∈ LinearMap.range i }),
              (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ LinearMap.range i }),
                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
        x
[PROOFSTEP]
rw [← LinearMap.map_smul, ← (r • x).2.choose_spec] at eq1 
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
r : R
x : { x // x ∈ LinearMap.range i }
eq1 : ↑i (r • Exists.choose (_ : ↑x ∈ LinearMap.range i)) = ↑i (Exists.choose (_ : ↑(r • x) ∈ LinearMap.range i))
⊢ AddHom.toFun
      { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
        map_add' :=
          (_ :
            ∀ (x y : { x // x ∈ LinearMap.range i }),
              (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ LinearMap.range i }),
                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
        x
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
r : R
x : { x // x ∈ LinearMap.range i }
eq1 : ↑i (r • Exists.choose (_ : ↑x ∈ LinearMap.range i)) = ↑i (Exists.choose (_ : ↑(r • x) ∈ LinearMap.range i))
⊢ ↑f (Exists.choose (_ : ↑(r • x) ∈ LinearMap.range i)) = r • ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))
[PROOFSTEP]
rw [← Fact.out (p := Function.Injective i) eq1, LinearMap.map_smul]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
m : M
⊢ ↑f m =
    ↑{ domain := LinearMap.range i,
          toFun :=
            {
              toAddHom :=
                { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
                  map_add' :=
                    (_ :
                      ∀ (x y : { x // x ∈ LinearMap.range i }),
                        (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                          (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                            (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : { x // x ∈ LinearMap.range i }),
                    AddHom.toFun
                        { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
                          map_add' :=
                            (_ :
                              ∀ (x y : { x // x ∈ LinearMap.range i }),
                                (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                                    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
                        (r • x) =
                      ↑(RingHom.id R) r •
                        AddHom.toFun
                          { toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
                            map_add' :=
                              (_ :
                                ∀ (x y : { x // x ∈ LinearMap.range i }),
                                  (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) (x + y) =
                                    (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) x +
                                      (fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i))) y) }
                          x) } }
      { val := ↑i m, property := (_ : ↑i m ∈ LinearMap.range i) }
[PROOFSTEP]
simp only [LinearPMap.mk_apply, LinearMap.coe_mk]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
m : M
⊢ ↑f m =
    ↑{ toFun := fun x => ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ LinearMap.range i }),
                ↑f (Exists.choose (_ : ↑(x + y) ∈ LinearMap.range i)) =
                  ↑f (Exists.choose (_ : ↑x ∈ LinearMap.range i)) + ↑f (Exists.choose (_ : ↑y ∈ LinearMap.range i))) }
      { val := ↑i m, property := (_ : ↑i m ∈ LinearMap.range i) }
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
m : M
⊢ ↑f m = ↑f (Exists.choose (_ : ↑i m ∈ LinearMap.range i))
[PROOFSTEP]
apply congrArg
[GOAL]
case h
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
m : M
⊢ m = Exists.choose (_ : ↑i m ∈ LinearMap.range i)
[PROOFSTEP]
exact Fact.out (p := Function.Injective i) (⟨i m, ⟨_, rfl⟩⟩ : LinearMap.range i).2.choose_spec.symm
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ ∃ a b, ↑x = ↑a + b • y
[PROOFSTEP]
have mem1 : x.1 ∈ (_ : Set _) := x.2
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
mem1 : ↑x ∈ ↑(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y
[PROOFSTEP]
rw [Submodule.coe_sup] at mem1 
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
mem1 : ↑x ∈ ↑(extensionOfMax i f).toLinearPMap.domain + ↑(Submodule.span R {y})
⊢ ∃ a b, ↑x = ↑a + b • y
[PROOFSTEP]
rcases mem1 with ⟨a, b, a_mem, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
a b : N
a_mem : a ∈ ↑(extensionOfMax i f).toLinearPMap.domain
b_mem : b ∈ Submodule.span R {y}
eq1 : (fun x x_1 => x + x_1) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y
[PROOFSTEP]
rw [Submodule.mem_span_singleton] at b_mem 
[GOAL]
case intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
a b : N
a_mem : a ∈ ↑(extensionOfMax i f).toLinearPMap.domain
b_mem : ∃ a, a • y = b
eq1 : (fun x x_1 => x + x_1) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y
[PROOFSTEP]
rcases b_mem with ⟨z, eq2⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
a b : N
a_mem : a ∈ ↑(extensionOfMax i f).toLinearPMap.domain
eq1 : (fun x x_1 => x + x_1) a b = ↑x
z : R
eq2 : z • y = b
⊢ ∃ a b, ↑x = ↑a + b • y
[PROOFSTEP]
exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
a b : N
a_mem : a ∈ ↑(extensionOfMax i f).toLinearPMap.domain
eq1 : (fun x x_1 => x + x_1) a b = ↑x
z : R
eq2 : z • y = b
⊢ ↑x = ↑{ val := a, property := a_mem } + z • y
[PROOFSTEP]
rw [← eq1, ← eq2]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
z1 z2 : { x // x ∈ ideal i f y }
⊢ (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) }) (z1 + z2) =
    (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) }) z1 +
      (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) }) z2
[PROOFSTEP]
simp_rw [← (extensionOfMax i f).toLinearPMap.map_add]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
z1 z2 : { x // x ∈ ideal i f y }
⊢ ↑(extensionOfMax i f).toLinearPMap { val := ↑(z1 + z2) • y, property := (_ : ↑(z1 + z2) ∈ ideal i f y) } =
    ↑(extensionOfMax i f).toLinearPMap
      ({ val := ↑z1 • y, property := (_ : ↑z1 ∈ ideal i f y) } +
        { val := ↑z2 • y, property := (_ : ↑z2 ∈ ideal i f y) })
[PROOFSTEP]
congr
[GOAL]
case e_a.e_val
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
z1 z2 : { x // x ∈ ideal i f y }
⊢ ↑(z1 + z2) • y =
    ↑{ val := ↑z1 • y, property := (_ : ↑z1 ∈ ideal i f y) } + ↑{ val := ↑z2 • y, property := (_ : ↑z2 ∈ ideal i f y) }
[PROOFSTEP]
apply add_smul
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
z1 : R
z2 : { x // x ∈ ideal i f y }
⊢ AddHom.toFun
      { toFun := fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) },
        map_add' :=
          (_ :
            ∀ (z1 z2 : { x // x ∈ ideal i f y }),
              (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) })
                  (z1 + z2) =
                (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) }) z1 +
                  (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) })
                    z2) }
      (z1 • z2) =
    ↑(RingHom.id R) z1 •
      AddHom.toFun
        { toFun := fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) },
          map_add' :=
            (_ :
              ∀ (z1 z2 : { x // x ∈ ideal i f y }),
                (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) })
                    (z1 + z2) =
                  (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) })
                      z1 +
                    (fun z => ↑(extensionOfMax i f).toLinearPMap { val := ↑z • y, property := (_ : ↑z ∈ ideal i f y) })
                      z2) }
        z2
[PROOFSTEP]
simp_rw [← (extensionOfMax i f).toLinearPMap.map_smul]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
z1 : R
z2 : { x // x ∈ ideal i f y }
⊢ ↑(extensionOfMax i f).toLinearPMap { val := ↑(z1 • z2) • y, property := (_ : ↑(z1 • z2) ∈ ideal i f y) } =
    ↑(extensionOfMax i f).toLinearPMap (↑(RingHom.id R) z1 • { val := ↑z2 • y, property := (_ : ↑z2 ∈ ideal i f y) })
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_val
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
y : N
z1 : R
z2 : { x // x ∈ ideal i f y }
⊢ ↑(z1 • z2) • y = ↑(RingHom.id R) z1 • ↑{ val := ↑z2 • y, property := (_ : ↑z2 ∈ ideal i f y) }
[PROOFSTEP]
apply mul_smul
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ ↑(extendIdealTo i f h y) r = 0
[PROOFSTEP]
have : r ∈ ideal i f y := by
  change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain
  rw [eq1]
  apply Submodule.zero_mem _
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ r ∈ ideal i f y
[PROOFSTEP]
change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ r • y ∈ (extensionOfMax i f).toLinearPMap.domain
[PROOFSTEP]
rw [eq1]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ 0 ∈ (extensionOfMax i f).toLinearPMap.domain
[PROOFSTEP]
apply Submodule.zero_mem _
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ ↑(extendIdealTo i f h y) r = 0
[PROOFSTEP]
rw [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h y r this]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ ↑(idealTo i f y) { val := r, property := this } = 0
[PROOFSTEP]
dsimp [ExtensionOfMaxAdjoin.idealTo]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
this : r ∈ ideal i f y
⊢ ↑(extensionOfMax i f).toLinearPMap { val := r • y, property := (_ : ↑{ val := r, property := this } ∈ ideal i f y) } =
    0
[PROOFSTEP]
simp only [LinearMap.coe_mk, eq1, Subtype.coe_mk, ← ZeroMemClass.zero_def, (extensionOfMax i f).toLinearPMap.map_zero]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ ↑(extendIdealTo i f h y) r = ↑(extendIdealTo i f h y) r'
[PROOFSTEP]
rw [← sub_eq_zero, ← map_sub]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ ↑(extendIdealTo i f h y) (r - r') = 0
[PROOFSTEP]
convert ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _
[GOAL]
case convert_2
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (r - r') • y = 0
[PROOFSTEP]
rw [sub_smul, sub_eq_zero, eq1]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
hr : r • y ∈ (extensionOfMax i f).toLinearPMap.domain
⊢ ↑(extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap { val := r • y, property := hr }
[PROOFSTEP]
simp only [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h _ _ hr, ExtensionOfMaxAdjoin.idealTo, LinearMap.coe_mk,
  Subtype.coe_mk, AddHom.coe_mk]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
a : { x // x ∈ (extensionOfMax i f).toLinearPMap.domain }
r : R
eq1 : ↑x = ↑a + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap a + ↑(extendIdealTo i f h y) r
[PROOFSTEP]
cases' a with a ha
[GOAL]
case mk
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap { val := a, property := ha } + ↑(extendIdealTo i f h y) r
[PROOFSTEP]
have eq2 : (ExtensionOfMaxAdjoin.fst i x - a : N) = (r - ExtensionOfMaxAdjoin.snd i x) • y :=
  by
  change x = a + r • y at eq1 
  rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul] at eq1 
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
⊢ ↑(fst i x) - a = (r - snd i x) • y
[PROOFSTEP]
change x = a + r • y at eq1 
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = a + r • y
⊢ ↑(fst i x) - a = (r - snd i x) • y
[PROOFSTEP]
rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul] at eq1 
[GOAL]
case mk
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap { val := a, property := ha } + ↑(extendIdealTo i f h y) r
[PROOFSTEP]
have eq3 :=
  ExtensionOfMaxAdjoin.extendIdealTo_eq i f h (r - ExtensionOfMaxAdjoin.snd i x)
    (by rw [← eq2]; exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha)
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ (r - snd i x) • ?m.219882 ∈ (extensionOfMax i f).toLinearPMap.domain
[PROOFSTEP]
rw [← eq2]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ ↑(fst i x) - a ∈ (extensionOfMax i f).toLinearPMap.domain
[PROOFSTEP]
exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha
[GOAL]
case mk
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) (r - snd i x) =
    ↑(extensionOfMax i f).toLinearPMap
      { val := (r - snd i x) • y, property := (_ : (r - snd i x) • y ∈ (extensionOfMax i f).toLinearPMap.domain) }
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap { val := a, property := ha } + ↑(extendIdealTo i f h y) r
[PROOFSTEP]
simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3 
[GOAL]
case mk
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap { val := a, property := ha } + ↑(extendIdealTo i f h y) r
[PROOFSTEP]
unfold ExtensionOfMaxAdjoin.extensionToFun
[GOAL]
case mk
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + ↑(extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap { val := a, property := ha } + ↑(extendIdealTo i f h y) r
[PROOFSTEP]
rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_mk]
[GOAL]
case mk
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + ↑(extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap
        { val := a + (r • y - snd i x • y),
          property := (_ : a + (r • y - snd i x • y) ∈ (extensionOfMax i f).toLinearPMap.domain) } +
      ↑(extendIdealTo i f h y) (snd i x)
[PROOFSTEP]
congr
[GOAL]
case mk.e_a.e_a
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ fst i x =
    { val := a + (r • y - snd i x • y),
      property := (_ : a + (r • y - snd i x • y) ∈ (extensionOfMax i f).toLinearPMap.domain) }
[PROOFSTEP]
ext
[GOAL]
case mk.e_a.e_a.a
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) =
    ↑{ val := a + (r • y - snd i x • y),
        property := (_ : a + (r • y - snd i x • y) ∈ (extensionOfMax i f).toLinearPMap.domain) }
[PROOFSTEP]
dsimp
[GOAL]
case mk.e_a.e_a.a
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + (r • y - snd i x • y)
[PROOFSTEP]
rw [Subtype.coe_mk, add_sub, ← eq1]
[GOAL]
case mk.e_a.e_a.a
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ supExtensionOfMaxSingleton i f y }
r : R
a : N
ha : a ∈ (extensionOfMax i f).toLinearPMap.domain
eq1 : ↑x = ↑{ val := a, property := ha } + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  ↑(extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap
        { val := r • y - snd i x • y,
          property := (_ : (fun x => x ∈ (extensionOfMax i f).toLinearPMap.domain) (r • y - snd i x • y)) } +
      ↑(extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = ↑x - snd i x • y
[PROOFSTEP]
exact eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
[PROOFSTEP]
have eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y :=
  by
  rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]
  ac_rfl
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
[PROOFSTEP]
rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ ↑(ExtensionOfMaxAdjoin.fst i a) + ExtensionOfMaxAdjoin.snd i a • y +
      (↑(ExtensionOfMaxAdjoin.fst i b) + ExtensionOfMaxAdjoin.snd i b • y) =
    ↑(ExtensionOfMaxAdjoin.fst i a) + ↑(ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a • y + ExtensionOfMaxAdjoin.snd i b • y)
[PROOFSTEP]
ac_rfl
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
[PROOFSTEP]
rw [ExtensionOfMaxAdjoin.extensionToFun_wd (y := y) i f h (a + b) _ _ eq1, LinearPMap.map_add, map_add]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      (↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
[PROOFSTEP]
unfold ExtensionOfMaxAdjoin.extensionToFun
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      (↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b))
[PROOFSTEP]
abel
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
a b : { x // x ∈ supExtensionOfMaxSingleton i f y }
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      (↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b))
[PROOFSTEP]
abel
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
a : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ AddHom.toFun
      { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
        map_add' :=
          (_ :
            ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
              ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b) }
      (r • a) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
          map_add' :=
            (_ :
              ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                  ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b) }
        a
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
a : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a
[PROOFSTEP]
have eq1 : r • (a : N) = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y :=
  by
  rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]
  rfl
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
a : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
[PROOFSTEP]
rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
a : { x // x ∈ supExtensionOfMaxSingleton i f y }
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
a : { x // x ∈ supExtensionOfMaxSingleton i f y }
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a
[PROOFSTEP]
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a) _ _ eq1, LinearMap.map_smul, LinearPMap.map_smul, ← smul_add]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
r : R
a : { x // x ∈ supExtensionOfMaxSingleton i f y }
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r •
      (↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a)) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a
[PROOFSTEP]
congr
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
m : M
⊢ ↑f m =
    ↑{ domain := supExtensionOfMaxSingleton i f y,
          toFun :=
            {
              toAddHom :=
                { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
                  map_add' :=
                    (_ :
                      ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                        ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                          ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (a : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                    AddHom.toFun
                        { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
                          map_add' :=
                            (_ :
                              ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                                ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                                  ExtensionOfMaxAdjoin.extensionToFun i f h a +
                                    ExtensionOfMaxAdjoin.extensionToFun i f h b) }
                        (r • a) =
                      ↑(RingHom.id R) r •
                        AddHom.toFun
                          { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
                            map_add' :=
                              (_ :
                                ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                                  ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                                    ExtensionOfMaxAdjoin.extensionToFun i f h a +
                                      ExtensionOfMaxAdjoin.extensionToFun i f h b) }
                          a) } }
      { val := ↑i m,
        property :=
          (_ :
            ↑i m ∈
              { domain := supExtensionOfMaxSingleton i f y,
                  toFun :=
                    {
                      toAddHom :=
                        { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
                          map_add' :=
                            (_ :
                              ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                                ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                                  ExtensionOfMaxAdjoin.extensionToFun i f h a +
                                    ExtensionOfMaxAdjoin.extensionToFun i f h b) },
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (a : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                            AddHom.toFun
                                { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
                                  map_add' :=
                                    (_ :
                                      ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                                        ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                                          ExtensionOfMaxAdjoin.extensionToFun i f h a +
                                            ExtensionOfMaxAdjoin.extensionToFun i f h b) }
                                (r • a) =
                              ↑(RingHom.id R) r •
                                AddHom.toFun
                                  { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h,
                                    map_add' :=
                                      (_ :
                                        ∀ (a b : { x // x ∈ supExtensionOfMaxSingleton i f y }),
                                          ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
                                            ExtensionOfMaxAdjoin.extensionToFun i f h a +
                                              ExtensionOfMaxAdjoin.extensionToFun i f h b) }
                                  a) } }.domain) }
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
m : M
⊢ ↑f m =
    ExtensionOfMaxAdjoin.extensionToFun i f h { val := ↑i m, property := (_ : ↑i m ∈ supExtensionOfMaxSingleton i f y) }
[PROOFSTEP]
rw [(extensionOfMax i f).is_extension, ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero, add_zero]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
m : M
⊢ ↑{ val := ↑i m, property := (_ : ↑i m ∈ supExtensionOfMaxSingleton i f y) } =
    ↑{ val := ↑i m, property := (_ : ↑i m ∈ (extensionOfMax i f).toLinearPMap.domain) } + 0 • y
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ (extensionOfMax i f).toLinearPMap.domain }
x' : { x // x ∈ (extensionOfMaxAdjoin i f h y).toLinearPMap.domain }
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMax i f).toLinearPMap x = ↑(extensionOfMaxAdjoin i f h y).toLinearPMap x'
[PROOFSTEP]
symm
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ (extensionOfMax i f).toLinearPMap.domain }
x' : { x // x ∈ (extensionOfMaxAdjoin i f h y).toLinearPMap.domain }
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMaxAdjoin i f h y).toLinearPMap x' = ↑(extensionOfMax i f).toLinearPMap x
[PROOFSTEP]
change ExtensionOfMaxAdjoin.extensionToFun i f h _ = _
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ (extensionOfMax i f).toLinearPMap.domain }
x' : { x // x ∈ (extensionOfMaxAdjoin i f h y).toLinearPMap.domain }
EQ : ↑x = ↑x'
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' = ↑(extensionOfMax i f).toLinearPMap x
[PROOFSTEP]
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero, add_zero]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
x : { x // x ∈ (extensionOfMax i f).toLinearPMap.domain }
x' : { x // x ∈ (extensionOfMaxAdjoin i f h y).toLinearPMap.domain }
EQ : ↑x = ↑x'
⊢ ↑x' = ↑x + 0 • y
[PROOFSTEP]
simp [EQ]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
⊢ (extensionOfMax i f).toLinearPMap.domain = ⊤
[PROOFSTEP]
refine' Submodule.eq_top_iff'.mpr fun y => _
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
⊢ y ∈ (extensionOfMax i f).toLinearPMap.domain
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
⊢ y ∈ (extensionOfMax i f).toLinearPMap.domain
[PROOFSTEP]
rw [← extensionOfMax_is_max i f _ (extensionOfMax_le i f h), extensionOfMaxAdjoin, Submodule.mem_sup]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
⊢ ∃ y_1, y_1 ∈ (extensionOfMax i f).toLinearPMap.domain ∧ ∃ z, z ∈ Submodule.span R {?y} ∧ y_1 + z = y
case y
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
⊢ N
case y
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i)
h : Baer R Q
y : N
⊢ N
[PROOFSTEP]
exact ⟨0, Submodule.zero_mem _, y, Submodule.mem_span_singleton_self _, zero_add _⟩
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i✝ : M →ₗ[R] N
f✝ : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i✝)
h : Baer R Q
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ↑i
f : X →ₗ[R] Q
this : Fact (Function.Injective ↑i)
x y : Y
⊢ (fun y =>
        ↑(extensionOfMax i f).toLinearPMap { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
      (x + y) =
    (fun y =>
          ↑(extensionOfMax i f).toLinearPMap
            { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
        x +
      (fun y =>
          ↑(extensionOfMax i f).toLinearPMap
            { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
        y
[PROOFSTEP]
rw [← LinearPMap.map_add]
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i✝ : M →ₗ[R] N
f✝ : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i✝)
h : Baer R Q
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ↑i
f : X →ₗ[R] Q
this : Fact (Function.Injective ↑i)
x y : Y
⊢ (fun y =>
        ↑(extensionOfMax i f).toLinearPMap { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
      (x + y) =
    ↑(extensionOfMax i f).toLinearPMap
      ({ val := x, property := (_ : x ∈ (extensionOfMax i f).toLinearPMap.domain) } +
        { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
[PROOFSTEP]
congr
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i✝ : M →ₗ[R] N
f✝ : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i✝)
h : Baer R Q
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ↑i
f : X →ₗ[R] Q
this : Fact (Function.Injective ↑i)
r : R
x : Y
⊢ AddHom.toFun
      {
        toFun := fun y =>
          ↑(extensionOfMax i f).toLinearPMap
            { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) },
        map_add' :=
          (_ :
            ∀ (x y : Y),
              (fun y =>
                    ↑(extensionOfMax i f).toLinearPMap
                      { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                  (x + y) =
                (fun y =>
                      ↑(extensionOfMax i f).toLinearPMap
                        { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                    x +
                  (fun y =>
                      ↑(extensionOfMax i f).toLinearPMap
                        { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                    y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        {
          toFun := fun y =>
            ↑(extensionOfMax i f).toLinearPMap
              { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) },
          map_add' :=
            (_ :
              ∀ (x y : Y),
                (fun y =>
                      ↑(extensionOfMax i f).toLinearPMap
                        { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                    (x + y) =
                  (fun y =>
                        ↑(extensionOfMax i f).toLinearPMap
                          { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                      x +
                    (fun y =>
                        ↑(extensionOfMax i f).toLinearPMap
                          { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                      y) }
        x
[PROOFSTEP]
rw [← LinearPMap.map_smul]
  -- Porting note: used to be congr
[GOAL]
R : Type u
inst✝⁷ : Ring R
Q : TypeMax
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M N : Type (max u v)
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i✝ : M →ₗ[R] N
f✝ : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ↑i✝)
h : Baer R Q
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ↑i
f : X →ₗ[R] Q
this : Fact (Function.Injective ↑i)
r : R
x : Y
⊢ AddHom.toFun
      {
        toFun := fun y =>
          ↑(extensionOfMax i f).toLinearPMap
            { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) },
        map_add' :=
          (_ :
            ∀ (x y : Y),
              (fun y =>
                    ↑(extensionOfMax i f).toLinearPMap
                      { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                  (x + y) =
                (fun y =>
                      ↑(extensionOfMax i f).toLinearPMap
                        { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                    x +
                  (fun y =>
                      ↑(extensionOfMax i f).toLinearPMap
                        { val := y, property := (_ : y ∈ (extensionOfMax i f).toLinearPMap.domain) })
                    y) }
      (r • x) =
    ↑(extensionOfMax i f).toLinearPMap
      (↑(RingHom.id R) r • { val := x, property := (_ : x ∈ (extensionOfMax i f).toLinearPMap.domain) })
[PROOFSTEP]
dsimp
