mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
/-- When a `d`-dimensional simplex `x` is a `1`-codimensional face of `y`, this is
the only `i : Fin (d + 2)`, such that `X.δ i y = x` (with an abuse of notation:
see `δ_index` and `δ_eq_iff` for well typed statements).  -/
SSet.S.IsUniquelyCodimOneFace.index : {X : SSet} → {x y : X.S} → x.IsUniquelyCodimOneFace y → {d : ℕ} → x.dim = d → Fin (d + 2)
-- Mathlib.Algebra.GroupWithZero.Basic
zpow_sub_one₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (n : ℤ), a ^ (n - 1) = a ^ n * a⁻¹
-- Std.Internal.Do.PredTrans
/-- `MonadStateOf` instance: `get` returns the state, `set` replaces it,
`modifyGet` applies a function to the state.  -/
Std.Internal.Do.instMonadStateOfPredTransForall : {σ : Type u} → {Pred : Type v} → {EPred : Type w} → MonadStateOf σ (Std.Internal.Do.PredTrans (σ → Pred) EPred)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Returns the list of elements of `mat` in the form `(i, j, mat[i, j])`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.getValues : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → α n m → List (ℕ × ℕ × ℚ)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.sup : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l₁ l₂ : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l₁] g → f =o[𝕜; l₂] g → f =o[𝕜; l₁ ⊔ l₂] g
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonadLiftIO : MonadLift IO Std.Async.ContextAsync
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_symm_apply : ∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (a : MulAction.orbitRel.Quotient G (J.obj (CategoryTheory.SingleObj.star G))),
  (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J).symm a =
    (CategoryTheory.Limits.Types.colimitEquivColimitType J).symm
      (Quot.lift (fun x => Quot.mk J.ColimitTypeRel ⟨CategoryTheory.SingleObj.star G, x⟩) ⋯ a)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.le_outerMeasure_compacts : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (K : TopologicalSpace.Compacts G),
  μ K ≤ μ.outerMeasure ↑K
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- Taking inverses in the colimit. See also `colimitInvAux`.  -/
GrpCat.FilteredColimits.colimitInv : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J GrpCat) → Inv ↑(GrpCat.FilteredColimits.G F)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.card_colorClasses_le : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) [inst : Fintype α]
  [inst_1 : Fintype ↑C.colorClasses], Fintype.card ↑C.colorClasses ≤ Fintype.card α
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_apply_ιMulti : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
  (ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ιMulti R n) v) = (f n) v
-- Mathlib.Algebra.Ring.Nat
Nat.instCommSemiring : CommSemiring ℕ
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamily_add : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)]
  (f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.piFamily (f + g) = MultilinearMap.piFamily f + MultilinearMap.piFamily g
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_equiv_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f1 f2 g1 g2 : CauSeq β abv},
  f1 ≈ f2 → g1 ≈ g2 → f1 * g1 ≈ f2 * g2
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_differentiableOn_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G},
  DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.mk.inj : ∀ {toGlueData : CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace}
  {f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (toGlueData.f i j)}
  {toGlueData_1 : CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace}
  {f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (toGlueData_1.f i j)},
  { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 } →
    toGlueData = toGlueData_1
-- Std.Http.Data.URI.Basic
_private.Std.Http.Data.URI.Basic.0.Std.Http.URI.Path.normalize.loop : List Std.Http.URI.EncodedSegment → List Std.Http.URI.EncodedSegment → List Std.Http.URI.EncodedSegment
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.filter_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool}, Std.ExtHashSet.filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = false
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.SemiCartesianMonoidalCategory.toUnit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C]
  (X : C),
  CategoryTheory.SemiCartesianMonoidalCategory.toUnit X =
    CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from X
-- Lean.SubExpr
Lean.SubExpr.instFromJsonMVarId : Lean.FromJson Lean.MVarId
-- Mathlib.Logic.Relator
Relator.LeftUnique.flip : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Relator.LeftUnique r → Relator.RightUnique (flip r)
-- Mathlib.LinearAlgebra.Prod
LinearMap.coe_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], ⇑(LinearMap.inr R M M₂) = Prod.mk 0
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.δ_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.δ_comp._auto_1) {Z : C}
      (h_1 : (DerivedCategory.homologyFunctor C n₁).obj T.obj₂ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ T n₀ n₁ h)
          (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n₁).map T.mor₁) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c).contains a = false
-- Mathlib.Data.Set.Lattice
Set.iUnion_sdiff : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), (⋃ i, t i) \ s = ⋃ i, t i \ s
-- Mathlib.Tactic.Attr.Register
/-- The simpset `push_end` translates the standard formulations of endomorphisms to the
algebraic formulation, so for example `Equiv.refl α` becomes `1 : Equiv α α` and
`b.trans a` becomes `a * b`.

The dual simpset is `pull_end`.
 -/
