mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.instSubsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData},
  Subsingleton (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- A subgraph is connected if it is connected when coerced to be a simple graph.

Note: This is a structure to make it so one can be precise about how dot notation resolves.  -/
SimpleGraph.Subgraph.Connected : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Prop
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IciExtend_self : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β), Set.IciExtend f a = f ⟨a, ⋯⟩
-- Mathlib.NumberTheory.SelbergSieve
/-- The `level` of the sieve controls how many terms we include in the inclusion-exclusion type
sum. A higher level will yield a tighter bound for the main term, but will also increase the
size of the error term.  -/
SelbergSieve.level : SelbergSieve → ℝ
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CasesTypes.mk.sizeOf_spec : ∀ (casesMap : Lean.PHashMap Lean.Name Bool), sizeOf { casesMap := casesMap } = 1 + sizeOf casesMap
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.tendsto_card_div_pow₄ : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Fintype ι],
  Bornology.IsBounded s →
    (∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) →
      ∀ᶠ (x : ℝ) in Filter.atTop,
        ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι ≤
          ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.lipschitzOnWith_of_abs_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ},
  ConcaveOn ℝ (Metric.ball x₀ r) f →
    0 < ε → (∀ (a : E), dist a x₀ < r → |f a| ≤ M) → LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_swap_mul_swap : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {x y z : α},
  [x, y, z].Nodup → (Equiv.swap x y * Equiv.swap y z).support = {x, y, z}
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticWithinAt.im_ofReal : ∀ {f : ℂ → ℂ} {s : Set ℝ} {x : ℝ},
  AnalyticWithinAt ℂ f (Complex.ofReal '' s) ↑x → AnalyticWithinAt ℝ (fun x => (f ↑x).im) s x
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.hasNoLoop_down : ∀ {α : Type u_2} [inst : AddZeroClass α] [inst_1 : IsRightCancelAdd α] [IsLeftCancelAdd α] [inst_3 : One α],
  1 ≠ 0 → (ComplexShape.down α).HasNoLoop
-- Mathlib.Logic.Equiv.Defs
Equiv.equivCongr_refl_right : ∀ {α : Sort u_1} {β : Sort u_2} (ab e : α ≃ β), (ab.equivCongr (Equiv.refl β)) e = ab.symm.trans e
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.connectedComponentEquiv_symm : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G'),
  φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Destruct a multiseries into a triple `(exp, coef, tl)`, where `exp` is the leading exponent,
`coef` is the leading coefficient, and `tl` is the tail.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Option
        (ℝ ×
          Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl ×
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- **Gram-Schmidt Orthonormalization**:
`gramSchmidtNormed` produces an orthonormal system of vectors after removing the vectors which
become zero in the process.  -/
InnerProductSpace.gramSchmidtNormed_orthonormal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E),
  Orthonormal 𝕜 fun i => InnerProductSpace.gramSchmidtNormed 𝕜 f ↑i
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.ext : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  (∀ (J : BoxIntegral.Box ι), J ∈ π₁ ↔ J ∈ π₂) → π₁ = π₂
-- Std.Data.TreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.TreeMap.ofList : {α : Type u} →
  {β : Type v} → List (α × β) → (cmp : autoParam (α → α → Ordering) Std.TreeMap.ofList._auto_1) → Std.TreeMap α β cmp
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The isomorphism between star and an abstract terminal object of `WithTerminal C`  -/
CategoryTheory.WithTerminal.starIsoTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.WithTerminal.star ≅ ⊤_ CategoryTheory.WithTerminal C
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNums.mk.sizeOf_spec : ∀ (tree : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt) (erased : Lean.PHashSet Lean.Name),
  sizeOf { tree := tree, erased := erased } = 1 + sizeOf tree + sizeOf erased
