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)
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)
rintro _ ⟨a, a_mem, rfl⟩ _ ⟨b, b_mem, rfl⟩ neq
no goals
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)
exact hchain a_mem b_mem (ne_of_apply_ne _ neq)