Parser.Attr.push_end : Lean.ParserDescr
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkPullbackInv : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (V : TopologicalSpace.Opens ↑X) (hV : x ∈ V),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ V x hV)
      (TopCat.Presheaf.stalkPullbackInv C f F x) =
    TopCat.Presheaf.germToPullbackStalk C f F V x hV
-- Mathlib.Data.Prod.Lex
Prod.Lex.le_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LE β] {x y : Lex (α × β)},
  x ≤ y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 ≤ (ofLex y).2
-- Mathlib.CategoryTheory.Quotient
/-- A functor induces a `HomRel` on its domain, relating those maps that have the same image.  -/
CategoryTheory.Functor.homRel : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → HomRel C
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsLeftAdjointTopCatToTopCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)], GeneratedByTopCat.toTopCat.IsLeftAdjoint
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.infinite_iff_in_eventualRange : ∀ {V : Type u} (G : SimpleGraph V) {K : (Finset V)ᵒᵖ} (C : G.componentComplFunctor.obj K),
  (SimpleGraph.ComponentCompl.supp C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K
-- Mathlib.Algebra.Polynomial.Mirror
/-- mirror of a polynomial: reverses the coefficients while preserving `Polynomial.natDegree`  -/
Polynomial.mirror : {R : Type u_1} → [inst : Semiring R] → Polynomial R → Polynomial R
-- Mathlib.Topology.Specialization
/-- An Alexandrov-discrete space is isomorphic to the upper set topology of its specialisation
order.  -/
homeoWithUpperSetTopologyorderIso : (α : Type u_1) → [inst : TopologicalSpace α] → [AlexandrovDiscrete α] → α ≃ₜ Topology.WithUpperSet (Specialization α)
-- Mathlib.Topology.Constructions
pi_generateFrom_eq : ∀ {ι : Type u_5} {A : ι → Type u_9} {g : (a : ι) → Set (Set (A a))},
  Pi.topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_eq_false_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ¬t = ∅
-- Lean.Elab.MutualInductive
/-- For handler use. The `inductive` uses it for the binders to the constructor.  -/
Lean.Elab.Command.CtorView.binders : Lean.Elab.Command.CtorView → Lean.Syntax
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Internal.ofToSliceWithProof.eq_1 : ∀ {s : String} (p : s.toSlice.Pos) (h : p ≠ s.toSlice.endPos),
  String.Internal.ofToSliceWithProof ⟨p, h⟩ = ⟨String.Pos.ofToSlice p, ⋯⟩
-- Mathlib.Topology.Bornology.Basic
Bornology.cobounded_eq_bot : ∀ (α : Type u_2) [inst : Bornology α] [BoundedSpace α], Bornology.cobounded α = ⊥
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- To show that `F` preserves the limit of `K`, we may assume that `K` has a limit.  -/
CategoryTheory.Limits.PreservesLimit.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D},
  (CategoryTheory.Limits.HasLimit K → CategoryTheory.Limits.PreservesLimit K F) →
    CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_singleton : ∀ {α : Type u_2} [inst : Sub α] {s : Set α} {b : α}, s - {b} = (fun x => x - b) '' s
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- A point lying on two internal angle bisectors is the incenter.  -/
Affine.Triangle.eq_incenter_of_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {p : P},
          EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p =
              EuclideanGeometry.oangle p (t.points i₁) (t.points i₃) →
            EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p =
                EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) →
              p = Affine.Simplex.incenter t
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instLTAbs : {α : Type u_1} → [inst : Field α] → [inst_1 : LinearOrder α] → [inst_2 : IsStrictOrderedRing α] → LT (CauSeq α abs)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.toLinearMap_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F),
  (LinearIsometry.rTensor G f).toLinearMap = LinearMap.rTensor G f.toLinearMap
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.cocone_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F],
  (CategoryTheory.Limits.colimit.cocone F).ι.app = CategoryTheory.Limits.colimit.ι F
-- Mathlib.Algebra.Lie.Weights.RootSystem
RootPairing.CorootForm.eq_1 : ∀ {ι : 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) [inst_5 : Fintype ι],
  P.CorootForm = P.flip.RootForm
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.congr_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.obj A).obj x = A.X
-- Mathlib.Data.Seq.Computation
Computation.terminates_of_liftRel : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Computation α} {t : Computation β},
  Computation.LiftRel R s t → (s.Terminates ↔ t.Terminates)
