-- 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
simp_rw :
  ∑ σ : 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))
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 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
⊢ (fromBlocks A B 0 D).det = A.det * D.det

Tactic:
classical
    simp_rw [det_apply']
    convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
    · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
    · rintro σ - hσn
      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
      obtain ⟨a, ha⟩ := not_forall.mp h1
      rcases hx : σ (Sum.inl a) with a2 | b
      · have hn := (not_exists.mp ha) a2
        exact absurd hx.symm hn
      · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]

Premises used: Matrix.fromBlocks_apply₁₁, Finset.mem_univ, Sum.map_inl, Matrix.fromBlocks_apply₂₂, Matrix.zero_apply, mul_mul_mul_comm, Finset.sum_nbij, Sum.inr.injEq, Equiv.Perm.sumCongr_apply, Equiv.Perm.sign_sumCongr, Finset.univ_product_univ, Matrix.fromBlocks_apply₂₁, Sum.inl.injEq, Finset.sum_product', Equiv.sumCongr_apply, MulZeroClass.mul_zero, Int.cast_mul, forall_prop_of_true, Prod.forall, Sum.map_inr, Set.mem_toFinset, Sum.forall, Matrix.det_apply', Eq.symm, Fintype.prod_sum_type, Finset.mem_coe, Units.val_mul, Finset.sum_mul_sum