awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
⊢ t ⊆ {i, j}

Tactic:
have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
ht' : t ⊆ {i, j}
refine_2 : ∀ (h0 : g i • f i + g j • f j = 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
refine_2₁ : ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → x ∉ t → g x • f x = 0
⊢ ∀ i ∈ t, g i = 0

Tactic:
rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0

Premises used: Finset.sum_pair, Finset.sum_subset
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ g i = 0

Tactic:
obtain ⟨hi0, hj0⟩ := h _ _ h0
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
hi0 : g i = 0
⊢ g j = 0

Tactic:
obtain ⟨hi0, hj0⟩ := h _ _ h0
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
hi0 : g i = 0
hj0 : g j = 0
⊢ ∀ i ∈ t, g i = 0

Tactic:
fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)

Premises used: Eq.rec, Or.elim, Eq.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
hi0 : g i = 0
hj0 : g j = 0
⊢ ∀ i ∈ t, g i = 0

Tactic:
exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)

Premises used: Or.elim
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
ht' : t ⊆ {i, j}
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → x ∉ t → g x • f x = 0

Tactic:
simp +contextual [hg0]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw rw₁ rw₂ :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
refine_2 refine_2₁ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
refine_2₂ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
refine_2₃ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : g i • f i + g j • f j = 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
refine_2₄ refine_2₅ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0) (ht' : t ⊆ {i, j}) (x : ι),
    Membership.mem (γ := Finset ι) {i, j} x → x ∉ t → g x • f x = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]

Premises used: Finset.sum_pair, Pi.single_apply, linearIndepOn_iff'', Ne.symm
-- 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
⊢ Ne (α := Fin (Nat.succ 0).succ) 0 1

Tactic:
trivial
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : (∀ (c d : R), c • ![x, y] 0 + d • ![x, y] 1 = 0 → c = 0 ∧ d = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
rw [← linearIndepOn_univ_iff, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0,1} from rfl,
    Finset.coe_insert, Finset.coe_singleton, LinearIndepOn.pair_iff _ (by trivial)]

Premises used: Finset.coe_singleton, Finset.coe_univ, linearIndepOn_univ_iff, Finset.coe_insert, LinearIndepOn.pair_iff, rfl
-- 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
⊢ (∀ (c d : R), c • ![x, y] 0 + d • ![x, y] 1 = 0 → c = 0 ∧ d = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 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
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]
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₂
mp₄ mp₅ 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₅ 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₂
mp₇ mp₈ 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₈ 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₂
mp₁₀ 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] →
    ∀ ⦃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₂
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

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

Tactic:
suffices ∀ x y : M, LinearIndependent R ![x, y] → LinearIndependent R ![y, x] by tauto
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
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
⊢ ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]

Tactic:
simp only [LinearIndependent.pair_iff]

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

Tactic:
specialize h t s
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x_1 y_1 x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
rwa : t • x + s • y = 0 → s = 0 ∧ t = 0
rwa₁ rwa₂ rwa₃ rwa₄ : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
rwa [add_comm, and_comm]

Premises used: and_comm, add_comm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
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
⊢ LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]

Tactic:
rw [pair_iff, 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 t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩

Premises used: Iff.intro
-- 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
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ -s • -x + t • y = 0

Tactic:
simpa using hst
-- 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
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
simpa using h (-s) t (by simpa using hst)

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

Tactic:
simpa using hst
-- 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
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
simpa using h (-s) t (by simpa using hst)

Premises used: Neg.neg
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : LinearIndependent R ![-y, x] ↔ LinearIndependent R ![x, y]
rw₁ : LinearIndependent R ![y, x] ↔ LinearIndependent R ![x, y]
rw₂ rw₃ : LinearIndependent R ![x, y] ↔ LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]

Tactic:
rw [pair_symm_iff, pair_neg_left_iff, pair_symm_iff]

Premises used: LinearIndependent.pair_neg_left_iff, LinearIndependent.pair_symm_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
u : S
hu : u ≠ 0
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
⊢ LinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y]

Tactic:
simp only [LinearIndependent.pair_iff]

Premises used: LinearIndependent.pair_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x 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

Tactic:
⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩

Premises used: Iff.intro
-- 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
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
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
⊢ (∀ (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:
refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩
-- 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
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
rw₄ rw₅ : Eq.{u_4 + 1} (α := M) 0 0
⊢ s • u • x + t • u • y = 0

Tactic:
rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_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
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 = 0 ∧ t = 0

Tactic:
exact h s t (by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_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
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
rw₄ rw₅ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (u • s) • x + (u • t) • y = 0

Tactic:
rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst]

Premises used: smul_assoc, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
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 = 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])

Premises used: 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
u : S
hu : u ≠ 0
s t : R
hst : s • u • x + t • u • y = 0
h : u • s = 0 ∧ u • t = 0
⊢ s = 0 ∧ t = 0

Tactic:
⟨(smul_eq_zero_iff_right hu).mp h.1, (smul_eq_zero_iff_right hu).mp h.2⟩

Premises used: smul_eq_zero_iff_right, And.right, And.left, And.intro, Iff.mp
-- 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
u : S
hu : u ≠ 0
s t : R
hst : s • u • x + t • u • y = 0
h : u • s = 0 ∧ u • t = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact ⟨(smul_eq_zero_iff_right hu).mp h.1, (smul_eq_zero_iff_right hu).mp h.2⟩
-- 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
h' : LinearIndependent R ![x, y]
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
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y]

Tactic:
simp only [LinearIndependent.pair_iff] at h' ⊢

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
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
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)
⊢ (a • s + c • t) • x + (b • s + d • t) • y = 0

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]

Premises used: smul_assoc, add_smul, SMulCommClass.smul_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
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 • a • x + t • c • x + (s • b • y + t • d • y) = s • a • x + s • b • y + (t • c • x + t • d • y)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x 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 = 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)

Premises used: HAdd.hAdd, 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 ∧ b • s + d • t = 0
⊢ a • s + c • t = 0

Tactic:
obtain ⟨h₁, h₂⟩ := h'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
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
⊢ b • s + d • t = 0

Tactic:
obtain ⟨h₁, h₂⟩ := h'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
S : Type u_6
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Module S R
inst_6 : Module S M
inst_7 : SMulCommClass S R M
inst_8 : IsScalarTower S R M
inst_9 : IsTorsionFree S R
a b c d : S
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
right : t = 0
⊢ s = 0 ∧ t = 0

Tactic:
constructor