mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldl_eq_foldl_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.DTreeMap.Raw.foldl (fun d a x => f d a) init t = Array.foldl f init t.keysArray
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.dpow_eq : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hJ : hI.IsSubDPIdeal J)
  [inst_1 : (x : A) → Decidable (x ∈ J)] (n : ℕ) (a : A),
  (DividedPowers.IsSubDPIdeal.dividedPowers hI hJ).dpow n a = if a ∈ J then hI.dpow n a else 0
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_ne_zero_iff : ∀ {x y : ℕ}, x ^^^ y ≠ 0 ↔ x ≠ y
-- Mathlib.Algebra.Group.Irreducible.Lemmas
irreducible_mul_iff : ∀ {M : Type u_2} [inst : Monoid M] {x y : M}, Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix is the rank of the space spanned by its columns.  -/
Matrix.rank_eq_finrank_span_cols : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] (A : Matrix m n R),
  A.rank = Module.finrank R ↥(Submodule.span R (Set.range A.col))
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.sub_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Sub β] (f g : MeasureTheory.SimpleFunc α β)
  (x : α), (f - g) x = f x - g x
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.rightFDRep.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G],
  TannakaDuality.FiniteGroup.rightFDRep = FDRep.of TannakaDuality.FiniteGroup.rightRegular
