awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
i j : ι
h_1 :
  ∀ (v : V),
    ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h :
  HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
      HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
    0
hj : ¬i = j
this :
  t = 0 ∨
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      (0 : R)
h' : t = 0
neg : s = 0
⊢ s = 0 ∧ t = 0

Tactic:
refine ⟨?_, h'⟩
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
i j : ι
h_1 :
  ∀ (v : V),
    ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
h :
  HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
      HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
    0
hj : ¬i = j
this :
  t = 0 ∨
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      (0 : R)
h' : t = 0
⊢ HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0

Tactic:
simp only [h', zero_smul, add_zero] at h

Premises used: zero_smul, add_zero
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
i j : ι
h_1 :
  ∀ (v : V),
    ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
hj : ¬i = j
this :
  t = 0 ∨
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      (0 : R)
h' : t = 0
h : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0
neg : ∀ (hj : ¬s = 0), i = j
⊢ s = 0

Tactic:
contrapose hj
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
i j : ι
h_1 :
  ∀ (v : V),
    ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
this :
  t = 0 ∨
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      (0 : R)
h' : t = 0
h : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0
hj : ¬s = 0
neg :
  HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) 0 ((b : (a : ι) → V) j : V)
⊢ i = j

Tactic:
apply b.linearIndependent.eq_of_smul_apply_eq_smul_apply s 0 i j hj

Premises used: LinearIndependent.eq_of_smul_apply_eq_smul_apply, Module.Basis.linearIndependent, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
i j : ι
h_1 :
  ∀ (v : V),
    ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
this :
  t = 0 ∨
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      (0 : R)
h' : t = 0
h : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0
hj : ¬s = 0
⊢ HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) 0 ((b : (a : ι) → V) j : V)

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
⊢ ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)

Tactic:
have feq (i) : f (b i) = (b.coord i) (f (b i)) • b i := by
    classical
    rw [b.ext_elem_iff]
    intro j
    simp only [LinearIndependent.pair_iff, not_forall] at h
    obtain ⟨s, t, ⟨h, h'⟩⟩ := h (b i)
    simp only [Basis.coord_apply, _root_.map_smul, Basis.repr_self, smul_single,
      smul_eq_mul, mul_one, Finsupp.single_apply]
    split_ifs with hj
    · simp [hj]
    · have : t = 0 ∨ b.repr (f (b i)) j = 0 := by
        rw [b.ext_elem_iff] at h
        simpa [single_eq_of_ne' hj] using h j
      apply Or.resolve_left this
      contrapose h'
      refine ⟨?_, h'⟩
      simp only [h', zero_smul, add_zero] at h
      contrapose hj
      apply b.linearIndependent.eq_of_smul_apply_eq_smul_apply s 0 i j hj
      simpa using h
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
⊢ ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![x, (f : (a : V) → V) x]

Tactic:
specialize h x
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
h : ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![x, (f : (a : V) → V) x]
⊢ ∃ (x_1 : R) (x_2 : R) (_ : x_1 • x + HSMul.hSMul (β := V) x_2 ((f : (a : V) → V) x : V) = 0), x_1 = 0 → ¬x_2 = 0

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd,
      LinearIndependent.pair_iff, not_forall, not_and] at h

Premises used: LinearIndependent.pair_iff, Nat.succ_eq_add_one, Nat.reduceAdd, not_and, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
h : ∃ (x_1 : R) (x_2 : R) (_ : x_1 • x + HSMul.hSMul (β := V) x_2 ((f : (a : V) → V) x : V) = 0), x_1 = 0 → ¬x_2 = 0
obtain :
  ∀ (s t : R) (h : s • x + HSMul.hSMul (β := V) t ((f : (a : V) → V) x : V) = 0) (hst : s = 0 → ¬t = 0),
    HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
      HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
⊢ HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)

Tactic:
obtain ⟨s, t, h, hst⟩ := h
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
h : s • x + HSMul.hSMul (β := V) t ((f : (a : V) → V) x : V) = 0
hst : s = 0 → ¬t = 0
⊢ ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0

Tactic:
simp only [b.ext_elem_iff, map_add, _root_.map_smul, coe_add, Finsupp.coe_smul,
      Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_zero, Finsupp.coe_zero, Pi.zero_apply] at h

Premises used: Pi.zero_apply, map_zero, map_add, Pi.add_apply, Finsupp.coe_add, Finsupp.coe_smul, Module.Basis.ext_elem_iff, smul_eq_mul, Finsupp.coe_zero, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
simp :
  (sum (update (Finsupp.single i 1) j r) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V)) =
    HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
⊢ x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))

Tactic:
simp only [Basis.repr_symm_apply, linearCombination_apply, x]

