[GOAL]
α : Type ?u.3
⊢ (fun {α β} e => ↑(uniqueCongr e)) (Equiv.refl α) = id
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {α β γ : Type ?u.3} (k : α ≃ β) (h : β ≃ γ),
    (fun {α β} e => ↑(uniqueCongr e)) (k.trans h) =
      (fun {α β} e => ↑(uniqueCongr e)) h ∘ (fun {α β} e => ↑(uniqueCongr e)) k
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.3738
⊢ (fun {α β} e p => (e.symm.trans p).trans e) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h.H
α : Type ?u.3738
x✝¹ : Perm α
x✝ : α
⊢ ↑((fun {α β} e p => (e.symm.trans p).trans e) (Equiv.refl α) x✝¹) x✝ = ↑(id x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
α✝ β✝ γ✝ : Type ?u.3738
x✝¹ : α✝ ≃ β✝
x✝ : β✝ ≃ γ✝
⊢ (fun {α β} e p => (e.symm.trans p).trans e) (x✝¹.trans x✝) =
    (fun {α β} e p => (e.symm.trans p).trans e) x✝ ∘ (fun {α β} e p => (e.symm.trans p).trans e) x✝¹
[PROOFSTEP]
ext
[GOAL]
case h.H
α✝ β✝ γ✝ : Type ?u.3738
x✝³ : α✝ ≃ β✝
x✝² : β✝ ≃ γ✝
x✝¹ : Perm α✝
x✝ : γ✝
⊢ ↑((fun {α β} e p => (e.symm.trans p).trans e) (x✝³.trans x✝²) x✝¹) x✝ =
    ↑(((fun {α β} e p => (e.symm.trans p).trans e) x✝² ∘ (fun {α β} e p => (e.symm.trans p).trans e) x✝³) x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.6374
⊢ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type ?u.6374
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (Equiv.refl α) x✝ ↔ a✝ ∈ id x✝
[PROOFSTEP]
simp
[GOAL]
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
⊢ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (k.trans h) =
    (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) h ∘ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) k
[PROOFSTEP]
ext _ a
[GOAL]
case h.a
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ a ∈ (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) (k.trans h) x✝ ↔
    a ∈
      ((fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) h ∘
          (fun {α β} e s => Finset.map (Equiv.toEmbedding e) s) k)
        x✝
[PROOFSTEP]
simp
[GOAL]
case h.a
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ (∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a) ↔ ↑k.symm (↑h.symm a) ∈ x✝
[PROOFSTEP]
constructor
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ (∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a) → ↑k.symm (↑h.symm a) ∈ x✝
[PROOFSTEP]
intro h'
[GOAL]
case h.a.mpr
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
⊢ ↑k.symm (↑h.symm a) ∈ x✝ → ∃ a_2, a_2 ∈ x✝ ∧ ↑h (↑k a_2) = a
[PROOFSTEP]
intro h'
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
h' : ∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a
⊢ ↑k.symm (↑h.symm a) ∈ x✝
[PROOFSTEP]
let ⟨a, ha₁, ha₂⟩ := h'
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
h' : ∃ a, a ∈ x✝ ∧ ↑h (↑k a) = a✝
a : α✝
ha₁ : a ∈ x✝
ha₂ : ↑h (↑k a) = a✝
⊢ ↑k.symm (↑h.symm a✝) ∈ x✝
[PROOFSTEP]
rw [← ha₂]
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
h' : ∃ a, a ∈ x✝ ∧ ↑h (↑k a) = a✝
a : α✝
ha₁ : a ∈ x✝
ha₂ : ↑h (↑k a) = a✝
⊢ ↑k.symm (↑h.symm (↑h (↑k a))) ∈ x✝
[PROOFSTEP]
simp
[GOAL]
case h.a.mp
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
h' : ∃ a, a ∈ x✝ ∧ ↑h (↑k a) = a✝
a : α✝
ha₁ : a ∈ x✝
ha₂ : ↑h (↑k a) = a✝
⊢ a ∈ x✝
[PROOFSTEP]
apply ha₁
[GOAL]
case h.a.mpr
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
h' : ↑k.symm (↑h.symm a) ∈ x✝
⊢ ∃ a_1, a_1 ∈ x✝ ∧ ↑h (↑k a_1) = a
[PROOFSTEP]
exists (Equiv.symm k) ((Equiv.symm h) a)
[GOAL]
case h.a.mpr
α✝ β✝ γ✝ : Type ?u.6374
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a : γ✝
h' : ↑k.symm (↑h.symm a) ∈ x✝
⊢ ↑k.symm (↑h.symm a) ∈ x✝ ∧ ↑h (↑k (↑k.symm (↑h.symm a))) = a
[PROOFSTEP]
simp [h']
[GOAL]
α : Type ?u.9577
⊢ (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h
α : Type ?u.9577
x✝ : Fintype α
⊢ (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) (Equiv.refl α) x✝ = id x✝
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {α β γ : Type ?u.9577} (k : α ≃ β) (h : β ≃ γ),
    (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) (k.trans h) =
      (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) h ∘
        (fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)) k
[PROOFSTEP]
simp
