-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma map_truncatedSup [DecidableRel (α := β) (· ≤ ·)] (e : α ≃o β) (s : Finset α) (a : α) :
    e (truncatedSup s a) = truncatedSup (s.map e.toEquiv.toEmbedding) (e a)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
⊢ e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s

Tactic:
simp

Result:
no goals

Proof state:
case e_t.h
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
h : a ∈ lowerClosure ↑s
⊢ (filter (fun b => a ≤ b) s).sup' ⋯ (⇑e ∘ id) = (filter (fun b => e a ≤ b) (map e.toEmbedding s)).sup' ⋯ id

Tactic:
simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
  OrderIso.le_iff_le, id, sup'_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then (filter (fun b => a ≤ b) s).sup' ⋯ (⇑e ∘ id) else ⊤) =
    if h : a ∈ lowerClosure ↑s then (filter (fun b => e a ≤ b) (map e.toEmbedding s)).sup' ⋯ id else ⊤

Tactic:
congr with h

Result:
case e_t.h
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
h : a ∈ lowerClosure ↑s
⊢ (filter (fun b => a ≤ b) s).sup' ⋯ (⇑e ∘ id) = (filter (fun b => e a ≤ b) (map e.toEmbedding s)).sup' ⋯ id

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)

Tactic:
simp_rw [truncatedSup, apply_dite e, map_finset_sup', map_top, this]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then (filter (fun b => a ≤ b) s).sup' ⋯ (⇑e ∘ id) else ⊤) =
    if h : a ∈ lowerClosure ↑s then (filter (fun b => e a ≤ b) (map e.toEmbedding s)).sup' ⋯ id else ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
⊢ e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)

Tactic:
have : e a ∈ lowerClosure (s.map e.toEquiv.toEmbedding : Set β) ↔ a ∈ lowerClosure s := by simp

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)