mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.any_eq_false_iff_forall_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a (Std.DHashMap.Const.get m a h) = false
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.replay? : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → Option (Lean.ReplayFn σ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_hom_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp h.isoPullback.hom (CategoryTheory.Limits.pullback.snd f g) = snd
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two additive monoid morphisms `f`, `g` to an additive commutative monoid,
`f + g` is the additive monoid morphism sending `x` to `f x + g x`.  -/
AddMonoidHom.add : {M : Type u_2} → {N : Type u_3} → [inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → Add (M →+ N)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.associated_map_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {f : Associates M →* M},
  Function.RightInverse (⇑f) Associates.mk → ∀ (a : M), Associated a (f (Associates.mk a))
-- Init.Data.SInt.Bitwise
instCommutativeInt8HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- The theory of algebraically closed fields of characteristic `p` as a theory over
the language of rings  -/
FirstOrder.Language.Theory.ACF : ℕ → FirstOrder.Language.ring.Theory
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.braiding_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (β_ M₁ M₂).inv.app X = (β_ (M₁.obj X) (M₂.obj X)).inv
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.formulaEntails_def : ∀ {n : ℕ} (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool)
  (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f =
    ((f.toList.all fun c => decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)) = true)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getMulThms : Lean.Meta.Grind.Arith.Cutsat.ToIntM Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_linear_lt_degree_C_mul_X_sq : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  a ≠ 0 → (Polynomial.C b * Polynomial.X + Polynomial.C c).degree < (Polynomial.C a * Polynomial.X ^ 2).degree
-- Mathlib.Algebra.Notation.Prod
Prod.instOne : {M : Type u_3} → {N : Type u_4} → [One M] → [One N] → One (M × N)
-- Mathlib.Data.Finset.Insert
Finset.insert_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α) (s : Finset α), insert a (insert b s) = insert b (insert a s)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Product of two continuous homomorphisms on the same space.  -/
ContinuousAddMonoidHom.prod : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      [inst : AddMonoid A] →
        [inst_1 : AddMonoid B] →
          [inst_2 : AddMonoid C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] → [inst_5 : TopologicalSpace C] → (A →ₜ+ B) → (A →ₜ+ C) → A →ₜ+ B × C
-- Init.Data.UInt.Lemmas
UInt8.le_antisymm : ∀ {a b : UInt8}, a ≤ b → b ≤ a → a = b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mulPow_nc.fun_cases_unfolding : ∀ (pw : Lean.Grind.CommRing.Power) (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Prop),
  motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit) →
    (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
        (pw.x == p.x) = true →
          motive (Lean.Grind.CommRing.Mon.mult p m) (Lean.Grind.CommRing.Mon.mult { x := pw.x, k := pw.k + p.k } m)) →
      (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
          (pw.x == p.x) = false →
            motive (Lean.Grind.CommRing.Mon.mult p m)
              (Lean.Grind.CommRing.Mon.mult pw (Lean.Grind.CommRing.Mon.mult p m))) →
        ∀ (m : Lean.Grind.CommRing.Mon), motive m (Lean.Grind.CommRing.Mon.mulPow_nc pw m)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.instInhabited : {S : Type u_6} → [inst : Ring S] → [inst_1 : LinearOrder S] → [IsStrictOrderedRing S] → Inhabited (AbsoluteValue S S)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toList_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {f : α → β → Bool},
  Std.DTreeMap.Const.toList (Std.DTreeMap.filter f t) = List.filter (fun p => f p.1 p.2) (Std.DTreeMap.Const.toList t)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_top : nhds ⊤ = ⨅ a, ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)
-- Init.Core
instNonemptyMProd : ∀ {α β : Type u_1} [h1 : Nonempty α] [h2 : Nonempty β], Nonempty (MProd α β)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K),
  (NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace K) x = (x.1, fun w => Complex.equivRealProd (x.2 w))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : Cᵒᵖ}
  (h : Opposite.op (CategoryTheory.Limits.pullback f.unop g.unop) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoOpPullback f g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f.unop g.unop).op h
