awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Circulant (goal)
Goal:
α : Type u_1
n : Type u_3
inst : SubtractionMonoid n
v : n → α
rw : (circulant v)ᵀ = circulant v ↔ ∀ (i : n), v (-i) = v i
rw₁ : (circulant fun (i : n) ↦ v (-i)) = circulant v ↔ ∀ (i : n), v (-i) = v i
rw₂ : (fun (i : n) ↦ v (-i)) = v ↔ ∀ (i : n), v (-i) = v i
⊢ (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
have rw₃ : (∀ (x : n), v (-x) = v x) ↔ ∀ (i : n), v (-i) = v i
Tactic: rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : DecidableEq m
inst_2 : AddMonoid α
inst_3 : StarAddMonoid α
i : m
j : n
a : α
⊢ (single i j a)ᴴ = single j i (star a)
have change : (single i j a)ᵀ.map (⇑starAddEquiv : (a : α) → α) = single j i (star a)
Tactic: change (single i j a).transpose.map starAddEquiv = single j i (star a)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᴴ = diagonal (star v)
have rw : (diagonal fun (m : n) ↦ star (v m)) = diagonal (star v)
Tactic: rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Mul α
inst_1 : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec (star v) (star w))ᵀ
have rw : (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ
Tactic: rw [← conjTranspose_vecMulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v)ᴴ ↔ M = diagonal (star v)
have rw : M = diagonal (star v) ↔ M = diagonal (star v)
Tactic: rw [diagonal_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v).map star ↔ M = diagonal (star v)
have rw : M = diagonal (star v) ↔ M = diagonal (star v)
Tactic: rw [map_diagonal_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
M : Matrix m n α
⊢ Mᴴ = 0 ↔ M = 0
have rw : Mᴴ = 0 ↔ Mᴴ = 0ᴴ
Tactic: rw [← conjTranspose_inj (A := M), conjTranspose_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
inst_1 : StarAddMonoid α
M : Matrix m n α
rw : Mᴴ = 0 ↔ Mᴴ = 0ᴴ
⊢ Mᴴ = 0 ↔ M = 0
have rw₁ : Mᴴ = 0 ↔ Mᴴ = 0
Tactic: rw [← conjTranspose_inj (A := M), conjTranspose_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
⊢ M = 1ᴴ ↔ M = 1
have rw : M = 1 ↔ M = 1
Tactic: rw [conjTranspose_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
d : ℕ
⊢ M = (↑d : Matrix n n α)ᴴ ↔ M = (↑d : Matrix n n α)
have rw : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
Tactic: rw [conjTranspose_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : StarRing α
M : Matrix n n α
d : ℕ
⊢ M = map (↑d : Matrix n n α) star ↔ M = (↑d : Matrix n n α)
have rw : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
Tactic: rw [map_natCast_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Ring α
inst_2 : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = (↑d : Matrix n n α)ᴴ ↔ M = (↑d : Matrix n n α)
have rw : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
Tactic: rw [conjTranspose_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Ring α
inst_2 : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = map (↑d : Matrix n n α) star ↔ M = (↑d : Matrix n n α)
have rw : M = (↑d : Matrix n n α) ↔ M = (↑d : Matrix n n α)
Tactic: rw [map_intCast_star]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ConjTranspose (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : StarRing R
inst_3 : TrivialStar R
inst_4 : Semiring α
inst_5 : StarRing α
inst_6 : Algebra R α
inst_7 : StarModule R α
r : R
M : Matrix n n α
⊢ (RingEquiv.toEquiv (StarRingEquiv.toRingEquiv (conjTransposeRingEquiv n α))).toFun (r • M) =
    r • (RingEquiv.toEquiv (StarRingEquiv.toRingEquiv (conjTransposeRingEquiv n α))).toFun M
have change : (conjTransposeRingEquiv n α : (a : Matrix n n α) → (Matrix n n α)ᵐᵒᵖ) (r • M) =
  HSMul.hSMul (β := (Matrix n n α)ᵐᵒᵖ) r
    ((conjTransposeRingEquiv n α : (a : Matrix n n α) → (Matrix n n α)ᵐᵒᵖ) M : (Matrix n n α)ᵐᵒᵖ)
Tactic: change conjTransposeRingEquiv n α (r • M) = r • conjTransposeRingEquiv n α M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ M.map id = M
have a : ∀ (i : m) (j : n), M.map id i j = M i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
⊢ (M.map f).map g = M.map (g ∘ f)
have a : ∀ (i : m) (j : n), (M.map f).map g i j = M.map (g ∘ f) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
⊢ dite P A B i j = if x : P then A x i j else B x i j
have pos : ∀ (h : P), dite P A B i j = if x : P then A x i j else B x i j
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
pos : ∀ (h : P), dite P A B i j = if x : P then A x i j else B x i j
⊢ dite P A B i j = if x : P then A x i j else B x i j
have neg : ∀ (h : ¬P), dite P A B i j = if x : P then A x i j else B x i j
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst : Zero α
inst_1 : Zero β
f : α → β
h : f 0 = 0
⊢ Eq (α := Matrix m n β) (map 0 f) 0
have a : ∀ (i : m) (j : n), map 0 f i j = 0 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty m
M N : Matrix m n α
⊢ M = N
have a : ∀ (i : m) (j : n), M i j = N i j
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : IsEmpty n
M N : Matrix m n α
⊢ M = N
have a : ∀ (i : m) (j : n), M i j = N i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : AddMonoid α
A : Matrix m n α
⊢ IsAddUnit A ↔ ∀ (i : m) (j : n), IsAddUnit (A i j)
have simp_rw : (∃ (b : Matrix m n α), (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
  ∃ (f : (x : m) → (x : n) → α),
    (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0
Tactic: simp_rw [isAddUnit_iff_exists, Classical.skolem, forall_and,
    ← Matrix.ext_iff, add_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ Mᵀᵀ = M
have a : ∀ (i : m) (j : n), Mᵀᵀ i j = M i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Add α
M N : Matrix m n α
⊢ (M + N)ᵀ = Mᵀ + Nᵀ
have a : ∀ (i : n) (j : m), (M + N)ᵀ i j = (Mᵀ + Nᵀ) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : Sub α
M N : Matrix m n α
⊢ (M - N)ᵀ = Mᵀ - Nᵀ
have a : ∀ (i : n) (j : m), (M - N)ᵀ i j = (Mᵀ - Nᵀ) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Defs (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
S : Set α
⊢ Eq (α := Set (Matrix m n α)) S.matrix
    (preimage (β := m → n → α) (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)
      (pi (α := fun (a : m) ↦ n → α) univ fun (x : m) ↦ pi (α := fun (a : n) ↦ α) univ fun (x : n) ↦ S))
have h : ∀ (x : Matrix m n α),
  Membership.mem (γ := Set (Matrix m n α)) S.matrix x ↔
    Membership.mem (γ := Set (Matrix m n α))
      (preimage (β := m → n → α) (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)
        (pi (α := fun (a : m) ↦ n → α) univ fun (x : m) ↦ pi (α := fun (a : n) ↦ α) univ fun (x : n) ↦ S))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ M.det = detp 1 M - detp (-1) M
have rw : HAdd.hAdd (α := R)
    (∑ x ∈ ofSign 1,
      HSMul.hSMul (α := ℤˣ) (β := R)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
        (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i))
    (∑ x ∈ ofSign (-1),
      HSMul.hSMul (α := ℤˣ) (β := R)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
        (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i)) =
  detp 1 M - detp (-1) M
Tactic: rw [det_apply, ← Equiv.sum_comp (Equiv.inv (Perm n)), ← ofSign_disjUnion, sum_disjUnion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R)
          (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
          (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R)
          (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
          (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i)) =
    detp 1 M - detp (-1) M
have simp_rw : HAdd.hAdd (α := R)
    (∑ x ∈ ofSign 1,
      HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
        (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1))
    (∑ x ∈ ofSign (-1),
      HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
        (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1)) =
  HAdd.hAdd (α := R) (∑ σ ∈ ofSign 1, ∏ k : n, M k ((σ : (a : n) → n) k))
    (∑ x ∈ ofSign (-1), -∏ k : n, M k ((x : (a : n) → n) k))
Tactic: simp_rw [inv_apply, sign_inv, sub_eq_add_neg, detp, ← sum_neg_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1)) =
    HAdd.hAdd (α := R) (∑ σ ∈ ofSign 1, ∏ k : n, M k ((σ : (a : n) → n) k))
      (∑ x ∈ ofSign (-1), -∏ k : n, M k ((x : (a : n) → n) k))
have refine_1 : ∀ (σ : Perm n) (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) σ),
  HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
    ∏ k : n, M k ((σ : (a : n) → n) k)
Tactic: refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (sum_congr rfl fun σ hσ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
refine_1 :
  ∀ (σ : Perm n) (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) σ),
    HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
        (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
      ∏ k : n, M k ((σ : (a : n) → n) k)
⊢ HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1)) =
    HAdd.hAdd (α := R) (∑ σ ∈ ofSign 1, ∏ k : n, M k ((σ : (a : n) → n) k))
      (∑ x ∈ ofSign (-1), -∏ k : n, M k ((x : (a : n) → n) k))
have refine_2 : ∀ (σ : Perm n) (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ),
  HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
    -∏ k : n, M k ((σ : (a : n) → n) k)
Tactic: refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (sum_congr rfl fun σ hσ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) σ
⊢ HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
    ∏ k : n, M k ((σ : (a : n) → n) k)
have refine_1 : HSMul.hSMul (α := ℤˣ) (β := R) 1 (∏ i : n, M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) i : n)) ((σ : (a : n) → n) i)) =
  ∏ k : n, M k ((σ : (a : n) → n) k)
Tactic: rw [mem_ofSign.mp hσ, ← Equiv.prod_comp σ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
⊢ HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
    -∏ k : n, M k ((σ : (a : n) → n) k)
have refine_2 : HSMul.hSMul (α := ℤˣ) (β := R) (-1) (∏ i : n, M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) i : n)) ((σ : (a : n) → n) i)) =
  -∏ k : n, M k ((σ : (a : n) → n) k)
Tactic: rw [mem_ofSign.mp hσ, ← Equiv.prod_comp σ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
⊢ (diagonal d).det = ∏ i : n, d i
have rw : Eq.{v + 1} (α := R)
  (∑ σ : Perm n,
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
  (∏ i : n, d i)
Tactic: rw [det_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
    (∏ i : n, d i)
have refine_1 : ∀ (b : Perm n),
  Membership.mem (γ := Finset (Perm n)) univ b →
    b ≠ 1 →
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) b) : ℤ) : R)
          (∏ i : n, diagonal d ((b : (a : n) → n) i) i) =
        0
Tactic: refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
refine_1 :
  ∀ (b : Perm n),
    Membership.mem (γ := Finset (Perm n)) univ b →
      b ≠ 1 →
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) b) : ℤ) : R)
            (∏ i : n, diagonal d ((b : (a : n) → n) i) i) =
          0
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
    (∏ i : n, d i)
have refine_2 : 1 ∉ univ →
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
      (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
    0
Tactic: refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
refine_1 :
  ∀ (b : Perm n),
    Membership.mem (γ := Finset (Perm n)) univ b →
      b ≠ 1 →
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) b) : ℤ) : R)
            (∏ i : n, diagonal d ((b : (a : n) → n) i) i) =
          0
