[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
src✝¹ : DivInvMonoid (Germ (↑φ) β) := divInvMonoid
src✝ : MonoidWithZero (Germ (↑φ) β) := monoidWithZero
⊢ ((fun x x_1 => x ∘ x_1) Inv.inv fun x => 0) =ᶠ[↑φ] fun x => 0
[PROOFSTEP]
simp only [Function.comp, inv_zero]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
src✝¹ : DivInvMonoid (Germ (↑φ) β) := divInvMonoid
src✝ : MonoidWithZero (Germ (↑φ) β) := monoidWithZero
⊢ (fun x => 0) =ᶠ[↑φ] fun x => 0
[PROOFSTEP]
exact EventuallyEq.refl _ fun _ => 0
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
f g : α → β
⊢ ↑f < ↑g ↔ ∀* (x : α), f x < g x
[PROOFSTEP]
simp only [lt_iff_le_not_le, eventually_and, coe_le, eventually_not, EventuallyLE]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
⊢ (fun x x_1 => x < x_1) = LiftRel fun x x_1 => x < x_1
[PROOFSTEP]
ext ⟨f⟩ ⟨g⟩
[GOAL]
case h.mk.h.mk.a
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
x✝¹ : Germ (↑φ) β
f : α → β
x✝ : Germ (↑φ) β
g : α → β
⊢ Quot.mk Setoid.r f < Quot.mk Setoid.r g ↔ LiftRel (fun x x_1 => x < x_1) (Quot.mk Setoid.r f) (Quot.mk Setoid.r g)
[PROOFSTEP]
exact coe_lt
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
⊢ max ↑a ↑b = map₂ max ↑a ↑b
[PROOFSTEP]
cases' le_total (a : β*) b with h h
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ max ↑a ↑b = map₂ max ↑a ↑b
[PROOFSTEP]
rw [max_eq_right h, map₂_coe, coe_eq]
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ b =ᶠ[↑φ] fun x => max (a x) (b x)
[PROOFSTEP]
exact h.mono fun i hi => (max_eq_right hi).symm
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ max ↑a ↑b = map₂ max ↑a ↑b
[PROOFSTEP]
rw [max_eq_left h, map₂_coe, coe_eq]
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ a =ᶠ[↑φ] fun x => max (a x) (b x)
[PROOFSTEP]
exact h.mono fun i hi => (max_eq_left hi).symm
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
⊢ min ↑a ↑b = map₂ min ↑a ↑b
[PROOFSTEP]
cases' le_total (a : β*) b with h h
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ min ↑a ↑b = map₂ min ↑a ↑b
[PROOFSTEP]
rw [min_eq_left h, map₂_coe, coe_eq]
[GOAL]
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)
[PROOFSTEP]
exact h.mono fun i hi => (min_eq_left hi).symm
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ min ↑a ↑b = map₂ min ↑a ↑b
[PROOFSTEP]
rw [min_eq_right h, map₂_coe, coe_eq]
[GOAL]
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)
[PROOFSTEP]
exact h.mono fun i hi => (min_eq_right hi).symm
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(max x y) = max ↑x ↑y
[PROOFSTEP]
rw [max_def, map₂_const]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(min x y) = min ↑x ↑y
[PROOFSTEP]
rw [min_def, map₂_const]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrderedAddCommGroup β
x : β
⊢ ↑|x| = |↑x|
[PROOFSTEP]
rw [abs_def, map_const]