-- Mathlib.Data.TypeVec
TypeVec.dropFun_splitFun : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.last → α'.last),
  TypeVec.dropFun (TypeVec.splitFun f g) = f
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E} {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f s x →
      DifferentiableWithinAt 𝕜 g s x →
        fderivWithin 𝕜 (fun y => f y + g y) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x
-- Init.Data.Nat.Lcm
Nat.lcm_lcm_self_right_right : ∀ (m n : ℕ), m.lcm (n.lcm m) = m.lcm n
-- Mathlib.Analysis.Normed.Module.Basic
/-- A group homomorphism from a normed group to a real normed space,
bounded on a neighborhood of `0`, must be continuous.  -/
AddMonoidHom.continuous_of_isBounded_nhds_zero : ∀ {G : Type u_6} {H : Type u_7} [inst : SeminormedAddCommGroup G] [inst_1 : SeminormedAddCommGroup H] [NormedSpace ℝ H]
  {s : Set G} (f : G →+ H), s ∈ nhds 0 → Bornology.IsBounded (⇑f '' s) → Continuous ⇑f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)}, (Std.DTreeMap.Const.insertMany t l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_prod_refl : ∀ {α : Type u_1} {β : Type u_2}, (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (z z' : CochainComplex.HomComplex.Cochain K L n)
  (Φ : CategoryTheory.Functor C D) [inst_4 : Φ.Additive], (z + z').map Φ = z.map Φ + z'.map Φ
-- Mathlib.Algebra.BigOperators.Pi
prod_mk_prod : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Finset ι) (f : ι → M)
  (g : ι → N), (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x)
-- Std.Tactic.BVDecide.LRAT.Internal.PosFin
Std.Tactic.BVDecide.LRAT.Internal.instHashablePosFin : {n : ℕ} → Hashable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_curry_index : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : AddCommMonoid N]
  (f : α × β →₀ M) (g : α → β → M → N), (f.curry.sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c
-- Init.Data.SInt.Lemmas
Int16.le_antisymm : ∀ {a b : Int16}, a ≤ b → b ≤ a → a = b
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The set difference of a reproducing cone with itself equals `Set.univ`.  -/
ConvexCone.IsReproducing.sub_eq_univ : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {C : ConvexCone R M}, C.IsReproducing → ↑C - ↑C = Set.univ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.Hom.ext : ∀ {A B : ProfiniteAddGrp.{u}} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  (Std.ExtDTreeMap.filterMap f t).getKey? k =
    (t.getKey? k).pfilter fun x h' => (f x (Std.ExtDTreeMap.Const.get t x ⋯)).isSome
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.map₂.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {X Y : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A}
  (u u_1 : CategoryTheory.OverPresheafAux.OverArrows η t),
  u = u_1 →
    ∀ (f f_1 : X ⟶ Y) (e_f : f = f_1) (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s),
      u.map₂ f hst = u_1.map₂ f_1 ⋯
-- Mathlib.CategoryTheory.Subobject.Types
/-- For `α : Type u`, `Subobject α` is order isomorphic to `Set α`.
 -/
Types.subobjectEquivSet : (α : Type u) → CategoryTheory.Subobject α ≃o Set α
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instStreamStream_1 : {α : Type u} → {β : Type v} → Std.Stream (RBTree.RBMap.Values.Stream α β) β
-- Mathlib.RingTheory.Etale.Locus
Algebra.basicOpen_subset_etaleLocus_iff_etale : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] {f : A},
  ↑(PrimeSpectrum.basicOpen f) ⊆ Algebra.etaleLocus R A ↔ Algebra.Etale R (Localization.Away f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_eq_true_iff_forall_mem_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p a m[a] = true)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑(groupHomology.cycles A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesMap f φ 0)) x) =
    (Rep.Hom.hom φ) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).hom) x)
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- The pullback of two maps can be identified as a subspace of `X × Y`.  -/
TopCat.pullbackIsoProdSubtype : {X Y Z : TopCat} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      CategoryTheory.Limits.pullback f g ≅
        TopCat.of { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }
-- Mathlib.Data.Fin.Rev
Fin.le_rev_iff : ∀ {n : ℕ} {i j : Fin n}, i ≤ j.rev ↔ j ≤ i.rev
-- Mathlib.Data.Finset.Range
Finset.range_val : ∀ (n : ℕ), (Finset.range n).val = Multiset.range n
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.completedLFunction.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  DirichletCharacter.completedLFunction χ s = ZMod.completedLFunction (⇑χ) s
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedSMul.mk : ∀ {G : Type u_3} {P : Type u_4} [inst : LE G] [inst_1 : LE P] [inst_2 : SMul G P],
  (∀ (a b : P), a ≤ b → ∀ (c : G), c • a ≤ c • b) → (∀ (c d : G), c ≤ d → ∀ (a : P), c • a ≤ d • a) → IsOrderedSMul G P