refine_2 :
  1 ∉ univ →
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
        (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
      0
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
    (∏ i : n, d i)
have refine_3 : HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
    (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
  ∏ i : n, d i
Tactic: refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) =
    0
have refine_1 : ∀ (x : n) (h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)),
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) =
    0
Tactic: obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) =
    0
have h : Eq.{v + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0
Tactic: convert! mul_zero (ε σ)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ Eq.{v + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0
have h : diagonal d ((σ : (a : n) → n) x) x = 0
Tactic: apply Finset.prod_eq_zero (mem_univ x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : IsEmpty n
⊢ Eq (α := (M : Matrix n n R) → R) det (const (Matrix n n R) 1)
have h : ∀ (x : Matrix n n R), x.det = const (Matrix n n R) 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Subsingleton n
A : Matrix n n R
k : n
⊢ A.det = A k k
have have : ∀ (this : Unique n), A.det = A k k
Tactic: have := uniqueOfSubsingleton k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
⊢ ∃ (i : n) (j : n), p i = p j ∧ i ≠ j
have H₁ : ¬∀ ⦃a₁ a₂ : n⦄, p a₁ = p a₂ → a₁ = a₂
Tactic: rw [← Finite.injective_iff_bijective, Injective] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x))
    0
have obtain : ∀ (i j : n) (hpij : p i = p j) (hij : i ≠ j),
  Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x))
    0
