awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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
⊢ 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)
have 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)) sorry :
            ↥(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: rw [← b.linearCombination_repr x, linearCombination_apply, map_finsuppSum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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
⊢ 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)
have 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)) sorry :
        ↥(Subring.center R))
      (HSMul.hSMul (β := V) b_1 ((b : (a : ι) → V) a : V)))
Tactic: simp only [smul_apply, End.one_apply, smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
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
⊢ 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)))
have 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)) sorry :
          ↥(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))
Tactic: apply sum_congr
-- 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]
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)
have 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)
Tactic: rw [b.ext_elem_iff]
-- 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]
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)
              (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)
have 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)
Tactic: simp only [LinearIndependent.pair_iff, not_forall] at h
Cleared hypotheses: h
-- 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
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)
⊢ 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)
have 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)
Tactic: obtain ⟨s, t, ⟨h, h'⟩⟩ := h (b i)
-- 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
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)
⊢ 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)
have 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)
Tactic: simp only [Basis.coord_apply, _root_.map_smul, Basis.repr_self, smul_single,
      smul_eq_mul, mul_one, Finsupp.single_apply]
-- 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
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)
⊢ 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)
have 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)
Tactic: split_ifs with hj
-- 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
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)
⊢ 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)
have 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)
Tactic: split_ifs with hj
-- 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
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)
have 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)
Tactic: rw [b.ext_elem_iff] at h
Cleared hypotheses: h, h', hj
-- 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
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) (0 : R)
have 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)
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
-- 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
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)
⊢ 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)
have neg : ¬t = 0
Tactic: apply Or.resolve_left 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
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)
⊢ ¬t = 0
have neg : ∀ (h' : t = 0), s = 0 ∧ t = 0
Tactic: contrapose h'
Cleared hypotheses: h'
-- 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
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
have neg : s = 0
Tactic: refine ⟨?_, h'⟩
-- 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
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
have h₁ : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0
Tactic: simp only [h', zero_smul, add_zero] at h
Cleared hypotheses: h
-- 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
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
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
h : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0
⊢ s = 0
have neg : ∀ (hj : ¬s = 0), i = j
Tactic: contrapose hj
Cleared hypotheses: hj
-- 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
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
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
h : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) = 0
hj : ¬s = 0
⊢ i = j
have neg : HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) 0 ((b : (a : ι) → V) j : V)
Tactic: apply b.linearIndependent.eq_of_smul_apply_eq_smul_apply s 0 i j hj
-- 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]
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)
have 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)
Tactic: classical
    rw [b.ext_elem_iff]
    intro j
    simp only [LinearIndependent.pair_iff, not_forall] at h
    obtain ⟨s, t, ⟨h, h'⟩⟩ := h (b i)
    simp only [Basis.coord_apply, _root_.map_smul, Basis.repr_self, smul_single,
      smul_eq_mul, mul_one, Finsupp.single_apply]
    split_ifs with hj
    · simp [hj]
    · 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
      apply Or.resolve_left this
      contrapose h'
      refine ⟨?_, h'⟩
      simp only [h', zero_smul, add_zero] at h
      contrapose hj
      apply b.linearIndependent.eq_of_smul_apply_eq_smul_apply s 0 i j hj
      simpa using h