mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_symm_apply : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') (p : X' × Y'),
  ↑(eX.prod eY).symm p = (↑eX.symm p.1, ↑eY.symm p.2)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_C_mul_X_pow : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : T},
  a ≠ 0 → ∀ (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).aroots S = n • {0}
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.inverseFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : C ≌ D} (f : X ⟶ Y),
  (CategoryTheory.Equivalence.inverseFunctor C D).map f =
    ((CategoryTheory.conjugateEquiv Y.toAdjunction X.toAdjunction) (CategoryTheory.Equivalence.asNatTrans f)).op
-- Mathlib.Logic.OpClass
/-- A right-commutative operation satisfies `op (op b a₁) a₂ = op (op b a₂) a₁`.  -/
RightCommutative.right_comm : ∀ {α : Sort u} {β : Sort v} {op : β → α → β} [self : RightCommutative op] (b : β) (a₁ a₂ : α),
  op (op b a₁) a₂ = op (op b a₂) a₁
-- Lean.Expr
Lean.instDecidableLtLiteral : (a b : Lean.Literal) → Decidable (a < b)
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.mk.sizeOf_spec : ∀ (declName : Lean.Name) (levelParams : List Lean.Name) (type value : Lean.Expr) (recArgPos : ℕ)
  (declNames : Array Lean.Name) (fixedParamPerms : Lean.Elab.FixedParamPerms),
  sizeOf
      { declName := declName, levelParams := levelParams, type := type, value := value, recArgPos := recArgPos,
        declNames := declNames, fixedParamPerms := fixedParamPerms } =
    1 + sizeOf declName + sizeOf levelParams + sizeOf type + sizeOf value + sizeOf recArgPos + sizeOf declNames +
      sizeOf fixedParamPerms
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.not_all_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)), ¬φ.all.IsQF
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleMapHomologicalComplex.eq_1 : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] [inst_4 : CategoryTheory.Limits.HasZeroObject W₁]
  [inst_5 : CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_6 : F.PreservesZeroMorphisms] (c : ComplexShape ι) [inst_7 : DecidableEq ι] (j : ι),
  HomologicalComplex.singleMapHomologicalComplex F c j =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        { hom := { f := fun i => if h : i = j then CategoryTheory.eqToHom ⋯ else 0, comm' := ⋯ },
          inv := { f := fun i => if h : i = j then CategoryTheory.eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ })
      ⋯
-- Std.Tactic.BVDecide.Syntax
/-- Set SAT solver options to improve counterexample search.
 -/
Lean.Elab.Tactic.BVDecide.SolverMode.counterexample : Lean.Elab.Tactic.BVDecide.SolverMode
-- Mathlib.Analysis.Real.Pi.Bounds
/-- From an upper bound on `sqrtTwoAddSeries 0 n = 2 cos (π / 2 ^ (n+1))` of the form
`sqrtTwoAddSeries 0 n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2)`, one can deduce the lower bound `a < π`
thanks to basic trigonometric inequalities as expressed in `pi_gt_sqrtTwoAddSeries`.  -/
Real.pi_lower_bound_start : ∀ (n : ℕ) {a : ℝ}, (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2 → a < Real.pi
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The constant functor `C ⥤ (D ⥤ C)` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_const : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v, max u' v, u, max (max (max u u') v) v'}
    (CategoryTheory.Functor.const D)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitAddMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitAddMonoid F =
    { add := Add.add, add_assoc := ⋯, zero := Zero.zero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.eqOfHomEq_inv_app : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g')
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg).inv.app X_1 =
    (CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) X_1).inv
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.dual_iff : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  t.Bounded o₁ o₂ ↔ t.dual.Bounded o₂ o₁
-- Mathlib.Order.Minimal
maximal_mem_image_monotone : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) → Maximal (fun x => x ∈ s) x → Maximal (fun x => x ∈ f '' s) (f x)
-- Mathlib.Data.Matrix.Mul
/-- `v ᵥ* M` (notation for `vecMul v M`) is the vector-matrix product of vector `v` and matrix `M`,
where `v` is seen as a row vector.