-- Aesop.Tree.Data
Aesop.Rapp.introducesMVar : Aesop.Rapp → Bool
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.mk.inj : ∀ {eAssignment : Array (Option Lean.Expr)} {uAssignment : Array (Option Lean.Level)}
  {ePending : Array (Lean.Expr × Lean.Expr)} {uPending : Array (Lean.Level × Lean.Level)}
  {iPending : Array (Lean.Expr × Lean.Expr)} {tPending : Array ℕ} {us : List Lean.Level} {args : Array Lean.Expr}
  {eAssignment_1 : Array (Option Lean.Expr)} {uAssignment_1 : Array (Option Lean.Level)}
  {ePending_1 : Array (Lean.Expr × Lean.Expr)} {uPending_1 : Array (Lean.Level × Lean.Level)}
  {iPending_1 : Array (Lean.Expr × Lean.Expr)} {tPending_1 : Array ℕ} {us_1 : List Lean.Level}
  {args_1 : Array Lean.Expr},
  { eAssignment := eAssignment, uAssignment := uAssignment, ePending := ePending, uPending := uPending,
        iPending := iPending, tPending := tPending, us := us, args := args } =
      { eAssignment := eAssignment_1, uAssignment := uAssignment_1, ePending := ePending_1, uPending := uPending_1,
        iPending := iPending_1, tPending := tPending_1, us := us_1, args := args_1 } →
    eAssignment = eAssignment_1 ∧
      uAssignment = uAssignment_1 ∧
        ePending = ePending_1 ∧
          uPending = uPending_1 ∧ iPending = iPending_1 ∧ tPending = tPending_1 ∧ us = us_1 ∧ args = args_1
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.instMonadGetStructOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.Meta.Grind.AC.MonadGetStruct m] → Lean.Meta.Grind.AC.MonadGetStruct n
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection_apply_of_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P) {x : P},
  x ∈ s → (EuclideanGeometry.reflection s) p = s.direction.reflection (p -ᵥ x) +ᵥ x
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection from a fiber bundle with a nonempty fiber to its base is a quotient
map.  -/
FiberBundle.isQuotientMap_proj : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [Nonempty F], Topology.IsQuotientMap Bundle.TotalSpace.proj
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.δ.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (e_x : x = x_1) {d : ℕ} {hd : x.dim = d + 1} {l l_1 : Fin (d + 1)} (e_l : l = l_1)
  (hl : SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ), hl.δ = ⋯.δ
-- Mathlib.Order.Filter.AtTopBot.Monoid
/-- If `f` is eventually bounded from above along `l` and `f + g` tends to `+∞`,
then `g` tends to `+∞`.  -/
Filter.Tendsto.atTop_of_isBoundedUnder_le_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f →
    Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_neg : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (x : QuadraticAlgebra R a b),
  QuadraticAlgebra.norm (-x) = QuadraticAlgebra.norm x
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDifferentiableAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x : E},
  LineDifferentiableAt 𝕜 f x 0
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_of_vle_of_veq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x ≤ᵥ y → y =ᵥ z → x ≤ᵥ z
-- Init.Prelude
Char.val_eq_of_eq : ∀ {c d : Char}, c = d → c.val = d.val
-- Mathlib.GroupTheory.GroupAction.Basic
Multiplicative.mulAction_orbit : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β] (b : β), MulAction.orbit (Multiplicative α) b = AddAction.orbit α b
-- Std.Data.DTreeMap.Basic
/-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.DTreeMap.keyAtIdx? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ℕ → Option α
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T.eq_4 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.T R (Int.negSucc n) =
    2 * Polynomial.X * Polynomial.Chebyshev.T R (-↑n) - Polynomial.Chebyshev.T R (-↑n + 1)
-- Mathlib.Data.Num.Lemmas
PosNum.lt_iff_cmp : ∀ {m n : PosNum}, m < n ↔ m.cmp n = Ordering.lt
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeUnop_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop),
  (CategoryTheory.Limits.coconeOfConeUnop c).pt = Opposite.op c.pt
-- Mathlib.RingTheory.Spectrum.Prime.Topology
RingHom.IsIntegral.comap_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsIntegral → Function.Injective ⇑f → Function.Surjective (PrimeSpectrum.comap f)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mk.injEq : ∀ (toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace)
  (local_affine :
    ∀ (x : ↑toLocallyRingedSpace.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))
  (toLocallyRingedSpace_1 : AlgebraicGeometry.LocallyRingedSpace)
  (local_affine_1 :
    ∀ (x : ↑toLocallyRingedSpace_1.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace_1.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))),
  ({ toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } =
      { toLocallyRingedSpace := toLocallyRingedSpace_1, local_affine := local_affine_1 }) =
    (toLocallyRingedSpace = toLocallyRingedSpace_1)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_sub_div_right : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), z ≠ 0 → z ∣ y → (x * z - y) / z = x - y / z
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsNegApply : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsNegApply (SchwartzMap E F) E F
-- Init.Data.String.OrderInstances
String.Slice.Pos.instLinearOrderPackage : {s : String.Slice} → Std.LinearOrderPackage s.Pos
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : { S // A ≤ S }),
  ↑((RelIso.symm A.primeSpectrumOrderEquiv) a).asIdeal = ⇑(A.inclusion ↑a ⋯) ⁻¹' ↑(IsLocalRing.maximalIdeal ↥↑a)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_coeFn_one : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [inst_1 : ∀ (i : I), NormOneClass (B i)], ↑1 = 1
-- Init.Data.List.Control
/-- Returns the first non-`none` result of applying the monadic function `f` to each element of the
list, in order. Returns `none` if `f` returns `none` for all elements.

`O(|l|)`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
List.findSomeM? : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (Option β)) → List α → m (Option β)