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 : 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
x : V
inr :
  Eq (α := V)
    (sum ((b.repr : (a : V) → ι →₀ R) x) fun (a : ι) (b_1 : R) ↦
        (f : (a : V) → V) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : 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)
        (sum ((b.repr : (a : V) → ι →₀ R) x) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V)) :
      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)

Tactic:
rw [← b.linearCombination_repr x, linearCombination_apply, map_finsuppSum]

Premises used: Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr, map_finsuppSum
-- 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
x : V
inr :
  Eq.{u_2 + 1} (α := V)
    (sum ((b.repr : (a : V) → ι →₀ R) x) fun (a : ι) (b_1 : R) ↦
      (f : (a : V) → V) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V)))
    (sum ((b.repr : (a : V) → ι →₀ R) x) fun (a : ι) (b_1 : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R))
        (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))
        (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V)))
⊢ Eq (α := V)
    (sum ((b.repr : (a : V) → ι →₀ R) x) fun (a : ι) (b_1 : R) ↦
        (f : (a : V) → V) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : 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)
        (sum ((b.repr : (a : V) → ι →₀ R) x) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V)) :
      V)

Tactic:
simp only [smul_apply, End.one_apply, smul_sum]

Premises used: LinearMap.smul_apply, Module.End.one_apply, Finsupp.smul_sum
-- 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
x : V
inr :
  ∀ (x_1 : ι),
    Membership.mem (γ := Finset ι) (support.{u_3, u_1} (M := R) ((b.repr : (a : V) → ι →₀ R) x)) x_1 →
      (f : (a : V) → V)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
            ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → V) x_1 : V)) =
        HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R))
          (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))
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
            ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → V) x_1 : V))
⊢ Eq.{u_2 + 1} (α := V)
    (sum ((b.repr : (a : V) → ι →₀ R) x) fun (a : ι) (b_1 : R) ↦
      (f : (a : V) → V) (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V)))
    (sum ((b.repr : (a : V) → ι →₀ R) x) fun (a : ι) (b_1 : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R))
        (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))
        (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V)))

Tactic:
apply sum_congr

Premises used: Finsupp.sum_congr
-- 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
x : V
j : ι
inr :
  Membership.mem (γ := Finset ι) (support.{u_3, u_1} (M := R) ((b.repr : (a : V) → ι →₀ R) x)) j →
    (f : (a : V) → V)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) j : R)
          ((b : (a : ι) → V) j : V)) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R))
        (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))
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) j : R)
          ((b : (a : ι) → V) j : V))
⊢ Membership.mem (γ := Finset ι) (support.{u_3, u_1} (M := R) ((b.repr : (a : V) → ι →₀ R) x)) j →
    (f : (a : V) → V)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) j : R)
          ((b : (a : ι) → V) j : V)) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R))
        (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))
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) j : R)
          ((b : (a : ι) → V) j : V))

Tactic:
_
-- 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
x : V
j : ι
h : Membership.mem (γ := Finset ι) (support.{u_3, u_1} (M := R) ((b.repr : (a : V) → ι →₀ R) x)) j
⊢ (f : (a : V) → V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) j : R)
        ((b : (a : ι) → V) j : V)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R))
      (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))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) j : R)
        ((b : (a : ι) → V) j : V))

Tactic:
simp [Subring.smul_def, h_allEq i j, hcomm j]

Premises used: Subring.smul_def
-- 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 : ι
rw :
  ∀ (i_1 : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i_1 : 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)
          i_1 :
        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)

Tactic:
rw [b.ext_elem_iff]

Premises used: Module.Basis.ext_elem_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
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
i j : ι
⊢ ∀ (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)

Tactic:
simp only [LinearIndependent.pair_iff, not_forall] at h

Premises used: LinearIndependent.pair_iff, 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
i 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)
obtain :
  ∀ (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)
⊢ 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:
obtain ⟨s, t, ⟨h, h'⟩⟩ := h (b i)

Premises used: 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
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
h' : ¬(s = 0 ∧ t = 0)
simp :
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then
        (((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i
      else 0 :
      R)
⊢ 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:
simp only [Basis.coord_apply, _root_.map_smul, Basis.repr_self, smul_single,
      smul_eq_mul, mul_one, Finsupp.single_apply]

Premises used: Finsupp.single_apply, smul_eq_mul, mul_one, Finsupp.smul_single, Module.Basis.coord_apply, Module.Basis.repr_self, map_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
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
h' : ¬(s = 0 ∧ t = 0)
pos :
  ∀ (hj : i = 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) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R)
neg :
  ∀ (hj : ¬i = 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)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then
        (((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i
      else 0 :
      R)

Tactic:
split_ifs with 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
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)
hj : i = 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) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
simp [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
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)
hj : ¬i = j
⊢ ∀ (i_1 : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
                  HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) :
              ι →₀ R) :
            (a : ι) → R)
          i_1 :
        R)
      (((b.repr : (a : V) → ι →₀ R) 0 : (a : ι) → R) i_1 : R)

Tactic:
rw [b.ext_elem_iff] at h

Premises used: Module.Basis.ext_elem_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
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
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
h₁ :
  ∀ (i_1 : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
                  HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) :
              ι →₀ R) :
            (a : ι) → R)
          i_1 :
        R)
      (((b.repr : (a : V) → ι →₀ R) 0 : (a : ι) → R) i_1 : R)
⊢ ¬(s = 0 ∧ t = 0)

Tactic:
rw [b.ext_elem_iff] at h

Premises used: Module.Basis.ext_elem_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
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
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
h₁ :
  ∀ (i_1 : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
                  HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) :
              ι →₀ R) :
            (a : ι) → R)
          i_1 :
        R)
      (((b.repr : (a : V) → ι →₀ R) 0 : (a : ι) → R) i_1 : R)
h'₁ : ¬(s = 0 ∧ t = 0)
⊢ ¬i = j

Tactic:
rw [b.ext_elem_iff] at h

Premises used: Module.Basis.ext_elem_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
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 :
  ∀ (i_1 : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
                  HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V)) :
              ι →₀ R) :
            (a : ι) → R)
          i_1 :
        R)
      (((b.repr : (a : V) → ι →₀ R) 0 : (a : ι) → R) i_1 : R)
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
⊢ 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)

Tactic:
simpa [single_eq_of_ne' hj] using h j

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
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
h' : ¬(s = 0 ∧ t = 0)
hj : ¬i = j
⊢ 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)

Tactic:
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
-- 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
h' : ¬(s = 0 ∧ t = 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)
neg : ¬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)

Tactic:
apply Or.resolve_left this

Premises used: Or.resolve_left
-- 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
h' : ¬(s = 0 ∧ t = 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)
neg : ∀ (h' : t = 0), s = 0 ∧ t = 0
⊢ ¬t = 0

Tactic:
contrapose 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
⊢ s = 0 ∧ t = 0

Tactic:
⟨?_, h'⟩

Premises used: And.intro