case H0
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s → Monotone (f i)
hf : ∀ (i : ι), i ∈ ∅ → Monotone (f i)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ ∅), f i j) = ⨅ (i : ι) (_ : i ∈ ∅), ⨆ (j : ι'), f i j

case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : ∀ (i : ι), i ∈ insert a s → Monotone (f i)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ insert a s), f i j) = ⨅ (i : ι) (_ : i ∈ insert a s), ⨆ (j : ι'), f i j
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s : Set ι
hs : Set.Finite s
f : ι → ι' → α
hf : ∀ (i : ι), i ∈ s → Monotone (f i)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
induction' s, hs using Set.Finite.dinduction_on with a s _ _ ihs hf
no goals
case H0
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s → Monotone (f i)
hf : ∀ (i : ι), i ∈ ∅ → Monotone (f i)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ ∅), f i j) = ⨅ (i : ι) (_ : i ∈ ∅), ⨆ (j : ι'), f i j
simp [iSup_const]
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : Monotone (f a) ∧ ∀ (x : ι), x ∈ s → Monotone (f x)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ insert a s), f i j) = ⨅ (i : ι) (_ : i ∈ insert a s), ⨆ (j : ι'), f i j
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : ∀ (i : ι), i ∈ insert a s → Monotone (f i)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ insert a s), f i j) = ⨅ (i : ι) (_ : i ∈ insert a s), ⨆ (j : ι'), f i j
rw [ball_insert_iff] at hf
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : Monotone (f a) ∧ ∀ (x : ι), x ∈ s → Monotone (f x)
⊢ (⨆ (j : ι'), f a j ⊓ ⨅ (x : ι) (_ : x ∈ s), f x j) = (⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : Monotone (f a) ∧ ∀ (x : ι), x ∈ s → Monotone (f x)
⊢ (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ insert a s), f i j) = ⨅ (i : ι) (_ : i ∈ insert a s), ⨆ (j : ι'), f i j
simp only [iInf_insert, ← ihs hf.2]
no goals
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    (⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j) = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : Monotone (f a) ∧ ∀ (x : ι), x ∈ s → Monotone (f x)
⊢ (⨆ (j : ι'), f a j ⊓ ⨅ (x : ι) (_ : x ∈ s), f x j) = (⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j
exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj