mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x` and `g = f` on some neighbourhood of `x`,
then `g` is a submersion at `x`.  -/
Manifold.IsSubmersionAtOfComplement.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞}
  {f g : M → N} {x : M},
  Manifold.IsSubmersionAtOfComplement F I J n f x → f =ᶠ[nhds x] g → Manifold.IsSubmersionAtOfComplement F I J n g x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.empty_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering}, ∅.toList = []
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {ΓR : Type u_6}
  {ΓA : Type u_7} [inst_3 : LinearOrderedCommGroupWithZero ΓR] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [inst_5 : vR.HasExtension vA] (r : ↥vR.integer) (a : ↥vA.integer),
  ↑(r • a) = ↑r • ↑a
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.divCoeffs.eq_def : ∀ (k : ℤ) (x : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.divCoeffs k x =
    match x with
    | Int.Internal.Linear.Poly.num k => true
    | Int.Internal.Linear.Poly.add k' v p => k' % k == 0 && Int.Internal.Linear.Poly.divCoeffs k p
-- Mathlib.Algebra.Group.Action.Faithful
/-- `Monoid.toMulAction` is faithful on cancellative monoids.  -/
RightCancelMonoid.faithfulSMul : ∀ {α : Type u_3} [inst : RightCancelMonoid α], FaithfulSMul α α
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
/-- A category `C` is locally presentable if it is `κ`-locally presentable
for some regular cardinal `κ`.  -/
CategoryTheory.IsLocallyPresentable : (C : Type u) → [hC : CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.ext_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R}, S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
-- Std.Http.Data.URI.Basic
/-- Returns a new URI with the query replaced.
 -/
Std.Http.URI.withQuery : Std.Http.URI → Std.Http.URI.Query → Std.Http.URI
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_self_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.rnDeriv (μ + ν) =ᵐ[ν] fun x => μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (g : G),
  (Action.FunctorCategoryEquivalence.inverse.obj F).ρ g = F.map g
-- Mathlib.Data.Int.Fib.Basic
Int.fib_zero : Int.fib 0 = 0
-- Mathlib.Algebra.Ring.Commute
Commute.add_left : ∀ {R : Type u} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) c
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconePrecomposeEquivalenceFunctor.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
Std.IterM.toHashSet_eq_fold : ∀ {α β : Type w} {x : BEq β} {x_1 : Hashable β} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.IteratorLoop α m m] {it : Std.IterM m β}, it.toHashSet = Std.IterM.fold (fun acc a => acc.insert a) ∅ it
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
Filter.Subsingleton.atTop_eq : ∀ (α : Type u_6) [Subsingleton α] [inst : Preorder α], Filter.atTop = ⊤
-- Mathlib.Topology.PartitionOfUnity
/-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
This is the set of `i : ι` such that `x₀ ∈ tsupport f i`.  -/
PartitionOfUnity.fintsupport : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → PartitionOfUnity ι X s → X → Finset ι
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_neg_sub_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.U R (-n - 2) = -Polynomial.Chebyshev.U R n
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
_private.Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex.0.SSet.Subcomplex.Pairing.RankFunction.isPushout_aux₁ : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (s : (SSet.Subcomplex.range (f.m j)).N),
  (f.mapN s).simplex ∈ X.nonDegenerate (f.mapN s).dim
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isRevMatch_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch p pos ↔
    ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Hom.of : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.LaxTrans.Modification η θ → CategoryTheory.Oplax.LaxTrans.Hom η θ
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isReduced_of_isIntegral : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X], AlgebraicGeometry.IsReduced X
-- Mathlib.Order.Atoms
/-- Every element other than `⊥` has an atom below it.  -/
IsAtomic.eq_bot_or_exists_atom_le : ∀ {α : Type u_2} {inst : PartialOrder α} {inst_1 : OrderBot α} [self : IsAtomic α] (b : α),
  b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
-- Mathlib.Data.Set.Sups
Set.image_subset_sups_right : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α} {a : α}, a ∈ s → (fun x1 x2 => x1 ⊔ x2) a '' t ⊆ s ⊻ t
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.fst_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  (a : WithZero (Lex (αˣ × βˣ))),
  (LinearOrderedCommGroupWithZero.fst α β) a =
    (MonoidWithZeroHom.fst α β) ((WithZero.map' ↑(ofLexMulEquiv (αˣ × βˣ))) a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A dependent version of `affineSpan_induction`.  -/
affineSpan_induction' : ∀ {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] {s : Set P} {p : (x : P) → x ∈ affineSpan k s → Prop},
  (∀ (y : P) (hys : y ∈ s), p y ⋯) →
    (∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
        p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯) →
      ∀ {x : P} (h : x ∈ affineSpan k s), p x h
-- Mathlib.Data.Finmap
Finmap.union_empty : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ : Finmap β}, s₁ ∪ ∅ = s₁
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_unitIso_inv_app_toFun : ∀ (X : Bipointed) (a : ((CategoryTheory.Functor.id Bipointed).obj X).X),
  (Bipointed.swapEquiv.unitIso.inv.app X).toFun a = a
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivInvMonoidOfMulOpposite : {M : Type u_1} → [DivInvMonoid Mᵐᵒᵖ] → DivInvMonoid Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- If `toAut F G` is surjective, then `G` acts transitively on the fibers of connected objects.
For a converse see `toAut_surjective`.  -/
CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [inst_4 : CategoryTheory.GaloisCategory C]
  [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.toAut F G) →
    ∀ (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X], MulAction.IsPretransitive G (F.obj X).obj
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.atEnd.sizeOf_spec : ∀ {s : String.Slice}, sizeOf String.Slice.Pattern.ForwardSliceSearcher.atEnd = 1
-- Mathlib.Topology.Closure
closure_subset_iff_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure s ⊆ s ↔ IsClosed s
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The contravariant functor turning monoid objects in the opposite category into comonoid objects.
 -/
CategoryTheory.Comon.MonOpOpToComon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ (CategoryTheory.Comon C)
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquivKer_symm_apply : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H) (a : α) (g : ↥f.ker),
  ↑((f.fiberEquivKer a).symm g) = a * ↑g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Aesop.Tree.Data
Aesop.RappData.appliedRule : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Aesop.RegularRule
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.rotateLeft.injEq : ∀ (n n_1 : ℕ), (Std.Tactic.BVDecide.BVUnOp.rotateLeft n = Std.Tactic.BVDecide.BVUnOp.rotateLeft n_1) = (n = n_1)
-- Init.NotationExtra
/-- Step-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
Lean.calc : Lean.ParserDescr
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.toEmbedding : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Embedding M N → M ↪ N
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearMap_trans : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ)
  (ψ : σ.Equiv τ), ↑(φ.trans ψ).toContinuousLinearEquiv = ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_list_sum_le : ∀ {S : Type u_1} [inst : Semiring S] (l : List (Polynomial S)),
  l.sum.natDegree ≤ List.foldr max 0 (List.map Polynomial.natDegree l)
-- Mathlib.ModelTheory.Definability
Set.definable_biInter_finset : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2}
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → ∀ (s : Finset ι), A.Definable L (⋂ i ∈ s, f i)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- The sum of a locally finite collection of sections is differentiable if each section is.
Version at a point within a set.  -/
MDifferentiableWithinAt.sum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {x₀ : B}
  {ι : Type u_9} {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), MDiffAt[u] (T% t) x₀) → (MDiffAt[u] fun x => ⟨x, ∑' (i : ι), t i x⟩) x₀
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesSummable.LSeriesHasSum : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesHasSum f s (LSeries f s)
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.qify_simps_proc : Lean.ParserDescr
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_zero : Nat.primeFactors 0 = ∅
-- Lean.Parser.Types
Lean.Parser.ParserFn.run : Lean.Parser.ParserFn →
  Lean.Parser.InputContext →
    Lean.Parser.ParserModuleContext → Lean.Parser.TokenTable → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β],
  OrderAddMonoidHom.instFunLike = { coe := fun f => (↑f.toAddMonoidHom).toFun, coe_injective := ⋯ }
-- Lean.SubExpr
Lean.SubExpr.Pos.push : Lean.SubExpr.Pos → ℕ → Lean.SubExpr.Pos
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.unique_irreducible : ∀ {R : Type u_1} [inst : CommRing R],
  IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R →
    ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.exists_of_fiberMk_eq_fiberMk : ∀ {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.IsCofiltered N] {U : N} {X : C} {f₁ f₂ : p.obj U ⟶ X},
  CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk f₁ =
      CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk f₂ →
    ∃ V g, CategoryTheory.CategoryStruct.comp (p.map g) f₁ = CategoryTheory.CategoryStruct.comp (p.map g) f₂
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.smul_fst : ∀ {p : ENNReal} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup α]
  [inst_2 : AddCommGroup β] (x : WithLp p (α × β)) (c : 𝕜) [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β],
  (c • x).fst = c • x.fst
-- Mathlib.Algebra.Polynomial.Eval.Irreducible
/-- A polynomial over an integral domain `R` is irreducible if it is monic and
irreducible after mapping into an integral domain `S`.

A special case of this lemma is that a polynomial over `ℤ` is irreducible if
it is monic and irreducible over `ℤ/pℤ` for some prime `p`.
 -/
Polynomial.Monic.irreducible_of_irreducible_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [IsDomain R] [inst_2 : CommRing S] [IsDomain S] (φ : R →+* S)
  (f : Polynomial R), f.Monic → Irreducible (Polynomial.map φ f) → Irreducible f
-- Qq.Macro
Qq.Impl.quoteLevel : Lean.Level → Qq.Impl.QuoteM Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.mk.injEq : ∀ (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof) (p_1 : Int.Internal.Linear.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof),
  ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_cons : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β}
  {hb : b ∉ s}, (Finset.cons b s hb).inf' ⋯ f = f b ⊓ s.inf' H f
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_pow : ∀ {R : Type u} {M : Type v} [inst : CommMonoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M] (x : TrivSqZeroExt R M) (n : ℕ),
  (x ^ n).snd = n • x.fst ^ n.pred • x.snd
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f ↔ IsLocalDiffeomorphOn I J n f Set.univ
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flip_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F),
  (f.flip y) x = (f x) y
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.right_eq_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y),
  f.right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.NumberTheory.SumPrimeReciprocals
_private.Mathlib.NumberTheory.SumPrimeReciprocals.0.ite_prime_eq_indicator : ∀ {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ → M),
  (fun n => if Nat.Prime n then f n else 0) = {n | Nat.Prime n}.indicator f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.foldlM_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  t₁.Equiv t₂ → Std.TreeMap.foldlM f init t₁ = Std.TreeMap.foldlM f init t₂
-- Lean.Message
Lean.MessageSeverity.warning.sizeOf_spec : sizeOf Lean.MessageSeverity.warning = 1
-- Init.Data.Order.Ord
Array.instReflCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp], Std.ReflCmp (Array.compareLex cmp)
-- Init.Data.Array.Lemmas
Array.extract_empty_of_stop_le_start : ∀ {α : Type u_1} {xs : Array α} {start stop : ℕ}, stop ≤ start → xs.extract start stop = #[]
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)),
  f.lift hg =
    { toFun := fun z => g (f.sec z).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.GroupTheory.Congruence.Defs
Con.conGen_sSup : ∀ {M : Type u_1} [inst : Mul M] (rs : Set (M → M → Prop)), conGen (sSup rs) = ⨆ r ∈ rs, conGen r
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (X : C),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso hj F X = CategoryTheory.eqToIso ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_π_apply : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b)
  (b : β) {F : C → C → Type uF} {carrier : C → Type w_1}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier (∏ᶜ f)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map p)) x) =
    (CategoryTheory.ConcreteCategory.hom (p b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
-- Mathlib.Data.Fin.VecNotation
/-- `vecAlt1 v` gives a vector with half the length of `v`, with
only alternate elements (odd-numbered).  -/
Matrix.vecAlt1 : {α : Type u} → {m n : ℕ} → m = n + n → (Fin m → α) → Fin n → α
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.counit_comul : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.counit t) =
    (CategoryTheory.Bicategory.leftUnitor t).inv
-- Mathlib.Data.Part
Part.le_total_of_le_of_le : ∀ {α : Type u_1} {x y : Part α} (z : Part α), x ≤ z → y ≤ z → x ≤ y ∨ y ≤ x
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_eq_self_of_ae_mem : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃μ : MeasureTheory.Measure α⦄,
  (∀ᵐ (x : α) ∂μ, x ∈ s) → μ.restrict s = μ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- A function `f` is `MemHolder r f` if it is Hölder continuous. Namely, `f` has a finite
`r`-Hölder constant. This is equivalent to `f` having finite Hölder norm.
c.f. `memHolder_iff`.  -/
MemHolder : {X : Type u_1} → {Y : Type u_2} → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → NNReal → (X → Y) → Prop
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_map_hom_apply_down : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y)
  (x : ULift.{w, v} (((CategoryTheory.sheafToPresheaf J (Type v)).obj (J.yoneda.obj X)).obj X_1)),
  ((CategoryTheory.ConcreteCategory.hom
          (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).obj X).obj.map f))
        x).down =
    CategoryTheory.CategoryStruct.comp f.unop x.down