-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem not_linearIndependent_pair_of_commute_of_flat_left [Module.Flat R M]
    (a b : ↥(M ⊓ N)) (hc : Commute a.1 b.1) : ¬LinearIndependent R ![a, b] := fun h ↦ by
  let n : Fin 2 → N := (inclusion inf_le_right) ∘ ![a, b]
  have hn : LinearIndependent R n := h.map' _ (ker_inclusion _ _ _)
  -- need this instance otherwise it only has semigroup structure
  letI : AddCommGroup (Fin 2 →₀ M) := Finsupp.instAddCommGroup
  let m : Fin 2 →₀ M := .single 0 ⟨b.1, b.2.1⟩ - .single 1 ⟨a.1, a.2.1⟩
  have hm : mulRightMap M n m = 0

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : b = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False

Tactic:
rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : b = 0 ∧ a = 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : (M.mulRightMap n) m = 0
⊢ False

Tactic:
rw [← LinearMap.mem_ker, H.linearIndependent_right_of_flat hn, mem_bot] at hm

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : m = 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
⊢ False

Tactic:
have hn : LinearIndependent R n := h.map' _ (ker_inclusion _ _ _)

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
⊢ False

Tactic:
let m : Fin 2 →₀ M := .single 0 ⟨b.1, b.2.1⟩ - .single 1 ⟨a.1, a.2.1⟩

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
⊢ (M.mulRightMap n) m = 0

Tactic:
simp [m, n, show _ * _ = _ * _ from hc]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : m = 0
⊢ False

Tactic:
simp only [Fin.isValue, sub_eq_zero, Finsupp.single_eq_single_iff, zero_ne_one, Subtype.mk.injEq,
  SetLike.coe_eq_coe, false_and, false_or, m] at hm

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : ⟨↑b, ⋯⟩ = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : ⟨↑b, ⋯⟩ = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False

Tactic:
repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : b = 0 ∧ a = 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
⊢ False

Tactic:
letI : AddCommGroup (Fin 2 →₀ M) := Finsupp.instAddCommGroup

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
⊢ False