mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k k' : α} {f : β → β},
  (t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.neg_zsmul : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (n : ℤ) (a : M), -n • a = -(n • a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ ∀ (a : α), t.contains a = false
-- Lean.Declaration
/-- Returns `true` if this declaration as a value for the purpose of reduction
and type-checking, i.e. is a definition.
With `allowOpaque := true`, theorems and opaque declarations are also considered to have values.
 -/
Lean.ConstantInfo.hasValue : Lean.ConstantInfo → optParam Bool false → Bool
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.ae_le_eLpNormEssSup : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : ENorm ε] {f : α → ε},
  ∀ᵐ (y : α) ∂μ, ‖f y‖ₑ ≤ MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- An ergodic map is quasi-ergodic.  -/
Ergodic.quasiErgodic : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α}, Ergodic f μ → QuasiErgodic f μ
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- **Alias** of `EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter`.

---

**Thales' theorem**: The angle inscribed in a semicircle is a right angle.  -/
EuclideanGeometry.Sphere.thales_theorem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P},
  s.IsDiameter p₁ p₃ → (EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s)
-- Batteries.Control.LawfulMonadState
/-- The `EStateM` monad always has a lawful state instance.  -/
LawfulMonadStateOf.instEStateM : ∀ {σ ε : Type u_1}, LawfulMonadStateOf σ (EStateM ε σ)
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_pos : ∀ {α : Type u_1} [Nonempty α], 0 < ENat.card α
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- `det` is an `AlternatingMap` in the rows of the matrix.  -/
Matrix.detRowAlternating : {n : Type u_2} → [DecidableEq n] → [Fintype n] → {R : Type v} → [inst : CommRing R] → (n → R) [⋀^n]→ₗ[R] R
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∪ m₂)[k]? = m₂[k]?
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The first part of the third cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.σ i) = CategoryTheory.CategoryStruct.id (X.obj { len := n })
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Satisfying the inhabited linter.  -/
TopCat.inhabitedLocalPredicate : (X : TopCat) → (T : Type u_3) → [TopologicalSpace T] → Inhabited (TopCat.LocalPredicate fun x => T)
-- Mathlib.Algebra.Category.BialgCat.Basic
CategoryTheory.Iso.toBialgEquiv_toBialgHom : ∀ {R : Type u} [inst : CommRing R] {X Y : BialgCat R} (i : X ≅ Y), ↑i.toBialgEquiv = i.hom.toBialgHom'
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.ofIsEmpty_isExpansionOn : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [inst : L.Structure M] [inst_1 : L'.Structure M]
  [inst_2 : L.IsAlgebraic] [inst_3 : L.IsRelational], (FirstOrder.Language.LHom.ofIsEmpty L L').IsExpansionOn M
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNew.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l toInsert : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l toInsert =
    match toInsert with
    | [] => l
    | ⟨k, v⟩ :: tl => Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) tl
-- Init.Data.Sum.Lemmas
Sum.isRight_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.isRight = true ↔ ∃ y, x = Sum.inr y
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postEquiv_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D),
  (CategoryTheory.Over.postEquiv X F).inverse =
    (CategoryTheory.Over.post F.inverse).comp (CategoryTheory.Over.map (F.unitIso.inv.app X))
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_eq_one_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} {e : ↑(p ⁻¹' {x})}
  {γ : FundamentalGroup X x}, (hp.fundamentalGroupToMulOpposite e) γ = 1 ↔ ⋯.monodromy γ e = e
-- Mathlib.RingTheory.WittVector.Defs
WittVector.mk'.inj : ∀ {p : ℕ} {R : Type u_1} {coeff coeff_1 : ℕ → R}, { coeff := coeff } = { coeff := coeff_1 } → coeff = coeff_1
-- Init.Data.SInt.Lemmas
ISize.toInt8_toInt32 : ∀ (n : ISize), n.toInt32.toInt8 = n.toInt8
-- Mathlib.Order.Atoms
IsAtom.le_iSup : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Order.Frame α] {f : ι → α} {a : α}, IsAtom a → (a ≤ iSup f ↔ ∃ i, a ≤ f i)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isNegInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Init.Data.Int.Gcd
Int.gcd_gcd_self_right_left : ∀ (m n : ℤ), m.gcd ↑(m.gcd n) = m.gcd n
-- Mathlib.Topology.UniformSpace.Cauchy
/-- If `K` is a complete subset, then any Cauchy sequence in `K` converges to a point in `K`  -/
cauchySeq_tendsto_of_isComplete : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {K : Set α},
  IsComplete K → ∀ {u : β → α}, (∀ (n : β), u n ∈ K) → CauchySeq u → ∃ v ∈ K, Filter.Tendsto u Filter.atTop (nhds v)
-- Mathlib.Algebra.Prime.Lemmas
Prime.eq_1 : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] (p : M),
  Prime p = (p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Basic.0.SimpleGraph.farFromTriangleFree_of_disjoint_triangles_aux : ∀ {α : Type u_1} {G H : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableRel H.Adj]
  [inst_3 : DecidableEq α] {tris : Finset (Finset α)},
  tris ⊆ G.cliqueFinset 3 →
    ((↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton) →
      H ≤ G → H.CliqueFree 3 → tris.card ≤ G.edgeFinset.card - H.edgeFinset.card
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectSuccessorOf.brecOn : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {a : Std.Iter β}
  {motive : (a_1 : Std.Iter β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop} {a_1 : Std.Iter β}
  (t : a.IsPlausibleIndirectSuccessorOf a_1),
  (∀ (a_2 : Std.Iter β) (t : a.IsPlausibleIndirectSuccessorOf a_2),
      Std.Iter.IsPlausibleIndirectSuccessorOf.below t → motive a_2 t) →
    motive a_1 t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.differentiableAt_tan : ∀ {x : ℝ}, DifferentiableAt ℝ Real.tan x ↔ Real.cos x ≠ 0
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.instInhabited : {α : Type u_1} → [inst : TopologicalSpace α] → Inhabited (CocompactMap α α)
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The relations span the kernel of the canonical map.  -/
Algebra.Presentation.span_range_relation_eq_ker : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : Algebra.Presentation R S ι σ), Ideal.span (Set.range self.relation) = self.ker
-- Init.System.IOError
IO.Error.protocolError.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.protocolError osCode details) = 1 + sizeOf osCode + sizeOf details
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Smooth.smooth_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Smooth f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Smooth
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.zero.sizeOf_spec : sizeOf FirstOrder.ringFunc.zero = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  r.toArray[i]? = Option.filter (fun x => decide (x ≤ r.upper)) (Std.PRange.succMany? (i + 1) r.lower)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.contains_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α},
  m.contains a = Std.DHashMap.Internal.Raw₀.contains ⟨m, ⋯⟩ a
