[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ s
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g ↔ ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g → ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s
[PROOFSTEP]
rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1, t₁_1 ∈ f ∧ ∃ t₂_1, t₂_1 ∈ g ∧ prod t₁_1 t₂_1 ⊆ t₁ ∩ t₂
[PROOFSTEP]
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s) → s ∈ comap Prod.fst f ⊓ comap Prod.snd g
[PROOFSTEP]
rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : prod t₁ t₂ ⊆ s
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g
[PROOFSTEP]
exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s} ∈ f
[PROOFSTEP]
rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ 𝓟 t ∧ t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1, t_1 ∈ f ∧ t_1 ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
[PROOFSTEP]
refine' exists_congr fun u => Iff.rfl.and ⟨_, fun h => ⟨t, mem_principal_self t, _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
⊢ (∃ t₂, t₂ ∈ 𝓟 t ∧ u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
[PROOFSTEP]
rintro ⟨v, v_in, hv⟩ a a_in b b_in
[GOAL]
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s
[PROOFSTEP]
exact hv (mk_mem_prod a_in <| v_in b_in)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
h : u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx, hy⟩
[GOAL]
case refine'_2.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
h : u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
x : α
y : β
hx : (x, y).fst ∈ u
hy : (x, y).snd ∈ t
⊢ (x, y) ∈ s
[PROOFSTEP]
exact h hx y hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
[PROOFSTEP]
rw [← principal_univ, mem_prod_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ {a | ∀ (b : β), b ∈ univ → (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
[PROOFSTEP]
simp only [mem_univ, forall_true_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
s : Set β
⊢ (∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ s → p (x, y)
[PROOFSTEP]
rw [eventually_iff, eventually_iff, mem_prod_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
s : Set β
⊢ {a | ∀ (b : β), b ∈ s → (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ (y : β), y ∈ s → p (x, y)} ∈ f
[PROOFSTEP]
simp only [mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
[PROOFSTEP]
erw [comap_inf, Filter.comap_comap, Filter.comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ f ×ˢ ⊤ = comap Prod.fst f
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ Filter.prod f ⊤ = comap Prod.fst f
[PROOFSTEP]
rw [Filter.prod, comap_top, inf_top_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g✝ : Filter β
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g✝ : Filter β
f₁ f₂ : Filter α
g : Filter β
⊢ Filter.prod (f₁ ⊔ f₂) g = Filter.prod f₁ g ⊔ Filter.prod f₂ g
[PROOFSTEP]
rw [Filter.prod, comap_sup, inf_sup_right, ← Filter.prod, ← Filter.prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ Filter.prod f (g₁ ⊔ g₂) = Filter.prod f g₁ ⊔ Filter.prod f g₂
[PROOFSTEP]
rw [Filter.prod, comap_sup, inf_sup_left, ← Filter.prod, ← Filter.prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
p : α × β → Prop
f : Filter α
g : Filter β
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
    ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
[PROOFSTEP]
simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
[PROOFSTEP]
rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
la : Filter α
lb : Filter β
p : α × β → Prop
h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
[PROOFSTEP]
exact ha.mono fun a ha => hb.mono fun b hb => h ha hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
⊢ ∀ᶠ (i : α) in f, p (i, i)
[PROOFSTEP]
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : α → Prop
hs : ∀ᶠ (y : α) in f, s y
hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)
⊢ ∀ᶠ (i : α) in f, p (i, i)
[PROOFSTEP]
apply (ht.and hs).mono fun x hx => hst hx.1 hx.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
⊢ (∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
refine' (ht.diag_of_prod.prod_mk hs).mono fun x hx => by simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
x : α × γ
hx : t (x.fst, x.fst) ∧ s x.snd
⊢ p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
⊢ (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
[PROOFSTEP]
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
[PROOFSTEP]
refine' (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
x : α × γ
hx : t x.fst ∧ s (x.snd, x.snd)
⊢ p (x.fst, x.snd, x.snd)
[PROOFSTEP]
simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ (i : ι), f i) ×ˢ g = ⨅ (i : ι), f i ×ˢ g
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ Filter.prod (⨅ (i : ι), f i) g = ⨅ (i : ι), Filter.prod (f i) g
[PROOFSTEP]
rw [Filter.prod, comap_iInf, iInf_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ ⨅ (x : ι), comap Prod.fst (f x) ⊓ comap Prod.snd g = ⨅ (i : ι), Filter.prod (f i) g
[PROOFSTEP]
simp only [Filter.prod, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ f ×ˢ ⨅ (i : ι), g i = ⨅ (i : ι), f ×ˢ g i
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ Filter.prod f (⨅ (i : ι), g i) = ⨅ (i : ι), Filter.prod f (g i)
[PROOFSTEP]
rw [Filter.prod, comap_iInf, inf_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ ⨅ (x : ι), comap Prod.fst f ⊓ comap Prod.snd (g x) = ⨅ (i : ι), Filter.prod f (g i)
[PROOFSTEP]
simp only [Filter.prod, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : β₁ → α₁
m₂ : β₂ → α₂
⊢ comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p => (m₁ p.fst, m₂ p.snd)) (f₁ ×ˢ f₂)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_comap, comap_inf, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ f ×ˢ g = comap Prod.swap (g ×ˢ f)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_comap, (· ∘ ·), inf_comm, Prod.swap, comap_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ f ×ˢ g = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
[PROOFSTEP]
rw [prod_comm', ← map_swap_eq_comap_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ Prod.swap <$> (g ×ˢ f) = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t, t ∈ f ∧ ∀ᶠ (y : β) in g, ∀ (x : α), x ∈ t → (x, y) ∈ s
[PROOFSTEP]
simp only [mem_prod_iff, prod_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ ∀ (x : α), x ∈ t₁ → ∀ (y : β), y ∈ t₂ → (x, y) ∈ s) ↔
    ∃ t, t ∈ f ∧ ∀ᶠ (y : β) in g, ∀ (x : α), x ∈ t → (x, y) ∈ s
[PROOFSTEP]
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
x✝ : Set α
⊢ (∃ t₂, t₂ ∈ g ∧ ∀ (x : α), x ∈ x✝ → ∀ (y : β), y ∈ t₂ → (x, y) ∈ s) ↔
    ∃ t, t ∈ g ∧ t ⊆ {x | (fun y => ∀ (x : α), x ∈ x✝ → (x, y) ∈ s) x}
[PROOFSTEP]
exact exists_congr fun _ => Iff.rfl.and forall₂_swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t, t ∈ g ∧ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ t → (x, y) ∈ s
[PROOFSTEP]
rw [prod_comm, mem_map, mem_prod_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t, t ∈ g ∧ ∀ᶠ (y : α) in f, ∀ (x : β), x ∈ t → (x, y) ∈ (fun p => (p.snd, p.fst)) ⁻¹' s) ↔
    ∃ t, t ∈ g ∧ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ t → (x, y) ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
⊢ map Prod.fst (f ×ˢ g) = f
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
[PROOFSTEP]
simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def, exists_mem_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map Prod.snd (f ×ˢ g) = g
[PROOFSTEP]
rw [prod_comm, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map (Prod.snd ∘ fun p => (p.snd, p.fst)) (g ×ˢ f) = g
[PROOFSTEP]
apply map_fst_prod
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
⊢ f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.1 ▸ h.2 ▸ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
haveI := neBot_of_le hle.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : NeBot f₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
haveI := neBot_of_le hle.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : NeBot f₂
this : NeBot g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p (Prod.swap y)
[PROOFSTEP]
rw [prod_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map (fun p => (p.snd, p.fst)) (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p (Prod.swap y)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
⊢ map (↑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
[PROOFSTEP]
simp_rw [← comap_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc, (· ∘ ·),
  Equiv.prodAssoc_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
⊢ map (↑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
[PROOFSTEP]
simp_rw [map_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc, Function.comp,
  Equiv.prodAssoc_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
[PROOFSTEP]
simp_rw [map_swap4_eq_comap, SProd.sprod, Filter.prod, comap_inf, comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p => (m₁ p.fst, m₂ p.snd)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p => (m₁ p.fst, m₂ p.snd)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s
[PROOFSTEP]
rwa [prod_image_image_eq, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β
F : Filter α
G : Filter γ
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)
[PROOFSTEP]
rw [← prod_map_map_eq', map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : β → γ
F : Filter α
G : Filter β
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
[PROOFSTEP]
rw [← prod_map_map_eq', map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
[PROOFSTEP]
erw [Tendsto, ← prod_map_map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d
[PROOFSTEP]
exact Filter.prod_mono hf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = seq (map (fun a b => m (a, b)) f) g
[PROOFSTEP]
simp [Filter.ext_iff, mem_prod_iff, mem_map_seq_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
⊢ ∀ (s : Set γ),
    (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔
      ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
[PROOFSTEP]
intro s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔
    ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) →
    ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s) →
    ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s
[PROOFSTEP]
exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s) →
    ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s
[PROOFSTEP]
exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ f ×ˢ g = seq (map Prod.mk f) g
[PROOFSTEP]
have h := f.map_prod id g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : map id (f ×ˢ g) = seq (map (fun a b => id (a, b)) f) g
⊢ f ×ˢ g = seq (map Prod.mk f) g
[PROOFSTEP]
rwa [map_id] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_inf, inf_comm, inf_assoc, inf_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g✝ : Filter β
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
[PROOFSTEP]
rw [prod_inf_prod, inf_idem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
[PROOFSTEP]
rw [prod_inf_prod, inf_idem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = prod s t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
a : α
f : Filter β
⊢ pure a ×ˢ f = map (Prod.mk a) f
[PROOFSTEP]
rw [prod_eq, map_pure, pure_seq_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B
[PROOFSTEP]
rw [Filter.pure_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ f ×ˢ pure b = map (fun a => (a, b)) f
[PROOFSTEP]
rw [prod_eq, seq_pure, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
a : α
b : β
⊢ pure a ×ˢ pure b = pure (a, b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
[PROOFSTEP]
simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop, Subtype.exists',
  exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ NeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g
[PROOFSTEP]
simp only [neBot_iff, Ne, prod_eq_bot, not_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔
    ∀ (W : Set γ), W ∈ z → ∃ U, U ∈ x ∧ ∃ V, V ∈ y ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
[PROOFSTEP]
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ g ×ˢ g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ Filter.prod g g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'
[PROOFSTEP]
unfold Filter.prod
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ comap Prod.fst g ⊓ comap Prod.snd g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'
[PROOFSTEP]
simp only [le_inf_iff, ← map_le_iff_le_comap, Tendsto]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (Filter.prod g g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
[PROOFSTEP]
unfold Filter.prod
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (comap Prod.fst g ⊓ comap Prod.snd g') ↔
    Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
[PROOFSTEP]
simp only [tendsto_inf, tendsto_comap_iff, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ Filter.coprod f g ↔ (∃ t₁, t₁ ∈ f ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, t₂ ∈ g ∧ Prod.snd ⁻¹' t₂ ⊆ s
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g l : Filter β
⊢ Filter.coprod ⊥ l = comap Prod.snd l
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
l : Filter α
⊢ Filter.coprod l ⊥ = comap Prod.fst l
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
⊢ Filter.coprod ⊥ ⊥ = ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ Filter.coprod la lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb
[PROOFSTEP]
simp only [Filter.coprod, mem_sup, compl_mem_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
⊢ NeBot (Filter.coprod f g) ↔ NeBot f ∧ Nonempty β ∨ Nonempty α ∧ NeBot g
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Filter.coprod (𝓟 s) (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
[PROOFSTEP]
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter, preimage_compl,
  preimage_compl, compl_compl, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂) ≤ Filter.coprod (map m₁ f₁) (map m₂ f₂)
[PROOFSTEP]
intro s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ Filter.coprod (map m₁ f₁) (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂)
[PROOFSTEP]
simp only [mem_map, mem_coprod_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ ((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
[PROOFSTEP]
rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
[PROOFSTEP]
refine' ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ _⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ _⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.fst ⁻¹' (m₁ ⁻¹' u₁)
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.fst ⁻¹' u₁
[PROOFSTEP]
convert hx
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.snd ⁻¹' (m₂ ⁻¹' u₂)
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.snd ⁻¹' u₂
[PROOFSTEP]
convert hx
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Filter.coprod (map (fun x => b) (𝓟 {a})) (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})
[PROOFSTEP]
simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton, image_id, prod_univ,
  univ_prod, id]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x => b) id) (Filter.coprod (𝓟 {a}) (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)
[PROOFSTEP]
rw [principal_coprod_principal, map_principal]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)
[PROOFSTEP]
congr
[GOAL]
case e_s
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ
[PROOFSTEP]
ext ⟨b', i'⟩
[GOAL]
case e_s.h.mk
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ
[PROOFSTEP]
constructor
[GOAL]
case e_s.h.mk.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ
[PROOFSTEP]
rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
[GOAL]
case e_s.h.mk.mp.intro.mk.intro.refl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x => b) a'', id i'') ∈ {b} ×ˢ univ
[PROOFSTEP]
simp
[GOAL]
case e_s.h.mk.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
[PROOFSTEP]
rintro ⟨h₁, _⟩
[GOAL]
case e_s.h.mk.mpr.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
[PROOFSTEP]
use(a, i')
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x => b) id (a, i') = (b', i')
[PROOFSTEP]
simpa using h₁.symm


[GOAL]
α : Type u_1
inst✝ : LT α
a : α
⊢ ¬IsSuccLimit a ↔ ∃ b, b ⋖ a
[PROOFSTEP]
simp [IsSuccLimit]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
⊢ IsMax a
[PROOFSTEP]
by_contra H
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
H : ¬IsMax a
⊢ False
[PROOFSTEP]
exact h a (covby_succ_of_not_isMax H)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : ¬IsMax a
⊢ ¬IsSuccLimit (succ a)
[PROOFSTEP]
contrapose! ha
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : IsSuccLimit (succ a)
⊢ IsMax a
[PROOFSTEP]
exact ha.isMax
[GOAL]
α : Type u_1
inst✝² : Preorder α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
h : IsSuccLimit a
b : α
⊢ succ b ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccLimit (succ b)
⊢ False
[PROOFSTEP]
exact not_isMax _ h.isMax
[GOAL]
α : Type u_1
inst✝³ : Preorder α
a : α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccLimit a
b : α
hb : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
[GOAL]
case intro.zero
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
h : IsSuccLimit (succ^[Nat.zero] b)
hb : b ≤ succ^[Nat.zero] b
⊢ succ^[Nat.zero] b ≤ b
[PROOFSTEP]
exact le_rfl
[GOAL]
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccLimit (succ^[Nat.succ n] b)
hb : b ≤ succ^[Nat.succ n] b
⊢ succ^[Nat.succ n] b ≤ b
[PROOFSTEP]
rw [iterate_succ_apply'] at h
[GOAL]
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccLimit (succ (succ^[n] b))
hb : b ≤ succ^[Nat.succ n] b
⊢ succ^[Nat.succ n] b ≤ b
[PROOFSTEP]
exact (not_isSuccLimit_succ _ h).elim
[GOAL]
α : Type u_1
inst✝⁴ : Preorder α
a : α
inst✝³ : SuccOrder α
inst✝² : IsSuccArchimedean α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccLimit a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
⊢ ¬IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a
[PROOFSTEP]
rw [not_isSuccLimit_iff_exists_covby]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a
[PROOFSTEP]
refine' exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (Covby.succ_eq hba)⟩, _⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b✝ : α
C : α → Sort u_2
b : α
h : ¬IsMax b
⊢ b ⋖ succ b
[PROOFSTEP]
exact covby_succ_of_not_isMax h
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
h : ¬IsSuccLimit a
⊢ a ∈ range succ
[PROOFSTEP]
cases' not_isSuccLimit_iff.1 h with b hb
[GOAL]
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
h : ¬IsSuccLimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ
[PROOFSTEP]
exact ⟨b, hb.2⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
⊢ succ a < b
[PROOFSTEP]
by_cases h : IsMax a
[GOAL]
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : IsMax a
⊢ succ a < b
[PROOFSTEP]
rwa [h.succ_eq]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
[PROOFSTEP]
rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b
[PROOFSTEP]
refine' ⟨ha, fun hab => _⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False
[PROOFSTEP]
subst hab
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
C : α → Sort u_2
h : ¬IsMax a
hb : IsSuccLimit (succ a)
ha : a < succ a
⊢ False
[PROOFSTEP]
exact (h hb.isMax).elim
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
⊢ C b
[PROOFSTEP]
by_cases hb : IsSuccLimit b
[GOAL]
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ C b
[PROOFSTEP]
exact hl b hb
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsSuccLimit b
⊢ C b
[PROOFSTEP]
have H := Classical.choose_spec (not_isSuccLimit_iff.1 hb)
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsSuccLimit b
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) = b
⊢ C b
[PROOFSTEP]
rw [← H.2]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsSuccLimit b
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) = b
⊢ C (succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)))
[PROOFSTEP]
exact hs _ H.1
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b hs hl = hl b hb
[PROOFSTEP]
classical exact dif_pos hb
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b hs hl = hl b hb
[PROOFSTEP]
exact dif_pos hb
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
⊢ isSuccLimitRecOn (succ b) hs hl = hs b hb
[PROOFSTEP]
have hb' := not_isSuccLimit_succ_of_not_isMax hb
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
⊢ isSuccLimitRecOn (succ b) hs hl = hs b hb
[PROOFSTEP]
have H := Classical.choose_spec (not_isSuccLimit_iff.1 hb')
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ isSuccLimitRecOn (succ b) hs hl = hs b hb
[PROOFSTEP]
rw [isSuccLimitRecOn]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ (if hb : IsSuccLimit (succ b) then hl (succ b) hb
    else
      let_fun H :=
        (_ :
          ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
            succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b);
      Eq.mpr (_ : C (succ b) = C (succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))))
        (hs (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))
          (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))))) =
    hs b hb
[PROOFSTEP]
simp only [cast_eq_iff_heq, hb', not_false_iff, eq_mpr_eq_cast, dif_neg]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq
    (hs (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))
      (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))))
    (hs b hb)
[PROOFSTEP]
congr 1
[GOAL]
case e_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b) = b
[PROOFSTEP]
first
| exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
| exact proof_irrel_heq H.left hb
[GOAL]
case e_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b) = b
[PROOFSTEP]
exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
[GOAL]
case e_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))) hb
[PROOFSTEP]
first
| exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
| exact proof_irrel_heq H.left hb
[GOAL]
case e_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))) hb
[PROOFSTEP]
exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
[GOAL]
case e_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))) hb
[PROOFSTEP]
exact proof_irrel_heq H.left hb
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort u_2
inst✝ : NoMaxOrder α
⊢ ¬IsSuccLimit a ↔ a ∈ range succ
[PROOFSTEP]
simp_rw [isSuccLimit_iff_succ_ne, not_forall, not_ne_iff]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort u_2
inst✝ : NoMaxOrder α
⊢ (∃ x, succ x = a) ↔ a ∈ range succ
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
h : IsSuccLimit a
b : α
hb : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ IsSuccLimit a → a ≤ b
[PROOFSTEP]
refine' Succ.rec (fun _ => le_rfl) (fun c _ H hc => _) hb
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
⊢ succ c ≤ b
[PROOFSTEP]
have := hc.isMax.succ_eq
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
this : succ c = c
⊢ succ c ≤ b
[PROOFSTEP]
rw [this] at hc ⊢
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit c
this : succ c = c
⊢ c ≤ b
[PROOFSTEP]
exact H hc
[GOAL]
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
a b : α
C : α → Sort u_2
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMinOrder α
⊢ ¬IsSuccLimit a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LT α
a✝ a : α
⊢ ¬IsPredLimit a ↔ ∃ b, a ⋖ b
[PROOFSTEP]
simp [IsPredLimit]
[GOAL]
α : Type u_1
inst✝ : LT α
a : α
⊢ IsSuccLimit (↑toDual a) ↔ IsPredLimit a
[PROOFSTEP]
simp [IsSuccLimit, IsPredLimit]
[GOAL]
α : Type u_1
inst✝ : LT α
a : α
⊢ IsPredLimit (↑toDual a) ↔ IsSuccLimit a
[PROOFSTEP]
simp [IsSuccLimit, IsPredLimit]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
h : IsPredLimit (pred a)
⊢ IsMin a
[PROOFSTEP]
by_contra H
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
h : IsPredLimit (pred a)
H : ¬IsMin a
⊢ False
[PROOFSTEP]
exact h a (pred_covby_of_not_isMin H)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
ha : ¬IsMin a
⊢ ¬IsPredLimit (pred a)
[PROOFSTEP]
contrapose! ha
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
ha : IsPredLimit (pred a)
⊢ IsMin a
[PROOFSTEP]
exact ha.isMin
[GOAL]
α : Type u_1
inst✝² : Preorder α
a : α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
h : IsPredLimit a
b : α
⊢ pred b ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
h : IsPredLimit (pred b)
⊢ False
[PROOFSTEP]
exact not_isMin _ h.isMin
[GOAL]
α : Type u_1
inst✝⁴ : Preorder α
a : α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsPredLimit a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort u_2
⊢ ¬IsPredLimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a
[PROOFSTEP]
rw [← isSuccLimit_toDual_iff]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort u_2
⊢ ¬IsSuccLimit (↑toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a
[PROOFSTEP]
exact not_isSuccLimit_iff
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort u_2
h : ¬IsPredLimit a
⊢ a ∈ range pred
[PROOFSTEP]
cases' not_isPredLimit_iff.1 h with b hb
[GOAL]
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b✝ : α
C : α → Sort u_2
h : ¬IsPredLimit a
b : α
hb : ¬IsMin b ∧ pred b = a
⊢ a ∈ range pred
[PROOFSTEP]
exact ⟨b, hb.2⟩
[GOAL]
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : PredOrder α
a b : α
C : α → Sort u_2
inst✝¹ : IsPredArchimedean α
inst✝ : NoMaxOrder α
⊢ ¬IsPredLimit a
[PROOFSTEP]
simp


[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ Monotone (↑toDual ∘ f ∘ ↑ofDual) ↔ Monotone f
[PROOFSTEP]
rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ Antitone (↑toDual ∘ f ∘ ↑ofDual) ↔ Antitone f
[PROOFSTEP]
rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ MonotoneOn f s
[PROOFSTEP]
rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ AntitoneOn f s
[PROOFSTEP]
rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (↑toDual ∘ f ∘ ↑ofDual) ↔ StrictMono f
[PROOFSTEP]
rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAnti (↑toDual ∘ f ∘ ↑ofDual) ↔ StrictAnti f
[PROOFSTEP]
rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ StrictMonoOn f s
[PROOFSTEP]
rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ StrictAntiOn f s
[PROOFSTEP]
rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f
[PROOFSTEP]
intro x y hf
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
⊢ x = y
[PROOFSTEP]
rcases lt_trichotomy x y with (hxy | rfl | hxy)
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : x < y
⊢ x = y
[PROOFSTEP]
exact absurd hf <| h _ _ hxy
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x : α
hf : f x = f x
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : y < x
⊢ x = y
[PROOFSTEP]
exact absurd hf.symm <| h _ _ hxy
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
⊢ StrictMono fun x => if p x then f x else g x
[PROOFSTEP]
intro x y h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
by_cases hy : p y
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
have hx : p x := hp h hy
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
simpa [hx, hy] using hf h
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
by_cases hx : p x
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
simpa [hx, hy] using hfg hx hy h
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
simpa [hx, hy] using hg h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b
[PROOFSTEP]
rw [lt_iff_le_not_le, lt_iff_le_not_le, hf.le_iff_le ha hb, hf.le_iff_le hb ha]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
simp_rw [Monotone, Antitone, not_forall, not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) ↔
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
refine' Iff.symm ⟨_, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) →
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
  exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩]
}
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
[PROOFSTEP]
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
case refine'_1.intro.intro.intro.intro.intro.inr.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
[PROOFSTEP]
exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) →
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
rintro ⟨⟨a, b, hab, hfba⟩, c, d, hcd, hfcd⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hda | had := le_total d a
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ obtain hfad | hfda := le_total (f a) (f d)
  {exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
  }
  {exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
  }
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfad | hfda := le_total (f a) (f d)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfad : f a ≤ f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfad : f a ≤ f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hac | hca := le_total a c
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ obtain hfdb | hfbd := le_or_lt (f d) (f b)
  {exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩
  }
  obtain hfca | hfac := lt_or_le (f c) (f a)
  {exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
  }
  obtain hbd | hdb := le_total b d
  {exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
  }
  {exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
  }
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfdb | hfbd := le_or_lt (f d) (f b)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfca | hfac := lt_or_le (f c) (f a)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hbd | hdb := le_total b d
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ obtain hfdb | hfbd := le_or_lt (f d) (f b)
  {exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩
  }
  obtain hfca | hfac := lt_or_le (f c) (f a)
  {exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
  }
  obtain hbd | hdb := le_total b d
  {exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
  }
  {exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
  }
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfdb | hfbd := le_or_lt (f d) (f b)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfca | hfac := lt_or_le (f c) (f a)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hbd | hdb := le_total b d
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ (∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
refine' exists₃_congr (fun a b c ↦ and_congr_left $ fun h ↦ (Ne.le_iff_lt _).and $ Ne.le_iff_lt _)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ a ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
⊢ r (f b) (f c)
[PROOFSTEP]
induction' hbc with k b_lt_k r_b_k
[GOAL]
case refl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
⊢ r (f b) (f (succ b))
case step
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
k : ℕ
b_lt_k : Nat.le (succ b) k
r_b_k : r (f b) (f k)
⊢ r (f b) (f (succ k))
[PROOFSTEP]
exacts [h _ hab, _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ∃ f, StrictMono f ∧ f 0 = a
[PROOFSTEP]
choose g hg using fun x : α ↦ exists_gt x
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
g : α → α
hg : ∀ (x : α), x < g x
⊢ ∃ f, StrictMono f ∧ f 0 = a
[PROOFSTEP]
exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)
[PROOFSTEP]
rcases lt.dest hab with ⟨n, rfl⟩
[GOAL]
case intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑(Nat.succ n)
⊢ r (f a) (f (a + ↑(Nat.succ n)))
[PROOFSTEP]
clear hab
[GOAL]
case intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑(Nat.succ n)))
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case intro.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + ↑(Nat.succ Nat.zero)))
[PROOFSTEP]
rw [Int.ofNat_one]
[GOAL]
case intro.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))
[PROOFSTEP]
apply h
[GOAL]
case intro.succ
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(Nat.succ (Nat.succ n))))
[PROOFSTEP]
rw [Int.ofNat_succ, ← Int.add_assoc]
[GOAL]
case intro.succ
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
[PROOFSTEP]
exact _root_.trans ihn (h _)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ∃ f, StrictMono f
[PROOFSTEP]
inhabit α
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ f, StrictMono f
[PROOFSTEP]
rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
⊢ ∃ f, StrictMono f
[PROOFSTEP]
rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∃ f, StrictMono f
[PROOFSTEP]
refine' ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ _⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∀ (n : ℤ), (Int.casesOn n f fun n => g (n + 1)) < Int.casesOn (n + 1) f fun n => g (n + 1)
[PROOFSTEP]
rintro (n | _ | n)
[GOAL]
case intro.intro.intro.intro.ofNat
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn (ofNat n) f fun n => g (n + 1)) < Int.casesOn (ofNat n + 1) f fun n => g (n + 1)
[PROOFSTEP]
exact hf n.lt_succ_self
[GOAL]
case intro.intro.intro.intro.negSucc.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (Int.casesOn -[Nat.zero+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.zero+1] + 1) f fun n => g (n + 1)
[PROOFSTEP]
show g 1 < f 0
[GOAL]
case intro.intro.intro.intro.negSucc.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < f 0
[PROOFSTEP]
rw [hf₀, ← hg₀]
[GOAL]
case intro.intro.intro.intro.negSucc.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < g 0
[PROOFSTEP]
exact hg Nat.zero_lt_one
[GOAL]
case intro.intro.intro.intro.negSucc.succ
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn -[Nat.succ n+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.succ n+1] + 1) f fun n => g (n + 1)
[PROOFSTEP]
exact hg (Nat.lt_succ_self _)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h1).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h2)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h2).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h1)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h1).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h2)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h2).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h1)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a < b → Prod.map f g a < Prod.map f g b
[PROOFSTEP]
simp only [Prod.lt_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd
[PROOFSTEP]
exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a
[PROOFSTEP]
simp only [Prod.lt_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd
[PROOFSTEP]
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)