-- Mathlib.Data.Set.Operations
/-- This lemma is intended for use with `rw` where a membership predicate is needed,
hence the explicit argument and the equality in the reverse direction from normal.
See also `Set.mem_ofPred_eq` for the reverse direction applied to an argument.  -/
Set.eq_mem_ofPred : ∀ {α : Type u} (p : α → Prop), p = fun x => x ∈ {a | p a}
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_sum_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
  {J : Type u_1} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (∑ j ∈ s, g j) h) =
    CategoryTheory.CategoryStruct.comp (∑ j ∈ s, CategoryTheory.CategoryStruct.comp f (g j)) h
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.transcendental_adjoin_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ [Nontrivial A] {s : Set ι} {i : ι}, Transcendental (↥(Algebra.adjoin R (x '' s))) (x i) ↔ i ∉ s
-- Mathlib.Algebra.Group.Action.Defs
IsLeftCancelVAdd.mk : ∀ {G : Type u_9} {P : Type u_10} [inst : VAdd G P],
  (∀ (a : G) (b c : P), a +ᵥ b = a +ᵥ c → b = c) → IsLeftCancelVAdd G P
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- A `PolynormableSpace` over `ℝ` is locally convex.

TODO: generalize to `RCLike`.  -/
instLocallyConvexSpaceRealOfPolynormableSpace : ∀ {E : Type u_6} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [PolynormableSpace ℝ E],
  LocallyConvexSpace ℝ E
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_inf_of_directed_le : ∀ {α : Type u_7} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Set α),
  s.Nonempty → DirectedOn (fun x1 x2 => x2 ≤ x1) s → ∀ (t : Finset α), (∀ x ∈ t, ∃ y ∈ s, y ≤ x) → ∃ x ∈ s, x ≤ t.inf id
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.noConfusionType : Sort v✝ → Lean.Lsp.SemanticTokenModifier → Lean.Lsp.SemanticTokenModifier → Sort v✝
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComonObjX_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.ofMonComonObjX M).X = M.X.X
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_at_natCast : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
  Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.success.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (response : α),
  sizeOf (Lean.Server.ServerRequestResponse.success response) = 1 + sizeOf response
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.snd.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], OrderAddMonoidHom.snd α β = { toAddMonoidHom := AddMonoidHom.snd α β, monotone' := ⋯ }
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.forall_mem_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {p : β → Prop}, (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (↑e x)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_ne_last_last : ∀ {n : ℕ} {a : Fin (n + 2)}, a ≠ Fin.last (n + 1) → a.succAbove (Fin.last n) = Fin.last (n + 1)
-- Mathlib.Data.ENNReal.Operations
ENNReal.lt_top_of_mul_ne_top_left : ∀ {a b : ENNReal}, a * b ≠ ⊤ → b ≠ 0 → a < ⊤
-- Std.Data.ExtDHashMap.Basic
/-- Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though is not possible
to get anything out of the hash map.
 -/
Std.ExtDHashMap.isEmpty : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → Bool
-- Init.Tactics
/-- `native_decide` is a synonym for `decide +native`.
It will attempt to prove a goal of type `p` by synthesizing an instance
of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
uses `#eval` to evaluate the decidability instance.

This should be used with care because it adds the entire lean compiler to the trusted
part, and a new axiom will show up in `#print axioms` for theorems using
this method or anything that transitively depends on them. Nevertheless, because it is
compiled, this can be significantly more efficient than using `decide`, and for very
large computations this is one way to run external programs and trust the result.
```lean
example : (List.range 1000).length = 1000 := by native_decide
```
 -/
Lean.Parser.Tactic.nativeDecide : Lean.ParserDescr
-- Lean.Data.Json.Basic
_private.Lean.Data.Json.Basic.0.Lean.Json.hash' : Lean.Json → UInt64
-- Mathlib.Algebra.RingQuot
RingQuot.instOne : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → One (RingQuot r)
-- Mathlib.Algebra.Tropical.Basic
Tropical.instAddCommSemigroupTropical : {R : Type u} → [LinearOrder R] → AddCommSemigroup (Tropical R)
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.completeLattice : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedGT ι] → CompleteLattice (Colex ((i : ι) → α i))
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.trans_assoc_reparam : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃),
  (p.trans q).trans r =
    (p.trans (q.trans r)).reparam (fun t => ⟨Path.Homotopy.transAssocReparamAux t, ⋯⟩)
      Path.Homotopy.trans_assoc_reparam._proof_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D Eᵒᵖ) (X : Cᵒᵖ),
  (F.leftOpComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.instIsLocalHomCarrierPtWalkingParallelPairEqualizerForkRingHomHomι : ∀ {A B : CommRingCat} (f g : A ⟶ B), IsLocalHom (CommRingCat.Hom.hom (CommRingCat.equalizerFork f g).ι)
-- Mathlib.Data.Nat.Prime.Factorial
Nat.Prime.coprime_factorial_of_lt : ∀ {p n : ℕ}, Nat.Prime p → n < p → p.Coprime n.factorial
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The domain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.HorizontalComp.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.HorizontalComp → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Algebra.Group.Action.Defs
/-- Multiplying `1` by a scalar gives `1`  -/
MulDistribMulAction.smul_one : ∀ {M : Type u_9} {N : Type u_10} {inst : Monoid M} {inst_1 : Monoid N} [self : MulDistribMulAction M N] (r : M),
  r • 1 = 1
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂TR.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          (x_2 : List α) →
            (x_3 : List β) →
              ((a : α) →
                  (as : List α) →
                    (b : β) →
                      (bs : List β) → (acca : List α) → (accb : List β) → motive (a :: as) (b :: bs) acca accb) →
                ((x : List α) →
                    (x_4 : List β) →
                      (acca : List α) →
                        (accb : List β) →
                          (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_4 = b :: bs → False) →
                            motive x x_4 acca accb) →
                  motive x x_1 x_2 x_3
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_def : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α}, s.lcm f = (Multiset.map f s.val).lcm
-- Mathlib.Analysis.Analytic.Binomial
/-- The radius of convergence of `binomialSeries 𝔸 a` is `1`, when `a` is not natural.  -/
binomialSeries_radius_eq_one : ∀ {𝕂 : Type v} [inst : RCLike 𝕂] {𝔸 : Type u} [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] {a : 𝕂},
  (∀ (k : ℕ), a ≠ ↑k) → (binomialSeries 𝔸 a).radius = 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
