mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.eventually_eventually : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {u : β → α},
  CauchySeq u → ∀ {V : SetRel α α}, V ∈ uniformity α → ∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) ∈ V
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.toHImp : {α : Type u_1} → [self : Order.Frame α] → HImp α
-- Mathlib.Computability.Ackermann
max_ack_right : ∀ (m n₁ n₂ : ℕ), ack m (max n₁ n₂) = max (ack m n₁) (ack m n₂)
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.jsxText.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Notation.Defs
/-- A star operation (e.g. complex conjugate).
 -/
Star.star : {R : Type u} → [self : Star R] → R → R
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.CollectDecVarsM : Type → Type
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- `E →L[𝕜] E` is a star algebra with the adjoint as the star operation.  -/
ContinuousLinearMap.instStarId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → Star (E →L[𝕜] E)
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.iInter_countable_halfSpaces_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E}
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  Convex ℝ s → IsClosed s → ∃ l c, ⋂ n, {x | RCLike.re ((l n) x) ≤ c n} = s
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_eq_ite_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α} [MulLeftMono α], a⁻ᵐ = if a < 1 then a⁻¹ else 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- If `f` and `g` are simplicially homotopic maps of simplicial sets,
then they induce chain-homotopic maps on the singular chain complexes
with coefficients in `R`. The assumption is in `SimplicialObject.Homotopy`,
see also `SSet.Homotopy.chainComplexMap` for the
variant using `SSet.Homotopy` as an assumption.
 -/
CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasCoproducts C] →
        {X Y : SSet} →
          {f g : X ⟶ Y} →
            CategoryTheory.SimplicialObject.Homotopy f g →
              (R : C) → Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)
