awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
hσ' : ∀ (x : n × o), ((σ.symm : (a : n × o) → n × o) x).2 = x.2
mk_apply_eq :
  ∀ (k : o) (x : n), Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
mk_inv_apply_eq :
  ∀ (k : o) (x : n),
    Eq (α := n × o) (((σ.symm : (a : n × o) → n × o) (x, k)).1, k) ((σ.symm : (a : n × o) → n × o) (x, k))
refine_3 :
  ∀ (k : n) (x : o),
    Eq.{u_2 + 1} (α := n)
      (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                  (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
              (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
                { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
                  invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
              ⋯ :
            (a : n × o) → n × o)
          (k, x)).1
      ((σ : (a : n × o) → n × o) (k, x)).1
⊢ (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
          (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
        (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
      (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
        { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
          invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
      ⋯ =
    σ
have refine_3₁ : ∀ (k : n) (x : o),
  Eq.{u_3 + 1} (α := o)
    (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
              (prodCongrLeft fun (k : o) ↦ σ k sorry : n × o ≃ n × o))
            (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
              { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
                invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := sorry, right_inv := sorry })
            sorry :
          (a : n × o) → n × o)
        (k, x)).2
    ((σ : (a : n × o) → n × o) (k, x)).2
Tactic: ext ⟨k, x⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ
⊢ ∏ x : o,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x ⋯)) : ℤ) : R)
        (∏ x_1 : n, M x ((σ x ⋯ : (a : n) → n) x_1) x_1) =
    HMul.hMul (α := R)
      (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha)) :
            ℤ) :
        R)
      (∏ i : n × o,
        blockDiagonal M
          (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                    (x :
                      Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                  (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                σ ha :
              (a : n × o) → n × o)
            i)
          i)
have refine_4 : HMul.hMul (α := R) (∏ x : o, (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x sorry)) : ℤ) : R))
    (∏ x : o, ∏ x_1 : n, M x ((σ x sorry : (a : n) → n) x_1) x_1) =
  HMul.hMul (α := R)
    (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
              ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                    (x :
                      Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                  (prodCongrLeft fun (k : o) ↦ σ k sorry : n × o ≃ n × o))
                σ ha)) :
          ℤ) :
      R)
    (∏ y : o,
      ∏ x : n,
        blockDiagonal M
          (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                    (x :
                      Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                  (prodCongrLeft fun (k : o) ↦ σ k sorry : n × o ≃ n × o))
                σ ha :
              (a : n × o) → n × o)
            (x, y))
          (x, y))
Tactic: rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : σ ∉ preserving_snd
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
    0
have hσ₁ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
Tactic: rw [mem_preserving_snd] at hσ
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
    0
have obtain : ∀ (k : n) (x : o) (hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2),
  HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
    0
Tactic: obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
k : n
x : o
hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
    0
