awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S M
inst_10 : Module S N
inst_11 : Module S P
inst_12 : IsScalarTower S R M
inst_13 : IsScalarTower S R N
inst_14 : IsScalarTower S R P
inst_15 : AddCommMonoid M'
inst_16 : Module S M'
inst_17 : AddCommMonoid N'
inst_18 : Module S N'
inst_19 : AddCommMonoid P'
inst_20 : Module S P'
inst_21 : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective.{u_8 + 1, u_5 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
B : M →ₗ[R] N →ₗ[R] P
hB :
  ∀ (m : M') (n : N'),
    Membership.mem (α := P) k.range
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
m : M'
n : N'
rw :
  Eq.{u_5 + 1} (α := P)
      ((k : (a : P') → P)
          ((((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n : P') :
        P)
      ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_5 + 1} (α := P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
      (0 : P)
rw₁ :
  Eq.{u_5 + 1} (α := P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
      ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_5 + 1} (α := P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
      (0 : P)
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
      (0 : P) ↔
    Eq.{u_5 + 1} (α := P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
      (0 : P)
⊢ Eq.{u_8 + 1} (α := P')
      ((((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n : P')
      (0 : P') ↔
    Eq.{u_5 + 1} (α := P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
      (0 : P)

Tactic:
rw [← hk.eq_iff, restrictScalarsRange₂_apply, map_zero]

Premises used: LinearMap.restrictScalarsRange₂_apply, Function.Injective.eq_iff, map_zero
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
simp :
  ∃ (x : R) (h : ∀ (g : R), g * x = x * g),
    f =
      HSMul.hSMul (β := V →ₗ[R] V)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) x ⋯) 1
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
simp only [SetLike.exists, Subring.mem_center_iff]

Premises used: Subring.mem_center_iff, SetLike.exists
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
inl :
  ∀ (hV : Subsingleton V),
    ∃ (x : R) (h : ∀ (g : R), g * x = x * g),
      f =
        HSMul.hSMul (β := V →ₗ[R] V)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) x ⋯) 1
inr :
  ∀ (hV : Nontrivial V),
    ∃ (x : R) (h : ∀ (g : R), g * x = x * g),
      f =
        HSMul.hSMul (β := V →ₗ[R] V)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) x ⋯) 1
⊢ ∃ (x : R) (h : ∀ (g : R), g * x = x * g),
    f =
      HSMul.hSMul (β := V →ₗ[R] V)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) x ⋯) 1

Tactic:
rcases subsingleton_or_nontrivial V with hV | hV

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
hV : Subsingleton V
⊢ ∀ (g : R), g * 1 = 1 * g

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
hV : Subsingleton V
inl :
  f =
    HSMul.hSMul (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) 1 ⋯) 1
⊢ ∃ (x : R) (h : ∀ (g : R), g * x = x * g),
    f =
      HSMul.hSMul (β := V →ₗ[R] V)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) x ⋯) 1

Tactic:
refine ⟨1, by simp, ?_⟩
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
hV : Subsingleton V
inl :
  ∀ (x : V),
    Eq (α := V) ((f : (a : V) → V) x : V)
      ((HSMul.hSMul (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) 1 ⋯) 1 :
            (a : V) → V)
          x :
        V)
⊢ f =
    HSMul.hSMul (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) 1 ⋯) 1

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
hV : Subsingleton V
x : V
⊢ Eq (α := V) ((f : (a : V) → V) x : V)
    ((HSMul.hSMul (α := ↥(Subring.center R)) (β := V →ₗ[R] V)
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) 1 ⋯) 1 :
          (a : V) → V)
        x :
      V)

Tactic:
simp [Subring.smul_def, hV.allEq (f x) x]

Premises used: Subsingleton.allEq, Subring.smul_def, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm :
  ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)))