The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `dotProduct`,
so that `v ᵥ* A ⬝ᵥ w ᵥ* B` is parsed as `(v ᵥ* A) ⬝ᵥ (w ᵥ* B)`.
 -/
Matrix.«term_ᵥ*_» : Lean.TrailingParserDescr
-- Mathlib.Topology.NhdsWithin
nhdsWithin_insert : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s : Set α), nhdsWithin a (insert a s) = pure a ⊔ nhdsWithin a s
-- Mathlib.Tactic.Trace
/-- `trace msg` displays `msg` in the info view. 

Extensions:

 * `msg` can be a literal string, or a term that evaluates to a string. -/
Lean.Parser.Tactic.trace : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- When `freeDFinsuppEquiv` is applied to a map with a single value of one the resulting multilinear
map sends inputs to a single value in the codomain, taking a product over images from each
component of the domain.
 -/
MultilinearMap.freeDFinsuppEquiv_single : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : (i : ι) → Fintype (κ i)] [inst_4 : (i : ι) → DecidableEq (κ i)]
  [inst_5 : DecidableEq ι'] (p : ((i : ι) → κ i) × ι') (r : R) (x : (i : ι) → Π₀ (x : κ i), R),
  (MultilinearMap.freeDFinsuppEquiv fun₀ | p => r) x = r • fun₀ | p.2 => ∏ i, (x i) (p.1 i)
-- Init.Control.Reader
/-- Fails with a recoverable error.
 -/
