Documentation

Mathlib.Order.Filter.Germ

Germ of a function at a filter #

The germ of a function f : α → β at a filter l : Filter α is the equivalence class of f with respect to the equivalence relation EventuallyEq l: f ≈ g means ∀ᶠ x in l, f x = g x.

Main definitions #

We define

We also define map (F : β → γ) : Germ l β → Germ l γ sending each germ f to F ∘ f.

For each of the following structures we prove that if β has this structure, then so does Germ l β:

Tags #

filter, germ

theorem Filter.const_eventuallyEq' {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {a : β} {b : β} :
(∀ᶠ (x : α) in l, a = b) a = b
theorem Filter.const_eventuallyEq {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {a : β} {b : β} :
((fun (x : α) => a) =ᶠ[l] fun (x : α) => b) a = b
def Filter.germSetoid {α : Type u_1} (l : Filter α) (β : Type u_5) :
Setoid (αβ)

Setoid used to define the space of germs.

Equations
Instances For
    def Filter.Germ {α : Type u_1} (l : Filter α) (β : Type u_5) :
    Type (max u_1 u_5)

    The space of germs of functions α → β at a filter l.

    Equations
    Instances For
      def Filter.productSetoid {α : Type u_1} (l : Filter α) (ε : αType u_5) :
      Setoid ((a : α) → ε a)

      Setoid used to define the filter product. This is a dependent version of Filter.germSetoid.

      Equations
      • Filter.productSetoid l ε = { r := fun (f g : (a : α) → ε a) => ∀ᶠ (a : α) in l, f a = g a, iseqv := }
      Instances For
        def Filter.Product {α : Type u_1} (l : Filter α) (ε : αType u_5) :
        Type (max u_1 u_5)

        The filter product (a : α) → ε a at a filter l. This is a dependent version of Filter.Germ.

        Equations
        Instances For
          instance Filter.Product.coeTC {α : Type u_1} {l : Filter α} {ε : αType u_5} :
          CoeTC ((a : α) → ε a) (Filter.Product l ε)
          Equations
          • Filter.Product.coeTC = { coe := Quotient.mk' }
          instance Filter.Product.inhabited {α : Type u_1} {l : Filter α} {ε : αType u_5} [(a : α) → Inhabited (ε a)] :
          Equations
          • Filter.Product.inhabited = { default := Quotient.mk' fun (a : α) => default }
          def Filter.Germ.ofFun {α : Type u_1} {β : Type u_2} {l : Filter α} :
          (αβ)Filter.Germ l β
          Equations
          • Filter.Germ.ofFun = Quotient.mk'
          Instances For
            instance Filter.Germ.instCoeTCForAllGerm {α : Type u_1} {β : Type u_2} {l : Filter α} :
            CoeTC (αβ) (Filter.Germ l β)
            Equations
            • Filter.Germ.instCoeTCForAllGerm = { coe := Filter.Germ.ofFun }
            def Filter.Germ.const {α : Type u_1} {β : Type u_2} {l : Filter α} (b : β) :
            Equations
            • b = fun (x : α) => b
            Instances For
              instance Filter.Germ.coeTC {α : Type u_1} {β : Type u_2} {l : Filter α} :
              CoeTC β (Filter.Germ l β)
              Equations
              • Filter.Germ.coeTC = { coe := Filter.Germ.const }
              def Filter.Germ.IsConstant {α : Type u_1} {β : Type u_2} {l : Filter α} (P : Filter.Germ l β) :

              A germ P of functions α → β is constant w.r.t. l.

              Equations
              Instances For
                theorem Filter.Germ.isConstant_coe {α : Type u_1} {β : Type u_2} {f : αβ} {l : Filter α} {b : β} (h : ∀ (x' : α), f x' = b) :
                @[simp]
                theorem Filter.Germ.isConstant_coe_const {α : Type u_1} {β : Type u_2} {l : Filter α} {b : β} :
                Filter.Germ.IsConstant fun (x : α) => b
                theorem Filter.Germ.isConstant_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : αβ} {g : βγ} (h : Filter.Germ.IsConstant f) :

                If f : α → β is constant w.r.t. l and g : β → γ, then g ∘ f : α → γ also is.

                @[simp]
                theorem Filter.Germ.quot_mk_eq_coe {α : Type u_1} {β : Type u_2} (l : Filter α) (f : αβ) :
                Quot.mk Setoid.r f = f
                @[simp]
                theorem Filter.Germ.mk'_eq_coe {α : Type u_1} {β : Type u_2} (l : Filter α) (f : αβ) :
                theorem Filter.Germ.inductionOn {α : Type u_1} {β : Type u_2} {l : Filter α} (f : Filter.Germ l β) {p : Filter.Germ l βProp} (h : ∀ (f : αβ), p f) :
                p f
                theorem Filter.Germ.inductionOn₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : Filter.Germ l β) (g : Filter.Germ l γ) {p : Filter.Germ l βFilter.Germ l γProp} (h : ∀ (f : αβ) (g : αγ), p f g) :
                p f g
                theorem Filter.Germ.inductionOn₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (f : Filter.Germ l β) (g : Filter.Germ l γ) (h : Filter.Germ l δ) {p : Filter.Germ l βFilter.Germ l γFilter.Germ l δProp} (H : ∀ (f : αβ) (g : αγ) (h : αδ), p f g h) :
                p f g h
                def Filter.Germ.map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {lc : Filter γ} (F : (αβ)γδ) (hF : (Filter.EventuallyEq l Filter.EventuallyEq lc) F F) :
                Filter.Germ l βFilter.Germ lc δ

                Given a map F : (α → β) → (γ → δ) that sends functions eventually equal at l to functions eventually equal at lc, returns a map from Germ l β to Germ lc δ.

                Equations
                Instances For
                  def Filter.Germ.liftOn {α : Type u_1} {β : Type u_2} {l : Filter α} {γ : Sort u_5} (f : Filter.Germ l β) (F : (αβ)γ) (hF : (Filter.EventuallyEq l fun (x x_1 : γ) => x = x_1) F F) :
                  γ

                  Given a germ f : Germ l β and a function F : (α → β) → γ sending eventually equal functions to the same value, returns the value F takes on functions having germ f at l.

                  Equations
                  Instances For
                    @[simp]
                    theorem Filter.Germ.map'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {lc : Filter γ} (F : (αβ)γδ) (hF : (Filter.EventuallyEq l Filter.EventuallyEq lc) F F) (f : αβ) :
                    Filter.Germ.map' F hF f = (F f)
                    @[simp]
                    theorem Filter.Germ.coe_eq {α : Type u_1} {β : Type u_2} {l : Filter α} {f : αβ} {g : αβ} :
                    f = g f =ᶠ[l] g
                    theorem Filter.EventuallyEq.germ_eq {α : Type u_1} {β : Type u_2} {l : Filter α} {f : αβ} {g : αβ} :
                    f =ᶠ[l] gf = g

                    Alias of the reverse direction of Filter.Germ.coe_eq.

                    def Filter.Germ.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (op : βγ) :
                    Filter.Germ l βFilter.Germ l γ

                    Lift a function β → γ to a function Germ l β → Germ l γ.

                    Equations
                    Instances For
                      @[simp]
                      theorem Filter.Germ.map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (op : βγ) (f : αβ) :
                      Filter.Germ.map op f = (op f)
                      @[simp]
                      theorem Filter.Germ.map_id {α : Type u_1} {β : Type u_2} {l : Filter α} :
                      theorem Filter.Germ.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (op₁ : γδ) (op₂ : βγ) (f : Filter.Germ l β) :
                      Filter.Germ.map op₁ (Filter.Germ.map op₂ f) = Filter.Germ.map (op₁ op₂) f
                      def Filter.Germ.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (op : βγδ) :
                      Filter.Germ l βFilter.Germ l γFilter.Germ l δ

                      Lift a binary function β → γ → δ to a function Germ l β → Germ l γ → Germ l δ.

                      Equations
                      Instances For
                        @[simp]
                        theorem Filter.Germ.map₂_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (op : βγδ) (f : αβ) (g : αγ) :
                        Filter.Germ.map₂ op f g = fun (x : α) => op (f x) (g x)
                        def Filter.Germ.Tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} (f : Filter.Germ l β) (lb : Filter β) :

                        A germ at l of maps from α to β tends to lb : Filter β if it is represented by a map which tends to lb along l.

                        Equations
                        Instances For
                          @[simp]
                          theorem Filter.Germ.coe_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : αβ} {lb : Filter β} :
                          theorem Filter.Tendsto.germ_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : αβ} {lb : Filter β} :
                          Filter.Tendsto f l lbFilter.Germ.Tendsto (f) lb

                          Alias of the reverse direction of Filter.Germ.coe_tendsto.

                          def Filter.Germ.compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : Filter.Germ l β) {lc : Filter γ} (g : Filter.Germ lc α) (hg : Filter.Germ.Tendsto g l) :

                          Given two germs f : Germ l β, and g : Germ lc α, where l : Filter α, if g tends to l, then the composition f ∘ g is well-defined as a germ at lc.

                          Equations
                          Instances For
                            @[simp]
                            theorem Filter.Germ.coe_compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : αβ) {lc : Filter γ} {g : Filter.Germ lc α} (hg : Filter.Germ.Tendsto g l) :
                            def Filter.Germ.compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : Filter.Germ l β) {lc : Filter γ} (g : γα) (hg : Filter.Tendsto g lc l) :

                            Given a germ f : Germ l β and a function g : γ → α, where l : Filter α, if g tends to l along lc : Filter γ, then the composition f ∘ g is well-defined as a germ at lc.

                            Equations
                            Instances For
                              @[simp]
                              theorem Filter.Germ.coe_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : αβ) {lc : Filter γ} {g : γα} (hg : Filter.Tendsto g lc l) :
                              Filter.Germ.compTendsto (f) g hg = (f g)
                              @[simp]
                              theorem Filter.Germ.compTendsto'_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : Filter.Germ l β) {lc : Filter γ} {g : γα} (hg : Filter.Tendsto g lc l) :
                              theorem Filter.Germ.Filter.Tendsto.congr_germ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βγ} {g : βγ} {l : Filter α} {l' : Filter β} (h : f =ᶠ[l'] g) {φ : αβ} (hφ : Filter.Tendsto φ l l') :
                              (f φ) = (g φ)
                              theorem Filter.Germ.isConstant_comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : αβ} {lc : Filter γ} {g : γα} (hf : Filter.Germ.IsConstant f) (hg : Filter.Tendsto g lc l) :
                              theorem Filter.Germ.isConstant_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : Filter.Germ l β} {lc : Filter γ} {g : γα} (hf : Filter.Germ.IsConstant f) (hg : Filter.Tendsto g lc l) :

                              If a germ f : Germ l β is constant, where l : Filter α, and a function g : γ → α tends to l along lc : Filter γ, the germ of the composition f ∘ g is also constant.

                              @[simp]
                              theorem Filter.Germ.const_inj {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {a : β} {b : β} :
                              a = b a = b
                              @[simp]
                              theorem Filter.Germ.map_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter α) (a : β) (f : βγ) :
                              Filter.Germ.map f a = (f a)
                              @[simp]
                              theorem Filter.Germ.map₂_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (l : Filter α) (b : β) (c : γ) (f : βγδ) :
                              Filter.Germ.map₂ f b c = (f b c)
                              @[simp]
                              theorem Filter.Germ.const_compTendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (b : β) {lc : Filter γ} {g : γα} (hg : Filter.Tendsto g lc l) :
                              Filter.Germ.compTendsto (b) g hg = b
                              @[simp]
                              theorem Filter.Germ.const_compTendsto' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (b : β) {lc : Filter γ} {g : Filter.Germ lc α} (hg : Filter.Germ.Tendsto g l) :
                              Filter.Germ.compTendsto' (b) g hg = b
                              def Filter.Germ.LiftPred {α : Type u_1} {β : Type u_2} {l : Filter α} (p : βProp) (f : Filter.Germ l β) :

                              Lift a predicate on β to Germ l β.

                              Equations
                              Instances For
                                @[simp]
                                theorem Filter.Germ.liftPred_coe {α : Type u_1} {β : Type u_2} {l : Filter α} {p : βProp} {f : αβ} :
                                Filter.Germ.LiftPred p f ∀ᶠ (x : α) in l, p (f x)
                                theorem Filter.Germ.liftPred_const {α : Type u_1} {β : Type u_2} {l : Filter α} {p : βProp} {x : β} (hx : p x) :
                                @[simp]
                                theorem Filter.Germ.liftPred_const_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [Filter.NeBot l] {p : βProp} {x : β} :
                                def Filter.Germ.LiftRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (r : βγProp) (f : Filter.Germ l β) (g : Filter.Germ l γ) :

                                Lift a relation r : β → γ → Prop to Germ l β → Germ l γ → Prop.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Filter.Germ.liftRel_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {r : βγProp} {f : αβ} {g : αγ} :
                                  Filter.Germ.LiftRel r f g ∀ᶠ (x : α) in l, r (f x) (g x)
                                  theorem Filter.Germ.liftRel_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {r : βγProp} {x : β} {y : γ} (h : r x y) :
                                  @[simp]
                                  theorem Filter.Germ.liftRel_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} [Filter.NeBot l] {r : βγProp} {x : β} {y : γ} :
                                  Filter.Germ.LiftRel r x y r x y
                                  instance Filter.Germ.inhabited {α : Type u_1} {β : Type u_2} {l : Filter α} [Inhabited β] :
                                  Equations
                                  • Filter.Germ.inhabited = { default := default }
                                  instance Filter.Germ.add {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] :
                                  Equations
                                  instance Filter.Germ.mul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] :
                                  Equations
                                  @[simp]
                                  theorem Filter.Germ.coe_add {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] (f : αM) (g : αM) :
                                  (f + g) = f + g
                                  @[simp]
                                  theorem Filter.Germ.coe_mul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] (f : αM) (g : αM) :
                                  (f * g) = f * g
                                  instance Filter.Germ.zero {α : Type u_1} {l : Filter α} {M : Type u_5} [Zero M] :
                                  Equations
                                  • Filter.Germ.zero = { zero := 0 }
                                  instance Filter.Germ.one {α : Type u_1} {l : Filter α} {M : Type u_5} [One M] :
                                  Equations
                                  • Filter.Germ.one = { one := 1 }
                                  @[simp]
                                  theorem Filter.Germ.coe_zero {α : Type u_1} {l : Filter α} {M : Type u_5} [Zero M] :
                                  0 = 0
                                  @[simp]
                                  theorem Filter.Germ.coe_one {α : Type u_1} {l : Filter α} {M : Type u_5} [One M] :
                                  1 = 1
                                  theorem Filter.Germ.addSemigroup.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddSemigroup M] (a : Filter.Germ l M) (b : Filter.Germ l M) (c : Filter.Germ l M) :
                                  a + b + c = a + (b + c)
                                  instance Filter.Germ.addSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [AddSemigroup M] :
                                  Equations
                                  instance Filter.Germ.semigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [Semigroup M] :
                                  Equations
                                  theorem Filter.Germ.addCommSemigroup.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddCommSemigroup M] (q₁ : Quotient (Filter.germSetoid l M)) (q₂ : Quotient (Filter.germSetoid l M)) :
                                  q₁ + q₂ = q₂ + q₁
                                  Equations
                                  instance Filter.Germ.commSemigroup {α : Type u_1} {l : Filter α} {M : Type u_5} [CommSemigroup M] :
                                  Equations
                                  instance Filter.Germ.instIsAddLeftCancel {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] [IsLeftCancelAdd M] :
                                  Equations
                                  • =
                                  instance Filter.Germ.instIsLeftCancelMul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] [IsLeftCancelMul M] :
                                  Equations
                                  • =
                                  Equations
                                  • =
                                  Equations
                                  • =
                                  instance Filter.Germ.instIsAddCancel {α : Type u_1} {l : Filter α} {M : Type u_5} [Add M] [IsCancelAdd M] :
                                  Equations
                                  • =
                                  instance Filter.Germ.instIsCancelMul {α : Type u_1} {l : Filter α} {M : Type u_5} [Mul M] [IsCancelMul M] :
                                  Equations
                                  • =
                                  Equations
                                  theorem Filter.Germ.addLeftCancelSemigroup.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddLeftCancelSemigroup M] :
                                  ∀ (x x_1 x_2 : Filter.Germ l M), x + x_1 = x + x_2x_1 = x_2
                                  Equations
                                  theorem Filter.Germ.addRightCancelSemigroup.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddRightCancelSemigroup M] :
                                  ∀ (x x_1 x_2 : Filter.Germ l M), x + x_1 = x_2 + x_1x = x_2
                                  Equations
                                  Equations
                                  theorem Filter.Germ.addZeroClass.proof_2 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddZeroClass M] (q : Quotient (Filter.germSetoid l M)) :
                                  q + 0 = q
                                  theorem Filter.Germ.addZeroClass.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddZeroClass M] (q : Quotient (Filter.germSetoid l M)) :
                                  0 + q = q
                                  instance Filter.Germ.addZeroClass {α : Type u_1} {l : Filter α} {M : Type u_5} [AddZeroClass M] :
                                  Equations
                                  instance Filter.Germ.mulOneClass {α : Type u_1} {l : Filter α} {M : Type u_5} [MulOneClass M] :
                                  Equations
                                  instance Filter.Germ.vadd {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [VAdd M G] :
                                  Equations
                                  instance Filter.Germ.smul {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [SMul M G] :
                                  Equations
                                  instance Filter.Germ.pow {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [Pow G M] :
                                  Equations
                                  @[simp]
                                  theorem Filter.Germ.coe_vadd {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [VAdd M G] (n : M) (f : αG) :
                                  (n +ᵥ f) = n +ᵥ f
                                  @[simp]
                                  theorem Filter.Germ.coe_smul {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [SMul M G] (n : M) (f : αG) :
                                  (n f) = n f
                                  @[simp]
                                  theorem Filter.Germ.const_vadd {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [VAdd M G] (n : M) (a : G) :
                                  (n +ᵥ a) = n +ᵥ a
                                  @[simp]
                                  theorem Filter.Germ.const_smul {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [SMul M G] (n : M) (a : G) :
                                  (n a) = n a
                                  @[simp]
                                  theorem Filter.Germ.coe_nsmul {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [SMul M G] (f : αG) (n : M) :
                                  (n f) = n f
                                  @[simp]
                                  theorem Filter.Germ.coe_pow {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [Pow G M] (f : αG) (n : M) :
                                  (f ^ n) = f ^ n
                                  @[simp]
                                  theorem Filter.Germ.const_nsmul {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [SMul M G] (a : G) (n : M) :
                                  (n a) = n a
                                  @[simp]
                                  theorem Filter.Germ.const_pow {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [Pow G M] (a : G) (n : M) :
                                  (a ^ n) = a ^ n
                                  theorem Filter.Germ.addMonoid.proof_2 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] :
                                  0 = 0
                                  theorem Filter.Germ.addMonoid.proof_7 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] (x : Filter.Germ l M) :
                                  theorem Filter.Germ.addMonoid.proof_4 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] :
                                  ∀ (x : αM) (x_1 : ), (x_1 x) = (x_1 x)
                                  theorem Filter.Germ.addMonoid.proof_3 {α : Type u_1} {l : Filter α} {M : Type u_2} [AddMonoid M] :
                                  ∀ (x x_1 : αM), (x + x_1) = (x + x_1)
                                  theorem Filter.Germ.addMonoid.proof_1 {α : Type u_1} {l : Filter α} {M : Type u_2} :
                                  theorem Filter.Germ.addMonoid.proof_8 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] (n : ) (x : Filter.Germ l M) :
                                  theorem Filter.Germ.addMonoid.proof_5 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] (a : Filter.Germ l M) :
                                  0 + a = a
                                  theorem Filter.Germ.addMonoid.proof_6 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddMonoid M] (a : Filter.Germ l M) :
                                  a + 0 = a
                                  instance Filter.Germ.addMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [AddMonoid M] :
                                  Equations
                                  instance Filter.Germ.monoid {α : Type u_1} {l : Filter α} {M : Type u_5} [Monoid M] :
                                  Equations
                                  theorem Filter.Germ.coeAddHom.proof_2 {α : Type u_1} {M : Type u_2} [AddMonoid M] (l : Filter α) :
                                  ∀ (x x_1 : αM), { toFun := Filter.Germ.ofFun, map_zero' := }.toFun (x + x_1) = { toFun := Filter.Germ.ofFun, map_zero' := }.toFun (x + x_1)
                                  def Filter.Germ.coeAddHom {α : Type u_1} {M : Type u_5} [AddMonoid M] (l : Filter α) :
                                  (αM) →+ Filter.Germ l M

                                  Coercion from functions to germs as an additive monoid homomorphism.

                                  Equations
                                  Instances For
                                    theorem Filter.Germ.coeAddHom.proof_1 {α : Type u_1} {M : Type u_2} [AddMonoid M] (l : Filter α) :
                                    0 = 0
                                    def Filter.Germ.coeMulHom {α : Type u_1} {M : Type u_5} [Monoid M] (l : Filter α) :
                                    (αM) →* Filter.Germ l M

                                    Coercion from functions to germs as a monoid homomorphism.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Filter.Germ.coe_coeAddHom {α : Type u_1} {l : Filter α} {M : Type u_5} [AddMonoid M] :
                                      (Filter.Germ.coeAddHom l) = Filter.Germ.ofFun
                                      @[simp]
                                      theorem Filter.Germ.coe_coeMulHom {α : Type u_1} {l : Filter α} {M : Type u_5} [Monoid M] :
                                      (Filter.Germ.coeMulHom l) = Filter.Germ.ofFun
                                      instance Filter.Germ.addCommMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [AddCommMonoid M] :
                                      Equations
                                      theorem Filter.Germ.addCommMonoid.proof_1 {α : Type u_2} {l : Filter α} {M : Type u_1} [AddCommMonoid M] (a : Filter.Germ l M) (b : Filter.Germ l M) :
                                      a + b = b + a
                                      instance Filter.Germ.commMonoid {α : Type u_1} {l : Filter α} {M : Type u_5} [CommMonoid M] :
                                      Equations
                                      instance Filter.Germ.natCast {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] :
                                      Equations
                                      • Filter.Germ.natCast = { natCast := fun (n : ) => n }
                                      @[simp]
                                      theorem Filter.Germ.coe_nat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ) :
                                      (fun (x : α) => n) = n
                                      @[simp]
                                      theorem Filter.Germ.const_nat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ) :
                                      n = n
                                      @[simp]
                                      theorem Filter.Germ.coe_ofNat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ) [Nat.AtLeastTwo n] :
                                      @[simp]
                                      theorem Filter.Germ.const_ofNat {α : Type u_1} {l : Filter α} {M : Type u_5} [NatCast M] (n : ) [Nat.AtLeastTwo n] :
                                      instance Filter.Germ.intCast {α : Type u_1} {l : Filter α} {M : Type u_5} [IntCast M] :
                                      Equations
                                      • Filter.Germ.intCast = { intCast := fun (n : ) => n }
                                      @[simp]
                                      theorem Filter.Germ.coe_int {α : Type u_1} {l : Filter α} {M : Type u_5} [IntCast M] (n : ) :
                                      (fun (x : α) => n) = n
                                      Equations
                                      • Filter.Germ.addMonoidWithOne = let __src := Filter.Germ.natCast; let __src_1 := Filter.Germ.addMonoid; let __src_2 := Filter.Germ.one; AddMonoidWithOne.mk
                                      Equations
                                      instance Filter.Germ.neg {α : Type u_1} {l : Filter α} {G : Type u_6} [Neg G] :
                                      Equations
                                      instance Filter.Germ.inv {α : Type u_1} {l : Filter α} {G : Type u_6} [Inv G] :
                                      Equations
                                      @[simp]
                                      theorem Filter.Germ.coe_neg {α : Type u_1} {l : Filter α} {G : Type u_6} [Neg G] (f : αG) :
                                      (-f) = -f
                                      @[simp]
                                      theorem Filter.Germ.coe_inv {α : Type u_1} {l : Filter α} {G : Type u_6} [Inv G] (f : αG) :
                                      f⁻¹ = (f)⁻¹
                                      @[simp]
                                      theorem Filter.Germ.const_neg {α : Type u_1} {l : Filter α} {G : Type u_6} [Neg G] (a : G) :
                                      (-a) = -a
                                      @[simp]
                                      theorem Filter.Germ.const_inv {α : Type u_1} {l : Filter α} {G : Type u_6} [Inv G] (a : G) :
                                      a⁻¹ = (a)⁻¹
                                      instance Filter.Germ.sub {α : Type u_1} {l : Filter α} {M : Type u_5} [Sub M] :
                                      Equations
                                      instance Filter.Germ.div {α : Type u_1} {l : Filter α} {M : Type u_5} [Div M] :
                                      Equations
                                      @[simp]
                                      theorem Filter.Germ.coe_sub {α : Type u_1} {l : Filter α} {M : Type u_5} [Sub M] (f : αM) (g : αM) :
                                      (f - g) = f - g
                                      @[simp]
                                      theorem Filter.Germ.coe_div {α : Type u_1} {l : Filter α} {M : Type u_5} [Div M] (f : αM) (g : αM) :
                                      (f / g) = f / g
                                      @[simp]
                                      theorem Filter.Germ.const_sub {α : Type u_1} {l : Filter α} {M : Type u_5} [Sub M] (a : M) (b : M) :
                                      (a - b) = a - b
                                      @[simp]
                                      theorem Filter.Germ.const_div {α : Type u_1} {l : Filter α} {M : Type u_5} [Div M] (a : M) (b : M) :
                                      (a / b) = a / b
                                      theorem Filter.Germ.involutiveNeg.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [InvolutiveNeg G] (q : Quotient (Filter.germSetoid l G)) :
                                      - -q = q
                                      instance Filter.Germ.involutiveNeg {α : Type u_1} {l : Filter α} {G : Type u_6} [InvolutiveNeg G] :
                                      Equations
                                      instance Filter.Germ.involutiveInv {α : Type u_1} {l : Filter α} {G : Type u_6} [InvolutiveInv G] :
                                      Equations
                                      instance Filter.Germ.hasDistribNeg {α : Type u_1} {l : Filter α} {G : Type u_6} [Mul G] [HasDistribNeg G] :
                                      Equations
                                      instance Filter.Germ.negZeroClass {α : Type u_1} {l : Filter α} {G : Type u_6} [NegZeroClass G] :
                                      Equations
                                      theorem Filter.Germ.negZeroClass.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [NegZeroClass G] :
                                      ((fun (x : αG) => Neg.neg x) fun (x : α) => 0) = fun (x : α) => 0
                                      instance Filter.Germ.invOneClass {α : Type u_1} {l : Filter α} {G : Type u_6} [InvOneClass G] :
                                      Equations
                                      theorem Filter.Germ.subNegMonoid.proof_2 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] (q : Quotient (Filter.germSetoid l G)) :
                                      (fun (z : ) (f : Filter.Germ l G) => z f) 0 q = 0
                                      instance Filter.Germ.subNegMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [SubNegMonoid G] :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      theorem Filter.Germ.subNegMonoid.proof_3 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] :
                                      ∀ (x : ) (q : Quotient (Filter.germSetoid l G)), (fun (z : ) (f : Filter.Germ l G) => z f) (Int.ofNat (Nat.succ x)) q = (fun (z : ) (f : Filter.Germ l G) => z f) (Int.ofNat x) q + q
                                      theorem Filter.Germ.subNegMonoid.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] (q₁ : Quotient (Filter.germSetoid l G)) (q₂ : Quotient (Filter.germSetoid l G)) :
                                      q₁ - q₂ = q₁ + -q₂
                                      theorem Filter.Germ.subNegMonoid.proof_4 {α : Type u_1} {l : Filter α} {G : Type u_2} [SubNegMonoid G] :
                                      ∀ (x : ) (q : Quotient (Filter.germSetoid l G)), (fun (z : ) (f : Filter.Germ l G) => z f) (Int.negSucc x) q = -(fun (z : ) (f : Filter.Germ l G) => z f) ((Nat.succ x)) q
                                      instance Filter.Germ.divInvMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [DivInvMonoid G] :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      theorem Filter.Germ.divisionAddMonoid.proof_2 {α : Type u_2} {l : Filter α} {G : Type u_1} [SubtractionMonoid G] (x : Filter.Germ l G) (y : Filter.Germ l G) :
                                      -(x + y) = -y + -x
                                      theorem Filter.Germ.divisionAddMonoid.proof_1 {α : Type u_2} {l : Filter α} {G : Type u_1} [SubtractionMonoid G] (a : Filter.Germ l G) :
                                      - -a = a
                                      Equations
                                      theorem Filter.Germ.divisionAddMonoid.proof_3 {α : Type u_2} {l : Filter α} {G : Type u_1} [SubtractionMonoid G] (x : Filter.Germ l G) (y : Filter.Germ l G) :
                                      x + y = 0-x = y
                                      instance Filter.Germ.divisionMonoid {α : Type u_1} {l : Filter α} {G : Type u_6} [DivisionMonoid G] :
                                      Equations
                                      theorem Filter.Germ.addGroup.proof_1 {α : Type u_1} {l : Filter α} {G : Type u_2} [AddGroup G] (q : Quotient (Filter.germSetoid l G)) :
                                      -q + q = 0
                                      instance Filter.Germ.addGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [AddGroup G] :
                                      Equations
                                      instance Filter.Germ.group {α : Type u_1} {l : Filter α} {G : Type u_6} [Group G] :
                                      Equations
                                      theorem Filter.Germ.addCommGroup.proof_1 {α : Type u_2} {l : Filter α} {G : Type u_1} [AddCommGroup G] (a : Filter.Germ l G) (b : Filter.Germ l G) :
                                      a + b = b + a
                                      instance Filter.Germ.addCommGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [AddCommGroup G] :
                                      Equations
                                      instance Filter.Germ.commGroup {α : Type u_1} {l : Filter α} {G : Type u_6} [CommGroup G] :
                                      Equations
                                      instance Filter.Germ.addGroupWithOne {α : Type u_1} {l : Filter α} {G : Type u_6} [AddGroupWithOne G] :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      instance Filter.Germ.nontrivial {α : Type u_1} {l : Filter α} {R : Type u_5} [Nontrivial R] [Filter.NeBot l] :
                                      Equations
                                      • =
                                      instance Filter.Germ.mulZeroClass {α : Type u_1} {l : Filter α} {R : Type u_5} [MulZeroClass R] :
                                      Equations
                                      instance Filter.Germ.mulZeroOneClass {α : Type u_1} {l : Filter α} {R : Type u_5} [MulZeroOneClass R] :
                                      Equations
                                      • Filter.Germ.mulZeroOneClass = let __src := Filter.Germ.mulZeroClass; let __src_1 := Filter.Germ.mulOneClass; MulZeroOneClass.mk
                                      instance Filter.Germ.monoidWithZero {α : Type u_1} {l : Filter α} {R : Type u_5} [MonoidWithZero R] :
                                      Equations
                                      • Filter.Germ.monoidWithZero = let __src := Filter.Germ.monoid; let __src_1 := Filter.Germ.mulZeroClass; MonoidWithZero.mk
                                      instance Filter.Germ.distrib {α : Type u_1} {l : Filter α} {R : Type u_5} [Distrib R] :
                                      Equations
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Equations
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Equations
                                      • Filter.Germ.nonUnitalNonAssocRing = let __src := Filter.Germ.addCommGroup; let __src_1 := Filter.Germ.nonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk
                                      instance Filter.Germ.nonUnitalRing {α : Type u_1} {l : Filter α} {R : Type u_5} [NonUnitalRing R] :
                                      Equations
                                      instance Filter.Germ.nonAssocRing {α : Type u_1} {l : Filter α} {R : Type u_5} [NonAssocRing R] :
                                      Equations
                                      • Filter.Germ.nonAssocRing = let __src := Filter.Germ.nonUnitalNonAssocRing; let __src_1 := Filter.Germ.nonAssocSemiring; let __src_2 := Filter.Germ.addGroupWithOne; NonAssocRing.mk
                                      instance Filter.Germ.semiring {α : Type u_1} {l : Filter α} {R : Type u_5} [Semiring R] :
                                      Equations
                                      • Filter.Germ.semiring = let __src := Filter.Germ.nonUnitalSemiring; let __src_1 := Filter.Germ.nonAssocSemiring; let __src_2 := Filter.Germ.monoidWithZero; Semiring.mk Monoid.npow
                                      instance Filter.Germ.ring {α : Type u_1} {l : Filter α} {R : Type u_5} [Ring R] :
                                      Equations
                                      • Filter.Germ.ring = let __src := Filter.Germ.semiring; let __src_1 := Filter.Germ.addCommGroup; let __src_2 := Filter.Germ.nonAssocRing; Ring.mk SubNegMonoid.zsmul
                                      Equations
                                      instance Filter.Germ.commSemiring {α : Type u_1} {l : Filter α} {R : Type u_5} [CommSemiring R] :
                                      Equations
                                      Equations
                                      • Filter.Germ.nonUnitalCommRing = let __src := Filter.Germ.nonUnitalRing; let __src_1 := Filter.Germ.commSemigroup; NonUnitalCommRing.mk
                                      instance Filter.Germ.commRing {α : Type u_1} {l : Filter α} {R : Type u_5} [CommRing R] :
                                      Equations
                                      def Filter.Germ.coeRingHom {α : Type u_1} {R : Type u_5} [Semiring R] (l : Filter α) :
                                      (αR) →+* Filter.Germ l R

                                      Coercion (α → R) → Germ l R as a RingHom.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem Filter.Germ.coe_coeRingHom {α : Type u_1} {l : Filter α} {R : Type u_5} [Semiring R] :
                                        (Filter.Germ.coeRingHom l) = Filter.Germ.ofFun
                                        instance Filter.Germ.instVAdd' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [VAdd M β] :
                                        Equations
                                        instance Filter.Germ.instSMul' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [SMul M β] :
                                        Equations
                                        @[simp]
                                        theorem Filter.Germ.coe_vadd' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [VAdd M β] (c : αM) (f : αβ) :
                                        (c +ᵥ f) = c +ᵥ f
                                        @[simp]
                                        theorem Filter.Germ.coe_smul' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [SMul M β] (c : αM) (f : αβ) :
                                        (c f) = c f
                                        theorem Filter.Germ.addAction.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (f : Filter.Germ l β) :
                                        0 +ᵥ f = f
                                        instance Filter.Germ.addAction {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [AddMonoid M] [AddAction M β] :
                                        Equations
                                        theorem Filter.Germ.addAction.proof_2 {α : Type u_2} {β : Type u_1} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (c₁ : M) (c₂ : M) (f : Filter.Germ l β) :
                                        c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)
                                        instance Filter.Germ.mulAction {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [Monoid M] [MulAction M β] :
                                        Equations
                                        instance Filter.Germ.addAction' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [AddMonoid M] [AddAction M β] :
                                        Equations
                                        theorem Filter.Germ.addAction'.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} {M : Type u_3} [AddMonoid M] [AddAction M β] (f : Filter.Germ l β) :
                                        0 +ᵥ f = f
                                        theorem Filter.Germ.addAction'.proof_2 {α : Type u_2} {β : Type u_3} {l : Filter α} {M : Type u_1} [AddMonoid M] [AddAction M β] (c₁ : Filter.Germ l M) (c₂ : Filter.Germ l M) (f : Filter.Germ l β) :
                                        c₁ + c₂ +ᵥ f = c₁ +ᵥ (c₂ +ᵥ f)
                                        instance Filter.Germ.mulAction' {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [Monoid M] [MulAction M β] :
                                        Equations
                                        instance Filter.Germ.distribMulAction {α : Type u_1} {l : Filter α} {M : Type u_5} {N : Type u_6} [Monoid M] [AddMonoid N] [DistribMulAction M N] :
                                        Equations
                                        instance Filter.Germ.distribMulAction' {α : Type u_1} {l : Filter α} {M : Type u_5} {N : Type u_6} [Monoid M] [AddMonoid N] [DistribMulAction M N] :
                                        Equations
                                        instance Filter.Germ.module {α : Type u_1} {l : Filter α} {M : Type u_5} {R : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] :
                                        Equations
                                        instance Filter.Germ.module' {α : Type u_1} {l : Filter α} {M : Type u_5} {R : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] :
                                        Equations
                                        instance Filter.Germ.le {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] :
                                        Equations
                                        theorem Filter.Germ.le_def {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] :
                                        (fun (x x_1 : Filter.Germ l β) => x x_1) = Filter.Germ.LiftRel fun (x x_1 : β) => x x_1
                                        @[simp]
                                        theorem Filter.Germ.coe_le {α : Type u_1} {β : Type u_2} {l : Filter α} {f : αβ} {g : αβ} [LE β] :
                                        f g f ≤ᶠ[l] g
                                        theorem Filter.Germ.coe_nonneg {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [Zero β] {f : αβ} :
                                        0 f ∀ᶠ (x : α) in l, 0 f x
                                        theorem Filter.Germ.const_le {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] {x : β} {y : β} :
                                        x yx y
                                        @[simp]
                                        theorem Filter.Germ.const_le_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [Filter.NeBot l] {x : β} {y : β} :
                                        x y x y
                                        instance Filter.Germ.preorder {α : Type u_1} {β : Type u_2} {l : Filter α} [Preorder β] :
                                        Equations
                                        instance Filter.Germ.partialOrder {α : Type u_1} {β : Type u_2} {l : Filter α} [PartialOrder β] :
                                        Equations
                                        • Filter.Germ.partialOrder = let __src := Filter.Germ.preorder; PartialOrder.mk
                                        instance Filter.Germ.bot {α : Type u_1} {β : Type u_2} {l : Filter α} [Bot β] :
                                        Equations
                                        • Filter.Germ.bot = { bot := }
                                        instance Filter.Germ.top {α : Type u_1} {β : Type u_2} {l : Filter α} [Top β] :
                                        Equations
                                        • Filter.Germ.top = { top := }
                                        @[simp]
                                        theorem Filter.Germ.const_bot {α : Type u_1} {β : Type u_2} {l : Filter α} [Bot β] :
                                        =
                                        @[simp]
                                        theorem Filter.Germ.const_top {α : Type u_1} {β : Type u_2} {l : Filter α} [Top β] :
                                        =
                                        instance Filter.Germ.orderBot {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [OrderBot β] :
                                        Equations
                                        instance Filter.Germ.orderTop {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [OrderTop β] :
                                        Equations
                                        instance Filter.Germ.instBoundedOrderGermLe {α : Type u_1} {β : Type u_2} {l : Filter α} [LE β] [BoundedOrder β] :
                                        Equations
                                        • Filter.Germ.instBoundedOrderGermLe = let __src := Filter.Germ.orderBot; let __src_1 := Filter.Germ.orderTop; BoundedOrder.mk
                                        instance Filter.Germ.sup {α : Type u_1} {β : Type u_2} {l : Filter α} [Sup β] :
                                        Equations
                                        instance Filter.Germ.inf {α : Type u_1} {β : Type u_2} {l : Filter α} [Inf β] :
                                        Equations
                                        @[simp]
                                        theorem Filter.Germ.const_sup {α : Type u_1} {β : Type u_2} {l : Filter α} [Sup β] (a : β) (b : β) :
                                        (a b) = a b
                                        @[simp]
                                        theorem Filter.Germ.const_inf {α : Type u_1} {β : Type u_2} {l : Filter α} [Inf β] (a : β) (b : β) :
                                        (a b) = a b
                                        instance Filter.Germ.semilatticeSup {α : Type u_1} {β : Type u_2} {l : Filter α} [SemilatticeSup β] :
                                        Equations
                                        • Filter.Germ.semilatticeSup = let __src := Filter.Germ.partialOrder; SemilatticeSup.mk
                                        instance Filter.Germ.semilatticeInf {α : Type u_1} {β : Type u_2} {l : Filter α} [SemilatticeInf β] :
                                        Equations
                                        • Filter.Germ.semilatticeInf = let __src := Filter.Germ.partialOrder; SemilatticeInf.mk
                                        instance Filter.Germ.lattice {α : Type u_1} {β : Type u_2} {l : Filter α} [Lattice β] :
                                        Equations
                                        • Filter.Germ.lattice = let __src := Filter.Germ.semilatticeSup; let __src_1 := Filter.Germ.semilatticeInf; Lattice.mk
                                        instance Filter.Germ.distribLattice {α : Type u_1} {β : Type u_2} {l : Filter α} [DistribLattice β] :
                                        Equations
                                        • Filter.Germ.distribLattice = let __src := Filter.Germ.semilatticeSup; let __src_1 := Filter.Germ.semilatticeInf; DistribLattice.mk
                                        theorem Filter.Germ.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommMonoid β] (f : Filter.Germ l β) (g : Filter.Germ l β) :
                                        f g∀ (c : Filter.Germ l β), c + f c + g
                                        Equations
                                        • Filter.Germ.orderedAddCommMonoid = let __src := Filter.Germ.partialOrder; let __src_1 := Filter.Germ.addCommMonoid; OrderedAddCommMonoid.mk
                                        instance Filter.Germ.orderedCommMonoid {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommMonoid β] :
                                        Equations
                                        • Filter.Germ.orderedCommMonoid = let __src := Filter.Germ.partialOrder; let __src_1 := Filter.Germ.commMonoid; OrderedCommMonoid.mk
                                        theorem Filter.Germ.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedCancelAddCommMonoid β] (f : Filter.Germ l β) (g : Filter.Germ l β) (h : Filter.Germ l β) :
                                        f + g f + hg h
                                        Equations
                                        Equations
                                        theorem Filter.Germ.orderedAddCommGroup.proof_6 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) (b : Filter.Germ l β) :
                                        a + b = b + a
                                        theorem Filter.Germ.orderedAddCommGroup.proof_7 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) (b : Filter.Germ l β) :
                                        a b∀ (c : Filter.Germ l β), c + a c + b
                                        theorem Filter.Germ.orderedAddCommGroup.proof_1 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) (b : Filter.Germ l β) :
                                        a - b = a + -b
                                        theorem Filter.Germ.orderedAddCommGroup.proof_5 {α : Type u_2} {β : Type u_1} {l : Filter α} [OrderedAddCommGroup β] (a : Filter.Germ l β) :
                                        -a + a = 0
                                        Equations
                                        • Filter.Germ.orderedAddCommGroup = let __src := Filter.Germ.orderedAddCancelCommMonoid; let __src_1 := Filter.Germ.addCommGroup; OrderedAddCommGroup.mk
                                        instance Filter.Germ.orderedCommGroup {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommGroup β] :
                                        Equations
                                        • Filter.Germ.orderedCommGroup = let __src := Filter.Germ.orderedCancelCommMonoid; let __src_1 := Filter.Germ.commGroup; OrderedCommGroup.mk
                                        instance Filter.Germ.existsAddOfLE {α : Type u_1} {β : Type u_2} {l : Filter α} [Add β] [LE β] [ExistsAddOfLE β] :
                                        Equations
                                        • =
                                        instance Filter.Germ.existsMulOfLE {α : Type u_1} {β : Type u_2} {l : Filter α} [Mul β] [LE β] [ExistsMulOfLE β] :
                                        Equations
                                        • =
                                        Equations
                                        • Filter.Germ.CanonicallyOrderedAddCommMonoid = let __src := Filter.Germ.orderedAddCommMonoid; let __src_1 := Filter.Germ.orderBot; let __src_2 := ; CanonicallyOrderedAddCommMonoid.mk
                                        theorem Filter.Germ.CanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} {l : Filter α} [CanonicallyOrderedAddCommMonoid β] :
                                        ∀ {a b : Filter.Germ l β}, a b∃ (c : Filter.Germ l β), b = a + c
                                        Equations
                                        • Filter.Germ.CanonicallyOrderedCommMonoid = let __src := Filter.Germ.orderedCommMonoid; let __src_1 := Filter.Germ.orderBot; let __src_2 := ; CanonicallyOrderedCommMonoid.mk
                                        instance Filter.Germ.orderedSemiring {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedSemiring β] :
                                        Equations
                                        • Filter.Germ.orderedSemiring = let __src := Filter.Germ.semiring; let __src_1 := Filter.Germ.orderedAddCommMonoid; OrderedSemiring.mk
                                        Equations
                                        • Filter.Germ.orderedCommSemiring = let __src := Filter.Germ.orderedSemiring; let __src_1 := Filter.Germ.commSemiring; OrderedCommSemiring.mk
                                        instance Filter.Germ.orderedRing {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedRing β] :
                                        Equations
                                        • Filter.Germ.orderedRing = let __src := Filter.Germ.ring; let __src_1 := Filter.Germ.orderedAddCommGroup; OrderedRing.mk
                                        instance Filter.Germ.orderedCommRing {α : Type u_1} {β : Type u_2} {l : Filter α} [OrderedCommRing β] :
                                        Equations
                                        • Filter.Germ.orderedCommRing = let __src := Filter.Germ.orderedRing; let __src_1 := Filter.Germ.orderedCommSemiring; OrderedCommRing.mk