mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.PreservesIsConnected.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {D : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X : C} [CategoryTheory.PreGaloisCategory.IsConnected X], CategoryTheory.PreGaloisCategory.IsConnected (F.obj X)) →
    CategoryTheory.PreGaloisCategory.PreservesIsConnected F
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instBEqContentLength : BEq Std.Http.Header.ContentLength
-- Mathlib.Order.RelIso.Basic
RelIso.bijective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), Function.Bijective ⇑e
-- Mathlib.Algebra.Group.Prod
Prod.SubtractionCommMonoid.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : SubtractionCommMonoid G] [inst_1 : SubtractionCommMonoid H],
  Prod.SubtractionCommMonoid = { toSubtractionMonoid := Prod.instSubtractionMonoid, add_comm := ⋯ }
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_eq_aeval_map : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : CommSemiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra T S] {φ : R →+* T},
  (algebraMap T S).comp φ = algebraMap R S →
    ∀ (p : Polynomial R) (a : S), (Polynomial.aeval a) p = (Polynomial.aeval a) (Polynomial.map φ p)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyPrepareParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.Algebra.Order.Quantale
AddQuantale.rightAddResiduation_le_iff_add_le : ∀ {α : Type u_1} {x y z : α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α],
  x ≤ AddQuantale.rightAddResiduation y z ↔ y + x ≤ z
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- Pigeonhole principle for a cardinality below the cardinality of the domain  -/
Cardinal.infinite_pigeonhole_card : ∀ {β α : Type u} (f : β → α),
  ∀ θ ≤ Cardinal.mk β, Cardinal.aleph0 ≤ θ → Cardinal.mk α < θ.ord.cof → ∃ a, θ ≤ Cardinal.mk ↑(f ⁻¹' {a})
-- Lean.Elab.AssertExists
/-- Find the dependency chain, starting at a module that imports `imported`, and ends with the
current module.

The path only contains the intermediate steps: it excludes `imported` and the current module.  -/
Lean.Environment.importPath : Lean.Environment → Lean.Name → Array Lean.Name
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.nontrivial_of_liesOver_of_isPrime : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [P.LiesOver p] [hp : p.IsPrime], Nontrivial (B ⧸ P)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides.  -/
InnerProductGeometry.cos_angle_add_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x‖ / ‖x + y‖
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} (a_1 : a ⟶ b) (x_1 : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda₀ x).map a_1).toFunctor.obj x_1 = CategoryTheory.CategoryStruct.comp a_1.unop x_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option β → Option β} {he : (Std.Internal.List.Const.alterKey k f l).isEmpty = false},
      Std.Internal.List.maxKey (Std.Internal.List.Const.alterKey k f l) he = k ↔
        (f (Std.Internal.List.getValue? k l)).isSome = true ∧
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.one : {J : Type w} → CategoryTheory.Limits.WalkingParallelFamily J
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- For any subobject `x`, the pullback of `h.Ω₀` along the characteristic map of `x`
given by `h.homEquiv` is `x` itself.  -/
CategoryTheory.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {X : C} (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x
-- Mathlib.Control.Functor.Multivariate
/-- given `x : F α` and a projection `i` of type vector `α`, `supp x i` is the set
of `α.i` contained in `x`  -/
MvFunctor.supp : {n : ℕ} → {F : TypeVec.{u} n → Type v} → [MvFunctor F] → {α : TypeVec.{u} n} → F α → (i : Fin2 n) → Set (α i)
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- The space of continuous linear maps equipped with the topology of pointwise convergence,
sometimes also called the *strong operator topology*. We avoid this terminology since so many other
things share similar names, and using "pointwise convergence" in the name is more informative.

This topology is also known as the weak⋆-topology in the case that `σ = RingHom.id 𝕜` and `F = 𝕜`  -/
PointwiseConvergenceCLM : {𝕜₁ : Type u_4} →
  {𝕜₂ : Type u_5} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (𝕜₁ →+* 𝕜₂) →
          (E : Type u_7) →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] → [TopologicalSpace F] → [Module 𝕜₁ E] → [Module 𝕜₂ F] → Type (max u_7 u_8)
