-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma map_truncatedInf (e : α ≃o β) (s : Finset α) (a : α) :
    e (truncatedInf s a) = truncatedInf (s.map e.toEquiv.toEmbedding) (e a)

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

Tactic:
congr with h

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

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

Tactic:
simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]

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

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

Tactic:
simp

Result:
no goals

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

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

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

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

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

Result:
no goals