awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
hbd : ¬(b = 0 ∧ d = 0)
⊢ ∀ (_ : HSMul.hSMul (β := R) d 1 = 0), HSMul.hSMul (β := R) (-b) 1 ≠ 0
have contrapose! : ∀ (hbd : HSMul.hSMul (β := R) d 1 = 0 ∧ HSMul.hSMul (β := R) (-b) 1 = 0), b = 0 ∧ d = 0
Tactic: contrapose! hbd
Cleared hypotheses: hbd
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
hbd : ¬(b = 0 ∧ d = 0)
⊢ ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
have neg : HSMul.hSMul (β := R) d 1 • (a • x + b • y) + HSMul.hSMul (β := R) (-b) 1 • (c • x + d • y) = 0
Tactic: refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
hbd : ¬(b = 0 ∧ d = 0)
⊢ HSMul.hSMul (β := R) d 1 • (a • x + b • y) + HSMul.hSMul (β := R) (-b) 1 • (c • x + d • y) = 0
have neg : (b * c) • x + (b * d) • y + ((-b * c) • x + (-b * d) • y) = 0
Tactic: simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
have inr : ∀ (h' : LinearIndependent R ![a • x + b • y, c • x + d • y]), LinearIndependent R ![x, y]
Tactic: refine ⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x, y]
have rwa : ∀ (this : LinearIndependent R ![x, y]), LinearIndependent R ![x, y]
Tactic: rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x, y]
have inr : LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y]
have 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)]
Tactic: convert! pair_add_smul_add_smul_iff_aux d (-b) (-c) a (by simpa [mul_comm d a]) h' using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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, (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)]
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ ![(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
have h₁ : ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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, ⋯⟩)
⊢ ![(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
have h₂ : ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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, (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, ⋯⟩)
have h₁ : (a * d - b * c) • x = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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, (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, ⋯⟩)
have h₁ : (a * d - b * c) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • d • y)
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
have inl : ∀ (hS : Subsingleton S), LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
Tactic: rcases subsingleton_or_nontrivial S with hS | hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
have inr : ∀ (hS : Nontrivial S), LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
Tactic: rcases subsingleton_or_nontrivial S with hS | hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
have inl : ∀ (hS : Subsingleton S), LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
Tactic: rcases subsingleton_or_nontrivial S with hS | hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
have inr : ∀ (hS : Nontrivial S), LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
Tactic: rcases subsingleton_or_nontrivial S with hS | hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ LinearIndependent R ![x, x + y] ↔ LinearIndependent R ![x, y]
have suffices : ∀ (x y : M), 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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
have 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
Tactic: simp only [LinearIndependent.pair_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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) • x + t • (x + y) = 0
have rw : s • x - t • x + (t • x + t • y) = s • x + t • y
Tactic: rw [sub_smul, smul_add, ← h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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 = 0 ∧ t = 0
have h₁ : s - t = 0
Tactic: obtain ⟨h₁, h₂⟩ := h (s - t) t (by rw [sub_smul, smul_add, ← h']; abel)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
⊢ s = 0 ∧ t = 0
have h₂ : t = 0
Tactic: obtain ⟨h₁, h₂⟩ := h (s - t) t (by rw [sub_smul, smul_add, ← h']; abel)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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 ∧ t = 0
have h₃ : s = 0
Tactic: rw [h₂, sub_zero] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]
have rw : LinearIndependent R ![y, x + y] ↔ LinearIndependent R ![x, y]
Tactic: rw [← pair_symm_iff, add_comm, pair_add_right_iff, pair_symm_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]
have rw₁ : LinearIndependent R ![y, y + x] ↔ LinearIndependent R ![x, y]
Tactic: rw [← pair_symm_iff, add_comm, pair_add_right_iff, pair_symm_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]
have rw₂ : LinearIndependent R ![y, x] ↔ LinearIndependent R ![x, y]
Tactic: rw [← pair_symm_iff, add_comm, pair_add_right_iff, pair_symm_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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]
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]
have rw₃ : LinearIndependent R ![x, y] ↔ LinearIndependent R ![x, y]
Tactic: rw [← pair_symm_iff, add_comm, pair_add_right_iff, pair_symm_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 : ι), f i)
have rw : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
Tactic: rw [iUnion_eq_iUnion_finset f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
have hs : Directed (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, f i_1
Tactic: apply linearIndepOn_iUnion_of_directed
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
have h : ∀ (i : Finset ι), LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ i, f i_1)
Tactic: apply linearIndepOn_iUnion_of_directed
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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))
⊢ Directed (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, f i_1
have hs : ∀ ⦃i j : Finset ι⦄, i ≤ j → Subset.{u_4} (α := Set M) (⋃ i_1 ∈ i, f i_1) (⋃ i ∈ j, f i)
Tactic: apply directed_of_isDirected_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ insert i s, f i_1)
have h : LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)
Tactic: rw [Finset.set_biUnion_insert]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
have h : Disjoint (α := Submodule R M) (span R (f i)) (span R (⋃ x ∈ s, f x))
Tactic: refine (hl _).id_union ih ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
⊢ Disjoint (α := Submodule R M) (span R (f i)) (span R (⋃ x ∈ s, f x))
have h : Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ s, span R (f i))
Tactic: rw [span_iUnion₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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))
t : Finset ι
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ t, f i)
have h : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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))
t : Finset ι
h : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ t, f i)
have h₁ : ∀ (i : ι) (s : Finset ι) (his : i ∉ s) (ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)),
  LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ insert i s, f i_1)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his
Cleared hypotheses: t