mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_inv`. -/
Monovary.inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {f : ι → α} {g : ι → β},
  Monovary f g → Monovary f⁻¹ g⁻¹
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_edist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α], Measurable fun p => edist p.1 p.2
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.cast_rat : ∀ {n : ℤ} {d : ℕ} {R : Type u_2} [inst : DivisionRing R] {a : R},
  Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d + 0
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isAddRightRegular_op`. -/
IsAddRightRegular.op : ∀ {R : Type u_1} [inst : Add R] {a : R}, IsAddLeftRegular a → IsAddRightRegular (AddOpposite.op a)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.const_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a : X} {b : Y}
  (ha : IsOpen {a}) (hb : IsOpen {b}), (OpenPartialHomeomorph.const ha hb).target = {b}
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.tensorProductTo_surjective : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Surjective ⇑(KaehlerDifferential.D R S).tensorProductTo
-- Std.Time.Format.Basic
/-- The format only parses a single timezone.  -/
Std.Time.Awareness.only : Std.Time.TimeZone → Std.Time.Awareness
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- If a functor `F` has a weak limit, so does any naturally isomorphic functor.
 -/
CategoryTheory.Limits.hasWeakLimit_of_iso : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F G : CategoryTheory.Functor J C}
  [CategoryTheory.Limits.HasWeakLimit F] (α : F ≅ G), CategoryTheory.Limits.HasWeakLimit G
