awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
Tactic: have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
    mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
have succ : Eq.{v + 1} (α := Matrix n n (MvPolynomial (n × n) ℤ))
  ((fun (x : Matrix n n (MvPolynomial (n × n) ℤ)) ↦ A'.det • x) A'.adjugate.adjugate)
  ((fun (x : Matrix n n (MvPolynomial (n × n) ℤ)) ↦ A'.det • x) (A'.det ^ (Fintype.card n - 2) • A'))
Tactic: apply is_reg.matrix
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • A'
have succ : A'.det • A'.adjugate.adjugate = (A'.det * A'.det ^ (Fintype.card n - 2)) • A'
Tactic: rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
succ : A'.det • A'.adjugate.adjugate = (A'.det * A'.det ^ (Fintype.card n - 2)) • A'
⊢ A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • A'
have succ₁ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2 + 1) • A'
Tactic: rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
succ : A'.det • A'.adjugate.adjugate = (A'.det * A'.det ^ (Fintype.card n - 2)) • A'
succ₁ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2 + 1) • A'
⊢ A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • A'
have succ₂ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 1) • A'
Tactic: rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
succ : A'.det • A'.adjugate.adjugate = (A'.det * A'.det ^ (Fintype.card n - 2)) • A'
succ₁ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2 + 1) • A'
succ₂ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 1) • A'
⊢ A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • A'
have succ₃ : A'.det ^ (Fintype.card n - 1) • A' = A'.det ^ (Fintype.card n - 1) • A'
Tactic: rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (goal)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
⊢ B i j ∈ K
have intro : ∀ (val : Fintype m), B i j ∈ K
Tactic: cases nonempty_fintype m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
⊢ B i j ∈ K
have hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
Tactic: have hA' : A'.map K.subtype = A.submatrix id e := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
⊢ IsUnit A'
have h_unit : IsUnit (M := Matrix m m L) (A.submatrix id (⇑e : (a : m) → n))
Tactic: have h_unit : IsUnit (A.submatrix id e) :=
      .of_mul_eq_one (B.submatrix e id) (by simpa)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
h_unit : IsUnit (M := Matrix m m L) (A.submatrix id (⇑e : (a : m) → n))
⊢ IsUnit A'
have h_det : det (A.submatrix id (⇑e : (a : m) → n)) = (K.subtype : (a : ↥K) → L) A'.det
Tactic: have h_det : (A.submatrix id e).det = K.subtype A'.det := by
      simp [A', K.subtype.map_det, map, submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
⊢ B i j ∈ K
have hA : IsUnit A'
Tactic: have hA : IsUnit A' := by
    have h_unit : IsUnit (A.submatrix id e) :=
      .of_mul_eq_one (B.submatrix e id) (by simpa)
    have h_det : (A.submatrix id e).det = K.subtype A'.det := by
      simp [A', K.subtype.map_det, map, submatrix]
    simpa [isUnit_iff_isUnit_det, h_det] using h_unit
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (goal)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
⊢ B i j ∈ K
have intro : ∀ (B' : Matrix.{u_1, u_1, u_3} m m ↥K) (hB : A' * B' = 1), B i j ∈ K
Tactic: obtain ⟨B', hB⟩ := isUnit_iff_exists_inv.mp hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (goal)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
⊢ B i j ∈ K
have intro : map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L) = B
Tactic: suffices (B'.submatrix e.symm id).map K.subtype = B by simp [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
⊢ HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1
have hB₁ : Eq (α := Matrix m m L)
  ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) (A' * B'))
  ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) 1)
Tactic: replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB :
  Eq (α := Matrix m m L)
    ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) (A' * B'))
    ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) 1)
⊢ HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1
have hB₁ : HMul.hMul (α := Matrix m m L) (A'.map (⇑K.subtype : (a : ↥K) → L)) (B'.map (⇑K.subtype : (a : ↥K) → L)) =
  map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)
Tactic: simp_rw [Matrix.map_mul] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB :
  HMul.hMul (α := Matrix m m L) (A'.map (⇑K.subtype : (a : ↥K) → L)) (B'.map (⇑K.subtype : (a : ↥K) → L)) =
    map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)
