mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_le_left : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  a ⊓ b ≤ a
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `hasStrictFDerivAt_finsetProd`. -/
hasStrictFDerivAt_finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} [inst_3 : DecidableEq ι] [Finite ι] {x : ι → 𝔸'},
  HasStrictFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.Data.Finset.Pairwise
List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint : ∀ {α : Type u_5} {ι : Type u_6} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {l : List ι}
  {f : ι → α}, (↑l.toFinset).PairwiseDisjoint f → l.Nodup → List.Pairwise (Function.onFun Disjoint f) l
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.toDilationClass : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β],
  DilationClass (α →ᵈ β) α β
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inr_coprodIsoPushout_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  {Z : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.bilin_of_zero_right : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)]
  (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {e : (i : ι) → E i} {f : (i : ι) → F i},
  Memℓp f 0 → Memℓp (fun i => ((B i) (e i)) (f i)) 0
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndOfSimpAnd : ∀ {φ : Prop} (σs : List (Type u_1)) (P P' Q QP : Std.Do.SPred σs) [Std.Do.SPred.Tactic.HasFrame P Q φ]
  [Std.Do.SPred.Tactic.SimpAnd Q P' QP], Std.Do.SPred.Tactic.HasFrame spred(P ∧ P') QP φ
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₃_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₃._auto_1),
  (X.sc₃ f g fg h n₀ n₁ hn₁).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The generators of `FreeGroup α` generate `FreeGroup α`. That is, the subgroup closure of the
set of generators equals `⊤`.  -/
FreeGroup.closure_range_of : ∀ (α : Type u_1), Subgroup.closure (Set.range FreeGroup.of) = ⊤
-- Mathlib.Data.Part
Part.add_mem_add : ∀ {α : Type u_1} [inst : Add α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma + mb ∈ a + b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).getD fallback
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.mutuallySingular_iff_disjoint_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.MutuallySingular ν ↔ Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs.default : Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_right_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow F f.left),
  ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).right.as = PUnit.unit
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Given a free variable, compute what needs to be added to the various discrimination trees.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.addFVar : Mathlib.Tactic.ClickSuggestions.Choice →
  Mathlib.Tactic.ClickSuggestions.Entries✝ → Lean.LocalDecl → Lean.MetaM Mathlib.Tactic.ClickSuggestions.Entries✝
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.DHashMap.map f m},
  (Std.DHashMap.map f m).getKey k h' = m.getKey k ⋯
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.specialUnitaryGroup_le_unitaryGroup : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α],
  Matrix.specialUnitaryGroup n α ≤ Matrix.unitaryGroup n α
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_pi : ∀ {G : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : Group G] [inst_1 : (i : ι) → MulAction G (α i)] (c : G)
  (I : Set ι) (s : (i : ι) → Set (α i)), c • I.pi s = I.pi (c • s)
