awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩

Premises used: _private.0.LinearIndependent.pair_add_smul_add_smul_iff_aux, _private.0.LinearIndependent.pair_add_smul_add_smul_iff.match_2, HAdd.hAdd, And.intro, LinearIndependent, Iff.intro, Matrix.vecEmpty, HSMul.hSMul, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
inr : ∀ (h' : LinearIndependent R ![a • x + b • y, c • x + d • y]), LinearIndependent R ![x, y]
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
refine ⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
this : LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y]
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : LinearIndependent R ![x, y]), LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, y]

Tactic:
rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this

Premises used: LinearIndependent.pair_smul_iff, sub_ne_zero_of_ne
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
inr : LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y]
⊢ LinearIndependent R ![x, y]

Tactic:
suffices LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y] by
    rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ d * a ≠ -b * -c

Tactic:
simpa [mul_comm d a]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
h₁ :
  ![(a * d - b * c) • x, (a * d - b * c) • y] =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)]
⊢ LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y]

Tactic:
convert! pair_add_smul_add_smul_iff_aux d (-b) (-c) a (by simpa [mul_comm d a]) h' using 1

Premises used: _private.0.LinearIndependent.pair_add_smul_add_smul_iff_aux, Neg.neg
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
h₁ :
  ∀ (i : Fin (Nat.succ 0).succ),
    ![(a * d - b * c) • x, (a * d - b * c) • y] i =
      ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] i
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)]

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
i : Fin (Nat.succ 0).succ
h₁ :
  ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] i =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] i

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
h₁ : (a * d - b * c) • x = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
h₁ : (a * d - b * c) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • d • y)
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • x = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))

Tactic:
module
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
inst_10 : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • d • y)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
c : S
inl : ∀ (hS : Subsingleton S), LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
inr : ∀ (hS : Nontrivial S), LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
rcases subsingleton_or_nontrivial S with hS | hS

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
c : S
hS : Subsingleton S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
simp [hS.elim c 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
c : S
hS : Nontrivial S
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
c : S
hS : Nontrivial S
h : Nontrivial R
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
simpa using pair_add_smul_add_smul_iff (x := x) (y := y) 1 0 c 1

Premises used: OfNat.ofNat, LinearIndependent.pair_add_smul_add_smul_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
b : S
inl : ∀ (hS : Subsingleton S), LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
inr : ∀ (hS : Nontrivial S), LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

Tactic:
rcases subsingleton_or_nontrivial S with hS | hS

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
b : S
hS : Subsingleton S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

Tactic:
simp [hS.elim b 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
b : S
hS : Nontrivial S
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
b : S
hS : Nontrivial S
h : Nontrivial R
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

Tactic:
simpa using pair_add_smul_add_smul_iff (x := x) (y := y) 1 b 0 1

Premises used: OfNat.ofNat, LinearIndependent.pair_add_smul_add_smul_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
h : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![-x, -x + (x + y)]

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
h : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, x + y]

Tactic:
simpa using this (-x) (x + y) (by simpa)

Premises used: HAdd.hAdd, Neg.neg
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
suffices : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, x + y] ↔ LinearIndependent R ![x, y]

Tactic:
suffices ∀ x y : M, LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y] from
    ⟨this x y, fun h ↦ by simpa using this (-x) (x + y) (by simpa)⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
simp :
  ∀ (x y : M), (∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]

Tactic:
simp only [LinearIndependent.pair_iff]

Premises used: LinearIndependent.pair_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
rw : s • x - t • x + (t • x + t • y) = s • x + t • y
⊢ (s - t) • x + t • (x + y) = 0

Tactic:
rw [sub_smul, smul_add, ← h']

Premises used: sub_smul, smul_add
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ s • x - t • x + (t • x + t • y) = s • x + t • y

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ s - t = 0

Tactic:
obtain ⟨h₁, h₂⟩ := h (s - t) t (by rw [sub_smul, smul_add, ← h']; abel)

Premises used: HSub.hSub
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
h₁ : s - t = 0
⊢ t = 0

Tactic:
obtain ⟨h₁, h₂⟩ := h (s - t) t (by rw [sub_smul, smul_add, ← h']; abel)

Premises used: HSub.hSub
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
h₁ : s - t = 0
h₂ : t = 0
⊢ s = 0

Tactic:
rw [h₂, sub_zero] at h₁

Premises used: sub_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
h₁ : s - t = 0
h₂ : t = 0
h₃ : s = 0
⊢ t = 0

Tactic:
rw [h₂, sub_zero] at h₁

Premises used: sub_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
h₁ : s = 0
h₂ : t = 0
left : s = 0
right : t = 0
⊢ s = 0 ∧ t = 0

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : LinearIndependent R ![y, x + y] ↔ LinearIndependent R ![x, y]
rw₁ : LinearIndependent R ![y, y + x] ↔ LinearIndependent R ![x, y]
rw₂ : LinearIndependent R ![y, x] ↔ LinearIndependent R ![x, y]
rw₃ rw₄ : LinearIndependent R ![x, y] ↔ LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]

Tactic:
rw [← pair_symm_iff, add_comm, pair_add_right_iff, pair_symm_iff]

Premises used: add_comm, LinearIndependent.pair_symm_iff, LinearIndependent.pair_add_right_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
rw : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), f i)

Tactic:
rw [iUnion_eq_iUnion_finset f]

Premises used: Set.iUnion_eq_iUnion_finset
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
hs : Directed (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, f i_1
h : ∀ (i : Finset ι), LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ i, f i_1)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)

Tactic:
apply linearIndepOn_iUnion_of_directed

Premises used: linearIndepOn_iUnion_of_directed
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
hs : ∀ ⦃i j : Finset ι⦄, i ≤ j → Subset.{u_4} (α := Set M) (⋃ i_1 ∈ i, f i_1) (⋃ i ∈ j, f i)
⊢ Directed (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, f i_1

Tactic:
apply directed_of_isDirected_le

Premises used: directed_of_isDirected_le
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ ∀ ⦃i j : Finset ι⦄, i ≤ j → Subset.{u_4} (α := Set M) (⋃ i_1 ∈ i, f i_1) (⋃ i ∈ j, f i)

Tactic:
fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h

Premises used: Set.iUnion_subset_iUnion_const, Set.iUnion_mono
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ ∀ ⦃i j : Finset ι⦄, i ≤ j → Subset.{u_4} (α := Set M) (⋃ i_1 ∈ i, f i_1) (⋃ i ∈ j, f i)

Tactic:
exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h

Premises used: Set.iUnion_subset_iUnion_const, Set.iUnion_mono
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)
h : LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ insert i s, f i_1)

Tactic:
rw [Finset.set_biUnion_insert]

Premises used: Finset.set_biUnion_insert
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)

Tactic:
(hl _).id_union ih ?_

Premises used: LinearIndepOn.id_union
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)
h : Disjoint (α := Submodule R M) (span R (f i)) (span R (⋃ x ∈ s, f x))
⊢ LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)

Tactic:
refine (hl _).id_union ih ?_

Premises used: LinearIndepOn.id_union
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)
h : Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ s, span R (f i))
⊢ Disjoint (α := Submodule R M) (span R (f i)) (span R (⋃ x ∈ s, f x))

Tactic:
rw [span_iUnion₂]

Premises used: Submodule.span_iUnion₂