awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearPMap
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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = (x_fst, x_snd).2

Tactic:
exact (existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx

Premises used: Submodule.existsUnique_from_graph, ExistsUnique.unique, Submodule.valFromGraph_mem
-- Module: Mathlib.LinearAlgebra.LinearPMap
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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
rwa : map (LinearMap.snd R E F) g.toLinearPMap.graph = map (LinearMap.snd R E F) g
rwa₁ : map (LinearMap.snd R E F) g = map (LinearMap.snd R E F) g
hg₁ : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
rwa₂ : map (LinearMap.snd R E F) g = map (LinearMap.snd R E F) g
hg₂ hg₃ hg₄ : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g

Tactic:
rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]

Premises used: Submodule.toLinearPMap_graph_eq, LinearPMap.graph_map_snd_eq_range
-- Module: Mathlib.LinearAlgebra.LinearPMap
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
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.domain = f.toFun.range
rw₁ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.toFun.range
rw₂ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.snd R E F) f.graph
rw₃ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.fst R F E ∘ₗ (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E)) f.graph
rw₄ rw₅ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph)
⊢ f.inverse.domain = f.toFun.range

Tactic:
rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]

Premises used: LinearPMap.inverse, LinearEquiv.fst_comp_prodComm, Submodule.map_comp, Submodule.toLinearPMap_domain, LinearPMap.graph_map_snd_eq_range
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 = ⊥
x : F × E
hv : x ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
hv' : x.1 = 0
rcases :
  ∀ (x : F) (y : E) (hv : (x, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph)
    (hv' : (x, y).1 = 0), (x, y).2 = 0
⊢ x.2 = 0

Tactic:
rcases x with ⟨x, y⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 = ⊥
x : F
y : E
hv : (x, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
hv' : (x, y).1 = 0
subst : ∀ (hv : (0, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph), (0, y).2 = 0
⊢ (x, y).2 = 0

Tactic:
subst hv'
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 : E
hv : (0, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
⊢ ∃ (y_1 : ↥f.domain), (↑y_1 : E) = y ∧ (↑f : ↥f.domain → F) y_1 = 0

Tactic:
simp only [Submodule.map_equiv_eq_comap_symm, Submodule.mem_comap, LinearEquiv.symm_prodComm,
    LinearEquiv.coe_coe, LinearEquiv.prodComm_apply, mem_graph_iff, Prod.swap] at hv

Premises used: Submodule.mem_comap, LinearEquiv.prodComm_apply, Submodule.map_equiv_eq_comap_symm, LinearPMap.mem_graph_iff, Prod.swap, LinearEquiv.symm_prodComm, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 : E
hv : ∃ (y_1 : ↥f.domain), (↑y_1 : E) = y ∧ (↑f : ↥f.domain → F) y_1 = 0
rcases : ∀ (z : ↥f.domain) (hz : (↑f : ↥f.domain → F) z = 0), (0, (↑z : E)).2 = 0
⊢ (0, y).2 = 0

Tactic:
rcases hv with ⟨z, rfl, hz⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 = ⊥
z : ↥f.domain
hz : (↑f : ↥f.domain → F) z = 0
rw :
  ∀ (hf : ∀ (m : ↥f.domain), Eq.{u_5 + 1} (α := F) ((f.toFun : (a : ↥f.domain) → F) m : F) (0 : F) → m = 0)
    (z : ↥f.domain) (hz : (↑f : ↥f.domain → F) z = 0), (0, (↑z : E)).2 = 0
⊢ (0, (↑z : E)).2 = 0

Tactic:
rw [LinearMap.ker_eq_bot'] at hf

Premises used: LinearMap.ker_eq_bot'
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 : ∀ (m : ↥f.domain), Eq.{u_5 + 1} (α := F) ((f.toFun : (a : ↥f.domain) → F) m : F) (0 : F) → m = 0
z : ↥f.domain
hz : (↑f : ↥f.domain → F) z = 0
⊢ (0, (↑z : E)).2 = 0

Tactic:
simp [hf z hz]
-- Module: Mathlib.LinearAlgebra.LinearPMap
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
rw₁ 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
⊢ f.inverse.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)]

Premises used: LinearPMap.inverse, LinearPMap.mem_inverse_graph_snd_eq_zero, Submodule.toLinearPMap_graph_eq
-- Module: Mathlib.LinearAlgebra.LinearPMap
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
rw₄ 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)
⊢ f.inverse.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]

Premises used: LinearPMap.inverse, Submodule.toLinearPMap_range, Submodule.map_comp, LinearEquiv.snd_comp_prodComm, LinearPMap.mem_inverse_graph_snd_eq_zero, LinearPMap.graph_map_fst_eq_domain
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 = ⊥
x : ↥f.domain
⊢ ∃ (a : E) (b : F),
    (∃ (h : a ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) a ⋯) = b) ∧
      b = (↑f : ↥f.domain → F) x ∧ a = (↑x : E)

Tactic:
⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩

Premises used: And.intro, Exists.intro, Eq.refl, Subtype.val, Subtype.property, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 = ⊥
x : ↥f.domain
⊢ ∃ (a : E) (b : F),
    (∃ (h : a ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) a ⋯) = b) ∧
      b = (↑f : ↥f.domain → F) x ∧ a = (↑x : E)