-- Init.Data.Option.Lemmas
/-- See `Option.get_map` for a version that can be rewritten in the reverse direction.  -/
Option.apply_get : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {h : o.isSome = true}, f (o.get h) = (Option.map f o).get ⋯
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- **Alias** of `SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne`. -/
SimpleGraph.Walk.setOf_length_eq_zero_of_ne : ∀ {V : Type u} (G : SimpleGraph V) {u v : V}, u ≠ v → {p | p.length = 0} = ∅
-- Mathlib.Algebra.Algebra.Basic
/-- This has high priority because it is almost always the right instance when it applies.  -/
Algebra.to_smulCommClass : ∀ {R : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  SMulCommClass R A A
-- Mathlib.Analysis.Complex.Basic
/-- Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`.

This is an abbreviation for `conjCAE` coerced to a continuous linear map.  -/
Complex.conjCLE : ℂ ≃L[ℝ] ℂ
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.mk.inj : ∀ {α : Type w} {list list_1 : List α}, { list := list } = { list := list_1 } → list = list_1
-- Mathlib.RingTheory.Flat.TorsionFree
/-- If `R` is Bezout then an `R`-module is flat iff it has no torsion.  -/
Module.Flat.flat_iff_torsion_eq_bot_of_isBezout : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsBezout R]
  [IsDomain R], Module.Flat R M ↔ Submodule.torsion R M = ⊥
-- Lean.Parser.Basic
/-- Parse `suffix` after an antiquotation, e.g. `$x,*`, and put both into a new node.  -/
Lean.Parser.withAntiquotSuffixSplice : Lean.SyntaxNodeKind → Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Tactic.TermCongr
/-- `congr(expr)` generates a congruence from an expression containing
congruence holes of the form `$h` or `$(h)`.
In these congruence holes, `h : a = b` indicates that, in the generated congruence,
on the left-hand side `a` is substituted for `$h`
and on the right-hand side `b` is substituted for `$h`.

For example, if `h : a = b` then `congr(1 + $h) : 1 + a = 1 + b`.

This is able to make use of the expected type, for example `(congr(_ + $h) : 1 + _ = _)`
with `h : x = y` gives `1 + x = 1 + y`.
The expected type can be an `Iff`, `Eq`, or `HEq`.
If there is no expected type, then it generates an equality.

Note: the process of generating a congruence lemma involves elaborating the pattern
using terms with attached metadata and a reducible wrapper.
We try to avoid doing so, but these terms can leak into the local context through unification.
This can potentially break tactics that are sensitive to metadata or reducible functions.
Please report anything that goes wrong with `congr(...)` lemmas on Zulip.

For debugging, you can set `set_option trace.Elab.congr true`.
 -/
Mathlib.Tactic.TermCongr.elabTermCongr : Lean.Elab.Term.TermElab
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.casesPatterns : Array Aesop.CasesPattern → Aesop.Frontend.BuilderOption
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.nat_add_continuum : ∀ (n : ℕ), ↑n + Cardinal.continuum = Cardinal.continuum
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsFiltered J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c) {X A : C} (p : X ⟶ A) (s : (CategoryTheory.Functor.const J).obj X ⟶ D)
  [CategoryTheory.IsFinitelyPresentable (CategoryTheory.Under.mk p)] (f : A ⟶ c.pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = CategoryTheory.CategoryStruct.comp p f) →
    ∃ j q, CategoryTheory.CategoryStruct.comp p q = s.app j ∧ CategoryTheory.CategoryStruct.comp q (c.ι.app j) = f
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The stabilizer of an element under an action, i.e. what sends the element to
itself. An additive subgroup.  -/
AddAction.stabilizer : (G : Type u_1) → {α : Type u_2} → [inst : AddGroup G] → [AddAction G α] → α → AddSubgroup G
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.mapAlgHom_id : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁],
  MvPolynomial.mapAlgHom (AlgHom.id R S₁) = AlgHom.id R (MvPolynomial σ S₁)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.isRatStieltjesPoint_unit_prod_iff : ∀ {α : Type u_1} (f : α → ℚ → ℝ) (a : α),
  ProbabilityTheory.IsRatStieltjesPoint (fun p => f p.2) ((), a) ↔ ProbabilityTheory.IsRatStieltjesPoint f a
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Composition of a `SimpleFun` and a measurable function is a `SimpleFunc`.  -/
MeasureTheory.SimpleFunc.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] →
          MeasureTheory.SimpleFunc β γ → (g : α → β) → Measurable g → MeasureTheory.SimpleFunc α γ
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_natCast_le_lift : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.beth ↑n ≤ Cardinal.lift.{v, u} c ↔ Cardinal.beth ↑n ≤ c
-- Mathlib.Data.Countable.Defs
countable_iff_exists_injective : ∀ (α : Sort u), Countable α ↔ ∃ f, Function.Injective f
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.analyticOnNhd_weierstrassP : ∀ (L : PeriodPair), AnalyticOnNhd ℂ L.weierstrassP (↑L.lattice)ᶜ
-- Mathlib.CategoryTheory.Category.Cat.Terminal
/-- A discrete category with a unique object is terminal.  -/
CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    [Unique T] → [CategoryTheory.IsDiscrete T] → CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.sum_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ}
  {u : ℕ → α},
  Monotone u → (∀ (i : ℕ), u i ∈ s) → ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
-- Init.Data.SInt.Lemmas
ISize.toInt64_neg_of_ne : ∀ {x : ISize}, x ≠ ISize.minValue → (-x).toInt64 = -x.toInt64
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.one_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : One γ] (g : C(α, β)), ContinuousMap.comp 1 g = 1
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.unipotentUpper_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₁ ⟶ X₂),
  (CategoryTheory.Biprod.unipotentUpper r).inv =
    CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.id X₁) (-r) 0
      (CategoryTheory.CategoryStruct.id X₂)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Construct a `Mor₂` term from a Lean expression.  -/
Mathlib.Tactic.Monoidal.Mor₂OfExpr : Lean.Expr → Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.BicategoryLike.Mor₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α},
  t.WF →
    (List.find? (fun x => compare x.1 k == Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toList t) = none ↔
      Std.DTreeMap.Internal.Impl.contains k t = false)
-- Mathlib.Order.WithBotTop
WithBotTop.eq_1 : ∀ (ι : Type u_1), WithBotTop ι = WithBot (WithTop ι)
-- Init.Data.Int.DivMod.Lemmas
Int.tmod.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).tmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)
-- Init.Data.Iterators.PostconditionMonad
/-- Lifts an operation from `m` to `PostconditionT m` without asserting any nontrivial postcondition.

Caution: `lift` is not a lawful lift function.
For example, `pure a : PostconditionT m α` is not the same as
`PostconditionT.lift (pure a : m α)`.
 -/
Std.Iterators.PostconditionT.lift : {α : Type w} → {m : Type w → Type w'} → [Functor m] → m α → Std.Iterators.PostconditionT m α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.cosh` is complex analytic.  -/
Complex.analyticAt_cosh : ∀ {x : ℂ}, AnalyticAt ℂ Complex.cosh x
-- Plausible.Functions
/-- Produce a string for a given `TotalFunction`.
The output is of the form `[x₀ => f x₀, .. xₙ => f xₙ, _ => y]`.
 -/
Plausible.TotalFunction.repr : {α : Type u} → {β : Type v} → [Repr α] → [Repr β] → Plausible.TotalFunction α β → String
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.instEpiFunctorTypeToRange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F),
  CategoryTheory.Epi (CategoryTheory.Subfunctor.toRange p)
