mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Lean.AttributeExtra
/-- The environment extension for the attribute.  -/
Lean.TagAttributeExtra.ext : Lean.TagAttributeExtra → Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairing_short_long : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  P.pairing (RootPairing.EmbeddedG2.short P) (RootPairing.EmbeddedG2.long P) = -1
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.gammaPDF_of_nonneg : ∀ {a r x : ℝ},
  0 ≤ x → ProbabilityTheory.gammaPDF a r x = ENNReal.ofReal (r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x)))
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkHom_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor) {Z : C ≌ D} (h : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom β) h)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c), (HomologicalComplex.homologyFunctor C c i).obj K = K.homology i
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.mono : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s t : Set X}, HolderOnWith C r f s → t ⊆ s → HolderOnWith C r f t
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Coframe.MinimalAxioms.sup_iInf₂_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α],
  Order.Coframe.MinimalAxioms α → ∀ {f : (i : ι) → κ i → α} (a : α), a ⊔ ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a ⊔ f i j
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy_set : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 : Std.Sat.CNF ℕ} (cache1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf1)
  (cache2 : Std.Sat.AIG.toCNF.Cache✝ aig cnf2) (idx : ℕ) (hbound : idx < (Std.Sat.AIG.toCNF.Cache.marks✝ cache1).size),
  Std.Sat.AIG.toCNF.Cache.marks✝ cache2 = (Std.Sat.AIG.toCNF.Cache.marks✝ cache1).set idx true hbound →
    Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache2 idx ⋯
-- Mathlib.Order.Lattice
le_inf_sup : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.iInf_adj_of_nonempty : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a b : V} [Nonempty ι] {f : ι → G.Subgraph},
  (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
-- Mathlib.Analysis.InnerProductSpace.PiL2
_private.Mathlib.Analysis.InnerProductSpace.PiL2.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_5.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1}
  (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)))
  (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_5 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_6 t (Lean.Doc.Block.brecOn_5.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toContinuousAddEquiv_coe : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {M : Type u_8} [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] [inst_6 : Module R₁ M]
  (e : M₁ ≃L[R₁] M), ⇑e.toContinuousAddEquiv = ⇑e
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (x : (a : α) × β a)
  (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : (a : α) × β a) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_2 size k v r x
-- Mathlib.Data.Set.Image
Set.preimage_singleton_true : ∀ {α : Type u_1} (p : α → Prop), p ⁻¹' {True} = {a | p a}
-- Lean.Meta.Tactic.Cases
/-- The constructor of this subgoal. Is `none` in the catch-all of a sparse case match  -/
Lean.Meta.CasesSubgoal.ctorName : Lean.Meta.CasesSubgoal → Option Lean.Name
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.continuous_coe : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), Continuous fun x => { toCompletion := ↑x }
-- Mathlib.Logic.Equiv.PartialEquiv
/-- See Note [custom simps projection]  -/
PartialEquiv.Simps.symm_apply : {α : Type u_1} → {β : Type u_2} → PartialEquiv α β → β → α
-- Mathlib.RingTheory.Ideal.Height
/-- The height of an ideal is defined as the infimum of the heights of its minimal prime ideals.  -/
Ideal.height : {R : Type u_1} → [inst : CommRing R] → Ideal R → ℕ∞
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf), (hS.cokerIsoKer' k hk cc kf hcc hkf).hom = hS.cokerToKer' k hk cc kf hcc hkf
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The preimage of the normalizer is contained in the normalizer of the preimage.  -/
AddSubgroup.le_normalizer_comap : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {N : Type u_5} [inst_1 : AddGroup N] (f : N →+ G),
  AddSubgroup.comap f (AddSubgroup.normalizer ↑H) ≤ AddSubgroup.normalizer ↑(AddSubgroup.comap f H)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β k}, ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.whisker_exchange : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {E : Type u₂} [inst_4 : CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D}
  {H I : CategoryTheory.EnrichedFunctor V D E} (α : F ⟶ G) (β : H ⟶ I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerLeft F β)
      (CategoryTheory.EnrichedCat.whiskerRight α I) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α H)
      (CategoryTheory.EnrichedCat.whiskerLeft G β)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax right unity.  -/
