mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂Obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁) {X₂ Y₂ : C₂} (φ : X₂ ⟶ Y₂) (X₃ : C₃),
  ((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).map φ).app X₃ = (G.map ((F₁₂.obj X₁).map φ)).app X₃
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.parallelPairHom.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y')
  (p p_1 : X ⟶ X') (e_p : p = p_1) (q q_1 : Y ⟶ Y') (e_q : q = q_1)
  (wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g'),
  CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg =
    CategoryTheory.Limits.parallelPairHom f g f' g' p_1 q_1 ⋯ ⋯
-- Std.Time.Date.Unit.Year
Std.Time.Year.instOrdOffset : Ord Std.Time.Year.Offset
-- Mathlib.Analysis.Normed.Group.AddTorsor
edist_vadd_vadd_le : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v v' : V) (p p' : P), edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'
-- Mathlib.Computability.RecursiveIn
/-- If every function in `O` is partial recursive,
then a function which is `Nat.RecursiveIn O` is also partial recursive.  -/
Nat.RecursiveIn.partrec_of_oracle : ∀ {f : ℕ →. ℕ} {O : Set (ℕ →. ℕ)}, (∀ g ∈ O, Nat.Partrec g) → Nat.RecursiveIn O f → Nat.Partrec f
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrable_indicator_iff : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasurableSet s → (MeasureTheory.Integrable (s.indicator f) μ ↔ MeasureTheory.IntegrableOn f s μ)
-- Mathlib.Data.Vector.Basic
List.Vector.traverse_eq_map_id : ∀ {n : ℕ} {α β : Type u_6} (f : α → β) (x : List.Vector α n),
  List.Vector.traverse (pure ∘ f) x = pure (List.Vector.map f x)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_9 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (X Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C) (p : Y₁.Hom Y₂),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X p) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.FreeMonoidalCategory.projectObj f X)
      (CategoryTheory.FreeMonoidalCategory.projectMapAux f p)
-- Init.Data.List.ToArray
_private.Init.Data.Array.Basic.0.Array.findSomeRevM?.find.congr_simp : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f f_1 : α → m (Option β)),
  f = f_1 →
    ∀ (as as_1 : Array α) (e_as : as = as_1) (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ as.size),
      Array.findSomeRevM?.find✝ f as i a = Array.findSomeRevM?.find✝ f_1 as_1 i_1 ⋯
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.ker_mapRangeAddMonoidHom : ∀ {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [inst : (i : ι) → AddCommGroup (β₁ i)]
  [inst_1 : (i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i),
  (DFinsupp.mapRange.addMonoidHom f).ker =
    AddSubgroup.comap DFinsupp.coeFnAddMonoidHom (AddSubgroup.pi Set.univ fun x => (f x).ker)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIcoMod_symm_apply : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α) (x : ↑(Set.Ico a (a + p))), (QuotientAddGroup.equivIcoMod hp a).symm x = ↑↑x
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_right_add : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {y + x, y} = Ideal.span {x, y}
-- Mathlib.Order.Circular
Set.left_mem_cIcc : ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), a ∈ Set.cIcc a b
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_Φ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ),
  (W.baseChange B).Φ n = Polynomial.map (↑f) ((W.baseChange A).Φ n)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_filterMapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [Std.Iterators.Finite α Id] [inst_8 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.Iter.filterMapWithPostcondition f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out).run
      match __do_lift with
        | some c => g c acc
        | none => pure (ForInStep.yield acc)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₁_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  ¬c₁.Rel i₁ (c₁.next i₁) → ⋯ = ⋯
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.toEDist : {α : Type u} → [self : PseudoEMetricSpace α] → EDist α
-- Init.Data.UInt.Lemmas
USize.ne_of_toBitVec_ne : ∀ {a b : USize}, a.toBitVec ≠ b.toBitVec → a ≠ b
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {F : Type u_18}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {f : M → F},
  MDiffAt[s] f x →
    DifferentiableWithinAt 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
      (↑(extChartAt I x) x)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_union' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s t : Set α},
  autoParam (BddAbove s) csSup_union'._auto_1 →
    autoParam (BddAbove t) csSup_union'._auto_3 → sSup (s ∪ t) = max (sSup s) (sSup t)
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.inner_def : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f g : ↥(MeasureTheory.Lp E 2 μ)),
  inner 𝕜 f g = ∫ (a : α), inner 𝕜 (↑↑f a) (↑↑g a) ∂μ
-- Aesop.Tree.Traversal
Aesop.TreeRef.goal : Aesop.GoalRef → Aesop.TreeRef
-- Mathlib.Analysis.Normed.Group.Basic
norm_pos_iff' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, 0 < ‖a‖ ↔ a ≠ 1
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.le_index_mul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    MeasureTheory.Measure.haar.index (↑K) V ≤
      MeasureTheory.Measure.haar.index ↑K ↑K₀ * MeasureTheory.Measure.haar.index (↑K₀) V
