awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : Flat.{u, v} R ↥M
⊢ ¬LinearIndependent R ![a, b]

Tactic:
exact H.not_linearIndependent_pair_of_commute_of_flat_left a b hc

Premises used: Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : Flat.{u, v} R ↥N
⊢ ¬LinearIndependent R ![a, b]

Tactic:
H.not_linearIndependent_pair_of_commute_of_flat_right a b hc

Premises used: Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : Flat.{u, v} R ↥N
⊢ ¬LinearIndependent R ![a, b]

Tactic:
exact H.not_linearIndependent_pair_of_commute_of_flat_right a b hc

Premises used: Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h : Nontrivial R
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
_root_.rank_le fun s h ↦ ?_

Premises used: rank_le
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h : Nontrivial R
refine : ∀ (s : Finset ↥(M ⊓ N)) (h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))), s.card ≤ 1
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
refine _root_.rank_le fun s h ↦ ?_

Premises used: rank_le
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
by_contra : ∀ (hs : ¬s.card ≤ 1), False
⊢ s.card ≤ 1

Tactic:
by_contra hs
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : ¬s.card ≤ 1
⊢ Nontrivial.{v} ↥s

Tactic:
rw [not_le, ← Fintype.card_coe, Fintype.one_lt_card_iff_nontrivial] at hs

Premises used: not_le, Fintype.one_lt_card_iff_nontrivial, Fintype.card_coe
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
obtain : ∀ (a b : ↥s) (hab : a ≠ b), False
⊢ False

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

Premises used: Nontrivial.exists_pair_ne
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
⊢ False

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

Premises used: Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
refine : LinearIndependent R ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))]
⊢ False

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

Premises used: Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
i j : Fin (Nat.succ 0).succ
hij : ![a, b] i = ![a, b] j
0 :
  ∀ (hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j),
    (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = j
1 :
  ∀ (hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j),
    (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = j
⊢ i = j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j
0 :
  ∀
    (hij :
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h_2 :
  ∀
    (hij :
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![a, b] j
1 :
  ∀
    (hij :
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h_2 :
  ∀
    (hij :
      ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
hij :
  ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
hij :
  ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hab] at hij
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
hij :
  ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hab.symm] at hij

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
hij :
  ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![a, b] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
⊢ LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])

Tactic:
have := h.comp ![a, b] fun i j hij ↦ by
    fin_cases i <;> fin_cases j
    · rfl
    · simp [hab] at hij
    · simp [hab.symm] at hij
    · rfl
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
⊢ LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])

Tactic:
this
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
h₁ : ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] = (fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]
⊢ LinearIndependent R ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))]

Tactic:
convert! this
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
h₁ :
  ∀ (i : Fin (Nat.succ 0).succ),
    (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] i) : S) = (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) i) : S)
⊢ ![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] = (fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
i : Fin (Nat.succ 0).succ
h₁ :
  (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ))) :
      S) =
    (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) : S)
h₂ :
  (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ))) :
      S) =
    (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) : S)
⊢ (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] i) : S) = (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) i) : S)

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
⊢ (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ))) :
      S) =
    (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) : S)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
h_1 : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R (M := ↥(M ⊓ N)) fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))
hs : Nontrivial.{v} ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R (M := ↥(M ⊓ N)) ((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b])
⊢ (↑(![(↑a : ↥(M ⊓ N)), (↑b : ↥(M ⊓ N))] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ))) :
      S) =
    (↑(((fun (i : ↥s) ↦ (↑i : ↥(M ⊓ N))) ∘ ![a, b]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) : S)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
H.rank_inf_le_one_of_commute_of_flat (Or.inl ‹_›) hc

Premises used: Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, Or.inl
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute (↑m : S) (↑n : S)
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
H.rank_inf_le_one_of_commute_of_flat (Or.inr ‹_›) hc

Premises used: Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, Or.inr
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst_3 : Flat.{u, v} R ↥M
hc : ∀ (m n : ↥M), Commute (↑m : S) (↑n : S)
rw : ∀ (hc : ∀ (m n : ↥(M ⊓ M)), Commute (↑m : S) (↑n : S)), Module.rank R ↥(M ⊓ M) ≤ 1
⊢ Module.rank R ↥M ≤ 1

Tactic:
rw [← inf_of_le_left (le_refl M)] at hc ⊢

Premises used: le_refl, inf_of_le_left
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst_3 : Flat.{u, v} R ↥M
hc : ∀ (m n : ↥(M ⊓ M)), Commute (↑m : S) (↑n : S)
⊢ Module.rank R ↥(M ⊓ M) ≤ 1

Tactic:
H.rank_inf_le_one_of_commute_of_flat_left hc

Premises used: Set.Mem, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst_3 : Flat.{u, v} R ↥M
hc : ∀ (m n : ↥(M ⊓ M)), Commute (↑m : S) (↑n : S)
⊢ Module.rank R ↥(M ⊓ M) ≤ 1

Tactic:
exact H.rank_inf_le_one_of_commute_of_flat_left hc

Premises used: Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
⊢ ¬LinearIndependent R ![a, b]

Tactic:
H.not_linearIndependent_pair_of_commute_of_flat_left a b (mul_comm _ _)

Premises used: Set.Mem, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left, mul_comm
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
⊢ ¬LinearIndependent R ![a, b]

Tactic:
H.not_linearIndependent_pair_of_commute_of_flat_right a b (mul_comm _ _)

Premises used: Set.Mem, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right, mul_comm
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
⊢ ¬LinearIndependent R ![a, b]

Tactic:
H.not_linearIndependent_pair_of_commute_of_flat hf a b (mul_comm _ _)

Premises used: Set.Mem, mul_comm, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
H.rank_inf_le_one_of_commute_of_flat hf fun _ _ ↦ mul_comm _ _

Premises used: Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, Set.Mem, mul_comm, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
H.rank_inf_le_one_of_commute_of_flat_left fun _ _ ↦ mul_comm _ _

Premises used: Set.Mem, mul_comm, Subtype.val, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
⊢ Module.rank R ↥(M ⊓ N) ≤ 1

Tactic:
H.rank_inf_le_one_of_commute_of_flat_right fun _ _ ↦ mul_comm _ _

Premises used: Set.Mem, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right, mul_comm, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst_3 : Flat.{u, v} R ↥M
⊢ Module.rank R ↥M ≤ 1

Tactic:
H.rank_le_one_of_commute_of_flat_of_self fun _ _ ↦ mul_comm _ _

Premises used: Set.Mem, Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self, mul_comm, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
h :
  ∀ (x : ι) (x_1 : ι'),
    Eq.{u_4 + 1} (α := L) (((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') x x_1)
      (((⇑(algebraMap K L) : (a : K) → L) ∘ v x) x_1)
⊢ Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
x : ι
x_1 : ι'
⊢ Eq.{u_4 + 1} (α := L) (((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') x x_1)
    (((⇑(algebraMap K L) : (a : K) → L) ∘ v x) x_1)

Tactic:
simp [b', b, v', Module.Basis.extend, Algebra.algebraMap_eq_smul_one]

Premises used: Module.Basis.extend, Algebra.algebraMap_eq_smul_one