-- Aesop.Stats.Basic
Aesop.MonadStats.getStats : {m : Type → Type} → [self : Aesop.MonadStats m] → m Aesop.Stats
-- Init.Data.Array.Count
List.countP_toArray : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, Array.countP p l.toArray = List.countP p l
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_if : ∀ {m n : ℕ}, (m<...n).toArray = if m + 1 < n then #[m + 1] ++ ((m + 1)<...n).toArray else #[]
-- Mathlib.Data.Ordmap.Invariants
Ordnode.All.eq_1 : ∀ {α : Type u_1} (P : α → Prop), Ordnode.All P Ordnode.nil = True
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) {Z_1 : AlgebraicGeometry.Scheme}
  (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).hom
      (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp f h
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.cheapCasesOnly : Lean.Meta.Grind.GrindM Bool
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.isPWO_iUnion_support_powers : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] {x : HahnSeries Γ R}, 0 ≤ x.order → (⋃ n, (x ^ n).support).IsPWO
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Lean.Grind.ToInt.toInt.hcongr_4 : ∀ (α α' : Type u),
  α = α' →
    ∀ (range range' : Lean.Grind.IntInterval),
      range = range' →
        ∀ (self : Lean.Grind.ToInt α range) (self' : Lean.Grind.ToInt α' range'),
          self ≍ self' → ∀ (a : α) (a' : α'), a ≍ a' → ↑a ≍ ↑a'
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.mul`

---

Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic.  -/
AnalyticAt.fun_mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A} {z : E},
  AnalyticAt 𝕜 f z → AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (fun i => f i * g i) z
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.eta.eq_1 : ∀ {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.Cocone F),
  c.eta = CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl c.pt) ⋯
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_toSlice_iff : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.IsValidForSlice s.toSlice p ↔ String.Pos.Raw.IsValid s p
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- Unfold the definition of composition in the enriched opposite category.  -/
CategoryTheory.eComp_op_eq_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] {C : Type u} [inst_3 : CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ)
  {Z : V} (h : (z ⟶[V] x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h =
    CategoryTheory.CategoryStruct.comp
      (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z))
        h)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).contains k = (f (m.get? k)).isSome
-- Mathlib.Algebra.DirectSum.Algebra
/-- A graded version of `Algebra`. An instance of `DirectSum.GAlgebra R A` endows `(⨁ i, A i)`
with an `R`-algebra structure.  -/
DirectSum.GAlgebra : {ι : Type uι} →
  (R : Type uR) →
    (A : ι → Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [(i : ι) → Module R (A i)] → [inst : AddMonoid ι] → [DirectSum.GSemiring A] → Type (max uA uR)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ComposableArrows.Precomp.map.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (isLt : 0 < n + 1 + 1) (j : ℕ) (hj : j + 2 < n + 1 + 1) (x_3 : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩),
  CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x_3 =
    CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_strictMono : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], StrictMono Rat.cast
-- Std.Http.Data.Body.Length
Std.Http.Body.instReprLength.repr : Std.Http.Body.Length → ℕ → Std.Format
-- Mathlib.Util.WhatsNew
Mathlib.WhatsNew.whatsNew : Lean.Environment → Lean.Environment → Lean.CoreM Lean.MessageData
-- Batteries.Data.List.Basic
/-- Auxiliary for `replaceFTR`: `replaceFTR.go f xs acc = acc.toList ++ replaceF f xs`.  -/
List.replaceFTR.go : {α : Type u_1} → (α → Option α) → List α → Array α → List α
-- Mathlib.Order.Filter.Basic
Filter.disjoint_of_disjoint_of_mem : ∀ {α : Type u} {f g : Filter α} {s t : Set α}, Disjoint s t → s ∈ f → t ∈ g → Disjoint f g
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
QuasispectrumRestricts.isometric_cfc : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S]
  [inst_10 : NonUnitalRing A] [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A]
  [inst_14 : SMulCommClass S A A] [inst_15 : Algebra R S] [inst_16 : Module R A] [IsScalarTower R S A] [StarModule R S]
  [ContinuousSMul R S] [inst_20 : IsScalarTower R A A] [inst_21 : SMulCommClass R A A] [inst_22 : MetricSpace A]
  [NonUnitalIsometricContinuousFunctionalCalculus S A q] [CompleteSpace R] [ContinuousMapZero.UniqueHom R A]
  (f : C(S, R)),
  Isometry ⇑(algebraMap R S) →
    p 0 → (∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f) → NonUnitalIsometricContinuousFunctionalCalculus R A p
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- See also `setIntegral_toReal_rnDeriv_mul'` for a version that requires both measures to be
σ-finite, but doesn't require `s` to be a measurable set.  -/
MeasureTheory.setIntegral_toReal_rnDeriv_mul : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SigmaFinite μ],
  μ.AbsolutelyContinuous ν →
    ∀ {f : α → ℝ} {s : Set α},
      MeasurableSet s → ∫ (x : α) in s, (μ.rnDeriv ν x).toReal * f x ∂ν = ∫ (x : α) in s, f x ∂μ
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_preimage_le : ∀ {X Y : SSet} (B : X.Subcomplex) (f : Y ⟶ X), (B.preimage f).image f ≤ B
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.instIsInnerPairingOfIsInner : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsInner] [inst : h.IsProper], h.pairing.IsInner
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_map_image_lift : ∀ {α : Type u} {β : Type v} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : Set α),
  autoParam (X ⊆ M.E) Matroid.cRk_map_image_lift._auto_1 →
    Cardinal.lift.{u, v} ((M.map f hf).cRk (f '' X)) = Cardinal.lift.{v, u} (M.cRk X)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_diseq_subst_cert.eq_1 : ∀ (k₁ k₂ : ℤ) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_diseq_subst_cert k₁ k₂ p₁ p₂ p₃ =
    (decide (k₁.natAbs ≠ 0) && p₃ == (p₁.mul k₂).combine (p₂.mul k₁))
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.isCoveringMap_restrictPreimage : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} (s : Set X),
  IsCoveringMapOn f s → IsCoveringMap (s.restrictPreimage f)
