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
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
⊢ i = M'.mulMap N

Tactic:
have : i = mulMap M' N := by ext; simp [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
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
this : i = M'.mulMap N
⊢ M'.LinearDisjoint N

Tactic:
⟨this ▸ hi⟩

Premises used: Eq.rec, Submodule.LinearDisjoint.mk
-- 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
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
this : i = M'.mulMap N
⊢ M'.LinearDisjoint N

Tactic:
exact ⟨this ▸ hi⟩
-- 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
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
⊢ Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)

Tactic:
have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.lTensor_preserves_injective_linearMap _ <| inclusion_injective h
-- 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
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
a :
  ∀ (x : ↥M) (x_1 : ↥N'),
    Eq (α := S)
      (((((TensorProduct.AlgebraTensorModule.curry i : ↥M →ₗ[R] ↥N' →ₗ[R] S) : (a : ↥M) → ↥N' →ₗ[R] S) x :
              ↥N' →ₗ[R] S) :
            (a : ↥N') → S)
          x_1 :
        S)
      (((((TensorProduct.AlgebraTensorModule.curry (M.mulMap N') : ↥M →ₗ[R] ↥N' →ₗ[R] S) : (a : ↥M) → ↥N' →ₗ[R] S) x :
              ↥N' →ₗ[R] S) :
            (a : ↥N') → S)
          x_1 :
        S)
⊢ i = M.mulMap N'

Tactic:
ext
-- 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
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
x : ↥M
x_1 : ↥N'
⊢ Eq (α := S)
    (((((TensorProduct.AlgebraTensorModule.curry i : ↥M →ₗ[R] ↥N' →ₗ[R] S) : (a : ↥M) → ↥N' →ₗ[R] S) x : ↥N' →ₗ[R] S) :
          (a : ↥N') → S)
        x_1 :
      S)
    (((((TensorProduct.AlgebraTensorModule.curry (M.mulMap N') : ↥M →ₗ[R] ↥N' →ₗ[R] S) : (a : ↥M) → ↥N' →ₗ[R] S) x :
            ↥N' →ₗ[R] S) :
          (a : ↥N') → S)
        x_1 :
      S)

Tactic:
simp [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
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
⊢ i = M.mulMap N'

Tactic:
have : i = mulMap M N' := by ext; simp [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
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
this : i = M.mulMap N'
⊢ M.LinearDisjoint N'

Tactic:
⟨this ▸ hi⟩

Premises used: Eq.rec, Submodule.LinearDisjoint.mk
-- 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
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
this : i = M.mulMap N'
⊢ M.LinearDisjoint N'

Tactic:
exact ⟨this ▸ hi⟩
-- 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
M' N' : Submodule R S
hm : M' ≤ M
hn : N' ≤ N
inst_3 : Flat.{u, v} R ↥N
inst_4 : Flat.{u, v} R ↥M'
⊢ M'.LinearDisjoint N'

Tactic:
(H.of_le_left_of_flat hm).of_le_right_of_flat hn

Premises used: Submodule.LinearDisjoint.of_le_right_of_flat, Submodule.LinearDisjoint.of_le_left_of_flat
-- 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
M' N' : Submodule R S
hm : M' ≤ M
hn : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
inst_4 : Flat.{u, v} R ↥N'
⊢ M'.LinearDisjoint N'

Tactic:
(H.of_le_right_of_flat hn).of_le_left_of_flat hm

Premises used: Submodule.LinearDisjoint.of_le_right_of_flat, Submodule.LinearDisjoint.of_le_left_of_flat
-- 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 ≤ 1
inst_3 : Flat.{u, v} R ↥N
⊢ M.LinearDisjoint N

Tactic:
(one_left N).of_le_left_of_flat h

Premises used: Submodule.LinearDisjoint.one_left, Submodule.LinearDisjoint.of_le_left_of_flat
-- 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 : N ≤ 1
inst_3 : Flat.{u, v} R ↥M
⊢ M.LinearDisjoint N

Tactic:
(one_right M).of_le_right_of_flat h

Premises used: Submodule.LinearDisjoint.of_le_right_of_flat, Submodule.LinearDisjoint.one_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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
⊢ LinearIndependent R n

Tactic:
have hn : LinearIndependent R n := h.map' _ (ker_inclusion _ _ _)
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
⊢ Eq (α := S) ((M.mulRightMap n : (a : Fin 2 →₀ ↥M) → S) m : S) (0 : S)

Tactic:
simp [m, n, show _ * _ = _ * _ from hc]
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
⊢ Eq (α := S) ((M.mulRightMap n : (a : Fin 2 →₀ ↥M) → S) m : S) (0 : S)

Tactic:
have hm : mulRightMap M n m = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : Eq (α := S) ((M.mulRightMap n : (a : Fin 2 →₀ ↥M) → S) m : S) (0 : S)
⊢ m = 0

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

Premises used: Submodule.mem_bot, Submodule.LinearDisjoint.linearIndependent_right_of_flat, LinearMap.mem_ker
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : m = 0
⊢ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0

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

Premises used: Finsupp.single_eq_single_iff, sub_eq_zero, false_and, SetLike.coe_eq_coe, zero_ne_one, false_or, Fin.isValue, Subtype.mk.injEq
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0
⊢ b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0

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

Premises used: ZeroMemClass.coe_eq_zero, AddSubmonoid.mk_eq_zero
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0
⊢ b = 0 ∧ a = 0

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

Premises used: ZeroMemClass.coe_eq_zero, AddSubmonoid.mk_eq_zero
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0
⊢ b = 0 ∧ a = 0

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

Premises used: ZeroMemClass.coe_eq_zero, AddSubmonoid.mk_eq_zero
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : b = 0 ∧ a = 0
⊢ False

Tactic:
h.ne_zero 0 hm.2

Premises used: LinearIndependent.ne_zero, And.right, OfNat.ofNat
-- 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
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : b = 0 ∧ a = 0
⊢ False

Tactic:
exact h.ne_zero 0 hm.2

Premises used: LinearIndependent.ne_zero, And.right, OfNat.ofNat
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
⊢ LinearIndependent R m

Tactic:
have hm : LinearIndependent R m := h.map' _ (ker_inclusion _ _ _)
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
⊢ Eq (α := S) ((mulLeftMap N m : (a : Fin 2 →₀ ↥N) → S) n : S) (0 : S)

Tactic:
simp [m, n, show _ * _ = _ * _ from hc]
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
⊢ Eq (α := S) ((mulLeftMap N m : (a : Fin 2 →₀ ↥N) → S) n : S) (0 : S)

Tactic:
have hn : mulLeftMap N m n = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : Eq (α := S) ((mulLeftMap N m : (a : Fin 2 →₀ ↥N) → S) n : S) (0 : S)
⊢ n = 0

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

Premises used: Submodule.mem_bot, LinearMap.mem_ker, Submodule.LinearDisjoint.linearIndependent_left_of_flat
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : n = 0
⊢ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0

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, n] at hn

Premises used: Finsupp.single_eq_single_iff, sub_eq_zero, false_and, SetLike.coe_eq_coe, zero_ne_one, false_or, Fin.isValue, Subtype.mk.injEq
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0
⊢ b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0

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

Premises used: ZeroMemClass.coe_eq_zero, AddSubmonoid.mk_eq_zero
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0
⊢ b = 0 ∧ a = 0

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

Premises used: ZeroMemClass.coe_eq_zero, AddSubmonoid.mk_eq_zero
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯ = 0
⊢ b = 0 ∧ a = 0

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

Premises used: ZeroMemClass.coe_eq_zero, AddSubmonoid.mk_eq_zero
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : b = 0 ∧ a = 0
⊢ False

Tactic:
h.ne_zero 0 hn.2

Premises used: LinearIndependent.ne_zero, And.right, OfNat.ofNat
-- 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
inst_4 : Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥M) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N :=
  HSub.hSub (α := Fin 2 →₀ ↥N) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ N) (↑a : S) ⋯))
hn : b = 0 ∧ a = 0
⊢ False

Tactic:
exact h.ne_zero 0 hn.2

Premises used: LinearIndependent.ne_zero, And.right, OfNat.ofNat
-- 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
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
inl : Flat.{u, v} R ↥M → ¬LinearIndependent R ![a, b]
inr : Flat.{u, v} R ↥N → ¬LinearIndependent R ![a, b]
⊢ ¬LinearIndependent R ![a, b]

Tactic:
rcases hf with _ | _
-- 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:
H.not_linearIndependent_pair_of_commute_of_flat_left a b hc

Premises used: Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left