Theorem: Equiv.Perm.Subtype.image_preimage_of_val (Jordan/PermMaximal.lean)

State before:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
⊢ Subtype.val '' (Subtype.val ⁻¹' B) = B
Tactic:
apply Set.Subset.antisymm (Set.image_preimage_subset Subtype.val B)
State after:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
⊢ B ⊆ Subtype.val '' (Subtype.val ⁻¹' B)

State before:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
⊢ B ⊆ Subtype.val '' (Subtype.val ⁻¹' B)
Tactic:
intro x hx
State after:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ x ∈ Subtype.val '' (Subtype.val ⁻¹' B)

State before:
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ x ∈ Subtype.val '' (Subtype.val ⁻¹' B)
Tactic:
use ⟨x, h hx⟩
State after:
case h
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ { val := x, property := ⋯ } ∈ Subtype.val ⁻¹' B ∧ ↑{ val := x, property := ⋯ } = x

State before:
case h
α✝ : Type ?u.39088
inst✝³ : DecidableEq α✝
G : Type ?u.39100
inst✝² : Group G
inst✝¹ : MulAction G α✝
inst✝ : Fintype α✝
α : Type u_1
s B : Set α
h : B ⊆ s
x : α
hx : x ∈ B
⊢ { val := x, property := ⋯ } ∈ Subtype.val ⁻¹' B ∧ ↑{ val := x, property := ⋯ } = x
Tactic:
simp only [hx, Set.mem_preimage, Subtype.coe_mk, eq_self_iff_true, and_self_iff]
State after:
no goals