ReaderT.failure : {m : Type u_1 → Type u_2} → {ρ α : Type u_1} → [Alternative m] → ReaderT ρ m α
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.mem_centralizer_iff_commutator_eq_one : ∀ {G : Type u_1} [inst : Group G] {g : G} {s : Set G}, g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, ⁅h, g⁆ = 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceAddNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Algebra.Module.Basic
/-- The (topological-space) closure of a submodule of a topological `R`-module `M` is itself
a submodule.  -/
Submodule.topologicalClosure : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] → [ContinuousConstSMul R M] → [ContinuousAdd M] → Submodule R M → Submodule R M
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- A relation of `S.pullback f` gives rise to a relation of `S`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {f : Y ⟶ X} → {S : J.Cover X} → {I₁ I₂ : (S.pullback f).Arrow} → I₁.Relation I₂ → I₁.base.Relation I₂.base
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_ext_iff : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] [Finite ι] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M},
  f = g ↔ ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [inst_4 : DistribMulAction 𝕜 E] {s : Set E},
  Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 (-s)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableNeg` if `x ↦ -x` is a measurable function.  -/
MeasurableNeg : (G : Type u_2) → [Neg G] → [MeasurableSpace G] → Prop
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.memAddSubgroup : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddGroup Y]
  (D : Function.locallyFinsuppWithin U Y), ⇑D ∈ Function.locallyFinsuppWithin.addSubgroup U
-- Mathlib.Probability.Density
/-- A random variable that `HasPDF` is quasi-measure-preserving.  -/
MeasureTheory.HasPDF.quasiMeasurePreserving_of_measurable : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E) [MeasureTheory.HasPDF X ℙ μ],
  Measurable X → MeasureTheory.Measure.QuasiMeasurePreserving X ℙ μ
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.inv : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {f : α → 𝕜} {g : α → 𝕜'}, f =Θ[l] g → (fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker_zero : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N], AddMonoidHom.mker 0 = ⊤
-- ProofWidgets.Data.Html
/-- A plain text literal for JSX (notation for `Html.text`).  -/
ProofWidgets.Jsx.jsxText : Lean.Parser.Parser
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.hasStrictDerivAt_rpow_const : ∀ {x p : ℝ}, x ≠ 0 ∨ 1 ≤ p → HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι ⊕ ι'),
  (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey? k = m₁.getKey? k
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The subspace of vectors orthogonal to a given subspace, denoted `Kᗮ`.  -/
Submodule.orthogonal : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → Submodule 𝕜 E → Submodule 𝕜 E
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.addUnits.eq_1 : ∀ {ι : Type u_1} {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : AddMonoid N] [inst_2 : ContinuousAdd N]
  [inst_3 : T2Space N] {f : ι → AddUnits N} {r₁ r₂ : N} {l : Filter ι} [inst_4 : l.NeBot]
  (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂)),
  h₁.addUnits h₂ = { val := r₁, neg := r₂, val_neg := ⋯, neg_val := ⋯ }
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {a : 𝕜},
  RCLike.im RCLike.I = 1 → ((RCLike.map 𝕜 ℂ) a).sqrt = (RCLike.map 𝕜 ℂ) (RCLike.sqrt a)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C) {Z : C} (h : Ψ.r.obj (Φ.quotient.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom).app X)
      (CategoryTheory.CategoryStruct.comp ((Φ.colonπ Ψ).app X) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_neg' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜], deriv Neg.neg = fun x => -1
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.instInhabitedDirectLimitOfDefault : {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 : DirectedSystem G fun i j h => ⇑(f i j h)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : Inhabited ι] → [Inhabited (G default)] → Inhabited (FirstOrder.Language.DirectLimit G f)
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearMap.fixedSubmodule.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (f : V →ₗ[R] V),
  f.fixedSubmodule = { carrier := {x | f x = x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a commutative monoid, if it admits a surjective map that
preserves `1` and `*` from a commutative monoid. See note [reducible non-instances].  -/
Function.Surjective.commMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : One M₂] →
        [inst_2 : Pow M₂ ℕ] →
          [inst_3 : CommMonoid M₁] →
            (f : M₁ → M₂) →
              Function.Surjective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CommMonoid M₂
-- Mathlib.Order.UpperLower.Closure
/-- **Alias** of the reverse direction of `bddAbove_lowerClosure`. -/
BddAbove.lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove s → BddAbove ↑(lowerClosure s)
-- Mathlib.RingTheory.HahnSeries.Summable
/-- The coefficient function of a summable family, as a finsupp on the parameter type.  -/
HahnSeries.SummableFamily.coeff : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → HahnSeries.SummableFamily Γ R α → Γ → α →₀ R
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
MulAction.IsPretransitive.of_embedding_congr : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5},
  Function.Surjective σ →
    Function.Bijective ⇑f → (MulAction.IsPretransitive G (n ↪ α) ↔ MulAction.IsPretransitive H (n ↪ β))
-- Mathlib.SetTheory.ZFC.Ordinal
/-- **Alias** of the forward direction of `ZFSet.isTransitive_iff_subset_powerset`. -/
ZFSet.IsTransitive.subset_powerset : ∀ {x : ZFSet.{u}}, x.IsTransitive → x ⊆ x.powerset
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the uniform
structures of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same
uniform structure on `ι`.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.

Consider using `EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi'` and
`EquicontinuousOn.inducing_uniformOnFun_iff_pi'` instead to avoid rewriting instances,
as well as their unprimed versions in case `𝔖` covers `X`.  -/
EquicontinuousOn.comap_uniformOnFun_eq : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    (∀ K ∈ 𝔖, EquicontinuousOn F K) →
      UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
        UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i => α)
-- Init.Data.Bool
Bool.cond_decide : ∀ {α : Sort u_1} (p : Prop) [inst : Decidable p] (t e : α), (bif decide p then t else e) = if p then t else e
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorph_apply_ker : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (y : ↥(↑f').ker),
  ↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorph f f' hf hf') (↑y + a) = (f (↑y + a), y)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_intCast : ∀ {R : Type u_1} {a b : R} [inst : AddCommGroupWithOne R] (n : ℤ), (↑n).re = ↑n
-- Mathlib.Order.Lattice
inf_lt_of_left_lt : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a < c → a ⊓ b < c
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_left_inv : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M},
  x ∈ f.source → ↑(f.extend I).symm (↑(f.extend I) x) = x