-- Mathlib.Logic.Function.Basic
Function.FactorsThrough.comp_right : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : α → γ},
  Function.FactorsThrough g f → ∀ (g' : δ → α), Function.FactorsThrough (g ∘ g') (f ∘ g')
-- Init.Data.Nat.Lemmas
Nat.eq_of_dvd_of_div_eq_one : ∀ {a b : ℕ}, a ∣ b → b / a = 1 → a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.interval.eq_1 : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} (f : X.Path m) (j l : ℕ) (h : j + l ≤ m),
  f.interval j l h =
    { vertex := fun i => f.vertex ⟨j + ↑i, ⋯⟩, arrow := fun i => f.arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.inf_le_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeInf β] [inst_3 : ContinuousInf β] (f g : α →ₘ[μ] β), f ⊓ g ≤ f
-- Mathlib.Geometry.Manifold.Immersion
/-- A `C^n` immersion at `x` is continuous at `x`.  -/
Manifold.IsImmersionAt.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAt I J n f x → ContinuousAt f x
-- Mathlib.Order.Monotone.Monovary
/-- `f` monovaries with `g` on `s` if `g i < g j` implies `f i ≤ f j` for all `i, j ∈ s`.  -/
MonovaryOn : {ι : Type u_1} → {α : Type u_3} → {β : Type u_4} → [Preorder α] → [Preorder β] → (ι → α) → (ι → β) → Set ι → Prop
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_toSpanSingleton : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] (x : M₁),
  ↑(ContinuousLinearMap.toSpanSingleton R₁ x) = LinearMap.toSpanSingleton R₁ M₁ x
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMapTR.go.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : CategoryTheory.Limits.HasZeroObject D]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C] (F : C ⥤ₗ D),
  ((CategoryTheory.AdditiveFunctor.ofLeftExact C D).obj F).obj = F.obj
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- Let `M` be an `(m × n)`-matrix over `R`.
Then `Matrix.toMvPolynomial M` is the family (indexed by `i : m`)
of multivariate polynomials in `n` variables over `R` that evaluates on `c : n → R`
to the dot product of the `i`-th row of `M` with `c`:
`Matrix.toMvPolynomial M i` is the sum of the monomials `C (M i j) * X j`.  -/
Matrix.toMvPolynomial : {m : Type u_1} →
  {n : Type u_2} → {R : Type u_4} → [Fintype n] → [inst : CommSemiring R] → Matrix m n R → m → MvPolynomial n R
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instFiniteIdSearchStepOfStrictBackwardPattern : ∀ {ρ : Type} (pat : ρ) {s : String.Slice} [inst : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.StrictBackwardPattern pat],
  Std.Iterators.Finite (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s) Id
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isConstructible_basicOpen : ∀ {R : Type u} [inst : CommSemiring R] {f : R}, Topology.IsConstructible ↑(PrimeSpectrum.basicOpen f)
-- Mathlib.Topology.Homotopy.HSpaces
Path.delayReflLeft_zero : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Path.delayReflLeft 0 γ = (Path.refl x).trans γ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instInhabitedExpr : Inhabited Nat.Internal.Linear.Expr
-- Init.Data.SInt.Basic
/-- Strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the `<` operator.
 -/
ISize.lt : ISize → ISize → Prop
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.not_forall_eq : ∀ {α : Sort u_1} (s : α → Prop), (¬∀ (x : α), s x) = ∃ x, ¬s x
-- Mathlib.Data.Nat.Digits.Defs
/-- an n-digit number in base b is less than b^n if b > 1  -/
Nat.ofDigits_lt_base_pow_length : ∀ {b : ℕ} {l : List ℕ}, 1 < b → (∀ x ∈ l, x < b) → Nat.ofDigits b l < b ^ l.length
-- Init.Data.SInt.Lemmas
ISize.sub_le : ∀ {a b : ISize}, 0 ≤ b → b ≤ a → a - b ≤ a
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isConj_of_cycleType_eq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  σ.cycleType = τ.cycleType → IsConj σ τ
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ioc_add_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (a : α),
  ⋃ n, Set.Ioc (a + ↑n) (a + ↑n + 1) = Set.univ
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The restriction of a locally ringed space along an open embedding.
 -/