Tactic:
exact ⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
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 : ↥f.domain → F) x, (↑x : E)) ∈ f.inverse.graph

Tactic:
have := mem_inverse_graph hf x
-- Module: Mathlib.LinearAlgebra.LinearPMap
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)
this : ((↑f : ↥f.domain → F) x, (↑x : E)) ∈ f.inverse.graph
⊢ (↑f.inverse : ↥f.inverse.domain → E) y = (↑x : E)

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
⊢ IsLinearMap α (M₂ := α) fun (b : n → α) ↦ A.cramerMap b i

Tactic:
{ map_add := det_updateCol_add _ _
    map_smul := det_updateCol_smul _ _ }

Premises used: Matrix.det_updateCol_add, Matrix.det_updateCol_smul, IsLinearMap.mk
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
map_smul : ∀ (c : α) (x : n → α), A.cramerMap (c • x) = c • A.cramerMap x
⊢ IsLinearMap α A.cramerMap

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
x y : n → α
map_add : ∀ (i : n), A.cramerMap (x + y) i = (A.cramerMap x + A.cramerMap y) i
⊢ A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
c : α
x : n → α
map_smul : ∀ (i : n), A.cramerMap (c • x) i = (c • A.cramerMap x) i
⊢ A.cramerMap (c • x) = c • A.cramerMap x

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
x y : n → α
i : n
⊢ A.cramerMap (x + y) i = (A.cramerMap x + A.cramerMap y) i

Tactic:
apply (cramerMap_is_linear A i).1

Premises used: Matrix.cramerMap_is_linear, IsLinearMap.map_add
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
c : α
x : n → α
i : n
⊢ A.cramerMap (c • x) i = (c • A.cramerMap x) i

Tactic:
apply (cramerMap_is_linear A i).2

Premises used: Matrix.cramerMap_is_linear, IsLinearMap.map_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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.updateCol i b).det

Tactic:
rfl

Premises used: Matrix.cramerMap, Matrix.det, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw₂ rw₃ : (A.updateRow i b).det = (A.updateRow i b).det
⊢ (Aᵀ.cramer : (a : n → α) → n → α) b i = (A.updateRow i b).det

Tactic:
rw [cramer_apply, updateCol_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.cramer_apply, Matrix.updateCol_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
h :
  ∀ (j : n),
    Eq.{w + 1} (α := α) ((Aᵀ.cramer : (a : n → α) → n → α) (A i) j : α) (Pi.single (M := fun (j : n) ↦ α) i A.det j : α)
⊢ Eq (α := n → α) ((Aᵀ.cramer : (a : n → α) → n → α) (A i) : n → α)
    (Pi.single (M := fun (j : n) ↦ α) i A.det : (j : n) → α)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
h : (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0
⊢ Eq.{w + 1} (α := α) ((Aᵀ.cramer : (a : n → α) → n → α) (A i) j : α) (Pi.single (M := fun (j : n) ↦ α) i A.det j : α)

Tactic:
rw [cramer_apply, Pi.single_apply]

Premises used: Pi.single_apply, Matrix.cramer_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
neg : ∀ (h : ¬j = i), (Aᵀ.updateCol j (A i)).det = 0
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
pos : (Aᵀ.updateCol j (A j)).det = A.det
⊢ (Aᵀ.updateCol j (A i)).det = A.det

Tactic:
subst h
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
j : n
⊢ (Aᵀ.updateCol j (A j)).det = A.det

Tactic:
simp only [updateCol_transpose, det_transpose, updateRow_eq_self]

Premises used: Matrix.det_transpose, Matrix.updateRow_eq_self, Matrix.updateCol_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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.updateRow j (A i)).det = 0
⊢ (Aᵀ.updateCol j (A i)).det = 0

Tactic:
rw [updateCol_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.updateCol_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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.updateRow j (A i) j = A.updateRow j (A i) i
⊢ (A.updateRow j (A i)).det = 0

Tactic:
apply det_zero_of_row_eq h

Premises used: Matrix.det_zero_of_row_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
neg₁ neg₂ : A i = A i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i

Tactic:
rw [updateRow_self, updateRow_ne (Ne.symm h)]

Premises used: Ne.symm, Matrix.updateRow_ne, Matrix.updateRow_self
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw :
  Eq (α := n → α) ((Aᵀᵀ.cramer : (a : n → α) → n → α) b : n → α)
    (Pi.single (M := fun (j : n) ↦ α) i Aᵀ.det : (j : n) → α)
⊢ 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]

Premises used: Matrix.det_transpose, Matrix.transpose_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 → α) (Aᵀ i) : n → α)
    (Pi.single (M := fun (j : n) ↦ α) i Aᵀ.det : (j : n) → α)

