awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
rw :
  (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.graph =
    Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
⊢ f.inverse.graph = Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
have rw₁ : Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph =
  Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
Tactic: rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
⊢ f.inverse.toFun.range = f.domain
have rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.toFun.range = f.domain
Tactic: rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.toFun.range = f.domain
⊢ f.inverse.toFun.range = f.domain
have rw₁ : Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  f.domain
Tactic: rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.toFun.range = f.domain
rw₁ :
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.domain
⊢ f.inverse.toFun.range = f.domain
have rw₂ : Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  Submodule.map (LinearMap.fst R E F) f.graph
Tactic: rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.toFun.range = f.domain
rw₁ :
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.domain
rw₂ :
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.fst R E F) f.graph
⊢ f.inverse.toFun.range = f.domain
have rw₃ : Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  Submodule.map (LinearMap.snd R F E ∘ₗ (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E)) f.graph
Tactic: rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.toFun.range = f.domain
rw₁ :
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.domain
rw₂ :
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.fst R E F) f.graph
rw₃ :
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.snd R F E ∘ₗ (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E)) f.graph
⊢ f.inverse.toFun.range = f.domain
have rw₄ : Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph)
Tactic: rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
    ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
y : ↥f.inverse.domain
x : ↥f.domain
hxy : (↑f : ↥f.domain → F) x = (↑y : F)
⊢ (↑f.inverse : ↥f.inverse.domain → E) y = (↑x : E)
have this : ((↑f : ↥f.domain → F) x, (↑x : E)) ∈ f.inverse.graph
Tactic: have := mem_inverse_graph hf x
-- 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 α
⊢ IsLinearMap α A.cramerMap
have map_add : ∀ (x y : n → α), A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y
Tactic: constructor
-- 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 α
map_add : ∀ (x y : n → α), A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y
⊢ IsLinearMap α A.cramerMap
have map_smul : ∀ (c : α) (x : n → α), A.cramerMap (c • x) = c • A.cramerMap x
Tactic: constructor
-- 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 α
x y : n → α
⊢ A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y
have map_add : ∀ (i : n), A.cramerMap (x + y) i = (A.cramerMap x + A.cramerMap y) i
Tactic: ext i
-- 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 α
c : α
x : n → α
⊢ A.cramerMap (c • x) = c • A.cramerMap x
have map_smul : ∀ (i : n), A.cramerMap (c • x) i = (c • A.cramerMap x) i
Tactic: ext i
-- 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 α
b : n → α
i : n
⊢ (Aᵀ.cramer : (a : n → α) → n → α) b i = (A.updateRow i b).det
have rw : (Aᵀ.updateCol i b).det = (A.updateRow i b).det
Tactic: rw [cramer_apply, updateCol_transpose, det_transpose]
-- 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 α
b : n → α
i : n
rw : (Aᵀ.updateCol i b).det = (A.updateRow i b).det
⊢ (Aᵀ.cramer : (a : n → α) → n → α) b i = (A.updateRow i b).det
have rw₁ : (A.updateRow i b)ᵀ.det = (A.updateRow i b).det
Tactic: rw [cramer_apply, updateCol_transpose, det_transpose]
-- 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 α
b : n → α
i : n
rw : (Aᵀ.updateCol i b).det = (A.updateRow i b).det
rw₁ : (A.updateRow i b)ᵀ.det = (A.updateRow i b).det
⊢ (Aᵀ.cramer : (a : n → α) → n → α) b i = (A.updateRow i b).det
have rw₂ : (A.updateRow i b).det = (A.updateRow i b).det
Tactic: rw [cramer_apply, updateCol_transpose, det_transpose]
-- 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 α
i : n
⊢ Eq (α := n → α) ((Aᵀ.cramer : (a : n → α) → n → α) (A i) : n → α)
    (Pi.single (M := fun (j : n) ↦ α) i A.det : (j : n) → α)
have h : ∀ (j : n),
  Eq.{w + 1} (α := α) ((Aᵀ.cramer : (a : n → α) → n → α) (A i) j : α) (Pi.single (M := fun (j : n) ↦ α) i A.det j : α)
