-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) :
    (Matrix.fromBlocks A B 0 D).det = A.det * D.det

Proof state:
case h.e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
⊢ σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2 → σ₁ = σ₂

Tactic:
intro h

Result:
case h.e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
⊢ σ₁ = σ₂

Proof state:
case h.e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x : m, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x : n, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) * ((∏ x : m, A (σ₁ x) x) * ∏ x : n, D (σ₂ x) x)

Tactic:
rw [mul_mul_mul_comm]

Result:
case h.e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ ↑↑(sign σ₁) * ↑↑(sign σ₂) * ((∏ x : m, A (σ₁ x) x) * ∏ x : n, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) * ((∏ x : m, A (σ₁ x) x) * ∏ x : n, D (σ₂ x) x)

Proof state:
case h.e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : ∃ x, (sumCongrHom m n) x = σ
⊢ σ ∈ (fun σ => σ.1.sumCongr σ.2) '' ↑univ

Tactic:
obtain ⟨σ₁₂, hσ₁₂⟩ := hσ

Result:
case h.e'_3.refine_3.intro
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ ∈ (fun σ => σ.1.sumCongr σ.2) '' ↑univ

Proof state:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ₁₂ ∈ ↑univ ∧ (fun σ => σ.1.sumCongr σ.2) σ₁₂ = σ

Tactic:
rw [← hσ₁₂]

Result:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ₁₂ ∈ ↑univ ∧ (fun σ => σ.1.sumCongr σ.2) σ₁₂ = (sumCongrHom m n) σ₁₂

Proof state:
case convert_2.intro.inr
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]

Result:
case convert_2.intro.inr
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ fromBlocks A B 0 D (σ (Sum.inl a)) (Sum.inl a) = 0

Proof state:
case h.e'_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ (∑ σ : Perm m, ↑↑(sign σ) * ∏ i : m, A (σ i) i) * ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, D (σ i) i =
    ∑ x ∈ (↑(sumCongrHom m n).range).toFinset, ↑↑(sign x) * ∏ i : m ⊕ n, fromBlocks A B 0 D (x i) i

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

Result:
case h.e'_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∑ x : Perm m × Perm n, (↑↑(sign x.1) * ∏ i : m, A (x.1 i) i) * (↑↑(sign x.2) * ∏ i : n, D (x.2 i) i) =
    ∑ x ∈ (↑(sumCongrHom m n).range).toFinset, ↑↑(sign x) * ∏ i : m ⊕ n, fromBlocks A B 0 D (x i) i

Proof state:
case h.e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
⊢ (fun σ => σ.1.sumCongr σ.2) σ₁ = (fun σ => σ.1.sumCongr σ.2) σ₂ → σ₁ = σ₂

Tactic:
dsimp only

Result:
case h.e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
⊢ σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2 → σ₁ = σ₂

Proof state:
case h.e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
⊢ σ₁ = σ₂

Tactic:
ext x

Result:
case h.e'_3.refine_2.fst.H
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : m
⊢ σ₁.1 x = σ₂.1 x

case h.e'_3.refine_2.snd.H
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : n
⊢ σ₁.2 x = σ₂.2 x