α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
⊢ ↑f⁻¹ y ∈ s
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
⊢ ↑f⁻¹ y ∈ s
have h0 : ∀ y ∈ s, ∃ (x : _)(hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
  Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
    (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
case intro.intro
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ y ∈ s
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
⊢ ↑f⁻¹ y ∈ s
obtain ⟨y2, hy2, heq⟩ := h0 y hy
case h.e'_4
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ y = y2
case intro.intro
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ y ∈ s
convert hy2
case h.e'_4
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ ((fun i x => ↑f i) y2 hy2) = y2
case h.e'_4
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ y = y2
rw [heq]
no goals
case h.e'_4
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ ((fun i x => ↑f i) y2 hy2) = y2
simp only [inv_apply_self]