-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux3_symm_trans_trans [Finite α] [DecidableEq β] [Finite β] (f : Perm α) (e : α ≃ β)
    {s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
    signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
s : Multiset α
t : Multiset β
hs : ∀ (x : α), x ∈ s
ht : ∀ (x : β), x ∈ t
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Tactic:
induction' t, s using Quotient.inductionOn₂ with t s ht hs

Result:
case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Proof state:
case h.intro.intro
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
n : ℕ
e' : β ≃ Fin n
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f

Tactic:
rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _,
  ← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]

Result:
case h.intro.intro
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
n : ℕ
e' : β ≃ Fin n
⊢ signAux ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') =
    signAux (((e.trans e').symm.trans f).trans (e.trans e'))

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
n : ℕ
e' : β ≃ Fin n
x : Fin n
⊢ ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') x = (((e.trans e').symm.trans f).trans (e.trans e')) x

Tactic:
simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply]

Result:
no goals

Proof state:
case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f

Tactic:
rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩

Result:
case h.intro.intro
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
n : ℕ
e' : β ≃ Fin n
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f

Proof state:
case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Tactic:
show signAux2 _ _ = signAux2 _ _

Result:
case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f

Proof state:
case h.intro.intro
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
t : List β
s : List α
hs : ∀ (x : α), x ∈ ⟦s⟧
ht : ∀ (x : β), x ∈ ⟦t⟧
n : ℕ
e' : β ≃ Fin n
⊢ signAux ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') =
    signAux (((e.trans e').symm.trans f).trans (e.trans e'))

Tactic:
exact congr_arg signAux
  (Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])

Result:
no goals