Tactic: ext j
-- 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 α
i j : n
⊢ Eq.{w + 1} (α := α) ((Aᵀ.cramer : (a : n → α) → n → α) (A i) j : α) (Pi.single (M := fun (j : n) ↦ α) i A.det j : α)
have h : (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0
Tactic: rw [cramer_apply, Pi.single_apply]
-- 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 α
i j : n
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0
have pos : ∀ (h : j = i), (Aᵀ.updateCol j (A i)).det = A.det
Tactic: split_ifs with h
-- 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 α
i j : n
pos : ∀ (h : j = i), (Aᵀ.updateCol j (A i)).det = A.det
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0
have neg : ∀ (h : ¬j = i), (Aᵀ.updateCol j (A i)).det = 0
Tactic: split_ifs with h
-- 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 α
i j : n
h : j = i
⊢ (Aᵀ.updateCol j (A i)).det = A.det
have pos : (Aᵀ.updateCol j (A j)).det = A.det
Tactic: subst h
Cleared hypotheses: i, h
-- 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 α
i j : n
h : ¬j = i
⊢ (Aᵀ.updateCol j (A i)).det = 0
have neg : (A.updateRow j (A i)).det = 0
Tactic: rw [updateCol_transpose, det_transpose]
-- 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 α
i j : n
h : ¬j = i
⊢ (A.updateRow j (A i)).det = 0
have neg : A.updateRow j (A i) j = A.updateRow j (A i) i
Tactic: apply det_zero_of_row_eq h
-- 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 α
i j : n
h : ¬j = i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i
have neg : A i = A.updateRow j (A i) i
Tactic: rw [updateRow_self, updateRow_ne (Ne.symm h)]
-- 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 α
i j : n
h : ¬j = i
neg : A i = A.updateRow j (A i) i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i
have neg₁ : A i = A i
Tactic: rw [updateRow_self, updateRow_ne (Ne.symm h)]
-- 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 α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ Eq (α := n → α) ((A.cramer : (a : n → α) → n → α) b : n → α) (Pi.single (M := fun (j : n) ↦ α) i A.det : (j : n) → α)
have rw : Eq (α := n → α) ((Aᵀᵀ.cramer : (a : n → α) → n → α) b : n → α) (Pi.single (M := fun (j : n) ↦ α) i Aᵀ.det : (j : n) → α)
Tactic: rw [← transpose_transpose A, det_transpose]
-- 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 α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ Eq (α := n → α) ((Aᵀᵀ.cramer : (a : n → α) → n → α) b : n → α)
    (Pi.single (M := fun (j : n) ↦ α) i Aᵀ.det : (j : n) → α)
have h₁ : b = Aᵀ i
Tactic: convert! cramer_transpose_row_self Aᵀ i
-- 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 α
⊢ Eq (α := (n → α) →ₗ[α] n → α) (cramer 1) 1
have h : ∀ (i j : n),
  Eq.{w + 1} (α := α) ((cramer 1 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((1 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
Tactic: ext i j
-- 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 α
i j : n
⊢ Eq.{w + 1} (α := α) ((cramer 1 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((1 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
have h : Eq.{w + 1} (α := α) 1 (det.{w, v} (n := n) 1)
Tactic: convert! congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
-- 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 α
i j : n
h : Eq.{w + 1} (α := α) 1 (det.{w, v} (n := n) 1)
⊢ Eq.{w + 1} (α := α) ((cramer 1 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((1 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
have h₁ : ∀ (j : n), Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (1 j i : α)
Tactic: convert! congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
-- 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 α
i j_1 j : n
⊢ Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (1 j i : α)
have h : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (Pi.single (M := fun (x : n) ↦ α) j 1 i : α)
Tactic: rw [Matrix.one_eq_pi_single, Pi.single_comm]
-- 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 α
i j_1 j : n
h : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (Pi.single (M := fun (x : n) ↦ α) j 1 i : α)
⊢ Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (1 j i : α)
have h₁ : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j 1 i : α) (Pi.single (M := fun (x : n) ↦ α) j 1 i : α)
Tactic: rw [Matrix.one_eq_pi_single, Pi.single_comm]
-- 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 α
inst_3 : Subsingleton n
A : Matrix n n α
b : n → α
i : n
⊢ (A.cramer : (a : n → α) → n → α) b i = b i
have rw : (A.updateCol i b).det = b i
Tactic: rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]
-- 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 α
inst_3 : Subsingleton n
A : Matrix n n α
b : n → α
i : n
rw : (A.updateCol i b).det = b i
⊢ (A.cramer : (a : n → α) → n → α) b i = b i
have rw₁ : A.updateCol i b i i = b i
Tactic: rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]
-- 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 α
inst_3 : Subsingleton n
A : Matrix n n α
b : n → α
i : n
rw : (A.updateCol i b).det = b i
rw₁ : A.updateCol i b i i = b i
⊢ (A.cramer : (a : n → α) → n → α) b i = b i
have rw₂ : b i = b i
Tactic: rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]
-- 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 α
inst_3 : Nontrivial n
⊢ Eq (α := (n → α) →ₗ[α] n → α) (cramer 0) 0
have h : ∀ (i j : n),
  Eq.{w + 1} (α := α) ((cramer 0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
Tactic: ext i j
-- 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 α
inst_3 : Nontrivial n
i j : n
⊢ Eq.{w + 1} (α := α) ((cramer 0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
have h : ∀ (j' : n) (hj' : j' ≠ j),
  Eq.{w + 1} (α := α) ((cramer 0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
Tactic: obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
-- 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 α
inst_3 : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ Eq.{w + 1} (α := α) ((cramer 0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : (a : α) → n → α) 1 j : α)
    (((0 ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] n → α) : (a : α) → n → α) 1 j : α)
have h : ∀ (i_1 : n),
  Eq.{w + 1} (α := α)
    (updateCol 0 j (((LinearMap.single α (fun (i : n) ↦ α) i : α →ₗ[α] (i : n) → α) : (a : α) → (i : n) → α) 1) i_1 j')
    0
Tactic: apply det_eq_zero_of_column_eq_zero j'
-- 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 α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ Eq.{w + 1} (α := α) ((∑ x ∈ s, (A.cramer : (a : n → α) → n → α) fun (j : n) ↦ f j x) i : α)
    ((A.cramer : (a : n → α) → n → α) (fun (j : n) ↦ ∑ x ∈ s, f j x) i : α)
have rw : (A.updateCol i (∑ x ∈ s, fun (j : n) ↦ f j x)).det = (A.cramer : (a : n → α) → n → α) (fun (j : n) ↦ ∑ x ∈ s, f j x) i
Tactic: rw [sum_cramer, cramer_apply]
-- 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 α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (A.updateCol i (∑ x ∈ s, fun (j : n) ↦ f j x)).det = (A.cramer : (a : n → α) → n → α) (fun (j : n) ↦ ∑ x ∈ s, f j x) i
have e_M : ∀ (j : n), Eq.{w + 1} (α := α) ((∑ x ∈ s, fun (j : n) ↦ f j x) j) (∑ x ∈ s, f j x)
Tactic: congr with j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
⊢ Eq (α := n → α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b : n → α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) :
      n → α)
have h : ∀ (i : n),
  Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) i :
      α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) i :
      α)
have h : Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
  ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)) ((e : (a : n) → m) i) : α)
Tactic: simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
h :
  Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)) ((e : (a : n) → m) i) : α)
⊢ Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) i :
      α)
have h₁ : (updateCol (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) i b).det =
  (A.updateCol ((e : (a : n) → m) i) (b ∘ (⇑e.symm : (a : m) → n))).det
Tactic: simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
h :
  Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)) ((e : (a : n) → m) i) : α)
h₁ :
  (updateCol (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) i b).det =
    (A.updateCol ((e : (a : n) → m) i) (b ∘ (⇑e.symm : (a : m) → n))).det
⊢ Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) i :
      α)
have h₂ : det.{w, v} (n := n)
    ((A.updateCol ((e : (a : n) → m) i) fun (i : m) ↦ b ((e.symm : (a : m) → n) i)).submatrix (⇑e : (a : n) → m)
      (⇑e : (a : n) → m)) =
  (A.updateCol ((e : (a : n) → m) i) (b ∘ (⇑e.symm : (a : m) → n))).det
Tactic: simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_def]