-- Mathlib/Algebra/Module/Injective.lean
theorem extensionOfMax_adjoin.aux1 {y : N} (x : supExtensionOfMaxSingleton i f y) :
    ∃ (a : (extensionOfMax i f).domain) (b : R), x.1 = a.1 + b • y

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
mem1 : ↑x ∈ ↑(extensionOfMax i f).domain + ↑(Submodule.span R {y})
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
rcases mem1 with ⟨a, a_mem, b, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩

Result:
case intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
b_mem : b ∈ Submodule.span R {y}
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
mem1 : ↑x ∈ ↑(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
rw [Submodule.coe_sup] at mem1

Result:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
mem1 : ↑x ∈ ↑(extensionOfMax i f).domain + ↑(Submodule.span R {y})
⊢ ∃ a b, ↑x = ↑a + b • y

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
have mem1 : x.1 ∈ (_ : Set _) := x.2

Result:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
mem1 : ↑x ∈ ↑(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
b_mem : ∃ a, a • y = b
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
rcases b_mem with ⟨z, eq2⟩

Result:
case intro.intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ ∃ a b, ↑x = ↑a + b • y

Proof state:
case intro.intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
b_mem : b ∈ Submodule.span R {y}
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
rw [Submodule.mem_span_singleton] at b_mem

Result:
case intro.intro.intro.intro
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
b_mem : ∃ a, a • y = b
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
⊢ ∃ a b, ↑x = ↑a + b • y

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
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 : ↥(supExtensionOfMaxSingleton i f y)
a : N
a_mem : a ∈ ↑(extensionOfMax i f).domain
b : N
eq1 : (fun x1 x2 => x1 + x2) a b = ↑x
z : R
eq2 : z • y = b
⊢ ↑x = ↑⟨a, a_mem⟩ + z • y

Tactic:
rw [← eq1, ← eq2]

Result:
no goals