awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
⊢ (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
have mpr : ∀ (h : (D - Bᴴ * A⁻¹ * B).PosSemidef) (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
Tactic: refine fun h => ⟨h.1, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
have mpr : 0 ≤
  star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
    star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Tactic: rw [dotProduct_mulVec, ← Sum.elim_comp_inl_inr x, schur_complement_eq₁₁ B D _ _ hA.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
have mpr : 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
Tactic: apply le_add_of_nonneg_of_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
mpr : 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
⊢ 0 ≤
    star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) +
      star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
have mpr₁ : 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Tactic: apply le_add_of_nonneg_of_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
have mpr : 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ⬝ᵥ A *ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)
Tactic: rw [← dotProduct_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype m
inst_4 : StarOrderedRing R'
inst_5 : Finite n
inst_6 : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst_7 : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
have mpr : 0 ≤ star (x ∘ Sum.inr) ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x ∘ Sum.inr
Tactic: rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : StarOrderedRing R'
inst_5 : Finite m
inst_6 : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst_7 : Invertible D
⊢ (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
have rw : (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
Tactic: rw [← posSemidef_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
    fromBlocks_submatrix_sum_swap_sum_swap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : StarOrderedRing R'
inst_5 : Finite m
inst_6 : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst_7 : Invertible D
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
have h : B = Bᴴᴴ
Tactic: convert! fromBlocks₁₁ Bᴴ A hD
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ QuadraticMap.PosDef Q
have rw : QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
  (LinearMap.BilinMap.toQuadraticMap
    (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
      (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
        (LinearMap.toAddHom
          ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
            ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
        (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
            (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
          Q))))
Tactic: rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : QuadraticMap.PosDef Q
⊢ Q.toMatrix'.PosDef
have hQ₁ : QuadraticMap.PosDef.{0, u_1, 0} (M := n → ℝ) (N := ℝ)
  (LinearMap.BilinMap.toQuadraticMap
    (LinearEquiv.invFun (LinearMap.toMatrix₂' ℝ : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) ≃ₗ[ℝ] Matrix n n ℝ)
      (AddHom.toFun (M := (n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ)
        (LinearMap.toAddHom
          ((↑(LinearMap.toMatrix₂' ℝ) : ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ) :
            ((n → ℝ) →ₗ[ℝ] (n → ℝ) →ₗ[ℝ] ℝ) →ₗ[ℝ] Matrix n n ℝ))
        (((QuadraticMap.associatedHom ℝ : QuadraticMap ℝ (n → ℝ) ℝ →ₗ[ℝ] LinearMap.BilinMap ℝ (n → ℝ) ℝ) :
            (a : QuadraticMap ℝ (n → ℝ) ℝ) → LinearMap.BilinMap ℝ (n → ℝ) ℝ)
          Q))))
Tactic: rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)] at hQ
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Reindex (goal)
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ Eq (α := Matrix m n A ≃ₗ[R] Matrix m'' n'' A) (reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂')
    (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
have h : ∀ (x : Matrix m n A) (i : m'') (j : n''),
  Eq.{u_12 + 1} (α := A)
    ((reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂' : (a : Matrix m n A) → Matrix m'' n'' A) x i j :
      A)
    ((reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : (a : Matrix m n A) → Matrix m'' n'' A) x i j : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Reindex (goal)
Goal:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ Eq (α := Matrix m n A → Matrix m'' n'' A)
    (Function.comp (β := Matrix m' n' A) (⇑(reindexLinearEquiv R A e₁' e₂') : (a : Matrix m' n' A) → Matrix m'' n'' A)
      (⇑(reindexLinearEquiv R A e₁ e₂) : (a : Matrix m n A) → Matrix m' n' A))
    (⇑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) : (a : Matrix m n A) → Matrix m'' n'' A)
have rw : Eq (α := Matrix m n A → Matrix m'' n'' A)
  (Function.comp (β := Matrix m' n' A) (⇑(reindexLinearEquiv R A e₁' e₂') : (a : Matrix m' n' A) → Matrix m'' n'' A)
    (⇑(reindexLinearEquiv R A e₁ e₂) : (a : Matrix m n A) → Matrix m' n' A))
  (⇑(reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂') : (a : Matrix m n A) → Matrix m'' n'' A)
Tactic: rw [← reindexLinearEquiv_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : MulOneClass R
x : n → R
⊢ vecMulVec x 1 = replicateCol m x
have a : ∀ (i : n) (j : m), vecMulVec x 1 i j = replicateCol m x i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : MulOneClass R
x : n → R
⊢ vecMulVec 1 x = replicateRow m x
have a : ∀ (i : m) (j : n), vecMulVec 1 x i j = replicateRow m x i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Nonempty ι
⊢ Function.Injective (α := m → α) (replicateCol ι)
have inhabit : ∀ (inhabited_h : Inhabited ι), Function.Injective (α := m → α) (replicateCol ι)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Add α
v w : m → α
⊢ replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w
have a : ∀ (i : m) (j : ι), replicateCol ι (v + w) i j = (replicateCol ι v + replicateCol ι w) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst : SMul R α
x : R
v : m → α
⊢ replicateCol ι (x • v) = x • replicateCol ι v
have a : ∀ (i : m) (j : ι), replicateCol ι (x • v) i j = (x • replicateCol ι v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Nonempty ι
⊢ Function.Injective (α := n → α) (replicateRow ι)
have inhabit : ∀ (inhabited_h : Inhabited ι), Function.Injective (α := n → α) (replicateRow ι)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Add α
v w : m → α
⊢ replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w
have a : ∀ (i : ι) (j : m), replicateRow ι (v + w) i j = (replicateRow ι v + replicateRow ι w) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst : SMul R α
x : R
v : m → α
⊢ replicateRow ι (x • v) = x • replicateRow ι v
have a : ∀ (i : ι) (j : m), replicateRow ι (x • v) i j = (x • replicateRow ι v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (replicateCol ι v)ᵀ = replicateRow ι v
have a : ∀ (i : ι) (j : m), (replicateCol ι v)ᵀ i j = replicateRow ι v i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (replicateRow ι v)ᵀ = replicateCol ι v
have a : ∀ (i : m) (j : ι), (replicateRow ι v)ᵀ i j = replicateCol ι v i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Star α
v : m → α
⊢ (replicateCol ι v)ᴴ = replicateRow ι (star v)
have a : ∀ (i : ι) (j : m), (replicateCol ι v)ᴴ i j = replicateRow ι (star v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Star α
v : m → α
⊢ (replicateRow ι v)ᴴ = replicateCol ι (star v)
have a : ∀ (i : m) (j : ι), (replicateRow ι v)ᴴ i j = replicateCol ι (star v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ replicateRow ι (v ᵥ* M) = replicateRow ι v * M
have a : ∀ (i : ι) (j : n), replicateRow ι (v ᵥ* M) i j = (replicateRow ι v * M) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ replicateCol ι (v ᵥ* M) = (replicateRow ι v * M)ᵀ
have a : ∀ (i : n) (j : ι), replicateCol ι (v ᵥ* M) i j = (replicateRow ι v * M)ᵀ i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ replicateCol ι (M *ᵥ v) = M * replicateCol ι v
have a : ∀ (i : m) (j : ι), replicateCol ι (M *ᵥ v) i j = (M * replicateCol ι v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ
have a : ∀ (i : ι) (j : m), replicateRow ι (M *ᵥ v) i j = (M * replicateCol ι v)ᵀ i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Mul α
inst_1 : AddCommMonoid α
inst_2 : Unique ι
a b : n → α
⊢ (replicateCol ι a * replicateRow ι b).diag = a * b
have h : ∀ (x : n), (replicateCol ι a * replicateRow ι b).diag x = (a * b) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Mul α
inst_1 : AddCommMonoid α
inst_2 : Unique ι
w : m → α
v : n → α
⊢ vecMulVec w v = replicateCol ι w * replicateRow ι v
have a : ∀ (i : m) (j : n), vecMulVec w v i j = (replicateCol ι w * replicateRow ι v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have pos : ∀ (h : i' = i), M.updateRow i b i' j = if i' = i then b j else M i' j
Tactic: by_cases h : i' = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
pos : ∀ (h : i' = i), M.updateRow i b i' j = if i' = i then b j else M i' j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have neg : ∀ (h : ¬i' = i), M.updateRow i b i' j = if i' = i then b j else M i' j
Tactic: by_cases h : i' = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have pos : M.updateRow i b i j = if i = i then b j else M i j
Tactic: rw [h, updateRow_self, if_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : i' = i
pos : M.updateRow i b i j = if i = i then b j else M i j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have pos₁ : b j = if i = i then b j else M i j
Tactic: rw [h, updateRow_self, if_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : i' = i
pos : M.updateRow i b i j = if i = i then b j else M i j
pos₁ : b j = if i = i then b j else M i j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have pos₂ : b j = b j
Tactic: rw [h, updateRow_self, if_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have neg : M i' j = if i' = i then b j else M i' j
Tactic: rw [updateRow_ne h, if_neg h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : ¬i' = i
neg : M i' j = if i' = i then b j else M i' j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
have neg₁ : M i' j = M i' j
Tactic: rw [updateRow_ne h, if_neg h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have pos : ∀ (h : j' = j), M.updateCol j c i j' = if j' = j then c i else M i j'
Tactic: by_cases h : j' = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
pos : ∀ (h : j' = j), M.updateCol j c i j' = if j' = j then c i else M i j'
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have neg : ∀ (h : ¬j' = j), M.updateCol j c i j' = if j' = j then c i else M i j'
Tactic: by_cases h : j' = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have pos : M.updateCol j c i j = if j = j then c i else M i j
Tactic: rw [h, updateCol_self, if_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : j' = j
pos : M.updateCol j c i j = if j = j then c i else M i j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have pos₁ : c i = if j = j then c i else M i j
Tactic: rw [h, updateCol_self, if_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : j' = j
pos : M.updateCol j c i j = if j = j then c i else M i j
pos₁ : c i = if j = j then c i else M i j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have pos₂ : c i = c i
Tactic: rw [h, updateCol_self, if_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have neg : M i j' = if j' = j then c i else M i j'
Tactic: rw [updateCol_ne h, if_neg h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : ¬j' = j
neg : M i j' = if j' = j then c i else M i j'
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'
have neg₁ : M i j' = M i j'
Tactic: rw [updateCol_ne h, if_neg h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : Subsingleton n
A : Matrix m n R
i : n
b : m → R
⊢ A.updateCol i b = submatrix (n := Fin 1) (replicateCol (Fin 1) b) id (Function.const n 0)
have a : ∀ (x : m) (y : n), A.updateCol i b x y = submatrix (n := Fin 1) (replicateCol (Fin 1) b) id (Function.const n 0) x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : Subsingleton m
A : Matrix m n R
i : m
b : n → R
⊢ A.updateRow i b = submatrix (m := Fin 1) (replicateRow (Fin 1) b) (Function.const m 0) id
have a : ∀ (x : m) (y : n), A.updateRow i b x y = submatrix (m := Fin 1) (replicateRow (Fin 1) b) (Function.const m 0) id x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
f : α → β
⊢ (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)
have a : ∀ (i_1 : m) (j : n), (M.updateRow i b).map f i_1 j = (M.map f).updateRow i (f ∘ b) i_1 j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
f : α → β
i_1 : m
j : n
⊢ (M.updateRow i b).map f i_1 j = (M.map f).updateRow i (f ∘ b) i_1 j
have a : f (if i_1 = i then b j else M i_1 j) = if i_1 = i then (f ∘ b) j else f (M i_1 j)
Tactic: rw [updateRow_apply, map_apply, map_apply, updateRow_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
f : α → β
⊢ (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)
have a : ∀ (i : m) (j_1 : n), (M.updateCol j c).map f i j_1 = (M.map f).updateCol j (f ∘ c) i j_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
f : α → β
i : m
j_1 : n
⊢ (M.updateCol j c).map f i j_1 = (M.map f).updateCol j (f ∘ c) i j_1
have a : f (if j_1 = j then c i else M i j_1) = if j_1 = j then (f ∘ c) i else f (M i j_1)
Tactic: rw [updateCol_apply, map_apply, map_apply, updateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
⊢ Mᵀ.updateRow j c = (M.updateCol j c)ᵀ
have a : ∀ (i : n) (j_1 : m), Mᵀ.updateRow j c i j_1 = (M.updateCol j c)ᵀ i j_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
i : n
j_1 : m
⊢ Mᵀ.updateRow j c i j_1 = (M.updateCol j c)ᵀ i j_1
have a : (if i = j then c j_1 else Mᵀ i j_1) = if i = j then c j_1 else M j_1 i
Tactic: rw [transpose_apply, updateRow_apply, updateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
⊢ Mᵀ.updateCol i b = (M.updateRow i b)ᵀ
have a : ∀ (i_1 : n) (j : m), Mᵀ.updateCol i b i_1 j = (M.updateRow i b)ᵀ i_1 j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
i_1 : n
j : m
⊢ Mᵀ.updateCol i b i_1 j = (M.updateRow i b)ᵀ i_1 j
have a : (if j = i then b i_1 else Mᵀ i_1 j) = if j = i then b i_1 else M j i_1
Tactic: rw [transpose_apply, updateRow_apply, updateCol_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
inst_1 : Star α
⊢ Mᴴ.updateRow j (star c) = (M.updateCol j c)ᴴ
have rw : ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ
Tactic: rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateRow_transpose,
    map_updateCol]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
inst_1 : Star α
⊢ Mᴴ.updateCol i (star b) = (M.updateRow i b)ᴴ
have rw : ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ
Tactic: rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateCol_transpose,
    map_updateRow]