AlgebraicGeometry.LocallyRingedSpace.restrict : {U : TopCat} →
  (X : AlgebraicGeometry.LocallyRingedSpace) →
    {f : U ⟶ X.toTopCat} →
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le_nat : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ProbabilityTheory.iCondIndepSet m' hm' s μ →
      ∀ (n : ℕ),
        ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s (n + 1)})
          (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) hm' μ
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulStrictMono_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  PosMulStrictMono α ↔ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b c : α⦄, b < c → a * b < a * c
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution.IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject.HoCat C))
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.exists_unify_eq : ∀ {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 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [Nonempty ι] {α : Type u_1} [Finite α]
  {x y : α → FirstOrder.Language.Structure.Sigma f},
  x ≈ y →
    ∃ i,
      ∃ (hx : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (Set.range (Sigma.fst ∘ y))),
        FirstOrder.Language.DirectLimit.unify f x i hx = FirstOrder.Language.DirectLimit.unify f y i hy
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.mkHom_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι), (CategoryTheory.Limits.Fork.mkHom k w).hom = k
-- Init.Data.Vector.MapIdx
Vector.mapIdx_set : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Vector α n} {i : ℕ} {h : i < n} {a : α},
  Vector.mapIdx f (xs.set i a h) = (Vector.mapIdx f xs).set i (f i a) h
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonDecls : Lean.FromJson Lean.Lsp.Decls
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C}
  [inst_1 : J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)),
  (E.bind F).toPreZeroHypercover = E.bind fun i => (F i).toPreZeroHypercover
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanModuleQuery.mk : String → Array Lean.Lsp.OpenNamespace → Lean.Lsp.LeanModuleQuery
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKey! k = t₂.getKey! k
-- Mathlib.RingTheory.Localization.Defs
/-- Given a localization map `f : M →* N`, a section function sending `z : N` to some
`(x, y) : M × S` such that `f x * (f y)⁻¹ = z`.  -/
IsLocalization.sec : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → S → R × ↥M
-- Init.Data.Vector.Lemmas
Vector.all_eq_not_any_not : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = !xs.any fun x => !p x
-- Init.Data.List.Sublist
List.infix_append_right : ∀ {α : Type u_1} {l₂ l₁ : List α}, l₂ <:+: l₁ ++ l₂
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι),
        i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) μ
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_two_mul_add_one : ∀ (n : ℕ), Nat.fib (2 * n + 1) = Nat.fib (n + 1) ^ 2 + Nat.fib n ^ 2
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix formed by reindexing via the bijection `e : B ≃ B'`.  -/
CoxeterMatrix.reindex : {B : Type u_1} → {B' : Type u_2} → B ≃ B' → CoxeterMatrix B → CoxeterMatrix B'
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minKey? l = some k ↔
      Std.Internal.List.getKey? k l = some k ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instUniqueSymbols : Unique FirstOrder.Language.order.Symbols
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.transAt.eq_1 : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (f g : ↑(GenLoop N X x)),
  GenLoop.transAt i f g =
    GenLoop.copy (GenLoop.fromLoop i (Path.trans (GenLoop.toLoop i f) (GenLoop.toLoop i g)))
      (fun t =>
        if ↑(t i) ≤ 1 / 2 then f (Function.update t i (Set.projIcc 0 1 GenLoop.transAt._proof_3 (2 * ↑(t i))))
        else g (Function.update t i (Set.projIcc 0 1 GenLoop.transAt._proof_3 (2 * ↑(t i) - 1))))
      ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (toPrelaxFunctorStruct : CategoryTheory.PrelaxFunctorStruct B C)
  (map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam)
  (map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct.map₂ η) (toPrelaxFunctorStruct.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam)
  (toPrelaxFunctorStruct_1 : CategoryTheory.PrelaxFunctorStruct B C)
  (map₂_id_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct_1.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct_1.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam)
  (map₂_comp_1 :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct_1.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct_1.map₂ η) (toPrelaxFunctorStruct_1.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam),
  ({ toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp } =
      { toPrelaxFunctorStruct := toPrelaxFunctorStruct_1, map₂_id := map₂_id_1, map₂_comp := map₂_comp_1 }) =
    (toPrelaxFunctorStruct = toPrelaxFunctorStruct_1)
-- Mathlib.Control.Functor
/-- Extract a term of `F (G α)` from a term of `Comp F G α`, which is the same type.  -/
Functor.Comp.run : {F : Type u → Type w} → {G : Type v → Type u} → {α : Type v} → Functor.Comp F G α → F (G α)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.fg_adjoin_finset : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (t : Finset E),
  (IntermediateField.adjoin F ↑t).FG
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.mk.inj : ∀ {arg type app arg_1 type_1 app_1 : Lean.Expr},
  { arg := arg, type := type, app := app } = { arg := arg_1, type := type_1, app := app_1 } →
    arg = arg_1 ∧ type = type_1 ∧ app = app_1
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries.default : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piFan_pt : ∀ {ι : Type v} (α : ι → TopCat), (TopCat.piFan α).pt = TopCat.of ((i : ι) → ↑(α i))
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Any function from `α` to `β` extends uniquely to an additive group homomorphism
from the additive free group over `α` to the additive free group over `β`.  -/
FreeAddGroup.map : {α : Type u} → {β : Type v} → (α → β) → FreeAddGroup α →+ FreeAddGroup β
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.dropWhile_eq_intermediateDropWhile : ∀ {α β : Type u_1} [Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  Std.Iter.dropWhile P it = Std.Iter.Intermediate.dropWhile P true it
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last.inj : ∀ {hs : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)} {decVars : Array Lean.FVarId}
  {hs_1 : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)} {decVars_1 : Array Lean.FVarId},
  Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last hs decVars =
      Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last hs_1 decVars_1 →
    hs = hs_1 ∧ decVars = decVars_1