hV : Nontrivial V
⊢ ∀ (i j : ι) (r : R),
    i ≠ j →
      f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
        (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f

Tactic:
simp only [commute_iff_eq] at hcomm

Premises used: commute_iff_eq
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (r : R),
    i ≠ j →
      f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
        (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f
i j : ι
hij : i ≠ j
r : R
⊢ f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
    (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f

Tactic:
have := hcomm i j r hij
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (r : R),
    i ≠ j →
      f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
        (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f
i j : ι
hij : i ≠ j
r : R
this :
  f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
    (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f
⊢ ∀ (x : V),
    Eq (α := V) ((f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) : (a : V) → V) x : V)
      (((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f : (a : V) → V) x : V)

Tactic:
rw [LinearMap.ext_iff] at this

Premises used: LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (r : R),
    i ≠ j →
      f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
        (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f
i j : ι
hij : i ≠ j
r : R
this :
  ∀ (x : V),
    Eq (α := V) ((f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) : (a : V) → V) x : V)
      (((b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f : (a : V) → V) x : V)
⊢ HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
      (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))

Tactic:
simpa [LinearMap.transvection.apply] using this (b i)

Premises used: LinearMap.transvection.apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (r : R),
    i ≠ j →
      f * (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) =
        (b.coord i).transvection (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V)) * f
⊢ ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))

Tactic:
replace hcomm (i j : ι) (hij : i ≠ j) (r : R) :
      r • f (b j) = b.coord i (f (b i)) • r • b j := by
    have := hcomm i j r hij
    rw [LinearMap.ext_iff] at this
    simpa [LinearMap.transvection.apply] using this (b i)
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
i j : ι
pos :
  ∀ (hij : j = i),
    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 :
  ∀ (hij : ¬j = i),
    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)
⊢ 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:
by_cases hij : j = i
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
i j : ι
hij : j = i
⊢ 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 [hij]
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
i j : ι
hij : ¬j = i
⊢ 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:
simpa using congr_arg (b.coord i) (hcomm j i hij 1)

Premises used: Module.Basis.coord, congr_arg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
⊢ ∀ (i j : ι),
    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:
have h_allEq (i j : ι) : b.coord i (f (b i)) = b.coord j (f (b j)) := by
    by_cases hij : j = i
    · simp [hij]
    simpa using congr_arg (b.coord i) (hcomm j i hij 1)
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
h_allEq :
  ∀ (i j : ι),
    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)
i : ι
r : R
obtain :
  ∀ (j : ι) (hji : j ≠ i),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))
⊢ HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
      (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))

Tactic:
obtain ⟨j, hji⟩ := 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 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
h_allEq :
  ∀ (i j : ι),
    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)
i : ι
r : R
j : ι
hji : j ≠ i
⊢ HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
      (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))

Tactic:
simpa [h_allEq j i] using hcomm j i hji r
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm :
  ∀ (i j : ι) (hij : i ≠ j) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
h_allEq :
  ∀ (i j : ι),
    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)
⊢ ∀ (i : ι) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))

Tactic:
replace hcomm (i : ι) (r : R) : r • f (b i) = b.coord i (f (b i)) • r • b i := by
    obtain ⟨j, hji⟩ := exists_ne i
    simpa [h_allEq j i] using hcomm j i hji r
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq :
  ∀ (i j : ι),
    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)
hcomm :
  ∀ (i : ι) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))
i : ι := Classical.ofNonempty
r : R
⊢ HMul.hMul (β := R) r ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) =
    HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r

Tactic:
simpa using congr(b.coord i $(hcomm i r))
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq :
  ∀ (i j : ι),
    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)
hcomm :
  ∀ (i : ι) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))
i : ι := Classical.ofNonempty
inr :
  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
⊢ ∃ (x : R) (h : ∀ (g : R), g * x = x * g),
    f =
      HSMul.hSMul (β := V →ₗ[R] V)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.center R) x) x ⋯) 1

Tactic:
refine ⟨b.coord i (f (b i)), fun r ↦ by simpa using congr(b.coord i $(hcomm i r)), ?_⟩
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_3
inst_3 : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq :
  ∀ (i j : ι),
    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)
hcomm :
  ∀ (i : ι) (r : R),
    HSMul.hSMul (β := V) r ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
        (HSMul.hSMul (β := V) r ((b : (a : ι) → V) i : V))
i : ι := Classical.ofNonempty
inr :
  ∀ (x : V),
    Eq (α := V) ((f : (a : V) → V) x : 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)
          x :
        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:
ext x