mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_neg : ∀ {x : ℝ*}, (-x).InfiniteNeg ↔ x.InfinitePos
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.prodMkLeft γ κ)
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.instToString : ToString Aesop.ForwardRulePriority
-- Init.Grind.Lemmas
Lean.Grind.Bool.and_eq_of_eq_false_right : ∀ {a b : Bool}, b = false → (a && b) = false
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_inv_comp_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsMonHom f] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Init.Conv
/-- `dsimp` is the definitional simplifier in `conv`-mode. It differs from `simp` in that it only
applies theorems that hold by reflexivity.

Examples:

```lean
example (a : Nat): (0 + 0) = a - a := by
  conv =>
    lhs
    dsimp
    rw [← Nat.sub_self a]
```
 -/
Lean.Parser.Tactic.Conv.dsimp : Lean.ParserDescr
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- An entire function which differs from the Mellin transform of `f - f₀`, where defined, by a
correction term of the form `A / s + B / (k - s)`.  -/
WeakFEPair.Λ₀ : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℂ → E
-- Mathlib.Algebra.Order.Group.Defs
neg_lt_self_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, -a < a ↔ 0 < a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.mk.injEq : ∀ (arg type app arg_1 type_1 app_1 : Lean.Expr),
  ({ arg := arg, type := type, app := app } = { arg := arg_1, type := type_1, app := app_1 }) =
    (arg = arg_1 ∧ type = type_1 ∧ app = app_1)
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.HasColimit.colimitCocone_pt_carrier : ∀ {R : Type w} [inst : Ring R] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [inst_2 : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))],
  ↑(ModuleCat.HasColimit.colimitCocone F).pt = ↑(ModuleCat.mkOfSMul' (ModuleCat.HasColimit.coconePointSMul F))
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_hom_homOfLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U V : X.Opens) (e : U ≤ V)
  {Z : AlgebraicGeometry.Scheme} (h : ↑((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).hom
      (CategoryTheory.CategoryStruct.comp (Y.homOfLE ⋯) h) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE e)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f V).hom h)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.topEquiv.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddSubsemigroup.topEquiv =
    { toFun := fun x => ↑x, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Data.Seq.Computation
Stream'.cons.eq_2 : ∀ {α : Type u} (a : α) (s : Stream' α) (n : ℕ), Stream'.cons a s n.succ = s n
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to1.tr.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1to1.Λ' Γ Λ σ → Sort u_4) (a : Γ)
  (q : Turing.TM1.Stmt Γ Λ σ) (h_1 : (l : Λ) → motive (Turing.TM1to1.Λ'.normal l))
  (h_2 : (a : Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1to1.Λ'.write a q)),
  (match Turing.TM1to1.Λ'.write a q with
    | Turing.TM1to1.Λ'.normal l => h_1 l
    | Turing.TM1to1.Λ'.write a q => h_2 a q) =
    h_2 a q
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- A variant of `eq_whisker` with a more convenient argument order for use in tactics.  -/
Mathlib.Tactic.Reassoc.eq_whisker' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Topology.Separation.Basic
r1_separation : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x y : X},
  ¬Inseparable x y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
-- Init.SizeOf
UInt64.ofBitVec.sizeOf_spec : ∀ (toBitVec : BitVec 64), sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.singleton_add_eq : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
  {r} + spectrum R a = spectrum R ((algebraMap R A) r + a)
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.instIsReflexivePairAlgebraTopMapBottomMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  CategoryTheory.IsReflexivePair (CategoryTheory.Monad.FreeCoequalizer.topMap X)
    (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.IsFiniteRelIndex K], H.relIndex K ≠ 0
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- See `zero_lt_two'` for a version with the type explicit.  -/
zero_lt_two : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 2
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- If `P` holds for `f : X ⟶ Y`, it also holds for `𝒰.f i ≫ f` for any `K`-cover `R` of `X`.  -/
CategoryTheory.MorphismProperty.IsLocalAtSource.comp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X → ∀ {U : C} (g : U ⟶ X), R g → P f → P (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Data.Set.Basic
Set.union_inter_distrib_right : ∀ {α : Type u} (s t u : Set α), (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sInf_apply : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} {m : Set (MeasureTheory.Measure α)},
  MeasurableSet s → (sInf m) s = (sInf (MeasureTheory.Measure.toOuterMeasure '' m)) s
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.IsFilteredOrEmpty.isSiftedOrEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C],
  CategoryTheory.IsSiftedOrEmpty C
-- Lean.Meta.Tactic.Grind.Types
/-- Auxiliary type used to implement `grind.ematch.instance`.
 -/
Lean.Meta.Grind.EMatchDiagSource : Type
-- Mathlib.Topology.Closure
notMem_of_notMem_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {P : X}, P ∉ closure s → P ∉ s
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a monoid homomorphism `f` from `M` to `P`, the kernel of `f` is the unique congruence
relation on `M` whose induced map from the quotient of `M` to `P` is injective.  -/
Con.ker_eq_lift_of_injective : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (c : Con M) (f : M →* P)
  (H : c ≤ Con.ker f), Function.Injective ⇑(c.lift f H) → Con.ker f = c
-- Mathlib.Topology.Order.LeftRightLim
tendsto_atTop_of_mapClusterPt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] [NoTopOrder α] {f g : α → β} {b : β},
  Filter.Tendsto f Filter.atTop (nhds b) →
    (∀ᶠ (x : α) in Filter.atTop, MapClusterPt (g x) (nhds x) f) → Filter.Tendsto g Filter.atTop (nhds b)
-- Mathlib.Topology.Instances.ENat
ENat.nhds_natCast : ∀ (n : ℕ), nhds ↑n = pure ↑n
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pos.find?_string_eq_find?_toSlice : ∀ {pat : String} {s : String.Slice} {p : s.Pos}, p.find? pat = p.find? pat.toSlice
-- Mathlib.Computability.NFA
NFA.Path.brecOn.eq : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {motive : (a a_1 : σ) → (a_2 : List α) → M.Path a a_1 a_2 → Sort u_1}
  {a a_1 : σ} {a_2 : List α} (t : M.Path a a_1 a_2)
  (F_1 : (a a_3 : σ) → (a_4 : List α) → (t : M.Path a a_3 a_4) → NFA.Path.below t → motive a a_3 a_4 t),
  NFA.Path.brecOn t F_1 = F_1 a a_1 a_2 t (NFA.Path.brecOn.go t F_1).2
-- Mathlib.Order.Concept
Concept.intent_copy : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent)
  (hi : i = c.intent), (c.copy e i he hi).intent = i
-- Aesop.Forward.State
/-- Forward state for one rule. Updates are lazy: when adding a hyp or pattern
subst to the rule, it is initially only enqueued in the cluster states. The
`update` method must be called to actually make the corresponding changes,
which result in new complete matches for the rule.  -/
Aesop.RuleState : Type
-- Mathlib.Data.Option.Basic
Option.casesOn'_none : ∀ {α : Type u_1} {β : Type u_2} (x : β) (f : α → β), none.casesOn' x f = x
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.mk.sizeOf_spec : ∀ (toMatcherInfo : Lean.Meta.MatcherInfo) (matcherName : Lean.Name) (matcherLevels : Array Lean.Level)
  (params : Array Lean.Expr) (motive : Lean.Expr) (discrs alts remaining : Array Lean.Expr),
  sizeOf
      { toMatcherInfo := toMatcherInfo, matcherName := matcherName, matcherLevels := matcherLevels, params := params,
        motive := motive, discrs := discrs, alts := alts, remaining := remaining } =
    1 + sizeOf toMatcherInfo + sizeOf matcherName + sizeOf matcherLevels + sizeOf params + sizeOf motive +
          sizeOf discrs +
        sizeOf alts +
      sizeOf remaining
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Ground terms from the `rhs` that have been abstracted so far.  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.rhss : Lean.Meta.Grind.AbstractM.State✝ → Array Lean.Expr
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.preimageIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y),
  (hF.preimageIso e).hom = hF.preimage e.hom
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHom : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} {x' y' : D} (f : x ⟶ y) (g : x' ⟶ y')
  [inst_4 : CategoryTheory.IsIso f] [inst_5 : CategoryTheory.IsIso g],
  CategoryTheory.inv (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g) =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom (CategoryTheory.inv f) (CategoryTheory.inv g)
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [hv : v.IsRankOneDiscrete], StrictMono ⇑(Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_eq_ciSup : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → Norm (β i)] (f : PiLp ⊤ β),
  ‖f‖ = ⨆ i, ‖f.ofLp i‖
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticChar_eq_pow_of_char_ne_two' : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∀ (a : F), ↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map₂_map_left_anticomm`.  -/
Option.map_map₂_antidistrib_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
  {β' : Type u_6} {g : γ → δ} {f' : β' → α → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' b) a) → Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' b) a