-- Std.Data.DTreeMap.Internal.Model
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.reverse : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.parseModifier : String → Lean.CoreM Lean.Meta.Grind.AttrKind
-- Mathlib.GroupTheory.Complement
AddSubgroup.instInhabitedLeftTransversal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  AddSubgroup.instInhabitedLeftTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.op_left : ∀ {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}
  (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂), ψ.op.left = ψ.right.op
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_const : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} {C : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (x : E),
  (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) (MeasureTheory.Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) =
    (T Set.univ) x
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.iff_toPrenex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n), ∅.Iff φ φ.toPrenex
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.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}
  {f' g' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → HasFDerivAtFilter g g' L → HasFDerivAtFilter (f + g) (f' + g') L
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- Geck's name for the "left" basis elements of `b.support ⊕ ι`.  -/
RootPairing.GeckConstruction.u : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} → {b : P.Base} → [DecidableEq ι] → ↥b.support → ↥b.support ⊕ ι → R
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_const' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E],
  p ≠ 0 → p ≠ ⊤ → ∀ (c : E), MeasureTheory.lpNorm (fun _x => c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹
-- Mathlib.Order.Filter.AtTopBot.Defs
Monotone.piecewise_eventually_eq_iUnion : ∀ {ι : Type u_1} {α : Type u_3} {β : α → Type u_6} [inst : Preorder ι] {s : ι → Set α}
  [inst_1 : (i : ι) → DecidablePred fun x => x ∈ s i] [inst_2 : DecidablePred fun x => x ∈ ⋃ i, s i],
  Monotone s →
    ∀ (f g : (a : α) → β a) (a : α), ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
-- Mathlib.Algebra.Opposites
MulOpposite.instUnique.eq_1 : ∀ {α : Type u_1} [inst : Unique α], MulOpposite.instUnique = Unique.mk' αᵐᵒᵖ
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_5.eq_2 : ∀ (motive : (n : ℕ) → (P : Fin n → Prop) → (inst : DecidablePred P) → Fin (Fin.countP fun x => decide (P x)) → Sort u_1)
  (n : ℕ) (P : Fin (n + 1) → Prop) (inst : DecidablePred P) (k : ℕ) (hk : k < Fin.countP fun x => decide (P x))
  (h_1 :
    (x : Fin 0 → Prop) →
      (x_1 : DecidablePred x) → (val : ℕ) → (h : val < Fin.countP fun x_2 => decide (x x_2)) → motive 0 x x_1 ⟨val, h⟩)
  (h_2 :
    (n : ℕ) →
      (P : Fin (n + 1) → Prop) →
        (inst : DecidablePred P) →
          (k : ℕ) → (hk : k < Fin.countP fun x => decide (P x)) → motive n.succ P inst ⟨k, hk⟩),
  (match n.succ, P, inst, ⟨k, hk⟩ with
    | 0, x, x_1, ⟨val, h⟩ => h_1 x x_1 val h
    | n.succ, P, inst, ⟨k, hk⟩ => h_2 n P inst k hk) =
    h_2 n P inst k hk
-- Mathlib.Combinatorics.SimpleGraph.Hall
/-- This is the version of **Hall's marriage theorem** for bipartite graphs that finds a perfect
matching given that the neighborhood-condition holds globally.  -/
SimpleGraph.exists_isPerfectMatching_of_forall_ncard_le : ∀ {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V},
  G.IsBipartiteWith p₁ p₂ → (∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) → ∃ M, M.IsPerfectMatching
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- **Alias** of the reverse direction of `affineIndependent_vadd`. -/
AffineIndependent.vadd : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P} {v : V}, AffineIndependent k p → AffineIndependent k (v +ᵥ p)
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The orthocenter is the only point lying in any two of the
altitudes.  -/
Affine.Triangle.eq_orthocenter_of_forall_mem_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P} {i₁ i₂ : Fin 3} {p : P},
  i₁ ≠ i₂ → p ∈ Affine.Simplex.altitude t i₁ → p ∈ Affine.Simplex.altitude t i₂ → p = t.orthocenter
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.MonadSatisfying.instEStateM.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → x = EStateM.Result.ok a s' → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → x = EStateM.Result.error e s' → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- Suppose that a function `f : ℂ → E` is *real* differentiable on a closed rectangle with opposite
corners at `z w : ℂ` and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then
the integral of `f` over the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle.  -/
Complex.integral_boundary_rect_of_differentiableOn_real : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ),
  DifferentiableOn ℝ f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
    MeasureTheory.IntegrableOn (fun z => Complex.I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) Complex.I)
        (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume →
      (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
            Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
          Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
        ∫ (x : ℝ) in z.re..w.re,
          ∫ (y : ℝ) in z.im..w.im,
            Complex.I • (fderiv ℝ f (↑x + ↑y * Complex.I)) 1 - (fderiv ℝ f (↑x + ↑y * Complex.I)) Complex.I
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α)
  (ord :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this := toPreorderOfLEArgs.decidableLE;
      Ord α)
      Std.Packages.LinearPreorderOfLEArgs.ord._autoParam)
  (le_total : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam)
  (isLE_compare :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this_1 := toPreorderOfLEArgs.decidableLE;
      let this_2 := ord;
      ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
      Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam)
  (isGE_compare :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this_1 := toPreorderOfLEArgs.decidableLE;
      have this_2 := le_total;
      let this_3 := ord;
      ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
      Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam),
  sizeOf
      { toPreorderOfLEArgs := toPreorderOfLEArgs, ord := ord, le_total := le_total, isLE_compare := isLE_compare,
        isGE_compare := isGE_compare } =
    1 + sizeOf toPreorderOfLEArgs + sizeOf ord
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.child : {n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    (a : P.A) →
      (f : P.last.B a → P.last.W) → (i : Fin2 n) → (j : P.last.B a) → P.WPath (f j) i → P.WPath (WType.mk a f) i
-- Mathlib.Topology.CompactOpen
Topology.IsQuotientMap.continuous_lift_prod_left : ∀ {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X₀]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Z] [LocallyCompactSpace Y]
  {f : X₀ → X}, Topology.IsQuotientMap f → ∀ {g : X × Y → Z}, (Continuous fun p => g (f p.1, p.2)) → Continuous g
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.bilinLeftCLM.congr_simp : ∀ {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D]
  [inst_7 : NormedSpace ℝ D] [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F]
  [inst_11 : NormedSpace 𝕜 E] [inst_12 : NormedSpace 𝕜 G] (B B_1 : E →L[𝕜] F →L[𝕜] G),
  B = B_1 →
    ∀ {g g_1 : D → F} (e_g : g = g_1) (hg : Function.HasTemperateGrowth g),
      SchwartzMap.bilinLeftCLM B hg = SchwartzMap.bilinLeftCLM B_1 ⋯
