-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Finite.iSup_biInf_of_monotone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (· ≤ ·)] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α}
    (hf : ∀ i ∈ s, Monotone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j

Proof state:
case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, f a✝¹ j ⊓ ⨅ x ∈ s✝, f x j = (⨆ j, f a✝¹ j) ⊓ ⨆ j, ⨅ i ∈ s✝, f i j

Tactic:
exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

Result:
no goals

Proof state:
case empty
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
hf : ∀ i ∈ ∅, Monotone (f i)
⊢ ⨆ j, ⨅ i ∈ ∅, f i j = ⨅ i ∈ ∅, ⨆ j, f i j

Tactic:
simp [iSup_const]

Result:
no goals

Proof state:
case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : ∀ i ∈ insert a✝¹ s✝, Monotone (f i)
⊢ ⨆ j, ⨅ i ∈ insert a✝¹ s✝, f i j = ⨅ i ∈ insert a✝¹ s✝, ⨆ j, f i j

Tactic:
rw [forall_mem_insert] at hf

Result:
case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, ⨅ i ∈ insert a✝¹ s✝, f i j = ⨅ i ∈ insert a✝¹ s✝, ⨆ j, f i j

Proof state:
case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, ⨅ i ∈ insert a✝¹ s✝, f i j = ⨅ i ∈ insert a✝¹ s✝, ⨆ j, f i j

Tactic:
simp only [iInf_insert, ← ihs hf.2]

Result:
case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, f a✝¹ j ⊓ ⨅ x ∈ s✝, f x j = (⨆ j, f a✝¹ j) ⊓ ⨆ j, ⨅ i ∈ s✝, f i j

Proof state:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : ι → ι' → α
hf : ∀ i ∈ s, Monotone (f i)
⊢ ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j

Tactic:
induction s, hs using Set.Finite.induction_on with
| empty => simp [iSup_const]
| insert _ _ ihs =>
  rw [forall_mem_insert] at hf
  simp only [iInf_insert, ← ihs hf.2]
  exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

Result:
no goals