-- Std.Do.WP.Sound
/-- Soundness lemma for `StateM.run`: `Id`-specialization of `StateT.of_wp_run`.  -/
Std.Do.StateM.of_wp_run_eq : ∀ {α σ : Type} {x : α × σ} {s : σ} {prog : StateM σ α},
  StateT.run prog s = x →
    ∀ (P : α × σ → Prop), (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.noThrow fun a s' => ⌜P (a, s')⌝) s) → P x
-- Mathlib.Topology.Bases
TopologicalSpace.Subtype.secondCountableTopology : ∀ {α : Type u} [t : TopologicalSpace α] (s : Set α) [SecondCountableTopology α], SecondCountableTopology ↑s
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_unitClosedBall : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (c : 𝕜), c • Metric.closedBall 0 1 = Metric.closedBall 0 ‖c‖
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_tilted_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (fun x => Real.exp (f x)) μ →
      AEMeasurable f ν →
        MeasureTheory.llr (μ.tilted f) ν =ᵐ[μ] fun x =>
          f x - Real.log (∫ (z : α), Real.exp (f z) ∂μ) + MeasureTheory.llr μ ν x
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.mk.inj : ∀ {tempMark doneMark : Lean.FVarIdHashSet} {newDecls : Array Lean.LocalDecl} {newArgs : Array Lean.Expr}
  {tempMark_1 doneMark_1 : Lean.FVarIdHashSet} {newDecls_1 : Array Lean.LocalDecl} {newArgs_1 : Array Lean.Expr},
  { tempMark := tempMark, doneMark := doneMark, newDecls := newDecls, newArgs := newArgs } =
      { tempMark := tempMark_1, doneMark := doneMark_1, newDecls := newDecls_1, newArgs := newArgs_1 } →
    tempMark = tempMark_1 ∧ doneMark = doneMark_1 ∧ newDecls = newDecls_1 ∧ newArgs = newArgs_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct a `Atom₁` term from a lean expression.  -/
