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
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 : -(d • c • t) = (c * b) • s
⊢ -(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]
-- 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 : -(d • c • t) = (c * b) • s
left₁ : -(d • c • t) = c • b • s
⊢ -(d • c • t) = (b * c) • s
have left₂ : d • c • t + c • b • s = 0
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← 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
left : -(d • c • t) = (c * b) • s
left₁ : -(d • c • t) = c • b • s
left₂ : d • c • t + c • b • s = 0
⊢ -(d • c • t) = (b * c) • s
have left₃ : c • b • s + d • c • t = 0
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← 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
left : -(d • c • t) = (c * b) • s
left₁ : -(d • c • t) = c • b • s
left₂ : d • c • t + c • b • s = 0
left₃ : c • b • s + d • c • t = 0
⊢ -(d • c • t) = (b * c) • s
have left₄ : c • b • s + c • d • t = 0
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← 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
left : -(d • c • t) = (c * b) • s
left₁ : -(d • c • t) = c • b • s
left₂ : d • c • t + c • b • s = 0
left₃ : c • b • s + d • c • t = 0
left₄ : c • b • s + c • d • t = 0
⊢ -(d • c • t) = (b * c) • s
have left₅ : c • (b • s + d • t) = 0
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← 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
left : -(d • c • t) = (c * b) • s
left₁ : -(d • c • t) = c • b • s
left₂ : d • c • t + c • b • s = 0
left₃ : c • b • s + d • c • t = 0
left₄ : c • b • s + c • d • t = 0
left₅ : c • (b • s + d • t) = 0
⊢ -(d • c • t) = (b * c) • s
have left₆ : HSMul.hSMul (β := R) c 0 = 0
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← 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
left : -(d • c • t) = (c * b) • s
left₁ : -(d • c • t) = c • b • s
left₂ : d • c • t + c • b • s = 0
left₃ : c • b • s + d • c • t = 0
left₄ : c • b • s + c • d • t = 0
left₅ : c • (b • s + d • t) = 0
left₆ : HSMul.hSMul (β := R) c 0 = 0
⊢ -(d • c • t) = (b * c) • s
have left₇ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← 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
this : (a * d) • t = (b * c) • t
⊢ t = 0
have by_contra : ∀ (ht : ¬t = 0), False
Tactic: by_contra ht
-- 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
⊢ t = 0
have right : (a * d) • t = (b * c) • t
Tactic: suffices (a * d) • t = (b * c) • t by
      by_contra ht; exact h (_root_.smul_left_injective S ht ‹_›)
-- 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) • t = a • d • t
have rw : a • d • t = a • d • t
Tactic: rw [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
⊢ a • d • t = -(a • b • s)
have rw : a • d • t + a • b • s = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, 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 : a • d • t + a • b • s = 0
⊢ a • d • t = -(a • b • s)
have rw₁ : a • (d • t + b • s) = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, 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 : a • d • t + a • b • s = 0
rw₁ : a • (d • t + b • s) = 0
⊢ a • d • t = -(a • b • s)
have rw₂ : a • (b • s + d • t) = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, 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 : a • d • t + a • b • s = 0
rw₁ : a • (d • t + b • s) = 0
rw₂ : a • (b • s + d • t) = 0
⊢ a • d • t = -(a • b • s)
have rw₃ : HSMul.hSMul (β := R) a 0 = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, 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 : a • d • t + a • b • s = 0
rw₁ : a • (d • t + b • s) = 0
rw₂ : a • (b • s + d • t) = 0
rw₃ : HSMul.hSMul (β := R) a 0 = 0
⊢ a • d • t = -(a • b • s)
have rw₄ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, 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) • t = (b * c) • t
have right : -(a • b • s) = (b * c) • t
Tactic: calc (a * d) • t
        = a • d • t := by rw [mul_smul]
      _ = -(a • b • s) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, h₂, smul_zero]
      _ = (b * c) • t := ?_
-- 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 • b • s) = (b * c) • t
have right : -(a • b • s) = b • c • t
Tactic: rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← 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
right : -(a • b • s) = b • c • t
⊢ -(a • b • s) = (b * c) • t
have right₁ : a • b • s + b • c • t = 0
Tactic: rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← 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
right : -(a • b • s) = b • c • t
right₁ : a • b • s + b • c • t = 0
⊢ -(a • b • s) = (b * c) • t
have right₂ : b • a • s + b • c • t = 0
Tactic: rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← 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
right : -(a • b • s) = b • c • t
right₁ : a • b • s + b • c • t = 0
right₂ : b • a • s + b • c • t = 0
⊢ -(a • b • s) = (b * c) • t
have right₃ : b • (a • s + c • t) = 0
Tactic: rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← 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
right : -(a • b • s) = b • c • t
right₁ : a • b • s + b • c • t = 0
right₂ : b • a • s + b • c • t = 0
right₃ : b • (a • s + c • t) = 0
⊢ -(a • b • s) = (b * c) • t
have right₄ : HSMul.hSMul (β := R) b 0 = 0
Tactic: rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← 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
right : -(a • b • s) = b • c • t
right₁ : a • b • s + b • c • t = 0
right₂ : b • a • s + b • c • t = 0
right₃ : b • (a • s + c • t) = 0
right₄ : HSMul.hSMul (β := R) b 0 = 0
⊢ -(a • b • s) = (b * c) • t
have right₅ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← 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
inst_10 : Nontrivial R
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
have inl : ∀ (h : a * d = b * c), LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
Tactic: rcases eq_or_ne (a * d) (b * c) with 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
inl :
  ∀ (h : a * d = b * c),
    LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ 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 : a * d ≠ b * c), LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
Tactic: rcases eq_or_ne (a * d) (b * c) with 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
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
have inl : ¬LinearIndependent R ![a • x + b • y, c • x + d • y]
Tactic: suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [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]
have inl : ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
Tactic: rw [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
a b c d : S
inst_10 : Nontrivial R
h : a * d = b * c
⊢ ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
have inl : ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
Tactic: push Not
-- 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
⊢ ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
have pos : ∀ (hbd : b = 0 ∧ d = 0), ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
Tactic: by_cases hbd : b = 0 ∧ d = 0
-- 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
pos : ∀ (hbd : b = 0 ∧ d = 0), ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
⊢ ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
have neg : ∀ (hbd : ¬(b = 0 ∧ d = 0)), ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0
Tactic: by_cases hbd : b = 0 ∧ d = 0
-- 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 pos : ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
Tactic: simp only [hbd.1, hbd.2, zero_smul, add_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
inst_10 : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
⊢ ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
have pos : ∀ (hac : a = 0 ∧ c = 0), ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
Tactic: by_cases hac : a = 0 ∧ c = 0
-- 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
pos : ∀ (hac : a = 0 ∧ c = 0), ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
⊢ ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
have neg : ∀ (hac : ¬(a = 0 ∧ c = 0)), ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
Tactic: by_cases hac : a = 0 ∧ c = 0
-- 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
hac : ¬(a = 0 ∧ c = 0)
⊢ ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
have neg : HSMul.hSMul (β := R) c 1 • a • x + HSMul.hSMul (β := R) (-a) 1 • c • x = 0
Tactic: refine ⟨c • 1, -a • 1, ?_, by aesop⟩
-- 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
hac : ¬(a = 0 ∧ c = 0)
⊢ HSMul.hSMul (β := R) c 1 • a • x + HSMul.hSMul (β := R) (-a) 1 • c • x = 0
have neg : c • a • x + -(a • c • x) = 0
Tactic: simp only [smul_assoc, one_smul, neg_smul]