Premises used: Finsupp.linearCombination_apply, Module.Basis.repr_symm_apply
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
rw :
  (sum (Finsupp.single i 1) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V)) +
      HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V) =
    HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((Finsupp.single i 1 : (a : ι) → R) j : R) ((b : (a : ι) → V) j : V)
hg : ∀ (i : ι), HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) 0 ((b : (a : ι) → V) i : V) = 0
hgg :
  ∀ (j : ι) (a₁ a₂ : R),
    HSMul.hSMul (β := V) (a₁ + a₂) ((b : (a : ι) → V) j : V) =
      HSMul.hSMul (β := V) a₁ ((b : (a : ι) → V) j : V) + HSMul.hSMul (β := V) a₂ ((b : (a : ι) → V) j : V)
⊢ (sum (update (Finsupp.single i 1) j r) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V)) =
    HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))

Tactic:
rw [← add_right_cancel_iff, sum_update_add]

Premises used: Finsupp.sum_update_add, add_right_cancel_iff
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
⊢ (sum (Finsupp.single i 1) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V)) +
      HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V) =
    HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((Finsupp.single i 1 : (a : ι) → R) j : R) ((b : (a : ι) → V) j : V)

Tactic:
simp [single_eq_of_ne' hij, add_smul]

Premises used: Finsupp.single_eq_of_ne', add_smul
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
⊢ ∀ (i : ι), HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) 0 ((b : (a : ι) → V) i : V) = 0

Tactic:
simp [single_eq_of_ne' hij, add_smul]

Premises used: Finsupp.single_eq_of_ne', add_smul
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
⊢ ∀ (j : ι) (a₁ a₂ : R),
    HSMul.hSMul (β := V) (a₁ + a₂) ((b : (a : ι) → V) j : V) =
      HSMul.hSMul (β := V) a₁ ((b : (a : ι) → V) j : V) + HSMul.hSMul (β := V) a₂ ((b : (a : ι) → V) j : V)

Tactic:
simp [single_eq_of_ne' hij, add_smul]

Premises used: Finsupp.single_eq_of_ne', add_smul
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
⊢ x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))

Tactic:
have hx : x = b i + r • b j := by
      simp only [Basis.repr_symm_apply, linearCombination_apply, x]
      rw [← add_right_cancel_iff, sum_update_add] <;>
        simp [single_eq_of_ne' hij, add_smul]
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
this :
  s +
      t *
        HAdd.hAdd (α := R)
          ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R)
          (HMul.hMul (β := R) r
            ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V)) : ι →₀ R) : (a : ι) → R) i :
              R)) =
    0
⊢ s +
      HMul.hMul (β := R) t
        ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R) =
    -HMul.hMul (β := R) (t * r)
        ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V)) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
rw [mul_add, ← add_assoc, ← mul_assoc, add_eq_zero_iff_eq_neg] at this

Premises used: add_assoc, mul_assoc, add_eq_zero_iff_eq_neg, mul_add
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
this :
  s +
      HMul.hMul (β := R) t
        ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R) =
    -HMul.hMul (β := R) (t * r)
        ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V)) : ι →₀ R) : (a : ι) → R) i : R)
rw :
  -HMul.hMul (β := R) (t * r)
        ((((b.repr : (a : V) → ι →₀ R)
                  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
                    ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
                    ((b : (a : ι) → V) j : V)) :
                ι →₀ R) :
              (a : ι) → R)
            i :
          R) =
    0
⊢ s + HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) = 0

Tactic:
rw [Basis.coord_apply, this, feq]

Premises used: Module.Basis.coord_apply
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
this :
  s +
      HMul.hMul (β := R) t
        ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R) =
    -HMul.hMul (β := R) (t * r)
        ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V)) : ι →₀ R) : (a : ι) → R) i : R)
⊢ -HMul.hMul (β := R) (t * r)
        ((((b.repr : (a : V) → ι →₀ R)
                  (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
                    ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
                    ((b : (a : ι) → V) j : V)) :
                ι →₀ R) :
              (a : ι) → R)
            i :
          R) =
    0

Tactic:
simp [single_eq_of_ne hij]

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
suffices :
  s +
      t *
        HAdd.hAdd (α := R)
          ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R)
          (HMul.hMul (β := R) r
            ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V)) : ι →₀ R) : (a : ι) → R) i :
              R)) =
    0
⊢ s + HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) = 0

Tactic:
suffices s + t * ((b.repr (f (b i))) i + r * (b.repr (f (b j))) i) = 0 by
        rw [mul_add, ← add_assoc, ← mul_assoc, add_eq_zero_iff_eq_neg] at this
        rw [Basis.coord_apply, this, feq]
        simp [single_eq_of_ne hij]