case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ min ↑a ↑b = map₂ min ↑a ↑b

case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ min ↑a ↑b = map₂ min ↑a ↑b
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
⊢ min ↑a ↑b = map₂ min ↑a ↑b
cases' le_total (a : β*) b with h h
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x => min (a x) (b x)
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ min ↑a ↑b = map₂ min ↑a ↑b
rw [min_eq_left h, map₂_coe, coe_eq]
no goals
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x => min (a x) (b x)
exact h.mono fun i hi => (min_eq_left hi).symm
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ b =ᶠ[↑φ] fun x => min (a x) (b x)
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ min ↑a ↑b = map₂ min ↑a ↑b
rw [min_eq_right h, map₂_coe, coe_eq]
no goals
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ b =ᶠ[↑φ] fun x => min (a x) (b x)
exact h.mono fun i hi => (min_eq_right hi).symm