Tactic:
cramer_transpose_row_self Aᵀ i

Premises used: Matrix.cramer_transpose_row_self, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
h₁ : b = Aᵀ i
⊢ Eq (α := n → α) ((Aᵀᵀ.cramer : (a : n → α) → n → α) b : n → α)
    (Pi.single (M := fun (j : n) ↦ α) i Aᵀ.det : (j : n) → α)

Tactic:
convert! cramer_transpose_row_self Aᵀ i

Premises used: Matrix.cramer_transpose_row_self, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
⊢ b = Aᵀ i

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
⊢ b = Aᵀ i

Tactic:
exact funext h

Premises used: funext
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
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 : α)
⊢ Eq (α := (n → α) →ₗ[α] n → α) (cramer 1) 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
i j : n
⊢ Eq.{w + 1} (α := α) ((cramer 1 : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1) j : α)
    (Pi.single (M := fun (j : n) ↦ α) i (det.{w, v} (n := n) 1) j : α)

Tactic:
congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j

Premises used: Matrix.cramer_row_self, Pi.single, congr_fun, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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)
h₁ : ∀ (j : n), Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (1 j i : α)
⊢ 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:
convert! congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j

Premises used: Matrix.cramer_row_self, Pi.single, congr_fun, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
i j : n
⊢ Eq.{w + 1} (α := α) 1 (det.{w, v} (n := n) 1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 : α)
h₁ h₂ : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j 1 i : α) (Pi.single (M := fun (x : n) ↦ α) j 1 i : α)
⊢ Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 j : α) (1 j i : α)

Tactic:
rw [Matrix.one_eq_pi_single, Pi.single_comm]

Premises used: Matrix.one_eq_pi_single, Pi.single_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
r : α
A : Matrix n n α
⊢ (r • A).cramer = HSMul.hSMul (β := (n → α) →ₗ[α] n → α) (r ^ (Fintype.card n - 1)) A.cramer

Tactic:
LinearMap.ext fun _ => funext fun _ => det_updateCol_smul_left _ _ _ _

Premises used: LinearMap.ext, funext, Matrix.det_updateCol_smul_left
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
rw₂ rw₃ : b i = b i
⊢ (A.cramer : (a : n → α) → n → α) b i = b i

Tactic:
rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]

Premises used: Matrix.updateCol_self, Matrix.cramer_apply, Matrix.det_eq_elem_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
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 : α)
⊢ Eq (α := (n → α) →ₗ[α] n → α) (cramer 0) 0

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
i j : n
⊢ ∃ (j' : n), j' ≠ j

Tactic:
exists_ne j

Premises used: exists_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
i j : n
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 : α)
⊢ 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

Premises used: exists_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
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
⊢ 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:
apply det_eq_zero_of_column_eq_zero j'

Premises used: Matrix.det_eq_zero_of_column_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
⊢ ∀ (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:
simp [updateCol_ne hj']

Premises used: Matrix.updateCol_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 → α
⊢ Eq (α := n → α) (∑ x ∈ s, (A.cramer : (a : n → α) → n → α) (f x) : n → α)
    ((A.cramer : (a : n → α) → n → α) (∑ x ∈ s, f x) : n → α)

Tactic:
(map_sum (cramer A) ..).symm

Premises used: Matrix.cramer, map_sum, Eq.symm