CategoryTheory.LaxFunctor.map₂_rightUnitor_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X))
      ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X)
-- Mathlib.Algebra.Homology.Additive
/-- A natural transformation between functors induces a natural transformation
between those functors applied to homological complexes.
 -/
CategoryTheory.NatTrans.mapHomologicalComplex : {ι : Type u_1} →
  {W₁ : Type u_3} →
    {W₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_3} W₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] →
              {F G : CategoryTheory.Functor W₁ W₂} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] →
                    (F ⟶ G) → (c : ComplexShape ι) → F.mapHomologicalComplex c ⟶ G.mapHomologicalComplex c
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_fst_prod : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {Y : α → Ω} {mβ : MeasurableSpace β} {γ : Type u_5}
  {mγ : MeasurableSpace γ} (X : α → β),
  AEMeasurable Y μ →
    ∀ (ν : MeasureTheory.Measure γ) [inst_4 : MeasureTheory.IsProbabilityMeasure ν],
      ⇑(ProbabilityTheory.condDistrib (fun ω => Y ω.1) (fun ω => X ω.1) (μ.prod ν)) =ᵐ[MeasureTheory.Measure.map X μ]
        ⇑(ProbabilityTheory.condDistrib Y X μ)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.noncommProd_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M)
  (comm : (↑t).Pairwise (Function.onFun Commute f)), (∀ c ∈ t, f c ∈ S) → t.noncommProd f comm ∈ S
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (List.filter (fun p => f p.fst p.snd) l) fallback =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValueCast x l ⋯)).getD fallback
-- Init.Data.SInt.Lemmas
Int32.ofInt_eq_ofNat : ∀ {n : ℕ}, Int32.ofInt ↑n = Int32.ofNat n
-- Mathlib.Data.Sum.Basic
Function.Bijective.sumMap : ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'},
  Function.Bijective f → Function.Bijective g → Function.Bijective (Sum.map f g)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashMap.unitOfList l).getKeyD k' fallback = k
-- Mathlib.Data.Finset.Sum
Finset.toRight_insert_inr : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (insert (Sum.inr b) u).toRight = insert b u.toRight
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of a natural `m` is one iff `p` doesn't divide `m`.  -/
padicNorm.nat_eq_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ), padicNorm p ↑m = 1 ↔ ¬p ∣ m
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_functorPullback_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Presieve (F.obj X)),
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.functorPullback F R) ≤
    CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.generate R)
-- Init.Data.List.Basic
List.elem_nil : ∀ {α : Type u} {a : α} [inst : BEq α], List.elem a [] = false
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.symm_mapAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (e : G ≃+ H),
  e.mapAddSubgroup.symm = e.symm.mapAddSubgroup
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length_Ioc : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) (a b : R),
  f.length (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)
