awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
i : ι
hi : i ∈ s
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
have rw : r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
Tactic: rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
i : ι
hi : i ∈ s
rw : r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
have rw₁ : eval x (Lagrange.basis s v i) * r i = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
Tactic: rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
i : ι
hi : i ∈ s
rw : r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
rw₁ : eval x (Lagrange.basis s v i) * r i = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
have rw₂ : eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i =
  eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
Tactic: rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v : (a : ι → F) → F[X]) r) =
    HDiv.hDiv (α := F) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹)
have rw : (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
    (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) =
  HDiv.hDiv (α := F) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹)
Tactic: rw [← div_one (eval x (interpolate s v r)), ← @eval_one _ _ x, ← interpolate_one hvs hs,
    eval_interpolate_not_at_node r hx, eval_interpolate_not_at_node 1 hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
⊢ Eq.{u_2 + 1} (α := S)
    ((abv : (a : R) → S)
        (HSMul.hSMul (α := ℤˣ) (β := R) (((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
          (∏ i : n, A ((σ : (a : n) → n) i) i)) :
      S)
    (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i) : S)
have rw : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (∏ i : n, A ((σ : (a : n) → n) i) i) : S)
  (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i) : S)
Tactic: rw [abv.map_units_int_smul, abv.map_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
rw :
  Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (∏ i : n, A ((σ : (a : n) → n) i) i) : S)
    (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i) : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((abv : (a : R) → S)
        (HSMul.hSMul (α := ℤˣ) (β := R) (((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
          (∏ i : n, A ((σ : (a : n) → n) i) i)) :
      S)
    (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i) : S)
have rw₁ : Eq.{u_2 + 1} (α := S) (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i))
  (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i))
Tactic: rw [abv.map_units_int_smul, abv.map_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
⊢ LE.le.{u_2} (α := S) (∑ σ : Perm n, ∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i))
    (∑ _σ : Perm n, ∏ _i : n, x)
have h : ∀ (i : Perm n),
  Membership.mem (γ := Finset (Perm n)) univ i →
    ∀ (i_1 : n), Membership.mem (γ := Finset n) univ i_1 → (abv : (a : R) → S) (A ((i : (a : n) → n) i_1) i_1) ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), (abv : (a : R) → S) (A k i j) ≤ x
i j : n
⊢ LE.le.{u_2} (α := S) (∑ k ∈ s, (abv : (a : R) → S) (A k i j)) (∑ _k ∈ s, x)
have h : ∀ i_1 ∈ s, (abv : (a : R) → S) (A i_1 i j) ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
d : n → R
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal d).charmatrix
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
have rw : HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
    ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
    ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
  diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
Tactic: rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
d : n → R
rw :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
      ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal d).charmatrix
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
have rw₁ : HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
    ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
  diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
Tactic: rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
d : n → R
rw :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
      ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₁ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal d).charmatrix
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
have rw₂ : HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X) ((diagonal d).map (⇑C : (a : R) → R[X])) =
  diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
Tactic: rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
d : n → R
rw :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
      ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₁ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₂ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X) ((diagonal d).map (⇑C : (a : R) → R[X])) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal d).charmatrix
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
have rw₃ : HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
    (diagonal fun (m : n) ↦ (C : (a : R) → R[X]) (d m)) =
  diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
Tactic: rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
d : n → R
rw :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
      ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₁ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
      ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) (diagonal d) : Matrix.{u_4, u_4, u_1} n n R[X]) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₂ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X) ((diagonal d).map (⇑C : (a : R) → R[X])) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
rw₃ :
  HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal fun (x : n) ↦ X)
      (diagonal fun (m : n) ↦ (C : (a : R) → R[X]) (d m)) =
    diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X])
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X]) (diagonal d).charmatrix
    (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
have rw₄ : Eq (α := Matrix.{u_4, u_4, u_1} n n R[X])
  (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
  (diagonal fun (i : n) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (d i) : R[X]))
Tactic: rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M.charmatrix =
    HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
      ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
have a : ∀ (k : ℕ) (i j : n),
  coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M.charmatrix) k i j =
    (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
          ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])).coeff
      k i j
Tactic: ext k i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M.charmatrix) k i j =
    (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
          ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])).coeff
      k i j