CategoryTheory.yonedaCommRingObj_map_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R : C} [inst_3 : CategoryTheory.CommRingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (x : Opposite.unop X ⟶ R),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaCommRingObj R).map f)) x =
    CategoryTheory.CategoryStruct.comp f.unop x
-- Mathlib.Topology.FiberBundle.Basic
/-- Promotion from a `Pretrivialization` to a `Trivialization`.  -/
FiberPrebundle.trivializationOfMemPretrivializationAtlas : {B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            (a : FiberPrebundle F E) →
              {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj} →
                e ∈ a.pretrivializationAtlas → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Init.Control.ExceptCps
ExceptCpsT.runCatch_bind_lift : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] (x : m α) (f : α → ExceptCpsT β m β),
  (ExceptCpsT.lift x >>= f).runCatch = do
    let a ← x
    (f a).runCatch
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_eq_bot_iff : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  LieIdeal.map f I = ⊥ ↔ I ≤ f.ker
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.map_lift_piComparison : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (P : C)
  (g : (j : β) → P ⟶ f j),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g))
      (CategoryTheory.Limits.piComparison G f) =
    CategoryTheory.Limits.Pi.lift fun j => G.map (g j)
-- Lean.Meta.Basic
/-- The function being cached information about. It is quite often an `Expr.const`.  -/
Lean.Meta.InfoCacheKey.expr : Lean.Meta.InfoCacheKey → Lean.Expr
-- Mathlib.Probability.Distributions.Cauchy
/-- The pdf of the cauchy distribution depending on its location `x₀` and scale `γ` parameters.  -/
ProbabilityTheory.cauchyPDFReal : ℝ → NNReal → ℝ → ℝ
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.ne_zero_of_coe_le_degree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, ↑n ≤ p.degree → p ≠ 0
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose n k` is congruent to `choose (n % p) (k % p) * choose (n / p) (k / p)`
modulo `p`. Also see `choose_modEq_choose_mod_mul_choose_div` for the version with `ZMOD`.  -/
Choose.choose_modEq_choose_mod_mul_choose_div_nat : ∀ {n k p : ℕ} [Fact (Nat.Prime p)], n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.Clause.of_maxLiteral_eq_some : ∀ {maxLit : ℕ} (c : Std.Sat.CNF.Clause ℕ),
  c.maxLiteral = some maxLit → ∀ (lit : ℕ), Std.Sat.CNF.Clause.Mem lit c → lit ≤ maxLit