-- Init.Data.UInt.Lemmas
UInt32.zero_lt_one : 0 < 1
-- Mathlib.Tactic.FunProp.Core
/-- Try to prove `e` using the *apply lambda theorem*.

For example, `e = q(Continuous fun f ↦ f x)` and `funPropDecl` is `FunPropDecl` for `Continuous`.
 -/
Mathlib.Meta.FunProp.applyApplyRule : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
      Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.calleeMeasures : Lean.Elab.WF.GuessLex.RecCallCache → Array Lean.Elab.WF.GuessLex.BasicMeasure
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div_iff_of_pos_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c : G₀}, 0 < a → 0 < b → 0 < c → (a / b < a / c ↔ c < b)
-- Mathlib.CategoryTheory.Types.Basic
Equiv.toIso_hom_hom_apply : ∀ {X Y : Type u} (e : X ≃ Y) (x : X), (CategoryTheory.ConcreteCategory.hom e.toIso.hom) x = e x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.erase_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {c : ℕ},
  (Std.DHashMap.Raw.emptyWithCapacity c).erase k = Std.DHashMap.Raw.emptyWithCapacity c
-- Init.Data.List.Find
List.getLast?_filter : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).getLast? = List.find? p l.reverse
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousOn_iInf_dom : ∀ {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_6} [uα : UniformSpace α] {t : κ → TopologicalSpace X'}
  {F : ι → X' → α} {S : Set X'} {k : κ}, EquicontinuousOn F S → EquicontinuousOn F S
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_diffs_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α},
  (s.diffs t).Nonempty → s.Nonempty
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₈_nat_eq_if_mod_eight : ∀ (n : ℕ), ZMod.χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
-- Mathlib.Order.Ideal
Order.Ideal.toLowerSet : {P : Type u_2} → [inst : LE P] → Order.Ideal P → LowerSet P
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- A variant of `colimitIsoFlipCompColim` where the arguments of `F` are flipped.  -/
CategoryTheory.Limits.colimitFlipIsoCompColim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) →
                CategoryTheory.Limits.colimit F.flip ≅ F.comp CategoryTheory.Limits.colim
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.Scheme.Hom.isSpectralMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f], IsSpectralMap ⇑f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.getProofFor : Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.Linarith.Datatypes
/-- A `Preprocessor` lifts to a `GlobalPreprocessor` by folding it over the input list.
 -/
Mathlib.Tactic.Linarith.Preprocessor.globalize : Mathlib.Tactic.Linarith.Preprocessor → Mathlib.Tactic.Linarith.GlobalPreprocessor
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.star_mul_self : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] (x : R), IsSelfAdjoint (star x * x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_false_iff_exists_contains_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool},
  m.WF →
    (m.all p = false ↔ ∃ a, ∃ (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = false)
-- Mathlib.Topology.Path
Path.coe_toContinuousMap : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), ⇑γ.toContinuousMap = ⇑γ
-- Init.Data.UInt.Bitwise
UInt64.not_neg_one : ~~~(-1) = 0
-- Init.Data.SInt.Lemmas
ISize.toInt32_toInt64 : ∀ (n : ISize), n.toInt64.toInt32 = n.toInt32
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.continuous_extend_zero : ∀ {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α'] [inst_1 : Zero β] [T2Space α']
  [inst_3 : TopologicalSpace β] {U : Set α'},
  IsOpen U → ∀ {f : ↑U → β}, Continuous f → HasCompactSupport f → Continuous (Function.extend Subtype.val f 0)
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautologicalSolution_var : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M] (a : M),
  (Module.Presentation.tautologicalSolution A M).var a = a
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q], P = AlgebraicGeometry.targetAffineLocally Q
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.coe_add : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x y : K),
  { toCompletion := ↑(WithAbs.toAbs (↑v) (x + y)) } =
    { toCompletion := ↑(WithAbs.toAbs (↑v) x) } + { toCompletion := ↑(WithAbs.toAbs (↑v) y) }