-- Mathlib.Order.Hom.Lattice
LatticeHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  {g₁ g₂ : LatticeHom β γ} {f : LatticeHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Aesop.Tree.Data
Aesop.RappData.mk.injEq : ∀ {Goal MVarCluster : Type} (id : Aesop.RappId) (parent : IO.Ref Goal) (children : Array (IO.Ref MVarCluster))
  (state : Aesop.NodeState) (isIrrelevant : Bool) (appliedRule : Aesop.RegularRule)
  (scriptSteps? : Option (Array Aesop.Script.LazyStep)) (originalSubgoals : Array Lean.MVarId)
  (successProbability : Aesop.Percent) (metaState : Lean.Meta.SavedState)
  (introducedMVars assignedMVars : Aesop.UnorderedArraySet Lean.MVarId) (id_1 : Aesop.RappId) (parent_1 : IO.Ref Goal)
  (children_1 : Array (IO.Ref MVarCluster)) (state_1 : Aesop.NodeState) (isIrrelevant_1 : Bool)
  (appliedRule_1 : Aesop.RegularRule) (scriptSteps?_1 : Option (Array Aesop.Script.LazyStep))
  (originalSubgoals_1 : Array Lean.MVarId) (successProbability_1 : Aesop.Percent) (metaState_1 : Lean.Meta.SavedState)
  (introducedMVars_1 assignedMVars_1 : Aesop.UnorderedArraySet Lean.MVarId),
  ({ id := id, parent := parent, children := children, state := state, isIrrelevant := isIrrelevant,
        appliedRule := appliedRule, scriptSteps? := scriptSteps?, originalSubgoals := originalSubgoals,
        successProbability := successProbability, metaState := metaState, introducedMVars := introducedMVars,
        assignedMVars := assignedMVars } =
      { id := id_1, parent := parent_1, children := children_1, state := state_1, isIrrelevant := isIrrelevant_1,
        appliedRule := appliedRule_1, scriptSteps? := scriptSteps?_1, originalSubgoals := originalSubgoals_1,
        successProbability := successProbability_1, metaState := metaState_1, introducedMVars := introducedMVars_1,
        assignedMVars := assignedMVars_1 }) =
    (id = id_1 ∧
      parent = parent_1 ∧
        children = children_1 ∧
          state = state_1 ∧
            isIrrelevant = isIrrelevant_1 ∧
              appliedRule = appliedRule_1 ∧
                scriptSteps? = scriptSteps?_1 ∧
                  originalSubgoals = originalSubgoals_1 ∧
                    successProbability = successProbability_1 ∧
                      metaState = metaState_1 ∧ introducedMVars = introducedMVars_1 ∧ assignedMVars = assignedMVars_1)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- This right homology map data expresses compatibilities of the right homology data
constructed by `RightHomologyData.ofEpiOfIsIsoOfMono'`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h : S₂.RightHomologyData) →
            [inst_2 : CategoryTheory.Epi φ.τ₁] →
              [inst_3 : CategoryTheory.IsIso φ.τ₂] →
                [inst_4 : CategoryTheory.Mono φ.τ₃] →
                  CategoryTheory.ShortComplex.RightHomologyMapData φ
                    (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h) h
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basis.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.basis✝ hs = Module.Basis.mk ⋯ ⋯
-- Batteries.Data.String.Matcher
/-- Make KMP matcher from pattern string  -/
String.Matcher.ofString : String → String.Matcher
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_eq_zero_iff_notMem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.minimalPeriod f x = 0 ↔ x ∉ Function.periodicPts f
-- Mathlib.Analysis.Convex.Cone.Dual
/-- The **double dual of a proper cone** is itself.  -/
ProperCone.dual_dual_flip : ∀ {E : Type u_1} {F : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E]
  [inst_3 : TopologicalSpace F] [inst_4 : AddCommGroup F] [inst_5 : Module ℝ E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] [inst_8 : Module ℝ F] (p : F →ₗ[ℝ] E →ₗ[ℝ] ℝ) [inst_9 : p.IsContPerfPair]
  (C : ProperCone ℝ E), ProperCone.dual p ↑(ProperCone.dual p.flip ↑C) = C
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instFullCoalgebraToComonadAdjComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C),
  (CategoryTheory.Comonad.comparison G.adj).Full
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAsPartialEquiv.eq_1 : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι),
  Z.localTrivAsPartialEquiv i =
    { toFun := fun p => (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd),
      invFun := fun p => ⟨p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2⟩, source := Z.proj ⁻¹' Z.baseSet i,
      target := Z.baseSet i ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
-- Lean.Setup
Lean.instInhabitedIRPhases.default : Lean.IRPhases
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f U)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization f) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map ((AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap f).app (Opposite.op ↑U)))
        (AlgebraicGeometry.IsAffineOpen.fromSpec ⋯))
      h
-- Mathlib.Probability.BrownianMotion.Basic
/-- A pre-Brownian motion has independent increments.  -/
ProbabilityTheory.IsPreBrownianReal.hasIndepIncrements : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ProbabilityTheory.HasIndepIncrements B P
-- Init.Meta.Defs
Lean.Meta.instReprConfig : Repr Lean.Meta.DSimp.Config
-- Lean.Server.CodeActions.Basic
Lean.Server.instToJsonCodeActionResolveData.toJson : Lean.Server.CodeActionResolveData → Lean.Json
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] [IsDomain R],
  M ≤ nonZeroDivisors R → ∀ (p : Polynomial S), IsLocalization.integerNormalization M p = 0 ↔ p = 0