-- Mathlib.Algebra.Group.Basic
sub_sub_sub_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c d : α), a - b - (c - d) = a - c - (b - d)
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Symm.swap_eq`. -/
Symmetric.swap_eq : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Function.swap r = r
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.exists_aeval_eq_zero_of_injective : ∀ (k : Type u) [inst : Field k] {R : Type u_1} [inst_1 : CommSemiring R] [IsAlgClosed k] [inst_3 : Algebra R k],
  Function.Injective ⇑(algebraMap R k) → ∀ (p : Polynomial R), p.degree ≠ 0 → ∃ x, (Polynomial.aeval x) p = 0
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.pushWhitespace : Std.Format → Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.toIsReduced : ∀ {ι : 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} [self : P.IsG2],
  P.IsReduced
-- Lean.Parser.Term
Lean.Parser.Term.waitIfContainsMVar.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- For an `n + 1`-truncated simplicial set `X`, `IsStrictSegal X` asserts the
mere existence of an inverse to `spine X m` for all `m ≤ n + 1`.  -/
SSet.Truncated.IsStrictSegal : {n : ℕ} → SSet.Truncated (n + 1) → Prop
-- Init.Control.Lawful.Instances
ReaderT.ext_iff : ∀ {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ReaderT ρ m α},
  x = y ↔ ∀ (ctx : ρ), x.run ctx = y.run ctx
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.equivStructuredArrow_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor = CategoryTheory.Limits.Cocone.toStructuredArrow F
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.add_singleton : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] {s : Finset α} (a : α), s + {a} = AddOpposite.op a +ᵥ s
-- Mathlib.RingTheory.Unramified.Finite
/-- If `S` is an unramified `R`-algebra, then `R`-flat implies `S`-flat. Iversen I.2.7  -/
Algebra.FormallyUnramified.flat_of_restrictScalars : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M]
  [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Module.Flat R M], Module.Flat S M
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- For any arrow `φ : a ⟶ b` in `𝒳`, `φ` lifts the arrow `p.map φ` in the base `𝒮`.  -/
CategoryTheory.IsHomLift.map : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {a b : 𝒳} (φ : a ⟶ b), p.IsHomLift (p.map φ) φ
-- Mathlib.Algebra.Order.Quantale
Quantale.sup_mul_distrib : ∀ {α : Type u_1} {x y z : α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  (x ⊔ y) * z = x * z ⊔ y * z
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.ε F) f)
      (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
        (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv))
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.setRed.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      ((c : RBTree.RBColor) →
          (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)) →
        (Unit → motive RBTree.RBNode.nil) → motive x
-- Mathlib.Data.Sign.Defs
SignType.lt_one_iff : ∀ {a : SignType}, a < 1 ↔ a ≤ 0
-- Batteries.Data.ByteSlice
/-- Folds a function over a `ByteSubarray` from left to right.  -/
ByteSlice.foldl : {β : Type u_1} → ByteSlice → (β → UInt8 → β) → β → β
-- Mathlib.GroupTheory.PGroup
IsPGroup.isOfFinOrder : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → p ≠ 0 → ∀ (g : G), IsOfFinOrder g
-- Mathlib.Probability.Process.Filtration
/-- Given a sequence of measurable sets `(sₙ)`, `filtrationOfSet` is the smallest filtration
such that `sₙ` is measurable with respect to the `n`-th sub-σ-algebra in `filtrationOfSet`.  -/
MeasureTheory.filtrationOfSet : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] → {s : ι → Set Ω} → (∀ (i : ι), MeasurableSet (s i)) → MeasureTheory.Filtration ι m
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.instSubringClass : ∀ {R : Type u} [inst : NonAssocRing R], SubringClass (Subring R) R
-- Lean.Data.KVMap
Lean.KVMap.instValueDataValue : Lean.KVMap.Value Lean.DataValue
-- Mathlib.Data.Vector.Mem
List.Vector.mem_iff_get : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), a ∈ v.toList ↔ ∃ i, v.get i = a
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.of_bijective : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Bijective ⇑f → f.Smooth
-- Lean.Meta.Match.Match
Lean.Meta.Match.processIndependentPatterns : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_hnot_le : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), Coheyting.boundary (￢a) ≤ Coheyting.boundary a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → ∀ {fallback : α}, t.maxKeyD fallback = fallback
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.map.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (b : Module.Basis ι R M) (f : M ≃ₗ[R] M'),
  b.map f = { repr := f.symm ≪≫ₗ b.repr }
-- Std.Time.DateTime.PlainDateTime
/-- Transforms a tuple of a `PlainDateTime` into a `Day.Ordinal.OfYear`.
 -/
Std.Time.PlainDateTime.dayOfYear : (date : Std.Time.PlainDateTime) → Std.Time.Day.Ordinal.OfYear date.year.isLeap
-- Mathlib.CategoryTheory.Limits.Cones
/-- The triangle made from the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.CoconeMorphism.w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cocone F}
  (self : CategoryTheory.Limits.CoconeMorphism A B) (j : J),
  CategoryTheory.CategoryStruct.comp (A.ι.app j) self.hom = B.ι.app j
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.inverse.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M →L[R] M₂), f.inverse = if h : f.IsInvertible then ↑(Classical.choose h).symm else 0
-- Mathlib.Algebra.Group.Basic
/-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`.  -/
hom_coe_pow : ∀ {M : Type u_4} {F : Type u_5} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = (c f)^[n]
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.ext : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} {inst : Semiring A} {inst_1 : Monoid G} {inst_2 : AddCommMonoid W}
  {inst_3 : Module A W} {ρ : Representation A G W} {x y : Subrepresentation ρ}, x.toSubmodule = y.toSubmodule → x = y
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app : ∀ (R : CommRingCat), AlgebraicGeometry.Scheme.SpecΓIdentity.inv.app R = (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
-- Init.Data.List.Attach
List.getElem?_attach : ∀ {α : Type u_1} {xs : List α} {i : ℕ}, xs.attach[i]? = Option.pmap Subtype.mk xs[i]? ⋯
-- Lean.Meta.HaveTelescope
/-- Remove unused-let declarations.  -/
Lean.Meta.zetaUnused : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instOrderedAddQ : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Lean.Grind.OrderedAdd (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_le_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  {s : Set α}, μ s ≤ 1
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.createsLimitsOfIsEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (H : CategoryTheory.Functor D C) →
          [H.IsEquivalence] → CategoryTheory.CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define a `GCDMonoid` structure on a monoid just from the existence of an `lcm`.  -/
gcdMonoidOfExistsLCM : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] → [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) → GCDMonoid α
-- Lean.Widget.InteractiveCode
_private.Lean.Widget.InteractiveCode.0.Lean.Widget.tagCodeInfos.go : Lean.Elab.ContextInfo →
  Lean.SubExpr.PosMap Lean.Elab.Info →
    Lean.Widget.TaggedText (ℕ × ℕ) → BaseIO (Lean.Widget.TaggedText Lean.Widget.SubexprInfo)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.arrowCongr_symm_apply : ∀ {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  {V₄ : Type u_9} [inst : AddCommGroup V₁] [inst_1 : AddCommGroup V₂] [inst_2 : AddCommGroup V₃]
  [inst_3 : AddCommGroup V₄] [inst_4 : AddTorsor V₁ P₁] [inst_5 : AddTorsor V₂ P₂] [inst_6 : AddTorsor V₃ P₃]
  [inst_7 : AddTorsor V₄ P₄] {R : Type u_10} [inst_8 : CommRing R] [inst_9 : Module R V₁] [inst_10 : Module R V₂]
  [inst_11 : Module R V₃] [inst_12 : Module R V₄] (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : P₃ ≃ᵃ[R] P₄) (f : P₂ →ᵃ[R] P₄) (x : P₁),
  ((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.restrict_killingForm_eq_sum : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K],
  (killingForm K L).restrict H.toSubmodule =
    ∑ α ∈ LieSubalgebra.root, (LieModule.Weight.toLinear K (↥H) L α).smulRight (LieModule.Weight.toLinear K (↥H) L α)
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The coherent Grothendieck topology on a precoherent category `C`.
 -/
CategoryTheory.coherentTopology : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Precoherent C] → CategoryTheory.GrothendieckTopology C
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_at_1_ne_zero : ∀ (R : Type u_1) [inst : CommRing R] [CharZero R] (n ν : ℕ),
  ν ≤ n → Polynomial.eval 1 ((⇑Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddLeftCancelSemigroup : {α : Type u_1} → [AddRightCancelSemigroup α] → AddLeftCancelSemigroup αᵃᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumClique.isClique : ∀ {α : Type u_3} [inst : Finite α] {G : SimpleGraph α} {s : Finset α}, G.IsMaximumClique s → G.IsClique ↑s
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingHom.eq_1 : ∀ {R : Type u_3} {S : Type u_4} (M : Type u_6) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (f : R →+* S),
  AddMonoidAlgebra.mapRingHom M f =
    { toFun := AddMonoidAlgebra.map ↑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies `True`.  -/
Mathlib.Meta.NormNum.evalTrue : Mathlib.Meta.NormNum.NormNumExt
-- Std.Time.Date.Unit.Week
Std.Time.Week.instToStringOffset : ToString Std.Time.Week.Offset
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_le_add_of_nonpos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a ≤ b + c → b ≤ 0 → a ≤ c
-- Mathlib.Order.ModularLattice
disjoint_sup_right_of_disjoint_sup_right : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : OrderBot α] [IsModularLattice α],
  Disjoint a (b ⊔ c) → Disjoint b (c ⊔ a) → Disjoint c (a ⊔ b)
-- Mathlib.Topology.WithTopology
WithTopology.instFintype : {X : Type u_1} → (t : TopologicalSpace X) → [Fintype X] → Fintype (WithTopology X t)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.extraction_forall_of_frequently : ∀ {P : ℕ → ℕ → Prop}, (∀ (n : ℕ), ∃ᶠ (k : ℕ) in Filter.atTop, P n k) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.Prepartition.disjUnion.congr_simp : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₁_1 : BoxIntegral.Prepartition I) (e_π₁ : π₁ = π₁_1)
  (π₂ π₂_1 : BoxIntegral.Prepartition I) (e_π₂ : π₂ = π₂_1) (h : Disjoint π₁.iUnion π₂.iUnion),
  π₁.disjUnion π₂ h = π₁_1.disjUnion π₂_1 ⋯