-- Mathlib.Logic.IsEmpty.Defs
/-- subtypes of an empty type are empty  -/
instIsEmptySubtype : ∀ {α : Sort u} [IsEmpty α] (p : α → Prop), IsEmpty (Subtype p)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.partialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (Multiplicative α)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.glueData.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J],
  AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F =
    { J := Shrink.{u, w} J, U := fun j => F.obj ((equivShrink J).symm j),
      V := fun ij =>
        ↑(AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm ij.1) ((equivShrink J).symm ij.2)),
      f := fun i j =>
        (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, j).1)
            ((equivShrink J).symm (i, j).2)).ι,
      f_mono := ⋯, f_hasPullback := ⋯, f_id := ⋯,
      t := fun i j => AlgebraicGeometry.Scheme.IsLocallyDirected.t F ((equivShrink J).symm i) ((equivShrink J).symm j),
      t_id := ⋯,
      t' := fun i j k =>
        CategoryTheory.Limits.pullback.lift
          (AlgebraicGeometry.IsOpenImmersion.lift
            (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm j) ((equivShrink J).symm k)).ι
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst
                (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, j).1)
                    ((equivShrink J).symm (i, j).2)).ι
                (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, k).1)
                    ((equivShrink J).symm (i, k).2)).ι)
              (AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F ((equivShrink J).symm i) ((equivShrink J).symm j)))
            ⋯)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst
              (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, j).1)
                  ((equivShrink J).symm (i, j).2)).ι
              (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm (i, k).1)
                  ((equivShrink J).symm (i, k).2)).ι)
            (AlgebraicGeometry.Scheme.IsLocallyDirected.t F ((equivShrink J).symm (i, j).1)
              ((equivShrink J).symm (i, j).2)))
          ⋯,
      t_fac := ⋯, cocycle := ⋯, f_open := ⋯ }
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set (as `ℝ≥0`) is continuous in point  -/
Metric.continuous_infNndist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), Continuous fun x => Metric.infNndist x s
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `absorbs_neg_neg`. -/
Absorbs.neg_neg : ∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
  [inst_3 : Bornology M] {s t : Set E}, Absorbs M s t → Absorbs M (-s) (-t)
