mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Hom
/-- Reinterpret a `RingHom` as an `ℕ`-algebra homomorphism.  -/
RingHom.toNatAlgHom : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → R →ₐ[ℕ] S
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` expressed with a distance `dist` instead of an extended distance `edist`.  -/
MeasureTheory.tendstoInMeasure_iff_dist : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : PseudoMetricSpace E] {f : ι → α → E} {l : Filter ι} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (nhds 0)
-- Mathlib.ModelTheory.Basic
/-- Composition of first-order homomorphisms is associative.  -/
FirstOrder.Language.Equiv.comp_assoc : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Equiv M N) (g : L.Equiv N P)
  (h : L.Equiv P Q), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.ofContinuousOpenRestrict_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)),
  (PartialHomeomorph.ofContinuousOpenRestrict e hc ho).toPartialEquiv = e
-- Mathlib.Algebra.Group.Basic
eq_sub_of_add_eq' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, c + a = b → a = b - c
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.comap_restrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₂₁ : R₂ →+* R}
  {p : Submodule R₂ M₂} {q : Submodule R M} {f : M₂ →ₛₗ[σ₂₁] M} (h : ∀ x ∈ p, f x ∈ q) (p' : Submodule R ↥q),
  Submodule.comap (f.restrict h) p' = Submodule.comap p.subtype (Submodule.comap f (Submodule.map q.subtype p'))
-- Init.Data.SInt.Lemmas
Int16.toInt16_toUInt16 : ∀ (x : Int16), x.toUInt16.toInt16 = x
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.prop_of_isGood : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] {l : Profinite.NobelingProof.Products I} (J : I → Prop)
  [inst_1 : (j : I) → Decidable (J j)],
  Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C J) l → ∀ a ∈ ↑l, J a
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.of_fiber_homeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {J : Type u_4} [inst_3 : TopologicalSpace J] (g : I ≃ₜ J) {x : X},
  IsEvenlyCovered f x I → IsEvenlyCovered f x J
-- Mathlib.Order.WithBot
WithBot.trichotomous.gt : ∀ {α : Type u_1} [inst : Preorder α] [Std.Trichotomous fun x1 x2 => x1 > x2], Std.Trichotomous fun x1 x2 => x1 > x2
-- Mathlib.GroupTheory.CoprodI
/-- A reduced word determines an element of the free product, given by multiplication.  -/
Monoid.CoprodI.Word.prod : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → Monoid.CoprodI.Word M → Monoid.CoprodI M
-- Mathlib.NumberTheory.LucasLehmer
/-- If `2^p - 1` is prime then 2 is a square mod `2^p - 1`.  -/
legendreSym_mersenne_two : ∀ {p : ℕ} [inst : Fact (Nat.Prime (mersenne p))], 3 ≤ p → legendreSym (mersenne p) 2 = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : Inhabited α] [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey! k = m₁.getKey! k
-- Init.Data.Vector.Lemmas
Vector.all_eq_false : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = false ↔ ∃ i, ∃ (x : i < n), ¬p xs[i] = true
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_eq_empty : ∀ {α : Type u_1} {s t : Set α}, s \ t = ∅ ↔ s ⊆ t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableAt_arcsin : ∀ {x : ℝ}, DifferentiableAt ℝ Real.arcsin x ↔ x ≠ -1 ∧ x ≠ 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData : (α : Type u) → [Ord α] → Type u
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.uniformContinuous_comp : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {δ : Type u_2}
  [inst_2 : UniformSpace δ] (g : C(β, δ)), UniformContinuous ⇑g → UniformContinuous g.comp
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The coproduct comparison morphism.

In `Mathlib/CategoryTheory/Limits/Preserves/` we show
this is always an iso iff F preserves binary coproducts.
 -/
CategoryTheory.Limits.coprodComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{w, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (A B : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B] →
              [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] →
                F.obj A ⨿ F.obj B ⟶ F.obj (A ⨿ B)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquiv_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'], W'.pointEquiv WeierstrassCurve.Affine.Point.zero = none
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k k' fallback : α}, (k == k') = true → m.getKeyD k fallback = m.getKeyD k' fallback
-- Mathlib.GroupTheory.Transfer
/-- The difference of two left transversals  -/
AddSubgroup.leftTransversals.diff : {G : Type u_1} →
  [inst : AddGroup G] →
    {H : AddSubgroup G} →
      {A : Type u_2} →
        [inst_1 : AddCommGroup A] → (↥H →+ A) → H.LeftTransversal → H.LeftTransversal → [H.FiniteIndex] → A
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_iff_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {a : α}, a ∈ m ↔ m.contains a = true
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {c : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α},
  (Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖) ↔ Asymptotics.IsBigOWith c l f' g'
-- Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Tactic.GCongr.ForwardExt.eval : Mathlib.Tactic.GCongr.ForwardExt → Lean.Expr → Lean.MVarId → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  (X : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A) (X_1 : Cᵒᵖ),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.counitIso.inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Mathlib.RingTheory.AdicCompletion.Topology
/-- `IsAdicComplete I R` is equivalent to being complete and hausdorff in the adic topology.  -/
IsAdic.isAdicComplete_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : UniformSpace R] [IsUniformAddGroup R] {I : Ideal R},
  IsAdic I → (IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R)
-- Mathlib.Topology.Order
isOpen_iSup_iff : ∀ {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α}, IsOpen s ↔ ∀ (i : ι), IsOpen s
-- Mathlib.Data.List.Basic
Function.Involutive.list_map : ∀ {α : Type u} {f : α → α}, Function.Involutive f → Function.Involutive (List.map f)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.ofExact_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₑ D), (CategoryTheory.LeftExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide if `t` is measurable.  -/
MeasureTheory.setIntegral_eq_of_subset_of_forall_sdiff_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t → s ⊆ t → (∀ x ∈ t \ s, f x = 0) → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.φ_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g h)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insert k v).minKey ⋯ = k
-- Mathlib.Order.GaloisConnection.Basic
isLUB_image2_of_isGLB_isGLB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) →
    (∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) →
      IsGLB s a₀ → IsGLB t b₀ → IsLUB (Set.image2 l s t) (l a₀ b₀)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.restoreM_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps]
  [inst_1 : Pure m] (x : stM m m α), ⦃(Std.Do.wp (pure x)).apply Q⦄ restoreM x ⦃Q⦄
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroupOfClass : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [v.IsRankOneDiscrete], IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
-- Mathlib.LinearAlgebra.LinearPMap
/-- The unique `LinearPMap` on `span R {x}` that sends a non-zero vector `x` to `y`.
This version works for modules over division rings.  -/
LinearPMap.mkSpanSingleton : {K : Type u_7} →
  {L : Type u_8} →
    {E : Type u_9} →
      {F : Type u_10} →
        [inst : DivisionRing K] →
          [inst_1 : DivisionRing L] →
            {σ : K →+* L} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module K E] →
                  [inst_4 : AddCommGroup F] → [inst_5 : Module L F] → (x : E) → F → x ≠ 0 → E →ₛₗ.[σ] F
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocDiv hp (a + m • p) b = toIocDiv hp a b - ↑m
-- Std.Data.Internal.Cut
Std.Internal.instIsStrictCutCompareThenGt : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] {k : α},
  Std.Internal.IsStrictCut compare fun k' => (compare k k').then Ordering.gt
-- Mathlib.Order.BoundedOrder.Basic
eq_bot_or_bot_lt : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] (a : α), a = ⊥ ∨ ⊥ < a
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
-- Mathlib.Logic.IsEmpty.Defs
isEmpty_iff : ∀ {α : Sort u}, IsEmpty α ↔ ∀ (a : α), False
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.Config.mk.sizeOf_spec : ∀ (toConfig : Mathlib.Tactic.AtomM.Recurse.Config) (ifUnchanged : Mathlib.Tactic.BehaviorIfUnchanged)
  (mode : Mathlib.Tactic.RingNF.RingMode),
  sizeOf { toConfig := toConfig, ifUnchanged := ifUnchanged, mode := mode } =
    1 + sizeOf toConfig + sizeOf ifUnchanged + sizeOf mode
-- Mathlib.Topology.DerivedSet
preperfect_iff_subset_derivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X}, Preperfect U ↔ U ⊆ derivedSet U
-- Mathlib.ModelTheory.DirectLimit
/-- Every finitely generated substructure of the direct limit corresponds to some
substructure in some component of the directed system.  -/
FirstOrder.Language.DirectLimit.exists_fg_substructure_in_Sigma : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι]
  (S : L.Substructure (FirstOrder.Language.DirectLimit G f)),
  S.FG → ∃ i T, FirstOrder.Language.Substructure.map (FirstOrder.Language.DirectLimit.of L ι G f i).toHom T = S
-- Init.Data.Array.Lemmas
Array.reverse_eq_iff : ∀ {α : Type u_1} {xs ys : Array α}, xs.reverse = ys ↔ xs = ys.reverse
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
_private.Mathlib.NumberTheory.LSeries.AbstractFuncEq.0.WeakFEPair.functional_equation_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (s : ℂ),
  mellin P.f (↑P.k - s) = P.ε • mellin P.g s
-- Lean.Parser.Command
Lean.Parser.Command.classTk.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.exists_walk_length_eq_edist : ∀ {V : Type u_1} {G : SimpleGraph V}, G.Connected → ∀ (u v : V), ∃ p, ↑p.length = G.edist u v
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.sc'Map_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
  (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'Map._auto_1)
  (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'Map._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'Map._auto_5),
  (CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk).τ₁ = φ.app ⟨i, ⋯⟩
-- Mathlib.Algebra.Star.Basic
StarMemClass.coe_star : ∀ {R : Type u} {S : Type w} [inst : Star R] [inst_1 : SetLike S R] [hS : StarMemClass S R] (s : S) (x : ↥s),
  ↑(star x) = star ↑x
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.nnbound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F),
  ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊
-- Mathlib.Data.PNat.Basic
PNat.pow_coe : ∀ (m : ℕ+) (n : ℕ), ↑(m ^ n) = ↑m ^ n
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a compact closed subset.
Compared to `MeasurableSet.exists_isCompact_lt_add`,
this version additionally assumes that `α` is an R₁ space with Borel σ-algebra.
 -/
MeasurableSet.exists_isCompact_isClosed_lt_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [R1Space α] [BorelSpace α] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.ofNat_eq : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : (n : ℕ) → OfNat α n]
  [Lean.Grind.ToInt.OfNat α i] (n : ℕ), ↑(OfNat.ofNat n) = i.wrap ↑n
-- Init.Data.Int.DivMod.Lemmas
Int.add_mul_fdiv_right : ∀ (a b : ℤ) {c : ℤ}, c ≠ 0 → (a + b * c).fdiv c = a.fdiv c + b
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_pow_eq_zero_of_le : ∀ (p : ℕ) {m n : ℕ}, n ≤ m → ↑p ^ m = 0
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_zero : Nat.factorization 0 = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMax'.eq_1 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α), x.splitMax' x_1 Ordnode.nil = (x, x_1)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iterate_mem_periodicOrbit : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∈ Function.periodicPts f → ∀ (n : ℕ), f^[n] x ∈ Function.periodicOrbit f x
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N],
  CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p =
    CategoryTheory.shrinkYoneda.{w, v, u}.comp
      (((CategoryTheory.Functor.whiskeringLeft Nᵒᵖ Cᵒᵖ (Type w)).obj p.op).comp CategoryTheory.Limits.colim)
-- Mathlib.RingTheory.IdealFilter.Basic
/-- We say that the quotient `K/L` is `F`-torsion if every element `k ∈ K` is annihilated
(modulo `L`) by some ideal in `F`. Equivalently, for each `k ∈ K` there exists `I ∈ F`
such that `I ≤ L.colon {k}`. This formulation avoids forming the quotient module explicitly.  -/
IdealFilter.IsTorsionQuot : {A : Type u_1} → [inst : Ring A] → IdealFilter A → Ideal A → Ideal A → Prop
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `contMDiffOn_baseSet_iff_localFrameCoeff`.

---

A section `s` of `V` is `C^k` on a trivialisation domain `e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
contMDiffOn_baseSet_iff_localFrame_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) e.baseSet ↔
    ∀ (i : ι),
      ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
        e.baseSet
