ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : l.Germ β<VAR>g : l.Germ γ<VAR>h : l.Germ δ<VAR>p : l.Germ β → l.Germ γ → l.Germ δ → Prop<VAR>H : ∀ (f : α → β) (g : α → γ) (h : α → δ), p ↑f ↑g ↑h<GOAL>p f g h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>lc : Filter γ<VAR>F : (α → β) → γ → δ<VAR>hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F<VAR>f : α → β<GOAL>Filter.Germ.map' F hF ↑f = ↑(F f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f g : α → β<GOAL>↑f = ↑g ↔ f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>op : β → γ<VAR>f : α → β<GOAL>Filter.Germ.map op ↑f = ↑(op ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<GOAL>Filter.Germ.map id = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>op₁ : γ → δ<VAR>op₂ : β → γ<VAR>f : l.Germ β<GOAL>Filter.Germ.map op₁ (Filter.Germ.map op₂ f) = Filter.Germ.map (op₁ ∘ op₂) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>op : β → γ → δ<VAR>f : α → β<VAR>g : α → γ<GOAL>Filter.Germ.map₂ op ↑f ↑g = ↑fun x => op (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>lb : Filter β<GOAL>(↑f).Tendsto lb ↔ Filter.Tendsto f l lb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>lc : Filter γ<VAR>g : lc.Germ α<VAR>hg : g.Tendsto l<GOAL>(↑f).compTendsto' g hg = Filter.Germ.map f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hg : Filter.Tendsto g lc l<GOAL>(↑f).compTendsto g hg = ↑(f ∘ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : l.Germ β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hg : Filter.Tendsto g lc l<GOAL>f.compTendsto' ↑g ⋯ = f.compTendsto g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : β → γ<VAR>l : Filter α<VAR>l' : Filter β<VAR>h : f =ᶠ[l'] g<VAR>φ : α → β<VAR>hφ : Filter.Tendsto φ l l'<GOAL>↑(f ∘ φ) = ↑(g ∘ φ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hf : (↑f).IsConstant<VAR>hg : Filter.Tendsto g lc l<GOAL>(↑(f ∘ g)).IsConstant
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : l.Germ β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hf : f.IsConstant<VAR>hg : Filter.Tendsto g lc l<GOAL>(f.compTendsto g hg).IsConstant
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>l.NeBot<VAR>a b : β<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>a : β<VAR>f : β → γ<GOAL>Filter.Germ.map f ↑a = ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>b : β<VAR>c : γ<VAR>f : β → γ → δ<GOAL>Filter.Germ.map₂ f ↑b ↑c = ↑(f b c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>b : β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hg : Filter.Tendsto g lc l<GOAL>(↑b).compTendsto g hg = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>b : β<VAR>lc : Filter γ<VAR>g : lc.Germ α<VAR>hg : g.Tendsto l<GOAL>(↑b).compTendsto' g hg = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<GOAL>Filter.Germ.LiftPred p ↑f ↔ ∀ᶠ (x : α) in l, p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>p : β → Prop<VAR>x : β<VAR>hx : p x<GOAL>Filter.Germ.LiftPred p ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>l.NeBot<VAR>p : β → Prop<VAR>x : β<GOAL>Filter.Germ.LiftPred p ↑x ↔ p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>r : β → γ → Prop<VAR>f : α → β<VAR>g : α → γ<GOAL>Filter.Germ.LiftRel r ↑f ↑g ↔ ∀ᶠ (x : α) in l, r (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>r : β → γ → Prop<VAR>x : β<VAR>y : γ<VAR>h : r x y<GOAL>Filter.Germ.LiftRel r ↑x ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>l.NeBot<VAR>r : β → γ → Prop<VAR>x : β<VAR>y : γ<GOAL>Filter.Germ.LiftRel r ↑x ↑y ↔ r x y
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Add M<VAR>f g : α → M<GOAL>↑(f + g) = ↑f + ↑g
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Mul M<VAR>f g : α → M<GOAL>↑(f * g) = ↑f * ↑g
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Zero M<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>One M<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>VAdd M G<VAR>n : M<VAR>f : α → G<GOAL>↑(n +ᵥ f) = n +ᵥ ↑f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>SMul M G<VAR>n : M<VAR>f : α → G<GOAL>↑(n • f) = n • ↑f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>SMul M G<VAR>n : M<VAR>a : G<GOAL>↑(n • a) = n • ↑a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>VAdd M G<VAR>n : M<VAR>a : G<GOAL>↑(n +ᵥ a) = n +ᵥ ↑a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>Pow G M<VAR>f : α → G<VAR>n : M<GOAL>↑(f ^ n) = ↑f ^ n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>SMul M G<VAR>f : α → G<VAR>n : M<GOAL>↑(n • f) = n • ↑f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>Pow G M<VAR>a : G<VAR>n : M<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>G : Type u_6<VAR>SMul M G<VAR>a : G<VAR>n : M<GOAL>↑(n • a) = n • ↑a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Monoid M<GOAL>⇑(Filter.Germ.coeMulHom l) = Filter.Germ.ofFun
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>AddMonoid M<GOAL>⇑(Filter.Germ.coeAddHom l) = Filter.Germ.ofFun
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>NatCast M<VAR>n : ℕ<GOAL>(↑fun x => ↑n) = ↑n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>NatCast M<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>NatCast M<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>IntCast M<VAR>n : ℤ<GOAL>(↑fun x => ↑n) = ↑n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>G : Type u_6<VAR>Neg G<VAR>f : α → G<GOAL>↑(-f) = -↑f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>G : Type u_6<VAR>Inv G<VAR>f : α → G<GOAL>↑f⁻¹ = (↑f)⁻¹
<VAR>α : Type u_1<VAR>l : Filter α<VAR>G : Type u_6<VAR>Neg G<VAR>a : G<GOAL>↑(-a) = -↑a
<VAR>α : Type u_1<VAR>l : Filter α<VAR>G : Type u_6<VAR>Inv G<VAR>a : G<GOAL>↑a⁻¹ = (↑a)⁻¹
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Div M<VAR>f g : α → M<GOAL>↑(f / g) = ↑f / ↑g
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Sub M<VAR>f g : α → M<GOAL>↑(f - g) = ↑f - ↑g
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Sub M<VAR>a b : M<GOAL>↑(a - b) = ↑a - ↑b
<VAR>α : Type u_1<VAR>l : Filter α<VAR>M : Type u_5<VAR>Div M<VAR>a b : M<GOAL>↑(a / b) = ↑a / ↑b
<VAR>α : Type u_1<VAR>l : Filter α<VAR>R : Type u_5<VAR>Semiring R<GOAL>⇑(Filter.Germ.coeRingHom l) = Filter.Germ.ofFun
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>M : Type u_5<VAR>VAdd M β<VAR>c : α → M<VAR>f : α → β<GOAL>↑(c +ᵥ f) = ↑c +ᵥ ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>M : Type u_5<VAR>SMul M β<VAR>c : α → M<VAR>f : α → β<GOAL>↑(c • f) = ↑c • ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>LE β<GOAL>(fun x x_1 => x ≤ x_1) = Filter.Germ.LiftRel fun x x_1 => x ≤ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f g : α → β<VAR>LE β<GOAL>↑f ≤ ↑g ↔ f ≤ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>LE β<VAR>Zero β<VAR>f : α → β<GOAL>0 ≤ ↑f ↔ ∀ᶠ (x : α) in l, 0 ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>LE β<VAR>x y : β<GOAL>x ≤ y → ↑x ≤ ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>LE β<VAR>l.NeBot<VAR>x y : β<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Bot β<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Top β<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Sup β<VAR>a b : β<GOAL>↑(a ⊔ b) = ↑a ⊔ ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Inf β<VAR>a b : β<GOAL>↑(a ⊓ b) = ↑a ⊓ ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>Filter.EventuallyConst f l ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>x : ι → α<VAR>h : l.HasBasis p s<VAR>hx : ∀ (i : ι), p i → x i ∈ s i<GOAL>Filter.EventuallyConst f l ↔ ∃ i, p i ∧ ∀ y ∈ s i, f y = f (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Nonempty β<GOAL>Filter.EventuallyConst f l ↔ ∃ x, Filter.Tendsto f l (pure x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>x : β<VAR>h : Filter.Tendsto f l (pure x)<GOAL>Filter.EventuallyConst f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Nonempty β<GOAL>Filter.EventuallyConst f l ↔ ∃ c, f =ᶠ[l] fun x => c
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : α → Prop<GOAL>Filter.EventuallyConst p l ↔ (p =ᶠ[l] fun x => False) ∨ p =ᶠ[l] fun x => True
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : α → Prop<GOAL>Filter.EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x
<VAR>α : Type u_1<VAR>l : Filter α<VAR>s : Set α<GOAL>Filter.EventuallyConst s l ↔ s =ᶠ[l] ∅ ∨ s =ᶠ[l] Set.univ
<VAR>α : Type u_1<VAR>l : Filter α<VAR>s : Set α<GOAL>Filter.EventuallyConst s l ↔ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, x ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>s : Set β<VAR>f : α → β<GOAL>Filter.EventuallyConst (f ⁻¹' s) l ↔ Filter.EventuallyConst s (Filter.map f l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<GOAL>Filter.EventuallyConst f l ↔ Filter.EventuallyConst g l
<VAR>α : Type u_1<VAR>l : Filter α<GOAL>Filter.EventuallyConst id l ↔ l.Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Filter.EventuallyConst f ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>c : β<GOAL>Filter.EventuallyConst (fun x => c) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f g : α → β<VAR>h : Filter.EventuallyConst f l<VAR>hg : f =ᶠ[l] g<GOAL>Filter.EventuallyConst g l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Subsingleton β<GOAL>Filter.EventuallyConst f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>l' : Filter α<VAR>h : Filter.EventuallyConst f l<VAR>hl' : l' ≤ l<GOAL>Filter.EventuallyConst f l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Subsingleton α<GOAL>Filter.EventuallyConst f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>h : Filter.EventuallyConst f l<VAR>g : β → γ<GOAL>Filter.EventuallyConst (g ∘ f) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Neg β<VAR>h : Filter.EventuallyConst f l<GOAL>Filter.EventuallyConst (-f) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Inv β<VAR>h : Filter.EventuallyConst f l<GOAL>Filter.EventuallyConst f⁻¹ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>lb : Filter β<VAR>g : β → γ<VAR>hg : Filter.EventuallyConst g lb<VAR>hf : Filter.Tendsto f l lb<GOAL>Filter.EventuallyConst (g ∘ f) l
<VAR>α : Type u_1<VAR>l : Filter α<VAR>ι : Type u_5<VAR>p : ι → Type u_6<VAR>g : α → (x : ι) → p x<VAR>h : Filter.EventuallyConst g l<VAR>i : ι<GOAL>Filter.EventuallyConst (fun x => g x i) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Filter.EventuallyConst f l<VAR>op : β → γ → δ<VAR>hg : Filter.EventuallyConst g l<GOAL>Filter.EventuallyConst (fun x => op (f x) (g x)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l : Filter α<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Filter.EventuallyConst f l<VAR>hg : Filter.EventuallyConst g l<GOAL>Filter.EventuallyConst (fun x => (f x, g x)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Mul β<VAR>g : α → β<VAR>hf : Filter.EventuallyConst f l<VAR>hg : Filter.EventuallyConst g l<GOAL>Filter.EventuallyConst (f * g) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>f : α → β<VAR>Add β<VAR>g : α → β<VAR>hf : Filter.EventuallyConst f l<VAR>hg : Filter.EventuallyConst g l<GOAL>Filter.EventuallyConst (f + g) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Zero β<VAR>s : Set α<VAR>c : β<VAR>h : Filter.EventuallyConst (s.indicator fun x => c) l<VAR>hc : c ≠ 0<GOAL>Filter.EventuallyConst s l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>One β<VAR>s : Set α<VAR>c : β<VAR>h : Filter.EventuallyConst (s.mulIndicator fun x => c) l<VAR>hc : c ≠ 1<GOAL>Filter.EventuallyConst s l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Zero β<VAR>s : Set α<VAR>h : Filter.EventuallyConst s l<VAR>c : β<GOAL>Filter.EventuallyConst (s.indicator fun x => c) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>One β<VAR>s : Set α<VAR>h : Filter.EventuallyConst s l<VAR>c : β<GOAL>Filter.EventuallyConst (s.mulIndicator fun x => c) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Zero β<VAR>s : Set α<VAR>c : β<VAR>hc : c ≠ 0<GOAL>Filter.EventuallyConst (s.indicator fun x => c) l ↔ Filter.EventuallyConst s l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>One β<VAR>s : Set α<VAR>c : β<VAR>hc : c ≠ 1<GOAL>Filter.EventuallyConst (s.mulIndicator fun x => c) l ↔ Filter.EventuallyConst s l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>One β<VAR>s : Set α<VAR>c : β<GOAL>Filter.EventuallyConst (s.mulIndicator fun x => c) l ↔ c = 1 ∨ Filter.EventuallyConst s l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>Zero β<VAR>s : Set α<VAR>c : β<GOAL>Filter.EventuallyConst (s.indicator fun x => c) l ↔ c = 0 ∨ Filter.EventuallyConst s l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>SemilatticeSup α<VAR>Nonempty α<GOAL>Filter.EventuallyConst f Filter.atTop ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i
<VAR>α : Type u_1<VAR>f : ℕ → α<GOAL>Filter.EventuallyConst f Filter.atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Sup α<VAR>Sup β<VAR>self : SupHom α β<VAR>a b : α<GOAL>self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Inf α<VAR>Inf β<VAR>self : InfHom α β<VAR>a b : α<GOAL>self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Sup α<VAR>Sup β<VAR>Bot α<VAR>Bot β<VAR>self : SupBotHom α β<GOAL>self.toFun ⊥ = ⊥
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Inf α<VAR>Inf β<VAR>Top α<VAR>Top β<VAR>self : InfTopHom α β<GOAL>self.toFun ⊤ = ⊤
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Lattice α<VAR>Lattice β<VAR>self : LatticeHom α β<VAR>a b : α<GOAL>self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>self : BoundedLatticeHom α β<GOAL>self.toFun ⊤ = ⊤
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>self : BoundedLatticeHom α β<GOAL>self.toFun ⊥ = ⊥
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Sup α<VAR>Sup β<VAR>FunLike F α β<VAR>self : SupHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⊔ b) = f a ⊔ f b
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Inf α<VAR>Inf β<VAR>FunLike F α β<VAR>self : InfHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⊓ b) = f a ⊓ f b
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Sup α<VAR>Sup β<VAR>Bot α<VAR>Bot β<VAR>FunLike F α β<VAR>self : SupBotHomClass F α β<VAR>f : F<GOAL>f ⊥ = ⊥
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Inf α<VAR>Inf β<VAR>Top α<VAR>Top β<VAR>FunLike F α β<VAR>self : InfTopHomClass F α β<VAR>f : F<GOAL>f ⊤ = ⊤
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Lattice α<VAR>Lattice β<VAR>FunLike F α β<VAR>self : LatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⊓ b) = f a ⊓ f b
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>self : BoundedLatticeHomClass F α β<VAR>f : F<GOAL>f ⊤ = ⊤
<VAR>F : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>self : BoundedLatticeHomClass F α β<VAR>f : F<GOAL>f ⊥ = ⊥
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : F<VAR>InfHomClass F α β<VAR>hf : Function.Injective ⇑f<VAR>a : α<GOAL>(orderEmbeddingOfInjective f hf) a = f a
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<VAR>h : Disjoint a b<GOAL>Disjoint (f a) (f b)
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>Codisjoint (f a) (f b)
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<VAR>h : IsCompl a b<GOAL>IsCompl (f a) (f b)
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>FunLike F α β<VAR>BoundedLatticeHomClass F α β<VAR>f : F<VAR>a : α<GOAL>f aᶜ = (f a)ᶜ
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>FunLike F α β<VAR>BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a \ b) = f a \ f b
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>FunLike F α β<VAR>BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (symmDiff a b) = symmDiff (f a) (f b)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : SupHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : α → β<VAR>hf : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b<GOAL>⇑{ toFun := f, map_sup' := hf } = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f g : SupHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : SupHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : SupHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_3<VAR>Sup α<GOAL>⇑(SupHom.id α) = id
<VAR>α : Type u_3<VAR>Sup α<VAR>a : α<GOAL>(SupHom.id α) a = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>f : SupHom β γ<VAR>g : SupHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>f : SupHom β γ<VAR>g : SupHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>Sup δ<VAR>f : SupHom γ δ<VAR>g : SupHom β γ<VAR>h : SupHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : SupHom α β<GOAL>f.comp (SupHom.id α) = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : SupHom α β<GOAL>(SupHom.id β).comp f = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>g₁ g₂ : SupHom β γ<VAR>f : SupHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>g : SupHom β γ<VAR>f₁ f₂ : SupHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>b : β<GOAL>⇑(SupHom.const α b) = Function.const α b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>b : β<VAR>a : α<GOAL>(SupHom.const α b) a = b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>f g : SupHom α β<GOAL>⇑(f ⊔ g) = ⇑(f ⊔ g)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>Bot β<GOAL>⇑⊥ = ⊥
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>Top β<GOAL>⇑⊤ = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>f g : SupHom α β<VAR>a : α<GOAL>(f ⊔ g) a = f a ⊔ g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>Bot β<VAR>a : α<GOAL>⊥ a = ⊥
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>SemilatticeSup β<VAR>Top β<VAR>a : α<GOAL>⊤ a = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : InfHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : α → β<VAR>hf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b<GOAL>⇑{ toFun := f, map_inf' := hf } = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f g : InfHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : InfHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : InfHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_3<VAR>Inf α<GOAL>⇑(InfHom.id α) = id
<VAR>α : Type u_3<VAR>Inf α<VAR>a : α<GOAL>(InfHom.id α) a = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>f : InfHom β γ<VAR>g : InfHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>f : InfHom β γ<VAR>g : InfHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>Inf δ<VAR>f : InfHom γ δ<VAR>g : InfHom β γ<VAR>h : InfHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : InfHom α β<GOAL>f.comp (InfHom.id α) = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : InfHom α β<GOAL>(InfHom.id β).comp f = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>g₁ g₂ : InfHom β γ<VAR>f : InfHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>g : InfHom β γ<VAR>f₁ f₂ : InfHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>b : β<GOAL>⇑(InfHom.const α b) = Function.const α b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>b : β<VAR>a : α<GOAL>(InfHom.const α b) a = b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>f g : InfHom α β<GOAL>⇑(f ⊓ g) = ⇑(f ⊓ g)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>Bot β<GOAL>⇑⊥ = ⊥
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>Top β<GOAL>⇑⊤ = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>f g : InfHom α β<VAR>a : α<GOAL>(f ⊓ g) a = f a ⊓ g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>Bot β<VAR>a : α<GOAL>⊥ a = ⊥
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>SemilatticeInf β<VAR>Top β<VAR>a : α<GOAL>⊤ a = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<GOAL>⇑f.toSupHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<GOAL>⇑f.toBotHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupHom α β<VAR>hf : f.toFun ⊥ = ⊥<GOAL>⇑{ toSupHom := f, map_bot' := hf } = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f g : SupBotHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f