-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedSup_infs (hs : a ∈ lowerClosure s) (ht : a ∈ lowerClosure t) :
    truncatedSup (s ⊼ t) a = truncatedSup s a ⊓ truncatedSup t a

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 => x1 ⊓ x2) (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t)).sup' ⋯
      fun x => id x) =
    (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯ fun i => id i.1 ⊓ id i.2

Tactic:
rw [sup'_image]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯
      ((fun x => id x) ∘ Function.uncurry fun x1 x2 => x1 ⊓ x2) =
    (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯ fun i => id i.1 ⊓ id i.2

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((filter (fun b => a ≤ b) s ⊼ filter (fun b => a ≤ b) t).sup' ⋯ fun x => id x) =
    (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯ fun i => id i.1 ⊓ id i.2

Tactic:
simp_rw [← image_inf_product]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 => x1 ⊓ x2) (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t)).sup' ⋯
      fun x => id x) =
    (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯ fun i => id i.1 ⊓ id i.2

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯
      ((fun x => id x) ∘ Function.uncurry fun x1 x2 => x1 ⊓ x2) =
    (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯ fun i => id i.1 ⊓ id i.2

Tactic:
simp [Function.uncurry_def]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a

Tactic:
simp only [truncatedSup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_le]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((filter (fun b => a ≤ b) s ⊼ filter (fun b => a ≤ b) t).sup' ⋯ fun x => id x) =
    (filter (fun b => a ≤ b) s ×ˢ filter (fun b => a ≤ b) t).sup' ⋯ fun i => id i.1 ⊓ id i.2