awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
h :
  HMul.hMul (α := R)
      (∑ σ : Perm m,
        HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
          (∏ i : m, A ((σ : (a : m) → m) i) i))
      (∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, D ((σ : (a : n) → n) i) i)) =
    ∑ x ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i)
convert_2 :
  ∀ (x : Perm (m ⊕ n)),
    Membership.mem (γ := Finset (Perm (m ⊕ n))) univ x →
      x ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset →
        HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
            (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i) =
          0
⊢ ∑ σ : Perm (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) =
    HMul.hMul (α := R)
      (∑ σ : Perm m,
        HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
          (∏ i : m, A ((σ : (a : m) → m) i) i))
      (∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, D ((σ : (a : n) → n) i) i))

Tactic:
convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_

Premises used: MonoidHom.range, Equiv.Perm.sumCongrHom, Set.toFinset, SetLike.coe, Finset.sum_subset, Eq.symm, Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
h :
  Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (a : n) → n) i) i))
    (∑ x ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i))
⊢ HMul.hMul (α := R)
      (∑ σ : Perm m,
        HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
          (∏ i : m, A ((σ : (a : m) → m) i) i))
      (∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, D ((σ : (a : n) → n) i) i)) =
    ∑ x ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i)

Tactic:
simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]

Premises used: Finset.univ_product_univ, Finset.sum_product', Finset.sum_mul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (a : n) → n) i) i))
    (∑ x ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i))

Tactic:
sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_

Premises used: Finset.sum_nbij, Prod.fst, Equiv.Perm.sumCongr, Prod.snd
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
h :
  ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
    Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
      (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a ∈
        (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h₁ :
  Set.InjOn (β := Perm (m ⊕ n)) (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2)
    (↑univ : Set (Perm m × Perm n))
h₂ :
  Set.SurjOn (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) (↑univ : Set (Perm m × Perm n))
    (↑(↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset : Set (Perm (m ⊕ n)))
h₃ :
  ∀ (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)
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (a : n) → n) i) i))
    (∑ x ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i))

Tactic:
refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_

Premises used: Finset.sum_nbij
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 :
  Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ σ₁₂ →
    (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ ∈
      (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
⊢ Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ σ₁₂ →
    (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ ∈
      (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 : Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ σ₁₂
⊢ (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ ∈
    (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 :
  σ₁ ∈ (↑univ : Set (Perm m × Perm n)) →
    ∀ ⦃x₂ : Prod.{u_1, u_2} (Perm m) (Perm n)⦄,
      x₂ ∈ (↑univ : Set (Perm m × Perm n)) →
        Eq (α := Perm (m ⊕ n)) ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁)
            ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) x₂) →
          σ₁ = x₂
⊢ σ₁ ∈ (↑univ : Set (Perm m × Perm n)) →
    ∀ ⦃x₂ : Prod.{u_1, u_2} (Perm m) (Perm n)⦄,
      x₂ ∈ (↑univ : Set (Perm m × Perm n)) →
        Eq (α := Perm (m ⊕ n)) ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁)
            ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) x₂) →
          σ₁ = x₂

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 :
  σ₂ ∈ (↑univ : Set (Perm m × Perm n)) →
    Eq (α := Perm (m ⊕ n)) ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁)
        ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₂) →
      σ₁ = σ₂
⊢ σ₂ ∈ (↑univ : Set (Perm m × Perm n)) →
    Eq (α := Perm (m ⊕ n)) ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁)
        ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₂) →
      σ₁ = σ₂

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
⊢ ∀ (x : m ⊕ n),
    Eq (α := m ⊕ n) ((σ₁.1.sumCongr σ₁.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
      ((σ₂.1.sumCongr σ₂.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)

Tactic:
have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 :
  ∀ (x : m ⊕ n),
    Eq (α := m ⊕ n) ((σ₁.1.sumCongr σ₁.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
      ((σ₂.1.sumCongr σ₂.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
⊢ (∀ (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)

Tactic:
simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2

Premises used: Sum.map_inl, Sum.inr.injEq, Equiv.Perm.sumCongr_apply, Sum.inl.injEq, Sum.map_inr, Sum.forall
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
h₂ : ∀ (x : n), Eq (α := n) ((σ₁.2 : (a : n) → n) x : n) ((σ₂.2 : (a : n) → n) x : n)
⊢ σ₁ = σ₂

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
x : m
⊢ Eq (α := m) ((σ₁.1 : (a : m) → m) x : m) ((σ₂.1 : (a : m) → m) x : m)

Tactic:
h2.left x

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
x : m
⊢ Eq (α := m) ((σ₁.1 : (a : m) → m) x : m) ((σ₂.1 : (a : m) → m) x : m)

Tactic:
exact h2.left x

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
x : n
⊢ Eq (α := n) ((σ₁.2 : (a : n) → n) x : n) ((σ₂.2 : (a : n) → n) x : n)

Tactic:
h2.right x

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
x : n
⊢ Eq (α := n) ((σ₁.2 : (a : n) → n) x : n) ((σ₂.2 : (a : n) → n) x : n)

Tactic:
exact h2.right x

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)))
⊢ σ ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n)))

Tactic:
rw [mem_coe, Set.mem_toFinset] at hσ

Premises used: Set.mem_toFinset, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)))
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))) σ
⊢ 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σ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)) σ₁₂ = σ
h : σ₁₂ ∈ (↑univ : Set (Perm m × Perm n)) ∧ (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ = σ
⊢ 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:
use σ₁₂
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)) σ₁₂ = σ
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))
⊢ σ₁₂ ∈ (↑univ : Set (Perm m × Perm n)) ∧ (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) σ₁₂ = σ

Tactic:
rw [← hσ₁₂]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)) ∧
    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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
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)
⊢ ∀ (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)

Tactic:
simp only [forall_prop_of_true, Prod.forall, mem_univ]

Premises used: Finset.mem_univ, forall_prop_of_true, Prod.forall
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
        (∏ 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₂))
⊢ 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)

Tactic:
rw [Fintype.prod_sum_type]

Premises used: Fintype.prod_sum_type
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
        (∏ 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)
⊢ 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:
simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]

Premises used: Matrix.fromBlocks_apply₁₁, Sum.map_inl, Matrix.fromBlocks_apply₂₂, Equiv.sumCongr_apply, Sum.map_inr