Mathlib.Tactic.BicategoryLike.MkAtom₁.ofExpr : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkAtom₁ m] → Lean.Expr → m Mathlib.Tactic.BicategoryLike.Atom₁
-- Mathlib.LinearAlgebra.Prod
/-- Product of modules is associative up to linear isomorphism.  -/
LinearEquiv.prodAssoc : (R : Type u_3) →
  (M₁ : Type u_4) →
    (M₂ : Type u_5) →
      (M₃ : Type u_6) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R M₃] → ((M₁ × M₂) × M₃) ≃ₗ[R] M₁ × M₂ × M₃
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOverHom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : C) [inst_1 : CategoryTheory.OverClass X S],
  CategoryTheory.OverClass.asOverHom S (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.OverClass.asOver X S)
-- Mathlib.RingTheory.Algebraic.Integral
instIsPushoutFractionRingPolynomial_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [inst_3 : IsDomain S] [inst_4 : FaithfulSMul R S],
  Algebra.IsPushout R S (FractionRing (Polynomial R)) (FractionRing (Polynomial S))
-- Lean.Elab.DeclModifiers
/-- Returns whether the given visibility modifier should be interpreted as `public` in the current
environment.

NOTE: `Environment.isExporting` defaults to `false` when command elaborators are invoked for
backward compatibility. It needs to be initialized apropriately first before calling this function
as e.g. done in `elabDeclaration`.
 -/
