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

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

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
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

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

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

Result:
no goals

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
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
⊢ ↑↑(sign σ) * ∏ i : m ⊕ n, fromBlocks A B 0 D (σ i) i = 0

Tactic:
obtain ⟨a, ha⟩ := not_forall.mp h1

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

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 ⊕ n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) x) x

Tactic:
rw [Fintype.prod_sum_type]

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 σ₂)) *
      ((∏ a₁ : m, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inl a₁)) (Sum.inl a₁)) *
        ∏ a₂ : n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inr a₂)) (Sum.inr a₂))

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) σ₁₂ = (sumCongrHom m n) σ₁₂

Tactic:
simp

Result:
no goals

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 σ₂)) *
      ((∏ a₁ : m, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inl a₁)) (Sum.inl a₁)) *
        ∏ a₂ : n, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inr a₂)) (Sum.inr a₂))

Tactic:
simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
  fromBlocks_apply₂₂]

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, A (σ₁ x) x) * ∏ x : n, D (σ₂ x) x)

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
⊢ fromBlocks A B 0 D (σ (Sum.inl a)) (Sum.inl a) = 0

Tactic:
rw [hx, fromBlocks_apply₂₁, zero_apply]

Result:
no goals

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

Tactic:
have hn := (not_exists.mp ha) a2

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
hn : ¬Sum.inl a2 = σ (Sum.inl a)
⊢ ↑↑(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
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
⊢ σ₁ = σ₂

Tactic:
have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
  DFunLike.congr_fun 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
h2 : ∀ (x : m ⊕ n), (σ₁.1.sumCongr σ₁.2) x = (σ₂.1.sumCongr σ₂.2) x
⊢ σ₁ = σ₂