-- 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_1
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
⊢ ∀ a ∈ univ, (fun σ => σ.1.sumCongr σ.2) a ∈ (↑(sumCongrHom m n).range).toFinset

Tactic:
intro σ₁₂ _

Result:
case h.e'_3.refine_1
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
⊢ (fun σ => σ.1.sumCongr σ.2) σ₁₂ ∈ (↑(sumCongrHom m n).range).toFinset

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
⊢ Set.SurjOn (fun σ => σ.1.sumCongr σ.2) ↑univ ↑(↑(sumCongrHom m n).range).toFinset

Tactic:
intro σ hσ

Result:
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σ : σ ∈ ↑(↑(sumCongrHom m n).range).toFinset
⊢ σ ∈ (fun σ => σ.1.sumCongr σ.2) '' ↑univ

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 : ∀ (x : m ⊕ n), (σ₁.1.sumCongr σ₁.2) x = (σ₂.1.sumCongr σ₂.2) x
⊢ σ₁ = σ₂

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

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
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
⊢ σ₁ = σ₂

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
⊢ ∑ 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

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

Result:
case h.e'_3.refine_1
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
⊢ ∀ a ∈ univ, (fun σ => σ.1.sumCongr σ.2) a ∈ (↑(sumCongrHom m n).range).toFinset

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
⊢ Set.InjOn (fun σ => σ.1.sumCongr σ.2) ↑univ

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
⊢ Set.SurjOn (fun σ => σ.1.sumCongr σ.2) ↑univ ↑(↑(sumCongrHom m n).range).toFinset

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
⊢ ∀ a ∈ univ,
    (↑↑(sign a.1) * ∏ i : m, A (a.1 i) i) * (↑↑(sign a.2) * ∏ i : n, D (a.2 i) i) =
      ↑↑(sign ((fun σ => σ.1.sumCongr σ.2) a)) * ∏ i : m ⊕ n, fromBlocks A B 0 D (((fun σ => σ.1.sumCongr σ.2) a) i) i

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
⊢ ∀ (a : Perm m) (b : Perm n),
    (↑↑(sign a) * ∏ x : m, A (a x) x) * (↑↑(sign b) * ∏ x : n, D (b x) x) =
      ↑↑(sign (a.sumCongr b)) * ∏ x : m ⊕ n, fromBlocks A B 0 D ((a.sumCongr b) x) x

Tactic:
intro σ₁ σ₂

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 σ₁) * ∏ x : m, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x : n, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) * ∏ x : m ⊕ n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) 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σ : σ ∈ ↑(↑(sumCongrHom m n).range).toFinset
⊢ σ ∈ (fun σ => σ.1.sumCongr σ.2) '' ↑univ

Tactic:
erw [Set.mem_toFinset, MonoidHom.mem_range] at hσ

Result:
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

Proof state:
case h.e'_3.refine_1
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
⊢ (fun σ => σ.1.sumCongr σ.2) σ₁₂ ∈ (↑(sumCongrHom m n).range).toFinset

Tactic:
simp

Result:
no goals

Proof state:
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
⊢ ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)

Tactic:
rw [Set.mem_toFinset] at hσn

Result:
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
⊢ ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)

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

Tactic:
simp_rw [det_apply']

Result:
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), ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i =
    (∑ σ : Perm m, ↑↑(sign σ) * ∏ i : m, A (σ i) i) * ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, D (σ i) i

Proof state:
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

Tactic:
exact h2.left x

Result:
no goals