Tactic: obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j := by
    rw [← Finite.injective_iff_bijective, Injective] at H
    push Not at H
    exact H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x) +
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
                  ((fun (σ : Perm n) (x : Membership.mem (γ := Finset (Perm n)) univ σ) ↦ σ * Equiv.swap i j) σ h)) :
              ℤ) :
          R)
        (∏ x : n,
          M
              (((fun (σ : Perm n) (x : Membership.mem (γ := Finset (Perm n)) univ σ) ↦ σ * Equiv.swap i j) σ h :
                  (a : n) → n)
                x)
              (p x) *
            N (p x) x) =
    0
have this : Eq.{v + 1} (α := R) (∏ x : n, M ((σ : (a : n) → n) x) (p x)) (∏ x : n, M ((σ * Equiv.swap i j : (a : n) → n) x) (p x))
Tactic: have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
          Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
⊢ (M * N).det =
    ∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i)
have simp : Eq.{v + 1} (α := R)
  (∑ x : Perm n,
    ∑ i : (a : n) → n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
        (∏ i_1 : n, M ((x : (a : n) → n) i_1) (i i_1) * N (i i_1) i_1))
  (∑ p : n → n,
    ∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
Tactic: simp only [det_apply', mul_apply, prod_univ_sum, mul_sum, Fintype.piFinset_univ]