⊢ HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1
have hB₁ : HMul.hMul (β := Matrix n m L) (A.submatrix id id)
    (submatrix (B'.map (⇑K.subtype : (a : ↥K) → L)) (⇑e.symm : (a : n) → m) id) =
  map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)
Tactic: rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
⊢ map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L) = B
have hB₁ : HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1
Tactic: replace hB : A * (B'.submatrix e.symm id).map K.subtype = 1 := by
    replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
    simp_rw [Matrix.map_mul] at hB
    rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB
    simpa using hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (hypothesis)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ A i j ∈ K
have hAB₁ : Bᵀ * Aᵀ = 1
Tactic: replace hAB : Bᵀ * Aᵀ = 1 := by simpa using congr_arg transpose hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BaseChange (goal)
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ A i j ∈ K
have rw : Aᵀ j i ∈ K
Tactic: rw [← A.transpose_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
v : ι → M
⊢ e.toMatrix v = (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)
have a : ∀ (i j : ι),
  e.toMatrix v i j =
    (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
v : ι → M
i j : ι
⊢ e.toMatrix v i j =
    (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j
have a : Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
  ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j : R)
Tactic: rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
v : ι → M
i j : ι
a :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
    ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j : R)
⊢ e.toMatrix v i j =
    (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j
have a₁ : Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
  ((((e.repr : (a : M) → ι →₀ R)
            ((((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v : M →ₗ[R] M) : (a : M) → M) ((e : (a : ι) → M) j : M)) :
          ι →₀ R) :
        (a : ι) → R)
      i :
    R)
Tactic: rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
v : ι → M
i j : ι
a :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
    ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j : R)
a₁ :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
    ((((e.repr : (a : M) → ι →₀ R)
              ((((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v : M →ₗ[R] M) : (a : M) → M) ((e : (a : ι) → M) j : M)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
⊢ e.toMatrix v i j =
    (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j
have a₂ : Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
  ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Finite ι
⊢ Eq (α := (v : ι → ι → R) → Matrix ι ι R) (toMatrix (Pi.basisFun R ι)) transpose
have h : ∀ (M : ι → ι → R) (i j : ι), toMatrix (Pi.basisFun R ι) M i j = Mᵀ i j
Tactic: ext M i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : DecidableEq ι
⊢ Eq (α := Matrix ι ι R) (e.toMatrix (⇑e : (a : ι) → M)) 1
have unfold : Eq (α := Matrix ι ι R) (fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i)
  1
Tactic: unfold Basis.toMatrix
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : DecidableEq ι
⊢ Eq (α := Matrix ι ι R)
    (fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i) 1
have a : ∀ (i j : ι),
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i : R) (1 i j : R)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
⊢ e.toMatrix (update (β := fun (a : ι') ↦ M) v j x) =
    (e.toMatrix v).updateCol j (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)
have a : ∀ (i' : ι) (k : ι'),
  e.toMatrix (update (β := fun (a : ι') ↦ M) v j x) i' k =
    (e.toMatrix v).updateCol j (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' k
Tactic: ext i' k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ e.toMatrix (update (β := fun (a : ι') ↦ M) v j x) i' k =
    (e.toMatrix v).updateCol j (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' k
have a : Eq.{u_5 + 1} (α := R)
  ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
  (if k = j then (((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i'
    else (((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' :
    R)
Tactic: rw [Basis.toMatrix, Matrix.updateCol_apply, e.toMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    (if k = j then (((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i'
      else (((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' :
      R)
have pos : ∀ (h : k = j),
  Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
pos :
  ∀ (h : k = j),
    Eq.{u_5 + 1} (α := R)
      ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
      ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    (if k = j then (((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i'
      else (((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' :
      R)
have neg : ∀ (h : ¬k = j),
  Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
have pos : Eq.{u_5 + 1} (α := R)
  ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x j) : ι →₀ R) : (a : ι) → R) i' : R)
  ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
Tactic: rw [h, update_self j x v]