awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_1 : σ₁ ∈ (↑univ : Set (Perm m × Perm n))
σ₂ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_2 : σ₂ ∈ (↑univ : Set (Perm m × Perm n))
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 :
  (∀ (a : m), Eq (α := m) ((σ₁.1 : (a : m) → m) a : m) ((σ₂.1 : (a : m) → m) a : m)) ∧
    ∀ (b : n), Eq (α := n) ((σ₁.2 : (a : n) → n) b : n) ((σ₂.2 : (a : n) → n) b : n)
h₁ : ∀ (x : m), Eq (α := m) ((σ₁.1 : (a : m) → m) x : m) ((σ₂.1 : (a : m) → m) x : m)
⊢ σ₁ = σ₂
have h₂ : ∀ (x : n), Eq (α := n) ((σ₁.2 : (a : n) → n) x : n) ((σ₂.2 : (a : n) → n) x : n)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : σ ∈ (↑(↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset : Set (Perm (m ⊕ n)))
⊢ Membership.mem (γ := Set (Perm (m ⊕ n)))
    ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) '' (↑univ : Set (Perm m × Perm n))) σ
have hσ₁ : σ ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n)))
Tactic: rw [mem_coe, Set.mem_toFinset] at hσ
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : σ ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n)))
⊢ Membership.mem (γ := Set (Perm (m ⊕ n)))
    ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) '' (↑univ : Set (Perm m × Perm n))) σ
have h : ∀ (σ₁₂ : Prod.{u_1, u_2} (Perm m) (Perm n)) (hσ₁₂ : (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) σ₁₂ = σ),
  Membership.mem (γ := Set (Perm (m ⊕ n)))
    ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) '' (↑univ : Set (Perm m × Perm n))) σ
Tactic: obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Prod.{u_1, u_2} (Perm m) (Perm n)
hσ₁₂ : (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) σ₁₂ = σ
⊢ Membership.mem (γ := Set (Perm (m ⊕ n)))
    ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) '' (↑univ : Set (Perm m × Perm n))) σ
have h : σ₁₂ ∈ (↑univ : Set (Perm m × Perm n)) ∧ (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ = σ
Tactic: use σ₁₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Prod.{u_1, u_2} (Perm m) (Perm n)
hσ₁₂ : (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) σ₁₂ = σ
⊢ σ₁₂ ∈ (↑univ : Set (Perm m × Perm n)) ∧ (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ = σ
have h : σ₁₂ ∈ (↑univ : Set (Perm m × Perm n)) ∧
  Eq (α := Perm (m ⊕ n)) ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ : Perm (m ⊕ n))
    ((sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) σ₁₂ : Perm (m ⊕ n))
Tactic: rw [← hσ₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
    Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) a.1) : ℤ) : R)
            (∏ i : m, A ((a.1 : (a : m) → m) i) i) *
          HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) a.2) : ℤ) : R)
            (∏ i : n, D ((a.2 : (a : n) → n) i) i) =
        HMul.hMul (α := R)
          (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ)
                    ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a)) :
                ℤ) :
            R)
          (∏ i : m ⊕ n,
            fromBlocks A B 0 D
              (((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a : (a : m ⊕ n) → m ⊕ n) i) i)
have h : ∀ (a : Perm m) (b : Perm n),
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) a) : ℤ) : R)
        (∏ x : m, A ((a : (a : m) → m) x) x) *
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) b) : ℤ) : R)
        (∏ x : n, D ((b : (a : n) → n) x) x) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (a.sumCongr b)) : ℤ) : R)
      (∏ x : m ⊕ n, fromBlocks A B 0 D ((a.sumCongr b : (a : m ⊕ n) → m ⊕ n) x) x)
Tactic: simp only [forall_prop_of_true, Prod.forall, mem_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (∏ x : m, A ((σ₁ : (a : m) → m) x) x) *
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
        (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)
      (∏ x : m ⊕ n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂ : (a : m ⊕ n) → m ⊕ n) x) x)
