mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.LiesOver.completionMap.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  NumberField.LiesOver.completionMap = NumberField.LiesOver.completionMap
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (range : Std.Legacy.Range) (f : ℕ → m PUnit.{u_1 + 1}) (i : ℕ),
  Std.Legacy.Range.forM.loop✝ range f i =
    if i < range.stop then do
      f i
      have this : 0 < range.step := ⋯
      Std.Legacy.Range.forM.loop✝ range f (i + range.step)
    else pure PUnit.unit
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_mul : ∀ {α : Type u_1} {R : Type u_14} {S : Type u_15} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] (b : S) (s : α →₀ R) {f : α → R → S}, s.sum f * b = s.sum fun a c => f a c * b
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ofCone_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Cone F)
  (j : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.Fork.ofCone t).π.app j =
    CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_right.injEq : ∀ {B : Type u} [inst : Quiver B] {a b c : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (h : b ⟶ c)
  (η η_1 : CategoryTheory.FreeBicategory.Hom₂ f g),
  (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η = CategoryTheory.FreeBicategory.Hom₂.whisker_right h η_1) =
    (η = η_1)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The property of a sheaf of being constant is invariant under equivalence of sheaf
categories.
 -/
CategoryTheory.Sheaf.isConstant_iff_of_equivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {C' : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} C'] (K : CategoryTheory.GrothendieckTopology C')
  [inst_4 : CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C')
  [inst_5 : ∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D]
  [inst_6 : CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) (F : CategoryTheory.Sheaf K D),
  CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).inverse.obj F) ↔
    CategoryTheory.Sheaf.IsConstant K F
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.inclLift_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (x : C),
  (CategoryTheory.WithInitial.inclLift F M hM).inv.app x = CategoryTheory.CategoryStruct.id (F.obj x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.tr_supports : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst_2 : Fintype σ] {S : Finset Λ},
  Turing.TM1.Supports M S → Turing.TM0.Supports (Turing.TM1to0.tr M) ↑(Turing.TM1to0.trStmts M S)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.addEmptyConstants_toLHom : ∀ (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α],
  (FirstOrder.Language.LEquiv.addEmptyConstants L α).toLHom = L.lhomWithConstants α
-- Init.Prelude
/-- Run `x : m α` with a modified value for the `ref`. This is not exactly
the same as `MonadRef.withRef`, because it uses `replaceRef` to avoid putting
syntax with bad spans in the state.
 -/
Lean.withRef : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → {α : Type} → Lean.Syntax → m α → m α
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkIndStx : Lean.Meta.Try.Collector.InductionCandidate → Lean.TSyntax `tactic → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The isomorphism between the Coxeter group associated to the reindexed matrix `M.reindex e` and
the Coxeter group associated to `M`.  -/
CoxeterMatrix.reindexGroupEquiv : {B : Type u_1} → {B' : Type u_2} → (M : CoxeterMatrix B) → (e : B ≃ B') → (CoxeterMatrix.reindex e M).Group ≃* M.Group
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
Algebra.trdeg.eq_1 : ∀ (R : Type u_2) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.trdeg R A = ⨆ ι, Cardinal.mk ↑↑ι
-- Mathlib.RingTheory.Nilpotent.Defs
nilpotencyClass_eq_one : ∀ {R : Type u_1} {x : R} [inst : MonoidWithZero R] [Nontrivial R], nilpotencyClass x = 1 ↔ x = 0
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff : ∀ {ι : 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.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι]
  (N_1 : LieSubmodule R (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → R)),
  RootPairing.GeckConstruction.ωConjLieSubmodule N_1 = ⊤ ↔ N_1 = ⊤
-- Init.Data.Option.List
Option.foldlM_toList : ∀ {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option β) (a : α)
  (f : α → β → m α), List.foldlM f a o.toList = o.elim (pure a) fun b => f a b
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Functor.IsLeftAdjoint.op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.IsLeftAdjoint], F.op.IsRightAdjoint
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.ExprVisited.mk.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf { e := e } = 1 + sizeOf e
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A strong epi-mono factorisation is a decomposition `f = e ≫ m` with `e` a strong epimorphism
and `m` a monomorphism.  -/
CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (self : CategoryTheory.Limits.StrongEpiMonoFactorisation f), CategoryTheory.StrongEpi self.e
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_iff_val_sub_one_lt_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_eq_empty_iff_le_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Set.Ioo a b = ∅ ↔ b ≤ Order.succ a
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- `P` can be checked locally around points of the source.  -/
AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q) →
    (P f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
            Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)))
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.ofMon_μ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  (CategoryTheory.Monad.ofMon M).μ = CategoryTheory.MonObj.mul
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- An affinely independent family is injective, if the underlying
ring is nontrivial.  -/
AffineIndependent.injective : ∀ {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] {ι : Type u_4} [Nontrivial k] {p : ι → P}, AffineIndependent k p → Function.Injective p
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- A type synonym to equip a type with its lexicographic order sorted by degrees.  -/
DegLex : Type u_1 → Type u_1
-- Mathlib.Algebra.Group.Defs
/-- Any `AddRightCancelSemigroup` satisfies `IsRightCancelAdd`.  -/
AddRightCancelSemigroup.toIsRightCancelAdd : ∀ {G : Type u} [self : AddRightCancelSemigroup G], IsRightCancelAdd G
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.WithInitial J → Sort u_2) →
    (x : CategoryTheory.WithInitial J) →
      ((a : J) → motive (CategoryTheory.WithInitial.of a)) → (Unit → motive CategoryTheory.WithInitial.star) → motive x
-- Mathlib.Topology.Order.ScottTopology
IsOpen.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen = TopologicalSpace.IsOpen
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- If `b` semiconjugates `x` to `y` and `a` semiconjugates `y` to `z`, then `a + b`
semiconjugates `x` to `z`.  -/
AddSemiconjBy.add_left : ∀ {S : Type u_1} [inst : AddSemigroup S] {a b x y z : S},
  AddSemiconjBy a y z → AddSemiconjBy b x y → AddSemiconjBy (a + b) x z
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [toIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid R]
  [toZeroLEOneClass : ZeroLEOneClass R] [toNontrivial : Nontrivial R] [toPosMulStrictMono : PosMulStrictMono R]
  [toMulPosStrictMono : MulPosStrictMono R], IsStrictOrderedRing R
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
/-- As submodules, subalgebras are idempotent.  -/
Subalgebra.isIdempotentElem_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), IsIdempotentElem (Subalgebra.toSubmodule S)
-- Init.System.IO
/-- Everything that was written to the process's standard output.  -/
IO.Process.Output.stdout : IO.Process.Output → String
-- Init.Data.Option.Lemmas
Option.pmap_guard : ∀ {α : Type u_1} {β : Type u_2} {q : α → Bool} {p : α → Prop} (f : (x : α) → p x → β) {x : α}
  (h : ∀ (a : α), Option.guard q x = some a → p a),
  Option.pmap f (Option.guard q x) h = if h' : q x = true then some (f x ⋯) else none
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.add_comp' : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B C : TopRep k G)
  (f g : A ⟶ B) (h : B ⟶ C),
  CategoryTheory.CategoryStruct.comp (f + g) h =
    CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h
-- Mathlib.RepresentationTheory.Basic
/-- Given a `k`-linear `G`-representation `(V, ρ)` and a `G`-invariant `k`-submodule `W ≤ V`, this
is the representation induced on `V ⧸ W` by `ρ`.  -/
Representation.quotient : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Ring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (W : Submodule k V) → (∀ (g : G), W ≤ Submodule.comap (ρ g) W) → Representation k G (V ⧸ W)
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.Extension.addEMatchAttr : Lean.Meta.Grind.Extension →
  Lean.Name →
    Lean.AttributeKind →
      Lean.Meta.Grind.EMatchTheoremKind →
        Lean.Meta.Grind.SymbolPriorities → optParam Bool false → optParam Bool false → Lean.MetaM Unit
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.coe_inclusion' : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X}, ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion') = Subtype.val
-- Mathlib.Tactic.Positivity.Core
/-- Extract a proof that `e` is positive, if possible, from `Strictness` information about `e`.  -/
Mathlib.Meta.Positivity.Strictness.toPositive : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      {e : Q(«$α»)} →
        {pα : Q(PartialOrder «$α»)} → Mathlib.Meta.Positivity.Strictness zα e (some pα) → Option Q(0 < «$e»)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instInv : (K : Type u) →
  [inst : Field K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Inv (PerfectClosure K p)
-- Std.Data.HashMap.Lemmas
Std.HashMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {l : List (α × β)}, Std.HashMap.ofList l = ∅.insertMany l
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.abs : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup β] [inst_2 : Lattice β] [AddLeftMono β]
  {f : α → β}, HasCompactSupport f → HasCompactSupport |f|
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefix?_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy), s.skipPrefix? pat = Option.map (fun x => x.cast ⋯) (t.skipPrefix? pat)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.inter_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F : I.Filtration M} (F' : I.Filtration M) [IsNoetherianRing R] [Module.Finite R M], F.Stable → (F ⊓ F').Stable
-- Mathlib.Topology.Separation.Hausdorff
t2Space_iff_disjoint_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ Pairwise fun x y => Disjoint (nhds x) (nhds y)
-- Mathlib.Data.Finset.Range
Finset.strictMono_range : StrictMono Finset.range
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_sub_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν] {i : Set α},
  MeasurableSet i → (μ.toSignedMeasure - ν.toSignedMeasure) i = μ.real i - ν.real i
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles : ∀ (S : CategoryTheory.ShortComplex Ab) (x : ↥(AddCommGrpCat.Hom.hom S.g).ker),
  (CategoryTheory.ConcreteCategory.hom S.iCycles) ((CategoryTheory.ConcreteCategory.hom S.abCyclesIso.inv) x) = ↑x
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorH1CotangentOfFlat.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T],
  P.tensorH1CotangentOfFlat T = P.tensorH1CotangentOfFlat T
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A functor `F` preserves pairwise pullbacks of a presieve `R` if for every pair
of morphisms `f` and `g` in `R`, the pullback of `f` and `g` is preserved by `F`.  -/
CategoryTheory.Functor.PreservesPairwisePullbacks : {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] →
        CategoryTheory.Functor C D → {X : C} → CategoryTheory.Presieve X → Prop
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.deltaDefinition : {α : Type} → Lean.ConstantInfo → List Lean.Level → (Unit → Lean.MetaM α) → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Data.Finset.Union
/-- `Finset.biUnion s t` is the union of `t a` over `a ∈ s`.

(This was formerly `bind` due to the monad structure on types with `DecidableEq`.)  -/
Finset.biUnion : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → Finset α → (α → Finset β) → Finset β
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)) →
            ((x : List α) →
                (x_2 : List β) →
                  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_2 = b :: bs → False) → motive x x_2) →
              motive x x_1
-- Mathlib.FieldTheory.AbelRuffini
gal_mul_isSolvable : ∀ {F : Type u_1} [inst : Field F] {p q : Polynomial F},
  Group.IsSolvable p.Gal → Group.IsSolvable q.Gal → Group.IsSolvable (p * q).Gal
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_symm_apply_map_eq : ∀ {α : Type u_1} {β : Type u_2} {x : FreeMonoid α} (e : α ≃ β), (FreeMonoid.map ⇑e.symm) ((FreeMonoid.map ⇑e) x) = x
-- Batteries.Control.AlternativeMonad
/-- `AlternativeMonad m` means that `m` has both a `Monad` and `Alternative` instance,
which both share the same underlying `Applicative` instance.
The main example is `Option`, but many monad transformers also preserve or add this structure.  -/
AlternativeMonad : (Type u_1 → Type u_2) → Type (max (u_1 + 1) u_2)
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationFstOfIsStableUnderBaseChangeFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [hg : HomotopicalAlgebra.Fibration g],
  HomotopicalAlgebra.Fibration (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Order.WellFounded
Set.range_injOn_strictAnti : ∀ {β : Type u_2} {γ : Type u_3} [inst : LinearOrder β] [inst_1 : Preorder γ] [WellFoundedGT β],
  Set.InjOn Set.range {f | StrictAnti f}
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instSecondCountableTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [SecondCountableTopology α],
  SecondCountableTopology (TopologicalSpace.Compacts α)
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.congr : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
  Asymptotics.SuperpolynomialDecay l k f → (∀ (x : α), f x = g x) → Asymptotics.SuperpolynomialDecay l k g
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.contains : {α : Type u} → {β : α → Type v} → [BEq α] → α → Std.DHashMap.Internal.AssocList α β → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- A pullback cone in `C` is a limit iff it is so after the application
of `coyoneda.obj X` for all `X : Cᵒᵖ`.  -/
CategoryTheory.Limits.PullbackCone.isLimitCoyonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (c : CategoryTheory.Limits.PullbackCone f g) →
            CategoryTheory.Limits.IsLimit c ≃
              ((X_1 : Cᵒᵖ) → CategoryTheory.Limits.IsLimit (c.map (CategoryTheory.coyoneda.obj X_1)))
-- Mathlib.Order.Hom.Basic
OrderEmbedding.toOrderHom_coe : ∀ {X : Type u_6} {Y : Type u_7} [inst : Preorder X] [inst_1 : Preorder Y] (f : X ↪o Y), ⇑f.toOrderHom = ⇑f
-- Mathlib.Algebra.GroupWithZero.Associated
/-- The setoid of the relation `x ~ᵤ y` iff there is a unit `u` such that `x * u = y`  -/
Associated.setoid : (M : Type u_2) → [Monoid M] → Setoid M
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : β k → β k} (h : m.WF) {hc : k' ∈ m.modify k f},
  (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The inclusion `BifibrantObject C ⥤ CofibrantObject C`.  -/
HomotopicalAlgebra.BifibrantObject.ιCofibrantObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C] →
          [inst_4 : CategoryTheory.Limits.HasTerminal C] →
            CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) (HomotopicalAlgebra.CofibrantObject C)
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.commensurator'_mem_iff : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : ConjAct G),
  g ∈ Subgroup.Commensurable.commensurator' H ↔ (g • H).Commensurable H
-- Mathlib.Algebra.Lie.Nilpotent
/-- We say a Lie ring is nilpotent when it is nilpotent as a Lie module over itself via the
adjoint representation.  -/
LieRing.IsNilpotent : (L : Type v) → [LieRing L] → Prop
-- Mathlib.Data.Complex.Basic
Complex.instAdd : Add ℂ
-- Mathlib.Analysis.InnerProductSpace.Basic
re_inner_self_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, 0 < RCLike.re (inner 𝕜 x x) ↔ x ≠ 0
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasFDerivAt.abs_of_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → f x < 0 → HasFDerivAt (fun x => |f x|) (-f') x
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- If the restriction of a global section to each member of an open cover is zero, then it is
globally zero.  -/
AlgebraicGeometry.Scheme.zero_of_zero_cover : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover),
  (∀ (i : 𝒰.I₀), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) s = 0) → s = 0
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.lift_comp_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (g : CliffordAlgebra Q →ₐ[R] A),
  (CliffordAlgebra.lift Q) ⟨g.toLinearMap ∘ₗ CliffordAlgebra.ι Q, ⋯⟩ = g
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceBEq : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Module.ULift
ULift.isScalarTower : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : SMul R M] [inst_1 : SMul M N] [inst_2 : SMul R N]
  [IsScalarTower R M N], IsScalarTower (ULift.{u_1, u} R) M N
-- Mathlib.Data.Num.Lemmas
Num.castNum_testBit : ∀ (m : Num) (n : ℕ), m.testBit n = (↑m).testBit n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_negY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).negY (⇑f ∘ P) = f (W'.negY P)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- For `s` to be a fundamental domain, it's enough to check
`MeasureTheory.AEDisjoint (g +ᵥ s) s` for `g ≠ 0`.  -/
MeasureTheory.IsAddFundamentalDomain.mk'' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) →
      (∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) →
        (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) →
          MeasureTheory.IsAddFundamentalDomain G s μ