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
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
have mem1 : x.1 ∈ (_ : Set _) := x.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)
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
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
rw [Submodule.coe_sup] at mem1
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
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
rcases mem1 with ⟨a, b, a_mem, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
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
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
rw [Submodule.mem_span_singleton] at b_mem
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
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
rcases b_mem with ⟨z, eq2⟩
no goals
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
exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩
no goals
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
rw [← eq1, ← eq2]