-- Init.Data.UInt.Bitwise
UInt32.ofFin_and : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a &&& b) = UInt32.ofFin a &&& UInt32.ofFin b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.tensorObj.instTensorObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.AddMonObj.tensorObj.instTensorObj =
    {
      zero :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero),
      add :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add),
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Init.Data.Array.Monadic
Array.foldrM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : Array (Subtype P)} {f : α → β → m β} {init : β},
  Array.foldrM f init xs.unattach =
    Array.foldrM
      (fun x b =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (binderNameHint b (f x) (f (wfParam x) b))))
      init xs
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The circumradius of a triangle may be expressed explicitly as half the length of a side
divided by the sine of the angle at the third point (a version of the law of sines or sine rule).  -/
Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        dist (t.points i₁) (t.points i₃) /
              Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)) /
            2 =
          Affine.Simplex.circumradius t
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instSub : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → Sub (E →ₛₗ.[σ] F)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Converts an isomorphism in the category `FGModuleCat R` to
a `LinearEquiv` between the underlying modules.  -/
FGModuleCat.isoToLinearEquiv : {R : Type u} → [inst : Ring R] → {V W : FGModuleCat R} → (V ≅ W) → ↑V ≃ₗ[R] ↑W
-- Mathlib.Order.Bounds.Basic
IsCoinitialFor.of_subset : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCoinitialFor s t
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_one : ∀ (n : ℕ), n.descFactorial 1 = n
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.ext_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.ElementaryEmbedding M N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Data.Finset.Empty
Finset.val_eq_zero : ∀ {α : Type u_1} {s : Finset α}, s.val = 0 ↔ s = ∅
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the left by a uniformly continuous function preserves
uniform convergence on a filter  -/
UniformContinuous.comp_tendstoUniformlyOnFilter : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
  {p : Filter ι} {p' : Filter α} [inst_1 : UniformSpace γ] {g : β → γ},
  UniformContinuous g → TendstoUniformlyOnFilter F f p p' → TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p'
-- Mathlib.Data.Rel
SetRel.core_univ : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.core Set.univ = Set.univ
-- Init.Data.Order.Ord
List.instLawfulEqCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp], Std.LawfulEqCmp (List.compareLex cmp)
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallIsoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P.isoClosure
-- Mathlib.Analysis.MeanInequalities
NNReal.Lr_le_Lp_mul_Lq_tsum : ∀ {ι : Type u} {f g : ι → NNReal} {p q r : ℝ},
  p.HolderTriple q r →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ q) →
        (∑' (i : ι), (f i * g i) ^ r) ^ (1 / r) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.eqToHom_f'_assoc : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
  (h : x = y) {Z : V} (h_1 : Y.obj y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (f.f y) h_1) =
    CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h) h_1)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- Canonical isomorphism between linear combinations and the span of linearly independent vectors.
 -/
LinearIndependent.linearCombinationEquiv : {ι : Type u'} →
  {R : Type u_2} →
    {M : Type u_4} →
      {v : ι → M} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] → LinearIndependent R v → (ι →₀ R) ≃ₗ[R] ↥(Submodule.span R (Set.range v))
-- Mathlib.Order.Preorder.Chain
/-- A chain `s` is a maximal chain if there does not exists a chain strictly including `s`.  -/
IsMaxChain : {α : Type u_1} → (α → α → Prop) → Set α → Prop
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given a category `C` that has a separator (`HasSeparator C`), `separator C` is an arbitrarily
chosen separator of `C`.
 -/
CategoryTheory.separator : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.HasSeparator C] → C
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofIntTruncate : ∀ {n : ℤ},
  ISize.minValue.toInt ≤ n →
    n ≤ ISize.maxValue.toInt → (ISize.ofIntClamp n).toBitVec = BitVec.ofInt System.Platform.numBits n
-- Init.Data.Vector.Zip
_private.Init.Data.Vector.Zip.0.Vector.getElem?_zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (a : α) (b : β), x = some a → x_1 = some b → False) →
    (match x, x_1 with
      | some a, some b => h_1 a b
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.Data.Set.Lattice
Set.iInter_or : ∀ {α : Type u_1} {p q : Prop} (s : p ∨ q → Set α), ⋂ (h : p ∨ q), s h = (⋂ (h : p), s ⋯) ∩ ⋂ (h : q), s ⋯
-- Mathlib.Geometry.Manifold.Algebra.SMul
Prod.prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : VAdd G M] [inst_17 : VAdd G N] {n : WithTop ℕ∞} [ContMDiffVAdd I I' n G M] [ContMDiffVAdd I I'' n G N],
  ContMDiffVAdd I (I'.prod I'') n G (M × N)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₁_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂),
      K.d₁ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotal c₁₂ i₁' i₂ i₁₂ h')
-- Init.Data.BitVec.Bitblast
/-- The number of bits in the remainder (and quotient)  -/
BitVec.DivModState.wr : {w : ℕ} → BitVec.DivModState w → ℕ
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.blankLine : Lean.Parser.ParserFn
-- Mathlib.Computability.Reduce
ManyOneDegree.instInhabited : Inhabited ManyOneDegree