have h : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (∏ x : m, A ((σ₁ : (a : m) → m) x) x) *
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
      (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
  (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
    HMul.hMul (α := R) (∏ a₁ : m, fromBlocks A B 0 D ((σ₁.sumCongr σ₂ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a₁)) (Sum.inl a₁))
      (∏ a₂ : n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂ : (a : m ⊕ n) → m ⊕ n) (Sum.inr a₂)) (Sum.inr a₂))
Tactic: rw [Fintype.prod_sum_type]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (∏ x : m, A ((σ₁ : (a : m) → m) x) x) *
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
        (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
      HMul.hMul (α := R)
        (∏ a₁ : m, fromBlocks A B 0 D ((σ₁.sumCongr σ₂ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a₁)) (Sum.inl a₁))
        (∏ a₂ : n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂ : (a : m ⊕ n) → m ⊕ n) (Sum.inr a₂)) (Sum.inr a₂))
have h : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (∏ x : m, A ((σ₁ : (a : m) → m) x) x) *
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
      (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
  (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
    HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)
Tactic: simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (∏ x : m, A ((σ₁ : (a : m) → m) x) x) *
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
        (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)
have h : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) *
    HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
  (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
    HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)
have h : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
  (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)
have h : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
  (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁ : ℤˣ)
            (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂ : ℤˣ)) :
        ℤ) :
    R)
Tactic: rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁ : ℤˣ)
              (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂ : ℤˣ)) :
          ℤ) :
      R)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)
have h₁ : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
  (↑(HMul.hMul (α := ℤ) (↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ)
        (↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ)) :
    R)
Tactic: rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁ : ℤˣ)
              (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂ : ℤˣ)) :
          ℤ) :
      R)
h₁ :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(HMul.hMul (α := ℤ) (↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ)
          (↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ)) :
      R)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)
have h₂ : HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
Tactic: rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
⊢ ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
have hσn₁ : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n)))
Tactic: rw [Set.mem_toFinset] at hσn
Cleared hypotheses: hσn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
have h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
Tactic: have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
        rw [Set.mem_toFinset] at hσn
        simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
have convert_2 : ∀ (a : m) (ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))),
  HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
Tactic: obtain ⟨a, ha⟩ := not_forall.mp h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
have convert_2 : ∀ (a2 : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)),
  HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
Tactic: rcases hx : σ (Sum.inl a) with a2 | b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
convert_2 :
  ∀ (a2 : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)),
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
      0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
have convert_2₁ : ∀ (b : n) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)),
  HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
Tactic: rcases hx : σ (Sum.inl a) with a2 | b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
a2 : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
have hn : ¬Eq (α := m ⊕ n) (Sum.inl a2) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
Tactic: have hn := (not_exists.mp ha) a2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
b : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0
have convert_2 : fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a)) (Sum.inl a) = 0
Tactic: rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
b : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)
⊢ fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a)) (Sum.inl a) = 0
have convert_2 : fromBlocks A B 0 D (Sum.inr b) (Sum.inl a) = 0
Tactic: rw [hx, fromBlocks_apply₂₁, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
b : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)
convert_2 : fromBlocks A B 0 D (Sum.inr b) (Sum.inl a) = 0
⊢ fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a)) (Sum.inl a) = 0
have convert_2₁ : Eq.{v + 1} (α := R) (0 b a) 0
Tactic: rw [hx, fromBlocks_apply₂₁, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
b : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)
convert_2 : fromBlocks A B 0 D (Sum.inr b) (Sum.inl a) = 0
convert_2₁ : Eq.{v + 1} (α := R) (0 b a) 0
⊢ fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a)) (Sum.inl a) = 0
have convert_2₂ : Eq.{v + 1} (α := R) 0 0
Tactic: rw [hx, fromBlocks_apply₂₁, zero_apply]