-- 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_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)

Tactic:
congr

Result:
case h.e'_3.refine_4.e_a
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 σ₂) = ↑↑(sign (σ₁.sumCongr σ₂))

Proof state:
case convert_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
⊢ ∀ x ∈ univ, x ∉ (↑(sumCongrHom m n).range).toFinset → ↑↑(sign x) * ∏ i : m ⊕ n, fromBlocks A B 0 D (x i) i = 0

Tactic:
rintro σ - hσn

Result:
case convert_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 ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

Proof state:
case convert_2.intro.inl
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)
a2 : m
hx : σ (Sum.inl a) = Sum.inl a2
hn : ¬Sum.inl a2 = σ (Sum.inl a)
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

Tactic:
exact absurd hx.symm hn

Result:
no goals

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

Tactic:
exact h2.right x

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), ↑↑(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

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

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
⊢ (∑ σ : 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

case convert_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
⊢ ∀ x ∈ univ, x ∉ (↑(sumCongrHom m n).range).toFinset → ↑↑(sign x) * ∏ i : m ⊕ n, fromBlocks A B 0 D (x i) i = 0

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 ∈ 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

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

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
⊢ ∀ (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

Proof state:
case convert_2.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)
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)
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

Tactic:
rcases hx : σ (Sum.inl a) with a2 | b

Result:
case convert_2.intro.inl
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)
a2 : m
hx : σ (Sum.inl a) = Sum.inl a2
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

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

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

Tactic:
intro σ₁ _ σ₂ _

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
⊢ (fun σ => σ.1.sumCongr σ.2) σ₁ = (fun σ => σ.1.sumCongr σ.2) σ₂ → σ₁ = σ₂

Proof state:
case h.e'_3.refine_4.e_a
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 σ₂) = ↑↑(sign (σ₁.sumCongr σ₂))

Tactic:
rw [sign_sumCongr, Units.val_mul, Int.cast_mul]

Result:
no goals

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

Tactic:
use σ₁₂

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) σ₁₂ = σ