Lean.Elab.Visibility.isInferredPublic : Lean.Environment → Lean.Elab.Visibility → Bool
-- Mathlib.RingTheory.SimpleModule.Basic
instIsSemisimpleModuleDFinsupp : ∀ {R : Type u_2} [inst : Ring R] {ι : Type u_7} (M : ι → Type u_6) [inst_1 : (i : ι) → AddCommGroup (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), IsSemisimpleModule R (M i)], IsSemisimpleModule R (Π₀ (i : ι), M i)
-- Mathlib.Order.Comparable
CompRel.symm : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, CompRel r a b → CompRel r b a
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instNontrivial : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [Nontrivial M],
  Nontrivial (ArchimedeanClass M)
-- Batteries.Data.List.Basic
List.all₂_eq_true : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Bool} (l₁ : List α) (l₂ : List β),
  List.all₂ r l₁ l₂ = true ↔ List.Forall₂ (fun x1 x2 => r x1 x2 = true) l₁ l₂
-- Init.Data.Vector.OfFn
Vector.back_ofFn : ∀ {α : Type u_1} {n : ℕ} [inst : NeZero n] {f : Fin n → α}, (Vector.ofFn f).back = f ⟨n - 1, ⋯⟩
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
StarAlgebra.elemental.characterSpaceToSpectrum_coe : ∀ {A : Type u_1} [inst : CStarAlgebra A] (x : A) (φ : ↑(WeakDual.characterSpace ℂ ↥(StarAlgebra.elemental ℂ x))),
  ↑(StarAlgebra.elemental.characterSpaceToSpectrum x φ) = φ ⟨x, ⋯⟩
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.Limits.coprod.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X X_1 : C) (e_X : X = X_1) (Y Y_1 : C) (e_Y : Y = Y_1)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y], (X ⨿ Y) = (X_1 ⨿ Y_1)
-- Init.Data.Vector.Lex
Vector.le_empty : ∀ {α : Type u_1} [inst : LT α] {xs : Vector α 0}, xs ≤ #v[] ↔ xs = #v[]
-- Mathlib.RepresentationTheory.Coinvariants
Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal],
  Representation.IsTrivial (MonoidHom.comp (ρ.toCoinvariants S) S.subtype)
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
DivisionCommMonoid.mul_comm : ∀ {G : Type u} [self : DivisionCommMonoid G] (a b : G), a * b = b * a
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_of_isEmpty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_3} [inst_2 : IsEmpty α]
  (s : (a : α) → Finset (γ a)), Fintype.piFinset s = Finset.univ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_eq_get! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)] {h : a ∈ t}, t.get a h = t.get! a
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The action of `Equiv.Perm α` on `Set.powersetCard α n` is preprimitive
provided `1 ≤ n < Nat.card α` and `Nat.card α ≠ 2 * n`.

This is a consequence that the stabilizer of such a combination
is a maximal subgroup.  -/
Set.powersetCard.isPreprimitive_perm : ∀ {α : Type u_2} [inst : DecidableEq α] {n : ℕ},
  1 ≤ n → n < Nat.card α → Nat.card α ≠ 2 * n → MulAction.IsPreprimitive (Equiv.Perm α) ↑(Set.powersetCard α n)
