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
σ : (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₂)
⊢ σ = σ'
have 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
-- 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 σ
σ' : (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
⊢ 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)
have rw : Eq (α := n × o) ((prodCongrLeft fun (k : o) ↦ σ' k sorry : (a : n × o) → n × o) (k, x) : n × o)
  ((prodCongrLeft fun (k : o) ↦ σ' k sorry : (a : n × o) → n × o) (k, x) : n × o)
Tactic: rw [eq]
-- 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
σ : (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
⊢ Eq (α := n) ((σ x hx : (a : n) → n) k : n) ((σ' x hx : (a : n) → n) k : n)
have this : ∀ (k : n) (x : o),
  Eq (α := n × o) ((prodCongrLeft fun (k : o) ↦ σ k sorry : (a : n × o) → n × o) (k, x) : n × o)
    ((prodCongrLeft fun (k : o) ↦ σ' k sorry : (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]
-- 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
σ : (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)
⊢ Eq (α := n) ((σ x hx : (a : n) → n) k : n) ((σ' x hx : (a : n) → n) k : n)
have this₁ : ∀ (k : n) (x : o), Eq (α := n) ((σ x sorry : (a : n) → n) k : n) ((σ' x sorry : (a : n) → n) k : n) ∧ True
Tactic: simp only [prodCongrLeft_apply, Prod.mk_inj] at this
Cleared hypotheses: this
-- 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
σ : n × o ≃ n × o
hσ : σ ∈ preserving_snd
⊢ ∃ (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 =
      σ
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 (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
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
⊢ ∃ (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 =
      σ
have hσ' : ∀ (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)
-- 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
k : o
x : n
⊢ Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
have fst : Eq.{u_2 + 1} (α := n) (((σ : (a : n × o) → n × o) (x, k)).1, k).1 ((σ : (a : n × o) → n × o) (x, k)).1
Tactic: ext
-- 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
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
⊢ Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
have snd : (((σ : (a : n × o) → n × o) (x, k)).1, k).2 = ((σ : (a : n × o) → n × o) (x, k)).2
Tactic: ext
-- 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
σ : 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
⊢ ∃ (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 =
      σ
have 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))
Tactic: have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by
        intro k x
        ext
        · simp only
        · simp only [hσ]
-- 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
σ : 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))
⊢ ∃ (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 =
      σ
have 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))
Tactic: have mk_inv_apply_eq : ∀ k x, ((σ.symm (x, k)).fst, k) = σ.symm (x, k) := by grind
-- 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))
⊢ ∃ (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 =
      σ
have 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
Tactic: refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
-- 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 : 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
⊢ ∃ (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 =
      σ
have 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
Tactic: refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
-- 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 : 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
⊢ ∃ (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 =
      σ
have 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 := sorry, right_inv := sorry }
Tactic: refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
-- 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 : 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 := ⋯ }
⊢ ∃ (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 =
      σ
have 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 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 =
  σ
Tactic: refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
-- 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))
⊢ (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_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 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)).1
    ((σ : (a : n × o) → n × o) (k, x)).1
Tactic: ext ⟨k, x⟩