awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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 : ι
rw rw₁ rw₂ rw₃ :
  ∀ (j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      ((((b.repr : (a : V) → ι →₀ R)
                (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)) :
              ι →₀ R) :
            (a : ι) → R)
          j :
        R)
⊢ (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)
have rw₄ : ∀ (j : ι)
  (h :
    ∀ (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)),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
    ((((b.repr : (a : V) → ι →₀ R)
              (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)) :
            ι →₀ R) :
          (a : ι) → R)
        j :
      R)
Tactic: 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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 : ι
rw rw₁ rw₂ rw₃ :
  ∀ (j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      ((((b.repr : (a : V) → ι →₀ R)
                (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)) :
              ι →₀ R) :
            (a : ι) → R)
          j :
        R)
rw₄ :
  ∀ (j : ι)
    (h :
      ∀ (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)),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      ((((b.repr : (a : V) → ι →₀ R)
                (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)) :
              ι →₀ R) :
            (a : ι) → R)
          j :
        R)
⊢ (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)
have rw₅ : ∀ (j : ι)
  (h :
    ∀ (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)
  (h' : ¬(s = 0 ∧ 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)
    ((((b.repr : (a : V) → ι →₀ R)
              (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)) :
            ι →₀ R) :
          (a : ι) → R)
        j :
      R)
Tactic: 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
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]
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
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)
⊢ 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)
have h₁ : ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![x, (f : (a : V) → V) x]
Tactic: specialize h x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
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]
⊢ 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)
have 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
Tactic: simp only [Nat.succ_eq_add_one, Nat.reduceAdd,
      LinearIndependent.pair_iff, not_forall, not_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨s, t, h, hst⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
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
⊢ 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)
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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))
have 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))
Tactic: simp only [Basis.repr_symm_apply, linearCombination_apply, x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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 (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))
have 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)
Tactic: rw [← add_right_cancel_iff, sum_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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)
⊢ (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))
have hg : ∀ (i : ι), HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) 0 ((b : (a : ι) → V) i : V) = 0
Tactic: rw [← add_right_cancel_iff, sum_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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
⊢ (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))
have 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)
Tactic: rw [← add_right_cancel_iff, sum_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
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
⊢ 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)
have hx : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
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.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) = 0
have 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)
Tactic: rw [mul_add, ← add_assoc, ← mul_assoc, add_eq_zero_iff_eq_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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)
⊢ s + HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) = 0
have 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
Tactic: rw [Basis.coord_apply, this, feq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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))
⊢ s + HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) = 0
have 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
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]