-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem rank_inf_le_one_of_commute_of_flat (hf : Module.Flat R M ∨ Module.Flat R N)
    (hc : ∀ (m n : ↥(M ⊓ N)), Commute m.1 n.1) : Module.rank R ↥(M ⊓ N) ≤ 1

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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
nontriviality R

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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Proof state:
case h.e'_4.h.a
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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i => ↑i
hs : Nontrivial { x // x ∈ s }
a b : { x // x ∈ s }
hab : a ≠ b
this : LinearIndependent R ((fun i => ↑i) ∘ ![a, b])
i : Fin (Nat.succ 0).succ
⊢ ↑(![↑a, ↑b] i) = ↑(((fun i => ↑i) ∘ ![a, b]) i)

Tactic:
fin_cases i <;> simp

Result:
no goals

Proof state:
case intro.intro
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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i => ↑i
hs : Nontrivial { x // x ∈ s }
a b : { x // x ∈ s }
hab : a ≠ b
⊢ False

Tactic:
refine H.not_linearIndependent_pair_of_commute_of_flat hf a.1 b.1 (hc a.1 b.1) ?_

Result:
case intro.intro
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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i => ↑i
hs : Nontrivial { x // x ∈ s }
a b : { x // x ∈ s }
hab : a ≠ b
⊢ LinearIndependent R ![↑a, ↑b]

Proof state:
case «0».«0»
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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i => ↑i
hs : Nontrivial { x // x ∈ s }
a b : { x // x ∈ s }
hab : a ≠ b
hij : ![a, b] ((fun i => i) ⟨0, ⋯⟩) = ![a, b] ((fun i => i) ⟨0, ⋯⟩)
⊢ (fun i => i) ⟨0, ⋯⟩ = (fun i => i) ⟨0, ⋯⟩

Tactic:
rfl

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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i => ↑i
hs : Nontrivial { x // x ∈ s }
⊢ False

Tactic:
obtain ⟨a, b, hab⟩ := hs.exists_pair_ne

Result:
case intro.intro
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
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i => ↑i
hs : Nontrivial { x // x ∈ s }
a b : { x // x ∈ s }
hab : a ≠ b
⊢ False