-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_sups (hs : a ∈ upperClosure s) (ht : a ∈ upperClosure t) :
    truncatedInf (s ⊻ t) a = truncatedInf s a ⊔ truncatedInf 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 ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a

Tactic:
simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ ((filter (fun b => b ≤ a) s ⊻ filter (fun b => b ≤ a) t).inf' ⋯ fun x => id x) =
    (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t).inf' ⋯ 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 ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t).inf' ⋯
      ((fun x => id x) ∘ Function.uncurry fun x1 x2 => x1 ⊔ x2) =
    (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t).inf' ⋯ 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 ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ ((filter (fun b => b ≤ a) s ⊻ filter (fun b => b ≤ a) t).inf' ⋯ fun x => id x) =
    (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t).inf' ⋯ fun i => id i.1 ⊔ id i.2

Tactic:
simp_rw [← image_sup_product]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 => x1 ⊔ x2) (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t)).inf' ⋯
      fun x => id x) =
    (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t).inf' ⋯ 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 ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 => x1 ⊔ x2) (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t)).inf' ⋯
      fun x => id x) =
    (filter (fun b => b ≤ a) s ×ˢ filter (fun b => b ≤ a) t).inf' ⋯ fun i => id i.1 ⊔ id i.2

Tactic:
rw [inf'_image]

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