awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
refine_2 :
  ∀ (ha₂ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ'),
    Eq (α := n × o ≃ 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₁)
        ((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₂) →
      σ = σ'
⊢ ∀ (ha₂ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ'),
    Eq (α := n × o ≃ 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₁)
        ((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₂) →
      σ = σ'

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (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 σ'
eq :
  Eq (α := n × o ≃ 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₁)
    ((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₂)
refine_2 :
  ∀ (x : o) (hx : Membership.mem (γ := Finset o) univ x) (k : n),
    Eq (α := n) ((σ x hx : (a : n) → n) k : n) ((σ' x hx : (a : n) → n) k : n)
⊢ σ = σ'

Tactic:
ext x hx k
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (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 σ'
eq : Eq (α := n × o ≃ n × o) (prodCongrLeft fun (k : o) ↦ σ k ⋯) (prodCongrLeft fun (k : o) ↦ σ' k ⋯)
x_1 : o
hx : Membership.mem (γ := Finset o) univ x_1
k_1 k : n
x : o
rw rw₁ :
  Eq (α := n × o) ((prodCongrLeft fun (k : o) ↦ σ' k ⋯ : (a : n × o) → n × o) (k, x) : n × o)
    ((prodCongrLeft fun (k : o) ↦ σ' k ⋯ : (a : n × o) → n × o) (k, x) : n × o)
⊢ Eq (α := n × o) ((prodCongrLeft fun (k : o) ↦ σ k ⋯ : (a : n × o) → n × o) (k, x) : n × o)
    ((prodCongrLeft fun (k : o) ↦ σ' k ⋯ : (a : n × o) → n × o) (k, x) : n × o)

Tactic:
rw [eq]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (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 σ'
eq : Eq (α := n × o ≃ n × o) (prodCongrLeft fun (k : o) ↦ σ k ⋯) (prodCongrLeft fun (k : o) ↦ σ' k ⋯)
x : o
hx : Membership.mem (γ := Finset o) univ x
k : n
⊢ ∀ (k : n) (x : o),
    Eq (α := n × o) ((prodCongrLeft fun (k : o) ↦ σ k ⋯ : (a : n × o) → n × o) (k, x) : n × o)
      ((prodCongrLeft fun (k : o) ↦ σ' k ⋯ : (a : n × o) → n × o) (k, x) : n × o)

Tactic:
have :
        ∀ k x,
          prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) =
            prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) :=
        fun k x => by rw [eq]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (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 σ'
eq : Eq (α := n × o ≃ n × o) (prodCongrLeft fun (k : o) ↦ σ k ⋯) (prodCongrLeft fun (k : o) ↦ σ' k ⋯)
x : o
hx : Membership.mem (γ := Finset o) univ x
k : n
this :
  ∀ (k : n) (x : o),
    Eq (α := n × o) ((prodCongrLeft fun (k : o) ↦ σ k ⋯ : (a : n × o) → n × o) (k, x) : n × o)
      ((prodCongrLeft fun (k : o) ↦ σ' k ⋯ : (a : n × o) → n × o) (k, x) : n × o)
⊢ ∀ (k : n) (x : o), Eq (α := n) ((σ x ⋯ : (a : n) → n) k : n) ((σ' x ⋯ : (a : n) → n) k : n) ∧ True

Tactic:
simp only [prodCongrLeft_apply, Prod.mk_inj] at this

Premises used: Prod.mk_inj, Equiv.prodCongrLeft_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (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 σ'
eq : Eq (α := n × o ≃ n × o) (prodCongrLeft fun (k : o) ↦ σ k ⋯) (prodCongrLeft fun (k : o) ↦ σ' k ⋯)
x : o
hx : Membership.mem (γ := Finset o) univ x
k : n
this : ∀ (k : n) (x : o), Eq (α := n) ((σ x ⋯ : (a : n) → n) k : n) ((σ' x ⋯ : (a : n) → n) k : n) ∧ True
⊢ Eq (α := n) ((σ x hx : (a : n) → n) k : n) ((σ' x hx : (a : n) → n) k : n)

Tactic:
(this k x).1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
σ' : (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 σ'
eq : Eq (α := n × o ≃ n × o) (prodCongrLeft fun (k : o) ↦ σ k ⋯) (prodCongrLeft fun (k : o) ↦ σ' k ⋯)
x : o
hx : Membership.mem (γ := Finset o) univ x
k : n
this : ∀ (k : n) (x : o), Eq (α := n) ((σ x ⋯ : (a : n) → n) k : n) ((σ' x ⋯ : (a : n) → n) k : n) ∧ True
⊢ Eq (α := n) ((σ x hx : (a : n) → n) k : n) ((σ' x hx : (a : n) → n) k : n)

Tactic:
exact (this k x).1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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σ : σ ∈ preserving_snd
⊢ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2

Tactic:
rw [mem_preserving_snd] at hσ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
x : n × o
⊢ ((σ.symm : (a : n × o) → n × o) x).2 = x.2

Tactic:
simpa [eq_comm] using hσ (σ.symm x)

Premises used: eq_comm, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
⊢ ∀ (x : n × o), ((σ.symm : (a : n × o) → n × o) x).2 = x.2

Tactic:
have hσ' x : (σ.symm x).snd = x.snd := by simpa [eq_comm] using hσ (σ.symm x)
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
k : o
x : n
fst : Eq.{u_2 + 1} (α := n) (((σ : (a : n × o) → n × o) (x, k)).1, k).1 ((σ : (a : n × o) → n × o) (x, k)).1
snd : (((σ : (a : n × o) → n × o) (x, k)).1, k).2 = ((σ : (a : n × o) → n × o) (x, k)).2
⊢ Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
k : o
x : n
⊢ Eq.{u_2 + 1} (α := n) (((σ : (a : n × o) → n × o) (x, k)).1, k).1 ((σ : (a : n × o) → n × o) (x, k)).1

Tactic:
simp only
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
k : o
x : n
⊢ (((σ : (a : n × o) → n × o) (x, k)).1, k).2 = ((σ : (a : n × o) → n × o) (x, k)).2

Tactic:
simp only [hσ]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
⊢ ∀ (k : o) (x : n), Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))

Tactic:
have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by
        intro k x
        ext
        · simp only
        · simp only [hσ]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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))
⊢ ∀ (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))

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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))
⊢ ∀ (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))

Tactic:
have mk_inv_apply_eq : ∀ k x, ((σ.symm (x, k)).fst, k) = σ.symm (x, k) := by grind
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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))
⊢ ∃ (a : (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 a),
    (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))
        a ha =
      σ

Tactic:
⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩

Premises used: Equiv.mk, Prod.mk, Prod.fst, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 : o),
    Membership.mem (γ := Finset o) univ k →
      LeftInverse (fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1) fun (x : n) ↦
        ((σ : (a : n × o) → n × o) (x, k)).1
refine_3₁ :
  ∀ (k : o),
    Membership.mem (γ := Finset o) univ k →
      RightInverse (fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1) fun (x : n) ↦
        ((σ : (a : n × o) → n × o) (x, k)).1
refine_3₂ :
  Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
    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 := ⋯ }
refine_3₃ :
  (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 : (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 a),
    (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))
        a ha =
      σ

Tactic:
refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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))
k : o
h : Membership.mem (γ := Finset o) univ k
x : n
⊢ (fun (x : n) ↦ (((σ.symm : (a : n × o) → n × o) (x, k)).1 : n))
      ((fun (x : n) ↦ (((σ : (a : n × o) → n × o) (x, k)).1 : n)) x) =
    x

Tactic:
simp [mk_apply_eq]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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))
k : o
h : Membership.mem (γ := Finset o) univ k
x : n
⊢ (fun (x : n) ↦ (((σ : (a : n × o) → n × o) (x, k)).1 : n))
      ((fun (x : n) ↦ (((σ.symm : (a : n × o) → n × o) (x, k)).1 : n)) x) =
    x

Tactic:
simp [mk_inv_apply_eq]