-- Mathlib.Algebra.Group.Ideal
/-- The additive semigroup ideal generated by `s` is `s ∪ Set.univ + s`.  -/
AddSemigroupIdeal.mem_closure' : ∀ {M : Type u_1} [inst : AddSemigroup M] {s : Set M} {x : M},
  x ∈ AddSemigroupIdeal.closure s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y + z = x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_eq_charFunDual_toDualMap : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} (t : E),
  MeasureTheory.charFun μ t = MeasureTheory.charFunDual μ ((InnerProductSpace.toDualMap ℝ E) t)
-- Lean.Parser.Do
Lean.Parser.Term.leftArrow.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Function.Basic
/-- Recursors can be pushed inside `Function.update`.

The `ctor` argument should be a one-argument constructor like `Sum.inl`,
and `recursor` should be an inductive recursor partially applied in all but that constructor,
such as `(Sum.rec · g)`.

In future, we should build some automation to generate applications like `Option.rec_update` for all
inductive types.  -/
Function.rec_update : ∀ {ι : Sort u_1} {κ : Sort u_2} {α : κ → Sort u_3} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] {ctor : ι → κ},
  Function.Injective ctor →
    ∀ (recursor : ((i : ι) → α (ctor i)) → (i : κ) → α i),
      (∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i) →
        (∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i ≠ k) → recursor f₁ k = recursor f₂ k) →
          ∀ (f : (i : ι) → α (ctor i)) (i : ι) (x : α (ctor i)),
            recursor (Function.update f i x) = Function.update (recursor f) (ctor i) x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instIsScalarTower_1 : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], IsScalarTower (CentroidHom α) α α
-- ProofWidgets.Cancellable
ProofWidgets.instRpcEncodableCheckRequestResponse : Lean.Server.RpcEncodable ProofWidgets.CheckRequestResponse
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.deg_pos : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) [Nontrivial S], 0 < f.natDegree
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.BicartesianSq.of_isPullback_isPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z},
  CategoryTheory.IsPullback f g h i → CategoryTheory.IsPushout f g h i → CategoryTheory.BicartesianSq f g h i
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.set_support_symm_eq : ∀ {α : Type u_1} (p : Equiv.Perm α), {x | (Equiv.symm p) x ≠ x} = {x | p x ≠ x}
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β) (k : α)
  (h : (l.getKey?ₘ k).isSome = true), l.getKeyₘ k h = (l.getKey?ₘ k).get h
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply : ∀ {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] (e : Bundle.Trivialization F proj) (p : ↑e.baseSet × F),
  e.sourceHomeomorphBaseSetProd.symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.sub : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.instCategoryUnder : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Under X)
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (x : α),
  ((Finsupp.sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x
-- Mathlib.Control.Functor
Functor.Comp.run_pure : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] {α : Type v} (x : α),
  (pure x).run = pure (pure x)
-- Mathlib.Order.Minimal
OrderEmbedding.minimal_apply_mem_iff : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {f : α ↪o β} {t : Set β},
  t ⊆ Set.range ⇑f → (Minimal (fun x => x ∈ t) (f x) ↔ Minimal (fun x => f x ∈ t) x)
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
CategoryTheory.Precoverage.Generates.isSheaf_of_forall_max : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C},
  K.Generates J →
    ∀ (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))),
      (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) → CategoryTheory.Presieve.IsSheaf J F
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.CC'₁.congr_simp : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
  (a a_1 : ↑(Profinite.NobelingProof.C' C ho)),
  a = a_1 → Profinite.NobelingProof.CC'₁ C hsC ho a = Profinite.NobelingProof.CC'₁ C hsC ho a_1
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.splitOnPTR p l = List.splitOnPTR.go✝ p l #[] #[]
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_le_of_le_left : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, H ≤ K → H.relIndex L ≠ 0 → K.relIndex L ≤ H.relIndex L