-- Mathlib.Order.Minimal
Maximal.or : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Maximal (fun x => P x ∨ Q x) x → Maximal P x ∨ Maximal Q x
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_mul : ∀ {a b : USize} (h : System.Platform.numBits = 64), (a * b).toBitVec64 h = a.toBitVec64 h * b.toBitVec64 h
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.condExp_condExp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [CompleteSpace E] (f : Ω → E) {μ : MeasureTheory.Measure Ω}
  (ℱ : MeasureTheory.Filtration ι m) {i j : ι},
  i ≤ j → ∀ [MeasureTheory.SigmaFinite (μ.trim ⋯)], μ[μ[f | ↑ℱ j] | ↑ℱ i] =ᵐ[μ] μ[f | ↑ℱ i]
-- Init.Data.List.Sublist
List.suffix_filterMap_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β},
  l₂ <:+ List.filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = List.filterMap f l
-- Mathlib.Algebra.Order.Monovary
monovaryOn_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → (MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s)
-- Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
NonarchimedeanAddGroup.instTotallySeparated : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [NonarchimedeanAddGroup G] [T2Space G],
  TotallySeparatedSpace G
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.linearCombination_apply : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M) (f : α → R), (Fintype.linearCombination R v) f = ∑ i, f i • v i
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.tensorObj_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) (f g : X ⟶ X),
  CategoryTheory.MonoidalCategoryStruct.tensorObj f g = CategoryTheory.CategoryStruct.comp f g
-- Init.Data.List.Basic
List.Sublist.brecOn : ∀ {α : Type u_1} {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} {a a_1 : List α} (t : a.Sublist a_1),
  (∀ (a a_2 : List α) (t : a.Sublist a_2), List.Sublist.below t → motive a a_2 t) → motive a a_1 t
-- Std.Time.Format.Modifier
/-- Minimum number of digits; output is zero-padded on the left to reach this width. Determined by the count of pattern letters.
 -/
Std.Time.Number.padding : Std.Time.Number → ℕ
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_inv : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).iso.inv =
    CategoryTheory.CategoryStruct.id (X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.mem_range_map_iff_coeffs_subset : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f : R →+* S₁}
  {x : MvPolynomial σ S₁}, x ∈ Set.range ⇑(MvPolynomial.map f) ↔ ↑x.coeffs ⊆ Set.range ⇑f
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Functor.toProfunctorRev_obj_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : D) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  (F.toProfunctorRev.obj X).map f = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (F.map f.unop) g