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
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 +
      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:
simpa [hx, single_eq_of_ne hij] using h i

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

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

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

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

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

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

Tactic:
simp [single_eq_of_ne' hij]

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

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

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

Tactic:
rw [add_eq_zero_iff_eq_neg] at h1

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

Tactic:
rw [add_eq_zero_iff_eq_neg] at h1

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

Tactic:
rw [h1, neg_mul, neg_add_eq_sub, mul_assoc, mul_assoc,
      ← mul_sub, mul_eq_zero, sub_eq_zero] at h2

Premises used: mul_sub, neg_add_eq_sub, sub_eq_zero, mul_assoc, mul_eq_zero, neg_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
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))
h1 : s = -HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
h2 :
  t = 0 ∨
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
      HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r
symm :
  HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
    HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r
⊢ HMul.hMul (α := R) ((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:
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
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))
h1 : s = -HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
h2 :
  t = 0 ∨
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
      HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r
apply : ¬t = 0
⊢ HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
    HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r

Tactic:
apply Or.resolve_left h2

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
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))
h1 : s = -HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
h2 :
  t = 0 ∨
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
      HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r
contrapose : ∀ (hst : t = 0), ¬(s = 0 → ¬t = 0)
⊢ ¬t = 0

Tactic:
contrapose 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
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 :
  ∀ (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))
h1 : s = -HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
h2 :
  t = 0 ∨
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
      HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r
hst : t = 0
⊢ ¬(s = 0 → ¬t = 0)

Tactic:
simp [h1, hst]