-- Plausible.Gen
/-- `frequency` picks a generator from the list `gs` according to the weights in `gs`.
If `gs` is empty, the `default` generator is returned.   -/
Plausible.Gen.frequency : {α : Type} → Plausible.Gen α → List (ℕ × Plausible.Gen α) → Plausible.Gen α
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piRight_symm_single : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : N) (i : ι) (m : M i),
  (TensorProduct.piRight R S N M).symm (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphStrict_subgraph_toSimpleGraphInclusive : ∀ {V : Type u_1} (G : Digraph V), G.toSimpleGraphStrict ≤ G.toSimpleGraphInclusive
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- A series of the form considered in Mahler's theorem.  -/
PadicInt.mahlerSeries : {p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    {E : Type u_1} →
      [inst : NormedAddCommGroup E] → [inst_1 : Module ℤ_[p] E] → [IsBoundedSMul ℤ_[p] E] → (ℕ → E) → C(ℤ_[p], E)
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.toHomeomorphSourceTarget_apply_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (a : ↑e.source), ↑(e.toHomeomorphSourceTarget a) = ↑e ↑a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.ofList_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  Std.DHashMap.Raw.Const.ofList ((k, v) :: tl) = Std.DHashMap.Raw.Const.insertMany (∅.insert k v) tl
-- Mathlib.Data.QPF.Univariate.Basic
QPF.liftp_iff_of_isUniform : ∀ {F : Type u → Type u} [q : QPF F],
  QPF.IsUniform → ∀ {α : Type u} (x : F α) (p : α → Prop), Functor.Liftp p x ↔ ∀ u ∈ Functor.supp x, p u
-- Mathlib.Algebra.BigOperators.Finprod
finprod_of_infinite_mulSupport : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M},
  (Function.mulSupport f).Infinite → ∏ᶠ (i : α), f i = 1
-- Mathlib.Data.List.Shortlex
List.Shortlex.asymm : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Asymm r], Std.Asymm (List.Shortlex r)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.isClosedEmbedding_subtypeL : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), IsClosed ↑p → Topology.IsClosedEmbedding ⇑p.subtypeL
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forM_eq_forM_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α × β → m PUnit.{w + 1}}, forM t f = forM t.toArray f
-- Mathlib.Order.WithBot
/-- Auxiliary definition for the order on `WithBot`.  -/
WithBot.LT : {α : Type u_1} → [LT α] → WithBot α → WithBot α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.mk.injEq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (pt : C) (fst : pt ⟶ P) (snd : pt ⟶ Q) (inl : P ⟶ pt) (inr : Q ⟶ pt)
  (inl_fst :
    autoParam (CategoryTheory.CategoryStruct.comp inl fst = CategoryTheory.CategoryStruct.id P)
      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam)
  (inl_snd :
    autoParam (CategoryTheory.CategoryStruct.comp inl snd = 0) CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam)
  (inr_fst :
    autoParam (CategoryTheory.CategoryStruct.comp inr fst = 0) CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam)
  (inr_snd :
    autoParam (CategoryTheory.CategoryStruct.comp inr snd = CategoryTheory.CategoryStruct.id Q)
      CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam)
  (pt_1 : C) (fst_1 : pt_1 ⟶ P) (snd_1 : pt_1 ⟶ Q) (inl_1 : P ⟶ pt_1) (inr_1 : Q ⟶ pt_1)
  (inl_fst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inl_1 fst_1 = CategoryTheory.CategoryStruct.id P)
      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam)
  (inl_snd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inl_1 snd_1 = 0)
      CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam)
  (inr_fst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inr_1 fst_1 = 0)
      CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam)
  (inr_snd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inr_1 snd_1 = CategoryTheory.CategoryStruct.id Q)
      CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam),
  ({ pt := pt, fst := fst, snd := snd, inl := inl, inr := inr, inl_fst := inl_fst, inl_snd := inl_snd,
        inr_fst := inr_fst, inr_snd := inr_snd } =
      { pt := pt_1, fst := fst_1, snd := snd_1, inl := inl_1, inr := inr_1, inl_fst := inl_fst_1, inl_snd := inl_snd_1,
        inr_fst := inr_fst_1, inr_snd := inr_snd_1 }) =
    (pt = pt_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1 ∧ inl ≍ inl_1 ∧ inr ≍ inr_1)
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Icc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (b : α i), Function.update f i '' Set.Icc (f i) b = Set.Icc f (Function.update f i b)
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image₂_image_left_comm`.  -/
Finset.image_image₂_distrib_left : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
  [inst_1 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {g : γ → δ}
  {f' : α' → β → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' a) b) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' s) t
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
/-- An object `X` in a category `C` is Artinian if `Subobject X`
satisfies the descending chain condition.  -/
CategoryTheory.IsArtinianObject : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Prop
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  {S'' : C} {q : S'' ⟶ S'} {ι'' : Type t''} {X'' : ι'' → C} {f'' : (k : ι'') → X'' k ⟶ S''} {β : ι'' → ι'}
  {q' : (k : ι'') → X'' k ⟶ X' (β k)}
  (w' :
    ∀ (k : ι''), CategoryTheory.CategoryStruct.comp (q' k) (f' (β k)) = CategoryTheory.CategoryStruct.comp (f'' k) q)
  (r : S'' ⟶ S) {r' : (k : ι'') → X'' k ⟶ X (α (β k))}
  (hr :
    autoParam (CategoryTheory.CategoryStruct.comp q p = r)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso._auto_1)
  (hr' :
    autoParam (∀ (k : ι''), CategoryTheory.CategoryStruct.comp (q' k) (p' (β k)) = r' k)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso._auto_3)
  (X_1 : F.DescentData f) (i : ι''),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso F w w' r hr hr').inv.app X_1).hom i =
    (F.mapComp' (p' (β i)).op.toLoc (q' i).op.toLoc (r' i).op.toLoc ⋯).hom.toNatTrans.app (X_1.obj (α (β i)))
-- Mathlib.Data.ENat.Lattice
ENat.mul_iSup : ∀ {ι : Sort u_2} (a : ℕ∞) (f : ι → ℕ∞), a * ⨆ i, f i = ⨆ i, a * f i
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.AC.DiseqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.AC.DiseqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.AC.DiseqCnstr) →
      ((t : Lean.Meta.Grind.AC.DiseqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.AC.DiseqCnstrProof) → t.below → motive_2 t) → motive_1 t ×' t.below
-- Qq.Macro
Qq.Impl.betaRev' : Lean.Expr → List Lean.Expr → Lean.Expr
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_3.splitter : {α : Type u_1} →
  (motive : List (Computation α) × Stream'.WSeq (Computation α) → Sort u_2) →
    (x : List (Computation α) × Stream'.WSeq (Computation α)) →
      ((l : List (Computation α)) → (S : Stream'.WSeq (Computation α)) → motive (l, S)) → motive x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k fallback : α),
  t.getKeyD k fallback =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => fallback
    | Std.DTreeMap.Internal.Impl.inner size k' v l r =>
      match compare k k' with
      | Ordering.lt => l.getKeyD k fallback
      | Ordering.gt => r.getKeyD k fallback
      | Ordering.eq => k'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_div_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a b c : K}, c ≠ 0 → (a ≤ᵥ b / c ↔ a * c ≤ᵥ b)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.isIntegral : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.RingOfIntegers K), IsIntegral ℤ x
-- Mathlib.Order.Defs.Unbundled
IsStrictOrder.toIrrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsStrictOrder α r], Std.Irrefl r
-- Lean.Environment
/-- Creates environment object from given imports.

If `leakEnv` is true, we mark the environment as persistent, which means it will not be freed. We
set this when the object would survive until the end of the process anyway. In exchange, RC updates
are avoided, which is especially important when they would be atomic because the environment is
shared across threads (potentially, storing it in an `IO.Ref` is sufficient for marking it as such).

If `loadExts` is true, we initialize the environment extensions using the imported data. Doing so
may use the interpreter and thus is only safe to do after calling `enableInitializersExecution`; see
also caveats there. If not set, every extension will have its initial value as its state. While the
environment's constant map can be accessed without `loadExts`, many functions that take
`Environment` or are in a monad carrying it such as `CoreM` may not function properly without it.

If `level` is `exported`, the module to be elaborated is assumed to be participating in the module
system and imports will be restricted accordingly. If it is `server`, the data for
`getModuleEntries (includeServer := true)` is loaded as well. If it is `private`, all data is loaded
as if no `module` annotations were present in the imports.
 -/
Lean.importModules : Array Lean.Import →
  Lean.Options →
    optParam UInt32 0 →
      optParam (Array Lean.Plugin) #[] →
        optParam Bool false →
          optParam Bool false →
            optParam Lean.OLeanLevel Lean.OLeanLevel.private →
              optParam (Lean.NameMap Lean.ImportArtifacts) ∅ → IO Lean.Environment
-- Init.System.Platform
/-- Checks whether the current platform is [Emscripten](https://emscripten.org/).
 -/
System.Platform.getIsEmscripten : Unit → Bool
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
isStrongFEPair_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P.symm ↔ IsStrongFEPair P
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] (g : β → γ) (h : γ → δ)
  (f : MeasureTheory.SimpleFunc α β),
  MeasureTheory.SimpleFunc.map h (MeasureTheory.SimpleFunc.map g f) = MeasureTheory.SimpleFunc.map (h ∘ g) f
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.CG.map_of_surjective : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.CG L M →
    ∀ (f : L.Hom M N), Function.Surjective ⇑f → FirstOrder.Language.Structure.CG L N
-- Mathlib.Data.Set.Lattice
Set.iUnion_of_empty : ∀ {α : Type u_1} {ι : Sort u_5} [IsEmpty ι] (s : ι → Set α), ⋃ i, s i = ∅
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get!ₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α fun x => β) (k : α) [inst_1 : Inhabited β],
  Std.DTreeMap.Internal.Impl.Const.get!ₘ l k = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).get!
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- An `R`-module `M` is isotypic of type `S` if all simple submodules of `M` are isomorphic
to `S`. If `M` is semisimple, it is equivalent to requiring that all simple quotients of `M` are
isomorphic to `S`.  -/
IsIsotypicOfType : (R : Type u_2) →
  (M : Type u) →
    (S : Type u_4) →
      [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : AddCommGroup S] → [Module R M] → [Module R S] → Prop
-- Mathlib.Analysis.Convex.Segment
mem_segment_add_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [Invertible 2] (x y : E), x ∈ segment 𝕜 (x + y) (x - y)
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instMulAction' : {M : Type u_1} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction M (Lex α)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isOpen_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsOpen (Metric.ball x ε)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_map_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₁ = f.f i
-- Mathlib.Data.Finset.Image
/-- Given a predicate `p : α → Prop`, produces an equivalence between
`Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`.  -/
Equiv.finsetSubtypeComm : {α : Type u_1} → (p : α → Prop) → Finset { a // p a } ≃ { s // ∀ a ∈ s, p a }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.ext_iff : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Jacobian R} {x y : W'.Point}, x = y ↔ x.point = y.point
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) =
    CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
-- Mathlib.Algebra.Group.Basic
neg_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), -(a - b) = b - a
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverPullbackIsoToOver_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : C} (f : Y ⟶ X) [inst_2 : CategoryTheory.ChosenPullbacksAlong f] (X_1 : C),
  ((CategoryTheory.toOverPullbackIsoToOver f).hom.app X_1).left =
    CategoryTheory.CartesianMonoidalCategory.lift
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Over.mapForget f).hom.app
          ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj ((CategoryTheory.toOver X).obj X_1)))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Over.Hom.left
            ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).counit.app ((CategoryTheory.toOver X).obj X_1)))
          (CategoryTheory.SemiCartesianMonoidalCategory.fst X_1 X)))
      ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj ((CategoryTheory.toOver X).obj X_1)).hom
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of `f` on a two-point set `{a, b}` is the distance between its two values.  -/
eVariationOn.pair : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (a b : α),
  eVariationOn f {a, b} = edist (f a) (f b)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE_ιE_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_ιE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_ιE._auto_3) {Z : C}
  (h : X.opcycles f₂ f₃ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁)
      (CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) h)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.approx_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β]
  [inst_3 : Zero β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] [inst_6 : MeasurableSpace β]
  [OpensMeasurableSpace β] {i : ℕ → β} {f : α → β} {n : ℕ} (a : α),
  Measurable f → (MeasureTheory.SimpleFunc.approx i f n) a = (Finset.range n).sup fun k => if i k ≤ f a then i k else 0
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Pre-composition of a `Bundle.Trivialization` and a `Homeomorph`.  -/
Bundle.Trivialization.compHomeomorph : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              Bundle.Trivialization F proj →
                {Z' : Type u_5} → [inst_3 : TopologicalSpace Z'] → (h : Z' ≃ₜ Z) → Bundle.Trivialization F (proj ∘ ⇑h)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup : ∀ {X : AlgebraicGeometry.Scheme} (Z : Set (TopologicalSpace.Closeds ↥X)),
  AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (sSup Z) =
    ⨅ z ∈ Z, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal z
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  [inst_6 : SizeOf C] (m₁ : Z₁₂ ⟶ Z₁₃) (m₃ : Z₁₃ ⟶ Z₂₃) (comm₁ : CategoryTheory.CategoryStruct.comp m₁ v₁₃ = v₁₂)
  (comm₂ :
    CategoryTheory.CategoryStruct.comp w₁₂ ((CategoryTheory.shiftFunctor C 1).map m₁) =
      CategoryTheory.CategoryStruct.comp u₂₃ w₁₃)
  (comm₃ : CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map m₃) = w₂₃)
  (comm₄ : CategoryTheory.CategoryStruct.comp m₃ v₂₃ = CategoryTheory.CategoryStruct.comp v₁₃ u₁₂)
  (mem :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles),
  sizeOf { m₁ := m₁, m₃ := m₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃, comm₄ := comm₄, mem := mem } =
    1 + sizeOf m₁ + sizeOf m₃ + sizeOf comm₁ + sizeOf comm₂ + sizeOf comm₃ + sizeOf comm₄ + sizeOf mem
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.handleEx : Lean.Name →
  Lean.Elab.Tactic.SavedState →
    Array Lean.Elab.Tactic.EvalTacticFailure →
      Lean.Exception →
        (Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.TacticM Unit) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Ring.Subsemiring.Defs
ofNat_mem : ∀ {S : Type u_1} {R : Type u_2} [inst : AddMonoidWithOne R] [inst_1 : SetLike S R] [AddSubmonoidWithOneClass S R]
  (s : S) (n : ℕ) [inst_3 : n.AtLeastTwo], OfNat.ofNat n ∈ s
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_two_left : ∀ {n : ℕ}, Nat.Coprime 2 n ↔ Odd n
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
AddMonoidAlgebra.nonUnitalAlgHom_ext' : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Add M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₙₐ[R] A},
  φ₁.toMulHom.comp (AddMonoidAlgebra.ofMagma R M) = φ₂.toMulHom.comp (AddMonoidAlgebra.ofMagma R M) → φ₁ = φ₂
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
_private.Mathlib.RingTheory.WittVector.FrobeniusFractionField.0.WittVector.term𝕎 : Lean.ParserDescr