-- Mathlib.Analysis.Normed.Module.RCLike.Real
dist_smul_add_one_sub_smul_le : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ} {x y : E},
  r ∈ Set.Icc 0 1 → dist (r • x + (1 - r) • y) x ≤ dist y x
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_rename_le : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] (f : σ → τ) (p : MvPolynomial σ R),
  ((MvPolynomial.rename f) p).totalDegree ≤ p.totalDegree
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The image of a binary cofan by a functor.  -/
CategoryTheory.Limits.BinaryCofan.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y : C} → CategoryTheory.Limits.BinaryCofan X Y → CategoryTheory.Limits.BinaryCofan (F.obj X) (F.obj Y)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.neg_le_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] {a : α}, 0 ≤ a → -a ≤ a
-- Mathlib.Analysis.Convex.Cone.TensorProduct
/-- If `C₁` is a simplicial and generating cone and `C₂` is a proper cone, then their minimal
and maximal tensor products are equal.  -/
PointedCone.minTensorProduct_eq_max_of_simplicial_generating_left : ∀ {E : Type u_1} {F : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] [FiniteDimensional ℝ F]
  [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (C₁ : PointedCone ℝ E) (C₂ : ProperCone ℝ F),
  C₁.IsSimplicial → Submodule.span ℝ ↑C₁ = ⊤ → C₁.minTensorProduct ↑C₂ = C₁.maxTensorProduct ↑C₂
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
/-- The canonical inclusion from `I ^ a • N ⧸ I ^ b • (I ^ a • N)` to `M ⧸ I ^ c • N`
when `c = b + a`.  -/
Submodule.powSMulQuotInclusion : {R : Type u_3} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {a b c : ℕ} → c = b + a → (N : Submodule R M) → ↥(I ^ a • N) ⧸ I ^ b • ⊤ →ₗ[R] M ⧸ I ^ c • N
-- Mathlib.Algebra.Group.Submonoid.Units
MonoidHom.isUnit_eqLocusM_mk_iff : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (f g : M →* N) {r : M} (hr : f r = g r),
  IsUnit ⟨r, hr⟩ ↔ IsUnit r
-- Init.Data.Format.Basic
Std.Format.instBEqFlattenAllowability : BEq Std.Format.FlattenAllowability
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.reCLM_norm : ‖Complex.reCLM‖ = 1
-- Lean.DocString.Markdown
/-- Renders a custom block element to Markdown. It receives renderers for inline and block content, the
saved `Dynamic` description of the custom element, and the element's fallback content.
 -/
Lean.Doc.BlockMdRenderer : Type
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.E.injEq : ∀ {B : Type v} (a a_1 : B), (CartanMatrix.Generators.E a = CartanMatrix.Generators.E a_1) = (a = a_1)
-- Init.Data.Nat.Basic
Nat.le_sub_of_add_le : ∀ {a b c : ℕ}, a + b ≤ c → a ≤ c - b
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.of_leftInverse : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι] (i : ι),
  Function.LeftInverse ⇑(Monoid.CoprodI.lift (Pi.mulSingle i (MonoidHom.id (M i)))) ⇑Monoid.CoprodI.of
-- Lean.Declaration
Lean.ConstantInfo.levelParams : Lean.ConstantInfo → List Lean.Name
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.ofTypeMonad_obj : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m] (x : Type u),
  (CategoryTheory.ofTypeMonad m).obj x = m x
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.limitCLM.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [inst_8 : IsTopologicalAddGroup V] [inst_9 : ContinuousSMul ℝ V]
  [inst_10 : LocallyConvexSpace ℝ V] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V]
  [inst_14 : IsScalarTower ℝ 𝕜 V] (toFun toFun_1 : TestFunction Ω F n → V) (e_toFun : toFun = toFun_1)
  (T T_1 : (K : TopologicalSpace.Compacts E) → ↑K ⊆ ↑Ω → ContDiffMapSupportedIn E F n K →L[𝕜] V) (e_T : T = T_1)
  (toFun_eq_T :
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : ContDiffMapSupportedIn E F n K),
      toFun (TestFunction.ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f),
  TestFunction.limitCLM 𝕜 toFun T toFun_eq_T = TestFunction.limitCLM 𝕜 toFun_1 T_1 ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Std.PRange.Nat.succ?_eq : ∀ {n : ℕ}, Std.PRange.succ? n = some (n + 1)