-- Lean.Message
Lean.MessageData.withContext.injEq : ∀ (a : Lean.MessageDataContext) (a_1 : Lean.MessageData) (a_2 : Lean.MessageDataContext) (a_3 : Lean.MessageData),
  (Lean.MessageData.withContext a a_1 = Lean.MessageData.withContext a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The range of a surjective non-unital ring homomorphism is the whole of the codomain.  -/
NonUnitalRingHom.srange_eq_top_of_surjective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
  Function.Surjective ⇑f → NonUnitalRingHom.srange f = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.instDecidableRelAdjFromEdgeSetOfDecidablePredSym2MemSetOfDecidableEq : {V : Type u} →
  (s : Set (Sym2 V)) → [DecidablePred fun x => x ∈ s] → [DecidableEq V] → DecidableRel (SimpleGraph.fromEdgeSet s).Adj
-- Init.Control.Lawful.Instances
StateT.run_seq : ∀ {m : Type u → Type u_1} {α β σ : Type u} [inst : Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α)
  (s : σ),
  (f <*> x).run s = do
    let fs ← f.run s
    (fun p => (fs.1 p.1, p.2)) <$> x.run fs.2
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.eqnInfoExt : Lean.MapDeclarationExtension Lean.Elab.WF.EqnInfo
-- Mathlib.Data.Set.Lattice
Set.sUnion_subset_sUnion : ∀ {α : Type u_1} {S T : Set (Set α)}, S ⊆ T → ⋃₀ S ⊆ ⋃₀ T
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipPrefixWhile_eq_startPos_iff_or : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice},
  s.skipPrefixWhile pat = s.startPos ↔
    ¬String.Slice.Pattern.Model.MatchesAt pat s.startPos ∨ String.Slice.Pattern.Model.IsLongestMatch pat s.startPos
-- Lean.Elab.Declaration
/-- Find the common namespace for the given names.
Example:
```
findCommonPrefix [`Lean.Elab.eval, `Lean.mkConst, `Lean.Elab.Tactic.evalTactic]
-- `Lean
```
 -/
Lean.Elab.Command.findCommonPrefix : List Lean.Name → Lean.Name
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalExprConfig_1.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.Abel.AbelNF.Config
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is a complex, this is the morphism from the cokernel of `S.map' k (k + 1)`
to the kernel of `S.map' (k + 2) (k + 3)`.  -/
CategoryTheory.ComposableArrows.IsComplex.cokerToKer : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S : CategoryTheory.ComposableArrows C (n + 3)} →
          S.IsComplex →
            (k : ℕ) →
              (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.cokerToKer._auto_1) →
                [inst_2 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)] →
                  [inst_3 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)] →
                    CategoryTheory.Limits.cokernel (S.map' k (k + 1) ⋯ ⋯) ⟶
                      CategoryTheory.Limits.kernel (S.map' (k + 2) (k + 3) ⋯ ⋯)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.ext : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {x y : SSet.RelativeMorphism A B φ},
  x.map = y.map → x = y
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
/-- A morphism of schemes `f : X ⟶ Y` is flat if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, the induced map `Γ(Y, U) ⟶ Γ(X, V)` is flat. This is equivalent to
asking that all stalk maps are flat (see `AlgebraicGeometry.Flat.iff_flat_stalkMap`).
 -/
AlgebraicGeometry.Flat : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.isMinor : Lean.Meta.RecursorInfo → ℕ → Bool
-- Mathlib.ModelTheory.Semantics
/-- A model of a theory is a structure in which every sentence is realized as true.  -/
FirstOrder.Language.«term_⊨__1» : Lean.TrailingParserDescr
-- Mathlib.Topology.Category.Locale
/-- Construct a bundled `Locale` from a `Frame`.  -/
Locale.of : (α : Type u_1) → [Order.Frame α] → Locale
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.equiv_iff_toList_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList