awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
⊢ HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
have h1 : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R) =
    0
have 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)
Tactic: rw [mul_add, ← add_assoc, add_right_comm, add_eq_zero_iff_eq_neg, ← mul_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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)
⊢ 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
have 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
Tactic: rw [Basis.coord_apply, this, feq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
h1 : s + HMul.hMul (β := R) t ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) = 0
⊢ HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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
⊢ HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
have h1₁ : 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
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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
⊢ HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
have 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
Tactic: rw [h1, neg_mul, neg_add_eq_sub, mul_assoc, mul_assoc,
      ← mul_sub, mul_eq_zero, sub_eq_zero] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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
⊢ HMul.hMul (α := R) ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) r =
    HMul.hMul (β := R) r ((b.coord j : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) j : V) : V) : R)
have 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
Tactic: symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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
⊢ 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
have apply : ¬t = 0
Tactic: apply Or.resolve_left h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
i j : ι
hij : i ≠ j
r : R
x : V := (b.repr.symm : (a : ι →₀ R) → V) (update (Finsupp.single i 1) j r)
s t : R
hst : s = 0 → ¬t = 0
h :
  ∀ (i : ι),
    HMul.hMul (β := R) s ((((b.repr : (a : V) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) +
        HMul.hMul (β := R) t ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) x) : ι →₀ R) : (a : ι) → R) i : R) =
      0
hx : x = HAdd.hAdd (α := V) ((b : (a : ι) → V) i : V) (HSMul.hSMul (β := V) r ((b : (a : ι) → V) j : V))
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
⊢ ¬t = 0
have contrapose : ∀ (hst : t = 0), ¬(s = 0 → ¬t = 0)
Tactic: contrapose hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
feq :
  ∀ (i : ι),
    (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
        ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
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)
have 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)
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
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)
⊢ (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)
have 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)
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
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
⊢ (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)
have 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)
Tactic: rw [← hij, ← feq]