-- Lean.Data.KVMap
Lean.KVMap.get : {α : Type} → [Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → α → α
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj W
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          Z)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
              Z).hom
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
        h)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instUnionOfBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Union (Std.HashMap.Raw α β)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.len : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {outWidth : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth → ℕ
-- Mathlib.CategoryTheory.Yoneda
/-- `coyoneda.obj X` is represented by `X`.  -/
CategoryTheory.Functor.CorepresentableBy.coyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : Cᵒᵖ) → (CategoryTheory.coyoneda.obj X).CorepresentableBy (Opposite.unop X)
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ici_disjoint_Iio : ∀ {α : Type v} [inst : Preorder α] {a b : α}, b ≤ a → Disjoint (Set.Ici a) (Set.Iio b)
-- Mathlib.Computability.Encoding
Computability.Γ'.blank.sizeOf_spec : sizeOf Computability.Γ'.blank = 1
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.convs'Aux.match_1.splitter : {K : Type u_1} →
  (motive : Stream'.Seq (GenContFract.Pair K) → ℕ → Sort u_2) →
    (x : Stream'.Seq (GenContFract.Pair K)) →
      (x_1 : ℕ) →
        ((x : Stream'.Seq (GenContFract.Pair K)) → motive x 0) →
          ((s : Stream'.Seq (GenContFract.Pair K)) → (n : ℕ) → motive s n.succ) → motive x x_1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toList_roo_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...n).toList[i]?.isNone = true) = ((n - (m + 1)).toNat ≤ i)
-- Lean.Elab.Tactic.ElabTerm
/-- Runs a term elaborator inside a tactic, finalizing elaboration with `Term.synthesizeSyntheticMVars`.
- `mayPostpone` controls the postponement behavior of `Term.synthesizeSyntheticMVars`.

This function ensures that term elaboration fails when backtracking,
i.e., in `first| tac term | other`.
 -/
Lean.Elab.Tactic.runTermElab : {α : Type} → Lean.Elab.TermElabM α → optParam Bool false → Lean.Elab.Tactic.TacticM α
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listDecode.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (a : α) (l : List (α ⊕ (i : ℕ) × L.Functions i)),
  FirstOrder.Language.Term.listDecode (Sum.inl a :: l) =
    FirstOrder.Language.var a :: FirstOrder.Language.Term.listDecode l
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).getKey? k = t₂.getKey? k
-- Mathlib.Logic.Encodable.Basic
Directed.sequence.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] {r : β → β → Prop} (f : α → β)
  (hf : Directed r f), Directed.sequence f hf 0 = default
-- Mathlib.Order.Cover
covBy_iff_le_iff_lt_left : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.unicode.fun : Lean.Option Bool
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive groups to additive monoids preserves all limits.

This means the underlying additive monoid of a limit can be computed as a limit in the category of
additive monoids.  -/
AddGrpCat.forget₂AddMonPreservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddGrpCat AddMonCat)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_copy : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →⋆ₙ+* B) (f' : A → B) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- When each `C i` is a braided monoidal category,
the natural pointwise monoidal structure on `∀ i, C i`
is also braided.
 -/
CategoryTheory.Pi.braidedCategory : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [(i : I) → CategoryTheory.BraidedCategory (C i)] → CategoryTheory.BraidedCategory ((i : I) → C i)
-- Init.Data.Option.List
Option.length_toList_eq_one_iff : ∀ {α : Type u_1} {o : Option α}, o.toList.length = 1 ↔ o.isSome = true
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.neg_right_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
not_isStationary_of_isEmpty : ∀ {α : Type v} {s : Set α} [inst : LinearOrder α] [IsEmpty α], ¬IsStationary s
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.G₂_det : CartanMatrix.G₂.det = 1
-- Mathlib.Algebra.Group.Pi.Basic
Pi.cancelMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → CancelMonoid (f i)],
  Pi.cancelMonoid = { toLeftCancelMonoid := Pi.leftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.Prestructure.rel_equiv : ∀ {L : FirstOrder.Language} {M : Type u_1} {s : Setoid M} [self : L.Prestructure s] {n : ℕ} {r : L.Relations n}
  (x y : Fin n → M), x ≈ y → FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r y
-- Mathlib.Geometry.Diffeology.Basic
/-- Constructs a diffeology from plots defined on open subsets or ℝⁿ rather than ℝⁿ itself,
organised in the form of the auxiliary `CorePlotsOn` structure.
This is more involved in most regards, but also often makes it quite a lot easier to prove
the locality condition.  -/
DiffeologicalSpace.ofCorePlotsOn : {X : Type u_1} → DiffeologicalSpace.CorePlotsOn X → DiffeologicalSpace X
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_le_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (n : ℕ) (x : X),
  Urysohns.CU.approx n c x ≤ 1
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- A good cylinder object `P` is very good if `P.π` is a (trivial) fibration.  -/
HomotopicalAlgebra.Cylinder.IsVeryGood : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.Cylinder A →
          [CategoryTheory.Limits.HasBinaryCoproduct A A] →
            [HomotopicalAlgebra.CategoryWithCofibrations C] → [HomotopicalAlgebra.CategoryWithFibrations C] → Prop
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_derivative : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R),
  Polynomial.sumIDeriv (Polynomial.derivative p) = Polynomial.derivative (Polynomial.sumIDeriv p)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Closed balls defined using the distance or the edistance coincide  -/
Metric.closedEBall_ofReal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ},
  0 ≤ ε → Metric.closedEBall x (ENNReal.ofReal ε) = Metric.closedBall x ε
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr.eq_1 : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N),
  AddMonoidAlgebra.domCongr R A e =
    { toEquiv := (AddMonoidAlgebra.mapDomainRingEquiv A e).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Data.Nat.Bits
Nat.bodd_zero : Nat.bodd 0 = false
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.getVert_injOn : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.ConnectedComponent.maximal_subgraph_connected_iff : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), Maximal SimpleGraph.Subgraph.Connected G' ↔ ∃ C, C.toSubgraph = G'