have a : coeff (M.charmatrix i j) k =
  HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
    (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
Tactic: simp only [matPolyEquiv_coeff_apply, coeff_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
have pos : ∀ (h : i = j),
  coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
pos :
  ∀ (h : i = j),
    coeff (M.charmatrix i j) k =
      HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
        (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
have neg : ∀ (h : ¬i = j),
  coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
have pos : coeff (M.charmatrix i i) k =
  HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
    (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff (M.charmatrix i i) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i
have pos : HSub.hSub (α := R) (coeff X k) (coeff ((C : (a : R) → R[X]) (M i i)) k) =
  HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
    (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i
Tactic: rw [charmatrix_apply_eq, coeff_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ HSub.hSub (α := R) (coeff X k) (coeff ((C : (a : R) → R[X]) (M i i)) k) =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i i
have pos : ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
  HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i
Tactic: simp only [coeff_X, coeff_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
    HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i
have pos : 1 = k → k = 0 → 1 - M i i = HSub.hSub (α := Matrix n n R) 1 M i i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i : n
pos : 1 = k → k = 0 → 1 - M i i = HSub.hSub (α := Matrix n n R) 1 M i i
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
    HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i
have neg : 1 = k → ¬k = 0 → HSub.hSub (α := R) 1 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i : n
pos : 1 = k → k = 0 → 1 - M i i = HSub.hSub (α := Matrix n n R) 1 M i i
neg : 1 = k → ¬k = 0 → HSub.hSub (α := R) 1 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i i
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
    HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i
have pos₁ : ¬1 = k → k = 0 → 0 - M i i = HSub.hSub (α := Matrix n n R) 0 M i i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i : n
pos : 1 = k → k = 0 → 1 - M i i = HSub.hSub (α := Matrix n n R) 1 M i i
neg : 1 = k → ¬k = 0 → HSub.hSub (α := R) 1 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i i
pos₁ : ¬1 = k → k = 0 → 0 - M i i = HSub.hSub (α := Matrix n n R) 0 M i i
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) =
    HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i i
have neg₁ : ¬1 = k → ¬k = 0 → HSub.hSub (α := R) 0 0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 0 0 i i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ coeff (M.charmatrix i j) k =
    HSub.hSub (α := Matrix n n R) (β := Matrix n n R) (coeff X k)
      (coeff ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) k) i j
have neg : (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j
Tactic: rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j
have pos : k = 0 → 1 = k → -M i j = HSub.hSub (α := Matrix n n R) 1 M i j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
pos : k = 0 → 1 = k → -M i j = HSub.hSub (α := Matrix n n R) 1 M i j
⊢ (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j
have neg : k = 0 → ¬1 = k → -M i j = HSub.hSub (α := Matrix n n R) 0 M i j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
pos : k = 0 → 1 = k → -M i j = HSub.hSub (α := Matrix n n R) 1 M i j
neg : k = 0 → ¬1 = k → -M i j = HSub.hSub (α := Matrix n n R) 0 M i j
⊢ (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j
have pos₁ : ¬k = 0 → 1 = k → -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
pos : k = 0 → 1 = k → -M i j = HSub.hSub (α := Matrix n n R) 1 M i j
neg : k = 0 → ¬1 = k → -M i j = HSub.hSub (α := Matrix n n R) 0 M i j
pos₁ : ¬k = 0 → 1 = k → -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 1 0 i j
⊢ (-if k = 0 then M i j else 0) = HSub.hSub (α := Matrix n n R) (if 1 = k then 1 else 0) (if k = 0 then M else 0) i j
have neg₁ : ¬k = 0 → ¬1 = k → -0 = HSub.hSub (α := Matrix n n R) (β := Matrix n n R) 0 0 i j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
M : Matrix n n R
e : n ≃ m
⊢ Eq (α := Matrix.{u_3, u_3, u_1} m m R[X]) (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M))
    ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix)
have a : ∀ (i j : m) (x : ℕ),
  Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
Tactic: ext i j x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
have pos : ∀ (h : i = j),
  Eq.{u_1 + 1} (α := R) (coeff (charmatrix ((reindex e e : (a : Matrix n n R) → Matrix m m R) M) i j) x)
    (coeff ((reindex e e : (a : Matrix n n R[X]) → Matrix m m R[X]) M.charmatrix i j) x)
Tactic: by_cases h : i = j