-- Mathlib.Order.Defs.Unbundled
IsPartialOrder.toIsPreorder : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsPartialOrder α r], IsPreorder α r
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Interpolating between affine maps with `lineMap` commutes with evaluation.  -/
AffineMap.lineMap_apply' : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} {P2 : Type u_6} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1] [inst_3 : AddCommGroup V2] [inst_4 : AddTorsor V2 P2]
  [inst_5 : Module k V1] [inst_6 : Module k V2] [inst_7 : SMulCommClass k k V2] (f g : P1 →ᵃ[k] P2) (c : k) (p : P1),
  ((AffineMap.lineMap f g) c) p = (AffineMap.lineMap (f p) (g p)) c
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- **Alias** of the reverse direction of `measurable_iff_comap_le`. -/
Measurable.of_comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β},
  MeasurableSpace.comap f m₂ ≤ m₁ → Measurable f
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape : ∀ {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.ReflectsColimitsOfShape J F],
  CategoryTheory.Limits.ReflectsColimit K F
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.directLimitRight_tmul_of : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (m : M) (g : G i),
  (TensorProduct.directLimitRight f M) (m ⊗ₜ[R] (Module.DirectLimit.of R ι G f i) g) =
    (Module.DirectLimit.of R ι (fun x => TensorProduct R M (G x)) (fun i j h => LinearMap.lTensor M (f i j h)) i)
      (m ⊗ₜ[R] g)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeOp_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] {F : CategoryTheory.Functor J C}
  (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Functor.mapConeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology] {Z : C} (h_1 : h.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ (CategoryTheory.CategoryStruct.comp h.leftHomologyIso.hom h_1) =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.hom (CategoryTheory.CategoryStruct.comp h.π h_1)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesMonomorphisms.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Mono (F.map f)) → F.PreservesMonomorphisms