-- Mathlib.Topology.Compactification.StoneCech
preStoneCechExtend_extends : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β]
  [inst_3 : CompactSpace β] {g : α → β} (hg : Continuous g), preStoneCechExtend hg ∘ preStoneCechUnit = g
-- Mathlib.Topology.Connected.PathConnected
Joined.inv : ∀ {G : Type u_4} [inst : Inv G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {x y : G}, Joined x y → Joined x⁻¹ y⁻¹
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_one_iff_eq : ∀ {α : Type u_2} [inst : One α] {s : Set α}, s ⊆ 1 ↔ s = ∅ ∨ s = 1
-- Mathlib.LinearAlgebra.Pi
Submodule.pi_univ_bot : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)], (Submodule.pi Set.univ fun i => ⊥) = ⊥
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.neg : {R : Type u} → {M : Type v} → [Neg R] → [Neg M] → Neg (TrivSqZeroExt R M)
-- Mathlib.Data.Matrix.Block
/-- We can form a single large matrix by flattening smaller 'block' matrices of compatible
dimensions.  -/
Matrix.fromBlocks : {l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      {o : Type u_4} →
        {α : Type u_12} → Matrix n l α → Matrix n m α → Matrix o l α → Matrix o m α → Matrix (n ⊕ o) (l ⊕ m) α
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
      _auto_146✝)
  (unit :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
          (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
        CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
      _auto_148✝)
  (tensor :
    autoParam
      (∀ (X Y : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
            (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
            (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y))
      _auto_150✝)
  (X : C), (CategoryTheory.LaxBraidedFunctor.isoOfComponents e ⋯ unit tensor).hom.hom.hom.app X = (e X).hom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ofList_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v}, Std.ExtDTreeMap.Const.ofList [] cmp = ∅
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.mkParams : Lean.Grind.Config → Lean.Meta.Grind.ExtensionStateArray → Lean.MetaM Lean.Meta.Grind.Params
-- Init.Data.String.Basic
String.copy_toSlice : ∀ {s : String}, s.toSlice.copy = s
-- Mathlib.MeasureTheory.Function.EssSup
essSup_smul_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {R : Type u_3} [inst_1 : Semiring R] [IsDomain R] [inst_3 : Module R ENNReal]
  [inst_4 : IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] {c : R},
  c ≠ 0 → ∀ (f : α → β), essSup f (c • μ) = essSup f μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.contDiff_arctan : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.arctan
-- Mathlib.Data.ZMod.Basic
ZMod.neg_val' : ∀ {n : ℕ} [NeZero n] (a : ZMod n), (-a).val = (n - a.val) % n
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.prod : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [inst : TopologicalSpace β] {s : Set α} {t_1 : Set β},
  TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable t_1 → TopologicalSpace.IsSeparable (s ×ˢ t_1)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.le_largerSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} (A : CategoryTheory.Subobject X),
  A ≤ CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG A
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.fold.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_1 ()
-- Mathlib.Algebra.Group.Finsupp
Finsupp.apply_single : ∀ {ι : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [ZeroHomClass F M N] (e : F) (i : ι) (m : M) (b : ι), e ((fun₀ | i => m) b) = (fun₀ | i => e m) b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- An affine subspace constructed from a point and a direction contains the result of adding a
vector in that direction to that point.  -/
AffineSubspace.vadd_mem_mk' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {v : V} (p : P) {direction : Submodule k V},
  v ∈ direction → v +ᵥ p ∈ AffineSubspace.mk' p direction
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPProofsWithType : Lean.Options → Bool
-- Std.Http.Data.Method
Std.Http.Method.mkworkspace.sizeOf_spec : sizeOf Std.Http.Method.mkworkspace = 1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.toList_nil : ∀ {α : Type u_1}, Ordnode.nil.toList = []
-- Init.Data.Fin.Lemmas
Fin.mk_val : ∀ {n : ℕ} (i : Fin n), ⟨↑i, ⋯⟩ = i
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.coe_le_coe : ∀ {E : Type u_3} [inst : Group E] {p q : GroupNorm E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Lean.Elab.DefView
/-- Incremental execution of main tactic block, if any.  -/
Lean.Elab.HeaderProcessedSnapshot.tacSnap? : Lean.Elab.HeaderProcessedSnapshot → Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.right_of_add_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.Integrable f (μ + ν) → MeasureTheory.Integrable f ν
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_ext : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l l' : List ((_ : α) × Unit)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys l' →
      (∀ (a : α), Std.Internal.List.getKey? a l = Std.Internal.List.getKey? a l') → l.Perm l'
-- Mathlib.Order.Heyting.Basic
Prod.instHImp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : HImp α] [inst_1 : HImp β],
  Prod.instHImp = { himp := fun a b => (a.1 ⇨ b.1, a.2 ⇨ b.2) }
-- Init.Grind.Tactics
/-- `lia` solves linear integer arithmetic goals.

It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
Please use `grind` instead if you need additional capabilities.
 -/
Lean.Parser.Tactic.lia : Lean.ParserDescr
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isBasis_sigma : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (α i)]
  {B : (i : ι) → Set (TopologicalSpace.Opens (α i))},
  (∀ (i : ι), TopologicalSpace.Opens.IsBasis (B i)) →
    TopologicalSpace.Opens.IsBasis (⋃ i, (fun U => { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i)
-- Init.Data.String.Basic
String.Slice.Pos.ofReplaceEnd : {s : String.Slice} → {p₀ : s.Pos} → (s.sliceTo p₀).Pos → s.Pos
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_hom_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.mop =
    (CategoryTheory.MonoidalCategoryStruct.associator { unmop := Z } { unmop := Y } { unmop := X }).inv
-- Mathlib.Dynamics.Ergodic.Function
/-- Let `f : α → α` be a quasi-ergodic map.
Let `g : α → X` be an a.e. strongly measurable function
from `α` to a nonempty metrizable topological space.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant.  -/
QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : α → α} {g : α → X},
  QuasiErgodic f μ → MeasureTheory.AEStronglyMeasurable g μ → g ∘ f =ᵐ[μ] g → ∃ c, g =ᵐ[μ] Function.const α c
-- Mathlib.Order.Zorn
/-- Local notation for the relation being considered.  -/
_private.Mathlib.Order.Zorn.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.Data.List.Sym
List.map_mk_sublist_sym2 : ∀ {α : Type u_1} (x : α) (xs : List α), x ∈ xs → (List.map (fun y => s(x, y)) xs).Sublist xs.sym2
-- Mathlib.Order.Fin.Tuple
antitone_vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  Antitone (Matrix.vecCons a f) ↔ f 0 ≤ a ∧ Antitone f
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.IterStep.successor.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Std.IterStep α β → Sort u_3) →
      (x : Std.IterStep α β) →
        ((it : α) → (out : β) → motive (Std.IterStep.yield it out)) →
          ((it : α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (t : R),
  Polynomial.derivative p ≠ 0 →
    Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (Polynomial.derivative p)
-- Mathlib.GroupTheory.OrderOfElement
finEquivZPowers.eq_1 : ∀ {G : Type u_1} [inst : Group G] {x : G} (hx : IsOfFinOrder x),
  finEquivZPowers hx = (finEquivPowers hx).trans (Equiv.setCongr ⋯)
-- Lean.Meta.Instances
Lean.Meta.Instances.instanceNames : Lean.Meta.Instances → Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsLocallyPresentable.mk : ∀ {C : Type u} [hC : CategoryTheory.Category.{v, u} C],
  (∃ κ, ∃ (x : Fact κ.IsRegular), CategoryTheory.IsCardinalLocallyPresentable C κ) →
    CategoryTheory.IsLocallyPresentable.{w, v, u} C
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' fallback : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).getKeyD k' fallback =
    if (k == k') = true then if (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then k else fallback
    else m.getKeyD k' fallback
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_le_opow_iff_right : ∀ {a b c : Ordinal.{u_1}}, 1 < a → (a ^ b ≤ a ^ c ↔ b ≤ c)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.botEquiv_symm : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (x : F),
  (IntermediateField.botEquiv F E).symm x = (algebraMap F ↥⊥) x
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_bot : ∀ {α : Type u_1}, ⊥.IsCountablyGenerated
-- Mathlib.Data.Set.Card
Set.encard_le_encard_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Set.InjOn f s → s.encard ≤ t.encard
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {x : M} {f : M → M'} {g : M → M''},
  MDiffAt f x → MDiffAt g x → (mfderiv% fun x => (f x, g x)) x = (mfderiv% f x).prod (mfderiv% g x)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.set : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {σ : Type u} [inst : MonadLift m n] [inst_1 : MonadStateOf σ m] (s : σ),
  set s = monadLift (set s)