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
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
mp : LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
mpr : LinearIndependent R ![y, x] → LinearIndependent R ![x, y]
mp₁ mp₂ : LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
mp₃ :
  LinearIndependent R ![x, y] →
    ∀ ⦃a₁ a₂ : Fin (Nat.succ 0).succ →₀ R⦄,
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R ![y, x] : (a : Fin (Nat.succ 0).succ →₀ R) → M) a₁ : M)
          ((Finsupp.linearCombination R ![y, x] : (a : Fin (Nat.succ 0).succ →₀ R) → M) a₂ : M) →
        a₁ = a₂
mpr₁ mpr₂ : LinearIndependent R ![y, x] → LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]
have mpr₃ : LinearIndependent R ![y, x] →
  ∀ ⦃a₁ a₂ : Fin (Nat.succ 0).succ →₀ R⦄,
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M) a₁ : M)
        ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M) a₂ : M) →
      a₁ = a₂
Tactic: tauto
-- 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] ↔ LinearIndependent R ![y, x]
have suffices : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
Tactic: suffices ∀ x y : M, LinearIndependent R ![x, y] → LinearIndependent R ![y, x] by tauto
-- 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, y] → LinearIndependent R ![y, x]
have simp : ∀ (x y : M), (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0
Tactic: simp only [LinearIndependent.pair_iff]
-- 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 • y = 0 → s = 0 ∧ t = 0
s t : R
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0
have h₁ : t • x + s • y = 0 → t = 0 ∧ s = 0
Tactic: specialize h t s
Cleared hypotheses: 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_1 y_1 x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0
have rwa : t • x + s • y = 0 → s = 0 ∧ t = 0
Tactic: rwa [add_comm, and_comm]
-- 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] ↔ LinearIndependent R ![x, y]
have rw : (∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
Tactic: rw [pair_iff, 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 y : M
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]
have rw : LinearIndependent R ![-y, x] ↔ LinearIndependent R ![x, y]
Tactic: rw [pair_symm_iff, pair_neg_left_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] ↔ LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]
have rw₁ : LinearIndependent R ![y, x] ↔ LinearIndependent R ![x, y]
Tactic: rw [pair_symm_iff, pair_neg_left_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] ↔ LinearIndependent R ![x, y]
rw₁ : LinearIndependent R ![y, x] ↔ LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]
have rw₂ : LinearIndependent R ![x, y] ↔ LinearIndependent R ![x, y]
Tactic: rw [pair_symm_iff, pair_neg_left_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
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
u : S
hu : u ≠ 0
⊢ LinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y]
have simp : (∀ (s t : R), s • u • x + t • u • 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 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
u : S
hu : u ≠ 0
⊢ (∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
have refine_1 : ∀ (h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0) (s t : R) (hst : s • x + t • y = 0), s = 0 ∧ t = 0
Tactic: refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩
-- 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
u : S
hu : u ≠ 0
refine_1 :
  ∀ (h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0) (s t : R) (hst : s • x + t • y = 0), s = 0 ∧ t = 0
⊢ (∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
have refine_2 : ∀ (h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) (s t : R) (hst : s • u • x + t • u • y = 0), s = 0 ∧ t = 0
Tactic: refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s • u • x + t • u • y = 0
have rw : u • s • x + t • u • y = 0
Tactic: rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
rw : u • s • x + t • u • y = 0
⊢ s • u • x + t • u • y = 0
have rw₁ : u • s • x + u • t • y = 0
Tactic: rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
rw : u • s • x + t • u • y = 0
rw₁ : u • s • x + u • t • y = 0
⊢ s • u • x + t • u • y = 0
have rw₂ : u • (s • x + t • y) = 0
Tactic: rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
rw : u • s • x + t • u • y = 0
rw₁ : u • s • x + u • t • y = 0
rw₂ : u • (s • x + t • y) = 0
⊢ s • u • x + t • u • y = 0
have rw₃ : HSMul.hSMul (β := M) u 0 = 0
Tactic: rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
rw : u • s • x + t • u • y = 0
rw₁ : u • s • x + u • t • y = 0
rw₂ : u • (s • x + t • y) = 0
rw₃ : HSMul.hSMul (β := M) u 0 = 0
⊢ s • u • x + t • u • y = 0
have rw₄ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ (u • s) • x + (u • t) • y = 0
have rw : u • s • x + (u • t) • y = 0
Tactic: rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
rw : u • s • x + (u • t) • y = 0
⊢ (u • s) • x + (u • t) • y = 0
have rw₁ : u • s • x + u • t • y = 0
Tactic: rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
rw : u • s • x + (u • t) • y = 0
rw₁ : u • s • x + u • t • y = 0
⊢ (u • s) • x + (u • t) • y = 0
have rw₂ : s • u • x + u • t • y = 0
Tactic: rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
rw : u • s • x + (u • t) • y = 0
rw₁ : u • s • x + u • t • y = 0
rw₂ : s • u • x + u • t • y = 0
rw₃ : s • u • x + t • u • y = 0
⊢ (u • s) • x + (u • t) • y = 0
have rw₄ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst]
-- 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0
have h₁ : u • s = 0 ∧ u • t = 0
Tactic: specialize h (u • s) (u • t) (by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst])
Cleared hypotheses: 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
h : a * d ≠ b * c
h' : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y]
have simp : ∀ (h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) (s t : R),
  s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
Tactic: simp only [LinearIndependent.pair_iff] at h' ⊢
Cleared hypotheses: 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
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ (a • s + c • t) • x + (b • s + d • t) • y = 0
have simp : s • a • x + t • c • x + (s • b • y + t • d • y) = s • a • x + s • b • y + (t • c • x + t • d • y)
Tactic: simp only [← hst, smul_add, add_smul,
    smul_assoc, smul_comm a s, smul_comm c t, smul_comm b s, smul_comm d t]
-- 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
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s = 0 ∧ t = 0
have h'₁ : a • s + c • t = 0 ∧ b • s + d • t = 0
Tactic: specialize h' (a • s + c • t) (b • s + d • t) (by simp only [← hst, smul_add, add_smul,
    smul_assoc, smul_comm a s, smul_comm c t, smul_comm b s, smul_comm d t]; abel)