-- Mathlib.FieldTheory.Finiteness
IsNoetherian.finsetBasis.eq_1 : ∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : IsNoetherian K V],
  IsNoetherian.finsetBasis K V =
    (Module.Basis.ofVectorSpace K V).reindex (⋯.mpr (Equiv.refl ↑(Module.Basis.ofVectorSpaceIndex K V)))
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.mk.inj : ∀ {carrier : Type u} {str : AddSemigroup carrier} {carrier_1 : Type u} {str_1 : AddSemigroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The category of sheaves on the bottom (trivial) Grothendieck topology is
equivalent to the category of presheaves.
 -/
CategoryTheory.sheafBotEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (A : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] → CategoryTheory.Sheaf ⊥ A ≌ CategoryTheory.Functor Cᵒᵖ A
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inr_inl_pushoutAssoc_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl
          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
        (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄)
      (CategoryTheory.Limits.pushout.inr g₁
        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
-- Init.Data.List.Lemmas
List.foldrM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {l : List α} {f : α → β → m β} {b : β},
  List.foldrM f b l.reverse = List.foldlM (fun x y => f y x) b l
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addFactStep.goFact : Lean.Expr → ℕ → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.SurjectiveOnStalks
-- Mathlib.Analysis.Convex.StrictConvexBetween
AffineMap.mk'.congr_simp : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f f_1 : P1 → P2) (e_f : f = f_1) (f' f'_1 : V1 →ₗ[k] V2)
  (e_f' : f' = f'_1) (p p_1 : P1) (e_p : p = p_1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p),
  AffineMap.mk' f f' p h = AffineMap.mk' f_1 f'_1 p_1 ⋯
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The relation identifying the endpoints of `Icc a (a + p)`.  -/
AddCircle.EndpointIdent : {𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [IsOrderedAddMonoid 𝕜] → (p a : 𝕜) → [hp : Fact (0 < p)] → ↑(Set.Icc a (a + p)) → ↑(Set.Icc a (a + p)) → Prop
-- Mathlib.FieldTheory.Normal.Closure
IsNormalClosure.mk : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L],
  (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤ → IsNormalClosure F K L
-- Mathlib.Order.Comparable
/-- **Alias** of `CompRel.of_compRel_of_antisymmRel`. -/
CompRel.trans_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  CompRel (fun x1 x2 => x1 ≤ x2) a b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → CompRel (fun x1 x2 => x1 ≤ x2) a c
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.dep.visitMain : (Lean.FVarId → Bool) → (Lean.MVarId → Bool) → Lean.Expr → Lean.DependsOn.M✝ Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_vert_isIso_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} [CategoryTheory.IsIso snd] [CategoryTheory.Mono f],
  CategoryTheory.CommSq fst snd f g → CategoryTheory.IsPullback fst snd f g
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.toContinuousAdd : ∀ (R : Type u_1) [inst : TopologicalSpace R] (A : Type u_2) [inst_1 : Add A] [inst_2 : SMul R A]
  [inst_3 : TopologicalSpace A] [IsModuleTopology R A], ContinuousAdd A
-- Batteries.Recycling.RBTree.Basic
/-- `upperBound? cut` retrieves the smallest entry larger than or equal to `cut`, if it exists.  -/
RBTree.RBNode.upperBound? : {α : Type u_1} → (α → Ordering) → RBTree.RBNode α → optParam (Option α) none → Option α
-- Mathlib.RingTheory.RingInvo
/-- A ring involution  -/
RingInvo : (R : Type u_2) → [Semiring R] → Type u_2
-- Init.Data.Array.FinRange
Array.size_finRange : ∀ {n : ℕ}, (Array.finRange n).size = n
-- Init.Data.Slice.List.Lemmas
List.mkSlice_roc_eq_mkSlice_roo : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.neg_1_smul : ∀ {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {a : A}, -1 • a = -a
-- Mathlib.Algebra.Opposites
AddOpposite.unop_injective : ∀ {α : Type u_1}, Function.Injective AddOpposite.unop
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  {P Q : CategoryTheory.Functor Cᵒᵖ A}
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallySurjective J f],
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f))
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- There is a primitive additive character on the finite field `F` if the characteristic
of the target is different from that of `F`.

We obtain it as the composition of the trace from `F` to `ZMod p` with a primitive
additive character on `ZMod p`, where `p` is the characteristic of `F`.  -/
AddChar.FiniteField.primitiveChar : (F : Type u_1) →
  (F' : Type u_2) →
    [inst : Field F] → [Finite F] → [inst_2 : Field F'] → ringChar F' ≠ ringChar F → AddChar.PrimitiveAddChar F F'
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whisker_exchange_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i)
  {Z : a ⟶ c} (h_1 : CategoryTheory.CategoryStruct.comp g i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g θ) h_1)
-- Mathlib.Analysis.Fourier.AddCircle
/-- The Fourier series of an `L2` function `f` sums to `f`, in the `L²` space of `AddCircle T`.  -/
hasSum_fourier_series_L2 : ∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)),
  HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_iff_lt_coe : ∀ {r : ℝ} {p : NNReal}, 0 ≤ r → (r.toNNReal < p ↔ r < ↑p)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict`.

---

Restrict domain of a function `f` to a set `s`. Same as `Subtype.restrict` but this version
takes an argument `↥s` instead of `Subtype s`.  -/
Set.restrict : {α : Type u_1} → {π : α → Type u_6} → (s : Set α) → ((a : α) → π a) → (a : ↑s) → π ↑a
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.casesOn_mk : ∀ {F : PFunctor.{uA, uB}} {r : F.M → Sort u_2} (x : ↑F F.M) (f : (x : ↑F F.M) → r (PFunctor.M.mk x)),
  (PFunctor.M.mk x).casesOn f = f x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roc_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m<...=n).toList[i]! = 0
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → ∀ {t : Set E}, s =ᶠ[nhds x] t → ContDiffWithinAt 𝕜 n f t x
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- Interpret a homogeneous `DFinsupp` as a `Finsupp`.

Note that the elaborator has a lot of trouble with this definition - it is often necessary to
write `(DFinsupp.toFinsupp f : ι →₀ M)` instead of `f.toFinsupp`, as for some unknown reason
using dot notation or omitting the type ascription prevents the type being resolved correctly.  -/
DFinsupp.toFinsupp : {ι : Type u_1} →
  {M : Type u_3} → [DecidableEq ι] → [inst : Zero M] → [(m : M) → Decidable (m ≠ 0)] → (Π₀ (x : ι), M) → ι →₀ M
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_def : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  (f g : UniformOnFun α β 𝔖), edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist ((UniformOnFun.toFun 𝔖) f x) ((UniformOnFun.toFun 𝔖) g x)
-- Mathlib.Order.Lattice
exists_ge_and_iff_exists : ∀ {α : Type u} [inst : SemilatticeSup α] {P : α → Prop} {x₀ : α}, Monotone P → ((∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instMin : {R : Type u} → {M : Type v} → [inst : SMul R M] → Min (SubMulAction R M)
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsM.incrementClauses : Std.Sat.CNF.DimacsM✝ Unit
-- Mathlib.Order.Heyting.Basic
inf_sdiff_sup_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ c ⊓ (a ⊔ b) = a \ c