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
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
by_contra : ∀ (hs : ¬s = 0), False
⊢ s = 0

Tactic:
by_contra hs
-- 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
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
hs : ¬s = 0
⊢ False

Tactic:
h (_root_.smul_left_injective S hs ‹_›)

Premises used: smul_left_injective
-- 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
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
hs : ¬s = 0
⊢ False

Tactic:
exact h (_root_.smul_left_injective S hs ‹_›)

Premises used: smul_left_injective
-- 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
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 : (a * d) • s = (b * c) • s
⊢ s = 0

Tactic:
suffices (a * d) • s = (b * c) • s by
      by_contra hs; exact h (_root_.smul_left_injective S hs ‹_›)
-- 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
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
rw₁ rw₂ : d • a • s = d • a • s
⊢ (a * d) • s = d • a • s

Tactic:
rw [mul_comm, mul_smul]

Premises used: mul_comm, SemigroupAction.mul_smul
-- 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
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ d • a • s = -(d • c • t)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]

Premises used: smul_zero, eq_neg_iff_add_eq_zero, 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 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

Tactic:
?_
-- 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
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) = (b * c) • s
⊢ (a * d) • s = (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 := ?_

Premises used: HMul.hMul, HSMul.hSMul
-- 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
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
left₇ left₈ : Eq.{u_2 + 1} (α := R) 0 0
⊢ -(d • c • t) = (b * c) • s

Tactic:
rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← smul_add, h₂,
        smul_zero]

Premises used: neg_eq_iff_add_eq_zero, smul_zero, add_comm, mul_comm, SMulCommClass.smul_comm, SemigroupAction.mul_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 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
by_contra : ∀ (ht : ¬t = 0), False
⊢ t = 0

Tactic:
by_contra ht
-- 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
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
ht : ¬t = 0
⊢ False

Tactic:
h (_root_.smul_left_injective S ht ‹_›)

Premises used: smul_left_injective
-- 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
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
ht : ¬t = 0
⊢ False

Tactic:
exact h (_root_.smul_left_injective S ht ‹_›)

Premises used: smul_left_injective
-- 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
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 * d) • t = (b * c) • t
⊢ t = 0

Tactic:
suffices (a * d) • t = (b * c) • t by
      by_contra ht; exact h (_root_.smul_left_injective S ht ‹_›)
-- 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
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 rw₁ : a • d • t = a • d • t
⊢ (a * d) • t = a • d • t

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- 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
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
rw₄ rw₅ : Eq.{u_2 + 1} (α := R) 0 0
⊢ a • d • t = -(a • b • s)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, h₂, smul_zero]

Premises used: smul_zero, add_comm, eq_neg_iff_add_eq_zero, 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 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

Tactic:
?_
-- 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
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 * d) • t = (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 := ?_

Premises used: HMul.hMul, HSMul.hSMul
-- 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
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
right₅ right₆ : Eq.{u_2 + 1} (α := R) 0 0
⊢ -(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]

Premises used: neg_eq_iff_add_eq_zero, smul_zero, SMulCommClass.smul_comm, SemigroupAction.mul_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 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
inr :
  ∀ (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

Tactic:
rcases eq_or_ne (a * d) (b * c) with h | h

Premises used: HMul.hMul, eq_or_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
this : ¬LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
simpa [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
inl : ¬LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [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
inl : ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
⊢ ¬LinearIndependent R ![a • x + b • y, c • x + d • y]

Tactic:
rw [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 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
inl : ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • 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:
push Not

Premises used: Not
-- 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
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
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
⊢ ∃ (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
-- 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
hbd : b = 0 ∧ d = 0
pos : ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0
⊢ ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0

Tactic:
simp only [hbd.1, hbd.2, zero_smul, add_zero]

Premises used: zero_smul, And.right, And.left, add_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 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
neg : ∀ (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

Tactic:
by_cases hac : a = 0 ∧ c = 0
-- 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
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) 1 (a • x) + HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (c • x) = 0

Tactic:
simp [hac.1, hac.2]

Premises used: And.right, And.left
-- 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
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ ∀ (_ : Eq.{u_2 + 1} (α := R) 1 0), Ne.{u_2 + 1} (α := R) 0 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
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

Tactic:
exact ⟨1, 0, by simp [hac.1, hac.2], by 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
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ ∀ (_ : HSMul.hSMul (β := R) c 1 = 0), HSMul.hSMul (β := R) (-a) 1 ≠ 0

Tactic:
aesop
-- 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
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
neg : HSMul.hSMul (β := R) c 1 • a • x + HSMul.hSMul (β := R) (-a) 1 • c • x = 0
⊢ ∃ (s : R) (t : R), s • a • x + t • c • x = 0 ∧ ∀ (_ : s = 0), t ≠ 0

Tactic:
refine ⟨c • 1, -a • 1, ?_, by aesop⟩
-- 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
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
neg : c • a • x + -(a • c • x) = 0
⊢ HSMul.hSMul (β := R) c 1 • a • x + HSMul.hSMul (β := R) (-a) 1 • c • x = 0

Tactic:
simp only [smul_assoc, one_smul, neg_smul]

Premises used: neg_smul, smul_assoc, one_smul
-- 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
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ c • a • x + -(a • c • x) = 0

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
hbd : ¬(b = 0 ∧ d = 0)
contrapose! : ∀ (hbd : HSMul.hSMul (β := R) d 1 = 0 ∧ HSMul.hSMul (β := R) (-b) 1 = 0), b = 0 ∧ d = 0
⊢ ∀ (_ : HSMul.hSMul (β := R) d 1 = 0), HSMul.hSMul (β := R) (-b) 1 ≠ 0

Tactic:
contrapose! hbd
-- 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
hbd : HSMul.hSMul (β := R) d 1 = 0 ∧ HSMul.hSMul (β := R) (-b) 1 = 0
⊢ b = 0 ∧ d = 0

Tactic:
simp_all
-- 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
hbd : ¬(b = 0 ∧ d = 0)
neg : HSMul.hSMul (β := R) d 1 • (a • x + b • y) + HSMul.hSMul (β := R) (-b) 1 • (c • x + d • y) = 0
⊢ ∃ (s : R) (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ ∀ (_ : s = 0), t ≠ 0

Tactic:
refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
-- 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
hbd : ¬(b = 0 ∧ d = 0)
neg : (b * c) • x + (b * d) • y + ((-b * c) • x + (-b * d) • y) = 0
⊢ HSMul.hSMul (β := R) d 1 • (a • x + b • y) + HSMul.hSMul (β := R) (-b) 1 • (c • x + d • y) = 0

Tactic:
simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]

Premises used: smul_assoc, smul_smul, one_smul, mul_comm, 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 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)
⊢ (b * c) • x + (b * d) • y + ((-b * c) • x + (-b * d) • y) = 0

Tactic:
module