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
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),
    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:
have h' (i j) (hij : i ≠ j) (r : R) : b.coord i (f (b i)) * r = r * b.coord j (f (b j)) := by
    -- we use that `f (b i + r • b j)` is a multiple of `b i + r • b j`
    let x := b.repr.symm ((Finsupp.single i 1).update j r)
    specialize h x
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd,
      LinearIndependent.pair_iff, not_forall, not_and] at h
    obtain ⟨s, t, h, hst⟩ := h
    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
    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]
    have h1 : s + t * (b.coord i (f (b i))) = 0 := by
      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]
      simpa [hx, single_eq_of_ne hij] using h i
    have h2 : s * r + t * r * b.coord j (f (b j)) = 0 := by
      suffices s * r + t * ((b.repr (f (b i))) j + r * (b.repr (f (b j))) j) = 0 by
        rw [mul_add, ← add_assoc, add_right_comm, add_eq_zero_iff_eq_neg, ← mul_assoc] at this
        rw [Basis.coord_apply, this, feq]
        simp [single_eq_of_ne' hij]
      simpa [hx, single_eq_same, single_eq_of_ne' hij] using h j
    rw [add_eq_zero_iff_eq_neg] at h1
    rw [h1, neg_mul, neg_add_eq_sub, mul_assoc, mul_assoc,
      ← mul_sub, mul_eq_zero, sub_eq_zero] at h2
    symm
    apply Or.resolve_left h2
    contrapose hst; simp [h1, hst]
-- 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)
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
i j : ι
pos :
  ∀ (hij : i = j),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
neg :
  ∀ (hij : ¬i = j),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
⊢ (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)

Tactic:
by_cases hij : i = j
-- 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)
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
i j : ι
hij : i = j
pos :
  (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)
pos₁ pos₂ :
  Eq (α := V) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)
⊢ (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)

Tactic:
rw [← hij, ← feq]
-- 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)
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
i j : ι
hij : ¬i = j
⊢ HMul.hMul (α := R) (β := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
      (1 : R) =
    HMul.hMul (α := R) (β := R) (1 : R)
      ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)

Tactic:
have := h' i j hij 1
-- 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)
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
i j : ι
hij : ¬i = j
this :
  HMul.hMul (α := R) (β := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
      (1 : R) =
    HMul.hMul (α := R) (β := R) (1 : R)
      ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
⊢ Eq.{u_1 + 1} (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
    ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)

Tactic:
simp only [mul_one, one_mul] at this

Premises used: mul_one, one_mul
-- 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)
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
i j : ι
hij : ¬i = j
this :
  Eq.{u_1 + 1} (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
    ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
neg :
  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) =
    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) j : V)
neg₁ neg₂ :
  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) j : 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) j : V)
⊢ (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)

Tactic:
rw [feq, ← this]
-- 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)
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
⊢ ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)

Tactic:
replace feq (i j) : f (b j) = b.coord i (f (b i)) • b j := by
    by_cases hij : i = j
    · rw [← hij, ← feq]
    · have := h' i j hij 1
      simp only [mul_one, one_mul] at this
      rw [feq, ← this]
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
r : R
obtain :
  ∀ (j : ι) (hij : j ≠ i), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r
⊢ Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r

Tactic:
obtain ⟨j, hij⟩ := exists_ne i

Premises used: exists_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
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
r : R
j : ι
hij : j ≠ i
rw :
  HMul.hMul (β := R) r
      ((b.coord j : (a : V) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
            ((b.coord i : (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)
            ((b : (a : ι) → V) j : V)) :
        R) =
    HMul.hMul (β := R) r
      ((b.coord i : (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)
⊢ Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r

Tactic:
rw [commute_iff_eq, h' i j (Ne.symm hij), feq i j, feq i i]

Premises used: commute_iff_eq, Ne.symm
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
r : R
j : ι
hij : j ≠ i
⊢ HMul.hMul (β := R) r
      ((b.coord j : (a : V) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
            ((b.coord i : (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)
            ((b : (a : ι) → V) j : V)) :
        R) =
    HMul.hMul (β := R) r
      ((b.coord i : (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)

Tactic:
simp
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
⊢ ∀ (r : R), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r

Tactic:
have ha (r) : Commute (b.coord i (f (b i))) r := by
    obtain ⟨j, hij⟩ := exists_ne i
    rw [commute_iff_eq, h' i j (Ne.symm hij), feq i j, feq i i]
    simp
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
⟨⟨b.coord i (f (b i)), ?_⟩, ?_⟩

Premises used: Module.Basis.coord, Subtype.mk, Exists.intro, DFunLike.coe
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r
refine_1 :
  Membership.mem (α := R) (γ := Subring R) (Subring.center R)
    ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
refine_2 :
  f =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x)
          ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) ⋯ :
        ↥(Subring.center R))
      1
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
refine ⟨⟨b.coord i (f (b i)), ?_⟩, ?_⟩
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r
⊢ Membership.mem (α := R) (γ := Subring R) (Subring.center R)
    ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)

Tactic:
simpa [Subring.mem_center_iff, commute_iff_eq, eq_comm] using ha

Premises used: Subring.mem_center_iff, commute_iff_eq, eq_comm
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r
refine_2 :
  ∀ (i_1 : ι),
    Eq (α := V) ((f : (a : V) → V) ((b : (a : ι) → V) i_1 : V) : V)
      ((HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x)
                  ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) ⋯ :
                ↥(Subring.center R))
              1 :
            (a : V) → V)
          ((b : (a : ι) → V) i_1 : V) :
        V)
⊢ f =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x)
          ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) ⋯ :
        ↥(Subring.center R))
      1

Tactic:
apply b.ext

Premises used: Module.Basis.ext
-- 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]
h' :
  ∀ (i j : ι) (hij : i ≠ j) (r : 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)
feq :
  ∀ (i j : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) j : 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) j : V)
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) r
⊢ ∀ (i_1 : ι),
    Eq (α := V) ((f : (a : V) → V) ((b : (a : ι) → V) i_1 : V) : V)
      ((HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x)
                  ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) ⋯ :
                ↥(Subring.center R))
              1 :
            (a : V) → V)
          ((b : (a : ι) → V) i_1 : V) :
        V)

Tactic:
simpa only [smul_apply, End.one_apply, Subring.smul_def] using feq i

Premises used: LinearMap.smul_apply, Module.End.one_apply, Subring.smul_def