-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (-1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
refine_2 :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n)
        ((fun (p : (_ : n) × Perm n)
              (x :
                Membership.mem (γ := Finset ((_ : n) × Perm n))
                  (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                    {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                  p) ↦
            f p)
          (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) ∧
    HMul.hMul (α := ℤˣ) (-1) (-1) = 1 ∧
      Eq (α := n) ((σ : (a : n) → n) i : n)
        (Sigma.fst (β := fun (i : n) ↦ Perm n)
            ((fun (p : (_ : n) × Perm n)
                  (x :
                    Membership.mem (γ := Finset ((_ : n) × Perm n))
                      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                        {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                      p) ↦
                f p)
              (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
          n)
⊢ Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n)
        ((fun (p : (_ : n) × Perm n)
              (x :
                Membership.mem (γ := Finset ((_ : n) × Perm n))
                  (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                    {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                  p) ↦
            f p)
          (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n)
              ((fun (p : (_ : n) × Perm n)
                    (x :
                      Membership.mem (γ := Finset ((_ : n) × Perm n))
                        (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                          {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                        p) ↦
                  f p)
                (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      Eq (α := n)
        (((Sigma.snd (β := fun (i : n) ↦ Perm n)
                  ((fun (p : (_ : n) × Perm n)
                        (x :
                          Membership.mem (γ := Finset ((_ : n) × Perm n))
                            (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                              {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                            p) ↦
                      f p)
                    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
                Perm n) :
              (a : n) → n)
            j :
          n)
        (Sigma.fst (β := fun (i : n) ↦ Perm n)
            ((fun (p : (_ : n) × Perm n)
                  (x :
                    Membership.mem (γ := Finset ((_ : n) × Perm n))
                      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                        {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                      p) ↦
                f p)
              (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
          n)

Tactic:
rw [Perm.mul_apply, sign_mul, hp.2.1, sign_swap h, swap_apply_right]

Premises used: Equiv.Perm.sign_mul, And.right, And.left, Equiv.Perm.mul_apply, Equiv.swap_apply_right, Equiv.Perm.sign_swap