-- Mathlib.Data.Sum.Order
OrderIso.sumAssoc_apply_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (c : γ),
  (OrderIso.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
-- Mathlib.Data.Set.Image
Set.image_univ_of_surjective : ∀ {β : Type u_2} {ι : Type u_5} {f : ι → β}, Function.Surjective f → f '' Set.univ = Set.univ
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.neg_v_mul_e0 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  -((CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q) =
    CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPullback_arrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Sieve (F.obj X)),
  CategoryTheory.Presieve.functorPullback F S.arrows = (CategoryTheory.Sieve.functorPullback F S).arrows
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_nil : ∀ {m n : ℕ}, n ≤ m + 1 → (m<...n).toArray = #[]
-- Mathlib.Data.Prod.Basic
Prod.instReflLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Refl r], Std.Refl (Prod.Lex r s)
-- Std.Data.HashSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.get? : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Option α
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measure_preimage_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → ∀ (s : Set β), μa (f ⁻¹' s) ≤ μb s
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
/-- A self-map preserving a finite measure is conservative: if `μ s ≠ 0`, then at least one point
`x ∈ s` comes back to `s` under iterations of `f`. Actually, a.e. point of `s` comes back to `s`
infinitely many times, see `MeasureTheory.MeasurePreserving.conservative` and theorems about
`MeasureTheory.Conservative`.  -/
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → α} {s : Set α}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MeasurePreserving f μ μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_eq_zero_iff_isRoot_eq_bot : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p ≠ 0 → (p.roots = 0 ↔ p.IsRoot = ⊥)
-- Mathlib.Topology.Hom.ContinuousEval
ContinuousEval.mk : ∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} [inst : FunLike F X Y]
  [inst_1 : TopologicalSpace F] [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y],
  (Continuous fun fx => fx.1 fx.2) → ContinuousEval F X Y
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_add_lt_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [AddLeftReflectLT α] {a b c : α}, a + b < a + c → b < c
-- Mathlib.Topology.Order.Compact
IsCompact.sSup_mem : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α]
  {s : Set α}, IsCompact s → s.Nonempty → sSup s ∈ s
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_himp : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Clopens α), ↑(s ⇨ t) = ↑s ⇨ ↑t
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.toLimit_surjective : ∀ (P : ProfiniteGrp.{u}), Function.Surjective ⇑(ProfiniteGrp.Hom.hom P.toLimit)
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- The **fundamental identity** of ramification index `e` and inertia degree `f`:
for `P` ranging over the primes lying over `p`, `∑ P, e P * f P = [Frac(S) : Frac(R)]`;
here `S` is a finite `R`-module (and thus `Frac(S) : Frac(R)` is a finite extension) and `p`
is maximal.  -/
Ideal.sum_ramification_inertia : ∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L] [IsDedekindDomain R]
  [inst_7 : Algebra R K] [IsFractionRing R K] [inst_9 : Algebra S L] [IsFractionRing S L] [inst_11 : Algebra K L]
  [inst_12 : Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal],
  p ≠ ⊥ → ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P = Module.finrank K L
-- Mathlib.Algebra.Category.MonCat.Adjunctions
CommMonCat.instIsRightAdjointForgetMonoidHomCarrier : (CategoryTheory.forget CommMonCat).IsRightAdjoint
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_compl : ∀ {α : Type u_1} (t s s' : Set α), tᶜ.ite s s' = t.ite s' s
-- Batteries.Lean.Position
/-- Return the indentation (number of leading spaces) of the line containing `pos`,
and whether `pos` is the first non-whitespace character in the line.
 -/
Lean.findIndentAndIsStart : String → String.Pos.Raw → ℕ × Bool
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsEpimorphisms : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor D C}
  (adj : F' ⊣ F) {X : C} {Y : D} (f : Y ⟶ F.obj X) [hf : CategoryTheory.Epi f] [F.ReflectsEpimorphisms],
  CategoryTheory.Epi ((adj.homEquiv' X Y) f)
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instTopologicalSpace.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] (N : AddSubgroup G),
  QuotientAddGroup.instTopologicalSpace N = instTopologicalSpaceQuotient
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
min_lt_of_add_lt_two_nsmul : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b c : M},
  a + b < 2 • c → min a b < c
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Order.Hom.Monoid
instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : EquivLike F α β] [inst_5 : OrderIsoClass F α β] [inst_6 : AddEquivClass F α β],
  instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass = { coe := OrderMonoidIsoClass.toOrderAddMonoidIso }
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedPasswdInfo : Inhabited Std.Internal.UV.System.PasswdInfo
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_iff_of_refl : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats : Type
-- Aesop.Rule
Aesop.Safety.instToString : ToString Aesop.Safety
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g g' : b ⟶ c} (η : g ⟶ g'),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.whiskerLeft f η) =
    CategoryTheory.Bicategory.whiskerRight (Bicategory.Opposite.op2 η) f.op
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.add_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommSemigroup α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ (a : α), Function.Antiperiodic (fun x => f (x + a)) c
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBasis_of_maximal_subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.Indep I →
    I ⊆ X →
      (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I) →
        autoParam (X ⊆ M.E) Matroid.Indep.isBasis_of_maximal_subset._auto_1 → M.IsBasis I X
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.bot : ∀ {M : Type u_1} [inst : AddMonoid M], ⊥.FG
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => Real.sinh (f x)) x
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.adjoin_rootSet_eq_range : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Field A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra R B] {f : Polynomial R},
  (Polynomial.map (algebraMap R A) f).Splits →
    ∀ (g : A →ₐ[R] B), Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