-- Mathlib.Analysis.Complex.Spectrum
SpectrumRestricts.real_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℂ A] {a : A},
  SpectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = ↑x.re
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_le_right_iff_le_one : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → ((AffineMap.lineMap a b) r ≤ b ↔ r ≤ 1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.initialBound.eq_1 : ∀ (ε : ℝ) (l : ℕ), SzemerediRegularity.initialBound ε l = max 7 (max l (⌊Real.log (100 / ε ^ 5) / Real.log 4⌋₊ + 1))
-- Init.Data.String.Substring
/-- Returns the character at the given position in the substring.

The position is relative to the substring, rather than the underlying string, and no bounds checking
is performed with respect to the substring's end position. If the relative position is not a valid
position in the underlying string, the fallback value `(default : Char)`, which is `'A'`, is
returned.  Does not panic.
 -/
Substring.Raw.get : Substring.Raw → String.Pos.Raw → Char
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.isIntegral_of_surjective : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → f.IsIntegral
-- Lean.Meta.HaveTelescope
Lean.Meta.instInhabitedHaveInfo.default : Lean.Meta.HaveInfo
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.union : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  e.IsImage s t → e.IsImage s' t' → e.IsImage (s ∪ s') (t ∪ t')
-- Mathlib.Data.List.Sublists
List.sublists'_eq_sublists : ∀ {α : Type u} (l : List α), l.sublists' = List.map List.reverse l.reverse.sublists
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The canonical map `WithLp.equiv` between `WithLp ∞ (α × β)` and `α × β` as a linear isometric
equivalence.  -/
WithLp.prodEquivₗᵢ : {𝕜 : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : SeminormedAddCommGroup α] →
        [inst_1 : SeminormedAddCommGroup β] →
          [inst_2 : SeminormedRing 𝕜] → [inst_3 : Module 𝕜 α] → [inst_4 : Module 𝕜 β] → WithLp ⊤ (α × β) ≃ₗᵢ[𝕜] α × β
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_smul_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t : Set β}, (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t