Cleared hypotheses: 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 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h' : a • s + c • t = 0 ∧ b • s + d • t = 0
⊢ s = 0 ∧ t = 0
have h₁ : a • s + c • t = 0
Tactic: obtain ⟨h₁, h₂⟩ := h'
Cleared hypotheses: 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 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h' : a • s + c • t = 0 ∧ b • s + d • t = 0
h₁ : a • s + c • t = 0
⊢ s = 0 ∧ t = 0
have h₂ : b • s + d • t = 0
Tactic: obtain ⟨h₁, h₂⟩ := h'
Cleared hypotheses: 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0 ∧ t = 0
have left : s = 0
Tactic: constructor
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
left : s = 0
⊢ s = 0 ∧ t = 0
have right : t = 0
Tactic: constructor
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
this : (a * d) • s = (b * c) • s
⊢ s = 0
have by_contra : ∀ (hs : ¬s = 0), False
Tactic: by_contra 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
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0
have left : (a * d) • s = (b * c) • s
Tactic: suffices (a * d) • s = (b * c) • s by
      by_contra hs; exact h (_root_.smul_left_injective S 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
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ (a * d) • s = d • a • s
have rw : (d * a) • s = d • a • s
Tactic: rw [mul_comm, mul_smul]
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
rw : (d * a) • s = d • a • s
⊢ (a * d) • s = d • a • s
have rw₁ : d • a • s = d • a • s
Tactic: rw [mul_comm, mul_smul]
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ d • a • s = -(d • c • t)
have rw : d • a • s + d • c • t = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
rw : d • a • s + d • c • t = 0
⊢ d • a • s = -(d • c • t)
have rw₁ : d • (a • s + c • t) = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
rw : d • a • s + d • c • t = 0
rw₁ : d • (a • s + c • t) = 0
⊢ d • a • s = -(d • c • t)
have rw₂ : HSMul.hSMul (β := R) d 0 = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
rw : d • a • s + d • c • t = 0
rw₁ : d • (a • s + c • t) = 0
rw₂ : HSMul.hSMul (β := R) d 0 = 0
⊢ d • a • s = -(d • c • t)
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ (a * d) • s = (b * c) • s
have left : -(d • c • t) = (b * c) • s
Tactic: calc (a * d) • s
        = d • a • s := by rw [mul_comm, mul_smul]
      _ = -(d • c • t) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
      _ = (b * c) • s := ?_
-- 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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = (b * c) • s
have left : -(d • c • t) = (c * b) • s
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← smul_add, h₂,
        smul_zero]