have rw : blockDiagonal M ((σ : (a : n × o) → n × o) (k, x)) (k, x) = 0
Tactic: rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
k : n
x : o
hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2
⊢ blockDiagonal M ((σ : (a : n × o) → n × o) (k, x)) (k, x) = 0
have h : ((σ : (a : n × o) → n × o) (k, x)).2 ≠ x
Tactic: rw [blockDiagonal_apply_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A B 0 D).det = A.det * D.det
have 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))
Tactic: simp_rw [det_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ ∑ σ : 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))
have 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)
Tactic: convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
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)
⊢ ∑ σ : 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))
have 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
Tactic: convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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)
have h : Eq.{v + 1} (α := R)
  (∑ x : Perm m × Perm n,
    HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
        (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
        (∏ i : n, D ((x.2 : (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))
Tactic: simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (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))
have h : ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
  Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
    (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a ∈
      (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
Tactic: refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
h :
  ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
    Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
      (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a ∈
        (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (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))
have h₁ : Set.InjOn (β := Perm (m ⊕ n)) (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2)
  (↑univ : Set (Perm m × Perm n))
Tactic: refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
h :
  ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
    Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
      (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a ∈
        (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h₁ :
  Set.InjOn (β := Perm (m ⊕ n)) (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2)
    (↑univ : Set (Perm m × Perm n))
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (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))
have h₂ : Set.SurjOn (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) (↑univ : Set (Perm m × Perm n))
  (↑(↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset : Set (Perm (m ⊕ n)))
Tactic: refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
h :
  ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
    Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
      (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a ∈
        (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h₁ :
  Set.InjOn (β := Perm (m ⊕ n)) (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2)
    (↑univ : Set (Perm m × Perm n))
h₂ :
  Set.SurjOn (fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) (↑univ : Set (Perm m × Perm n))
    (↑(↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset : Set (Perm (m ⊕ n)))
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm m × Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) x.1) : ℤ) : R)
          (∏ i : m, A ((x.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x.2) : ℤ) : R)
          (∏ i : n, D ((x.2 : (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))
have h₃ : ∀ (a : Prod.{u_1, u_2} (Perm m) (Perm n)),
  Membership.mem (γ := Finset (Prod.{u_1, u_2} (Perm m) (Perm n))) univ a →
    HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) a.1) : ℤ) : R)
          (∏ i : m, A ((a.1 : (a : m) → m) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) a.2) : ℤ) : R)
          (∏ i : n, D ((a.2 : (a : n) → n) i) i) =
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ)
                  ((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a)) :
              ℤ) :
          R)
        (∏ i : m ⊕ n,
          fromBlocks A B 0 D
            (((fun (σ : Prod.{u_1, u_2} (Perm m) (Perm n)) ↦ σ.1.sumCongr σ.2) a : (a : m ⊕ n) → m ⊕ n) i) i)
Tactic: refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
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
σ₁ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_1 : σ₁ ∈ (↑univ : Set (Perm m × Perm n))
σ₂ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_2 : σ₂ ∈ (↑univ : Set (Perm m × Perm n))
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
⊢ σ₁ = σ₂
have h2 : ∀ (x : m ⊕ n),
  Eq (α := m ⊕ n) ((σ₁.1.sumCongr σ₁.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
    ((σ₂.1.sumCongr σ₂.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
Tactic: have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
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
σ₁ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_1 : σ₁ ∈ (↑univ : Set (Perm m × Perm n))
σ₂ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_2 : σ₂ ∈ (↑univ : Set (Perm m × Perm n))
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 :
  ∀ (x : m ⊕ n),
    Eq (α := m ⊕ n) ((σ₁.1.sumCongr σ₁.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
      ((σ₂.1.sumCongr σ₂.2 : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)
⊢ σ₁ = σ₂
have h2₁ : (∀ (a : m), Eq (α := m) ((σ₁.1 : (a : m) → m) a : m) ((σ₂.1 : (a : m) → m) a : m)) ∧
  ∀ (b : n), Eq (α := n) ((σ₁.2 : (a : n) → n) b : n) ((σ₂.2 : (a : n) → n) b : n)
Tactic: simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
σ₁ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_1 : σ₁ ∈ (↑univ : Set (Perm m × Perm n))
σ₂ : Prod.{u_1, u_2} (Perm m) (Perm n)
h_2 : σ₂ ∈ (↑univ : Set (Perm m × Perm n))
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 :
  (∀ (a : m), Eq (α := m) ((σ₁.1 : (a : m) → m) a : m) ((σ₂.1 : (a : m) → m) a : m)) ∧
    ∀ (b : n), Eq (α := n) ((σ₁.2 : (a : n) → n) b : n) ((σ₂.2 : (a : n) → n) b : n)
⊢ σ₁ = σ₂
have h₁ : ∀ (x : m), Eq (α := m) ((σ₁.1 : (a : m) → m) x : m) ((σ₂.1 : (a : m) → m) x : m)
Tactic: ext x