mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Restrict
/-- `(⊤ : X.Opens)` as a scheme is isomorphic to `X`.  -/
AlgebraicGeometry.Scheme.topIso : (X : AlgebraicGeometry.Scheme) → ↑⊤ ≅ X
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.submodule_map_involute_eq_comap : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)),
  Submodule.map CliffordAlgebra.involute.toLinearMap p = Submodule.comap CliffordAlgebra.involute.toLinearMap p
-- Init.Data.Function
Function.surjective_id : ∀ {α : Sort u_1}, Function.Surjective id
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
_private.Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage.0.circleAverage_log_norm_sub_const₁_integral : ∫ (x : ℝ) in 0..2 * Real.pi, Real.log (4 * Real.sin (x / 2) ^ 2) / 2 = 0
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.restrictScalars_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {S : Type u_4} [inst_5 : CommSemiring S]
  [inst_6 : Module S A] [inst_7 : SMulCommClass S A A] [inst_8 : IsScalarTower S A A]
  [inst_9 : LinearMap.CompatibleSMul A A R S] (a : A), ↑R ((LinearMap.mul S A) a) = (LinearMap.mul R A) a
-- Mathlib.Logic.Equiv.Defs
/-- If `α` is equivalent to `β`, then `Perm α` is equivalent to `Perm β`.  -/
Equiv.permCongr : {α' : Type u_1} → {β' : Type u_2} → α' ≃ β' → Equiv.Perm α' ≃ Equiv.Perm β'
-- Mathlib.Data.List.Sort
RelEmbedding.pairwise_listMap : ∀ {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α},
  List.Pairwise rb (List.map (⇑e) l) ↔ List.Pairwise ra l
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.lie_h_e : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H) (i j : ι),
  ⁅self.h j, self.e i⁆ = self.A i j • self.e i
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_inv_associator : ∀ {R : Type u} [inst : CommRing R] {M N K : ModuleCat R},
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv =
    ↑(TensorProduct.assoc R ↑M ↑N ↑K).symm
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toOuterMeasure_ofFintype_apply : ∀ {α : Type u_1} [inst : Fintype α] {f : α → ENNReal} (h : ∑ a, f a = 1) (s : Set α),
  (PMF.ofFintype f h).toOuterMeasure s = ∑' (x : α), s.indicator f x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toSubmodule_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A],
  Function.Injective NonUnitalSubalgebra.toSubmodule
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_monomial : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (e : σ →₀ ℕ) (r : R),
      MvPowerSeries.subst a ((MvPowerSeries.monomial e) r) =
        (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n => a s ^ n
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.rank_of_isFractionRing : ∀ (R : Type u_1) [inst : CommRing R] (R' : Type u_4) (S : Type u) [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [inst_4 : Algebra R R'] [IsFractionRing R R'] [FaithfulSMul R S] [Algebra.IsAlgebraic R S]
  [NoZeroDivisors S] (S' : Type u) [inst_9 : CommRing S'] [inst_10 : Algebra R S'] [inst_11 : Algebra S S']
  [inst_12 : Module R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'],
  Module.rank R' S' = Module.rank R S
-- Mathlib.Data.Multiset.Bind
Multiset.filter_join : ∀ {α : Type u_1} (S : Multiset (Multiset α)) (p : α → Prop) [inst : DecidablePred p],
  Multiset.filter p S.join = (Multiset.map (Multiset.filter p) S).join
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.preservesEpimorphisms_π₃ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C],
  CategoryTheory.ShortComplex.π₃.PreservesEpimorphisms
-- Mathlib.Data.Nat.Find
/-- If `p` is a (decidable) predicate on `ℕ` and `hp : ∃ (n : ℕ), p n` is a proof that
there exists some natural number satisfying `p`, then `Nat.find hp` is the
smallest natural number satisfying `p`. Note that `Nat.find` is protected,
meaning that you can't just write `find`, even if the `Nat` namespace is open.

The API for `Nat.find` is:

* `Nat.find_spec` is the proof that `Nat.find hp` satisfies `p`.
* `Nat.find_min` is the proof that if `m < Nat.find hp` then `m` does not satisfy `p`.
* `Nat.find_min'` is the proof that if `m` does satisfy `p` then `Nat.find hp ≤ m`.
 -/
Nat.find : {p : ℕ → Prop} → [DecidablePred p] → (∃ n, p n) → ℕ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Fatou's lemma**, version with `Measurable` functions.  -/
MeasureTheory.lintegral_liminf_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ι → α → ENNReal}
  {u : Filter ι} [u.IsCountablyGenerated],
  (∀ (i : ι), Measurable (f i)) →
    ∫⁻ (a : α), Filter.liminf (fun i => f i a) u ∂μ ≤ Filter.liminf (fun i => ∫⁻ (a : α), f i a ∂μ) u
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (acc acc_1 : aig.Ref),
  acc = acc_1 →
    ∀ (idx idx_1 : ℕ),
      idx = idx_1 →
        ∀ (len : ℕ) (input input_1 : aig.RefVec len),
          input = input_1 →
            ∀ (f f_1 : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) (e_f : f = f_1)
              [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f],
              Std.Sat.AIG.RefVec.fold.go aig acc idx len input f =
                Std.Sat.AIG.RefVec.fold.go aig acc_1 idx_1 len input_1 f_1
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is slightly weaker than `MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_le` as the
latter provides `0 < M`.  -/
MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : α → β},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.StronglyMeasurable f →
      ∀ {ε : ℝ}, 0 < ε → ∃ M, MeasureTheory.eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
-- Mathlib.GroupTheory.Exponent
Monoid.exponent.eq_1 : ∀ (G : Type u) [inst : Monoid G], Monoid.exponent G = if h : Monoid.ExponentExists G then Nat.find h else 0
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ext : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} {x y : v.Completion},
  x.toCompletion = y.toCompletion → x = y
-- Mathlib.NumberTheory.Ostrowski
/-- If `f` is not bounded and not trivial, then it is equivalent to the standard absolute value on
`ℚ`.  -/
Rat.AbsoluteValue.equiv_real_of_unbounded : ∀ {f : AbsoluteValue ℚ ℝ}, (¬∀ (n : ℕ), f ↑n ≤ 1) → f.IsEquiv Rat.AbsoluteValue.real
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_pos : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), 0 < Dilation.ratio f
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_neg : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (x y : G), edist (-x) y = edist x (-y)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- An additive group is free if it admits an additive free group basis. In the definition, we
require the basis to be in the same universe as `G`, although this property follows from the
existence of a basis in any universe, see `FreeAddGroupBasis.isFreeAddGroup`.  -/
IsFreeAddGroup : (G : Type u) → [AddGroup G] → Prop
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.subset_ofPred`. -/
Set.subset_setOf : ∀ {α : Type u} {p : α → Prop} {s : Set α}, s ⊆ Set.ofPred p ↔ ∀ x ∈ s, p x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_one : ∀ {R : Type u_1} {a b : R} [inst : Zero R] [inst_1 : One R], QuadraticAlgebra.im 1 = 0
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `ωSup` is a lower bound of the set of upper bounds of the increasing sequence  -/
OmegaCompletePartialOrder.ωSup_le : ∀ {α : Type u_6} [self : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) (x : α),
  (∀ (i : ℕ), c i ≤ x) → OmegaCompletePartialOrder.ωSup c ≤ x
-- Mathlib.Tactic.GCongr.Core
/-- A version of the `rfl` tactic that also closes goals of the form `⊢ p → p`.  -/
Lean.MVarId.applyRflOrId : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_add_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} {f : α → E} {ν : MeasureTheory.Measure α}
  (hTμ : MeasureTheory.DominatedFinMeasAdditive μ T C) (hTν : MeasureTheory.DominatedFinMeasAdditive ν T' C'),
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable f ν →
      MeasureTheory.setToFun (μ + ν) (T + T') ⋯ f = MeasureTheory.setToFun μ T hTμ f + MeasureTheory.setToFun ν T' hTν f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`.  -/
Orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.instDecidableRelSameCycleOfNatOfDecidableEq : {α : Type u_2} → [DecidableEq α] → DecidableRel (Equiv.Perm.SameCycle 1)
-- Init.Tactics
/-- `mconstructor` is like `constructor`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
  mintro HQ
  mconstructor <;> mexact HQ
```
 -/
Lean.Parser.Tactic.mconstructorMacro : Lean.ParserDescr
-- Mathlib.Algebra.GCDMonoid.Basic
GCDMonoid.toIsCancelMulZero : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α], IsCancelMulZero α
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instCoeAdjoinAuxInsertSet_1 : ∀ {α : Type u_1} (x y : α) (s : Set α) [Algebra.CoeAdjoinAux x s], Algebra.CoeAdjoinAux x (insert y s)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_single_mul_apply`. -/
MonoidAlgebra.single_mul_apply : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x : MonoidAlgebra R G) (r : R) (g h : G),
  (MonoidAlgebra.single g r * x).coeff h = r * x.coeff (g⁻¹ * h)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_neg : ∀ (x : ℝ), Real.arcsin (-x) = -Real.arcsin x
-- Init.Data.List.TakeDrop
List.drop_set : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α},
  List.drop i (l.set j a) = if j < i then List.drop i l else (List.drop i l).set (j - i) a
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_hom : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R R' S : 𝒮} {a a' b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R}
  (h : f' = CategoryTheory.CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  [inst_3 : p.IsStronglyCartesian f' φ'],
  (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h φ φ').hom =
    CategoryTheory.Functor.IsStronglyCartesian.map p f φ h φ'
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.instNontrivialContinuousLinearMapIdOfContinuousSMul : ∀ {R : Type u_1} (V : Type u_2) [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [inst_4 : Module R V] [SeparatingDual R V] (W : Type u_3) [inst_6 : AddCommGroup W]
  [inst_7 : TopologicalSpace W] [inst_8 : Module R W] [Nontrivial W] [ContinuousSMul R W] [Nontrivial V],
  Nontrivial (V →L[R] W)
-- Mathlib.Order.SupClosed
IsUpperSet.supClosed : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, IsUpperSet s → SupClosed s
-- Mathlib.Logic.Function.Basic
Function.exists_update_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop),
  (∃ x, p x (Function.update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_mul_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (i : σ) (x : MvPolynomial σ R),
  ((MvPolynomial.X i * x).divMonomial fun₀ | i => 1) = x
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- By construction, the simplicial `Γ₀.obj K` is equipped with a splitting.  -/
AlgebraicTopology.DoldKan.Γ₀.splitting : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (K : ChainComplex C ℕ) → (AlgebraicTopology.DoldKan.Γ₀.obj K).Splitting
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_of_associated_right : ∀ {α : Type u_1} [inst : Monoid α] {a b c : α}, Associated b c → emultiplicity a b = emultiplicity a c
-- Mathlib.Algebra.DirectSum.Ring
_private.Mathlib.Algebra.DirectSum.Ring.0.DirectSum.mul_comm : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddCommMonoid ι] [inst_3 : DirectSum.GCommSemiring A] (a b : DirectSum ι fun i => A i), a * b = b * a
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.ext : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {S T : NonUnitalStarSubalgebra R A}, (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁_yonedaEquivFst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F X),
  (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).yonedaEquivFst = p.yonedaEquivFst
-- Init.Data.String.Lemmas.Iterate
String.mem_toList_iff_exists_get : ∀ {s : String} {c : Char}, c ∈ s.toList ↔ ∃ p, ∃ (h : p ≠ s.endPos), p.get h = c
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
InnerProductSpace.volume_closedBall_of_dim_odd : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {k : ℕ},
  Module.finrank ℝ E = 2 * k + 1 →
    ∀ (x : E) (r : ℝ),
      MeasureTheory.volume (Metric.closedBall x r) =
        ENNReal.ofReal r ^ Module.finrank ℝ E *
          ENNReal.ofReal (Real.pi ^ k * 2 ^ (k + 1) / ↑(Module.finrank ℝ E).doubleFactorial)
-- Lean.Parser.Do
Lean.Parser.Term.doIf.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.Lemmas
UInt64.add_assoc : ∀ (a b c : UInt64), a + b + c = a + (b + c)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_of_mem_inter_right : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ → a ∈ s₂
-- Mathlib.Data.Multiset.Bind
Multiset.zero_sigma : ∀ {α : Type u_1} {σ : α → Type u_4} (t : (a : α) → Multiset (σ a)), Multiset.sigma 0 t = 0
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.faithfulSMul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : SMulZeroClass R S] [FaithfulSMul R S]
  [Nonempty M], FaithfulSMul R (MonoidAlgebra S M)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hasRightExtension_iff_postcomp₁ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H),
  L'.HasRightKanExtension F ↔ L.HasRightKanExtension F
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeSet_edge : ∀ {V : Type u_1} (v w : V), (SimpleGraph.edge v w).edgeSet = {s(v, w)} \ Sym2.diagSet
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.generate_has_subset_generate_measurable : ∀ {α : Type u_3} {C : Set (Set α)} {s : Set α}, (MeasurableSpace.DynkinSystem.generate C).Has s → MeasurableSet s
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_le_expectation_sq : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → ℝ}, MeasureTheory.AEStronglyMeasurable X μ → ProbabilityTheory.variance X μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- Removing an edge from `G` for each subgraph isomorphic to `H` results in a graph that doesn't
contain `H`.  -/
SimpleGraph.free_killCopies : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, H ≠ ⊥ → H.Free (G.killCopies H)
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_functor_map_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {X_1 Y : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A} (f : X_1 ⟶ Y)
  (X_2 : (TopologicalSpace.Opens ↥U)ᵒᵖ),
  (U.sheafEquivOver.functor.map f).hom.app X_2 =
    f.hom.app (Opposite.op (U.overEquivalence.inverse.obj (Opposite.unop X_2)))
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  [P.HasOfPostcompProperty AlgebraicGeometry.IsOpenImmersion] [P.RespectsRight AlgebraicGeometry.IsOpenImmersion]
  [AlgebraicGeometry.IsZariskiLocalAtSource P], AlgebraicGeometry.IsZariskiLocalAtSource P.diagonal
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntryIfNew_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.insertEntryIfNew k v l).Perm (Std.Internal.List.insertEntryIfNew k v l')
-- Mathlib.Topology.Germ
Filter.Germ.value_ofFun : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y) (x : X), (↑f).value = f x
-- Lean.Language.Basic
/-- Range that is marked as being processed by the server while the task is running.  -/
Lean.Language.SnapshotTask.reportingRange : {α : Type} → Lean.Language.SnapshotTask α → Lean.Language.SnapshotTask.ReportingRange
-- Mathlib.Algebra.Order.Quantale
Quantale.instMulRightMono : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α], MulRightMono α
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_singleton : ∀ (n : ℕ), {n}.multinomial = 1
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder.eq_def : ∀ (x : ℕ),
  x.largeSchroder =
    match x with
    | 0 => 1
    | n.succ => n.largeSchroder + ∑ i, (↑i).largeSchroder * (n - ↑i).largeSchroder
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.instAddCommMonoidDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        [inst_2 : DecidableEq ι] → (f : (i j : ι) → i ≤ j → G i →+ G j) → AddCommMonoid (AddCommGroup.DirectLimit G f)
-- Init.Data.Array.Find
Array.findIdx_eq_size : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.findIdx p xs = xs.size ↔ ∀ x ∈ xs, p x = false
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalM.run : {α : Type} → Lean.Meta.Grind.Goal → Lean.Meta.Grind.GoalM α → Lean.Meta.Grind.GrindM (α × Lean.Meta.Grind.Goal)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M] {X Y₂ : Cᵒᵖ} (φ : X ⟶ Y₂),
  (CategoryTheory.yonedaAddMonObj M).map φ =
    AddMonCat.ofHom { toFun := fun x => CategoryTheory.CategoryStruct.comp φ.unop x, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.mk.injEq : ∀ (symState : Lean.Meta.Sym.State) (grindState : Lean.Meta.Grind.State) (goals : List Lean.Meta.Grind.Goal)
  (cache : Lean.Elab.Tactic.Grind.Cache) (symState_1 : Lean.Meta.Sym.State) (grindState_1 : Lean.Meta.Grind.State)
  (goals_1 : List Lean.Meta.Grind.Goal) (cache_1 : Lean.Elab.Tactic.Grind.Cache),
  ({ symState := symState, grindState := grindState, goals := goals, cache := cache } =
      { symState := symState_1, grindState := grindState_1, goals := goals_1, cache := cache_1 }) =
    (symState = symState_1 ∧ grindState = grindState_1 ∧ goals = goals_1 ∧ cache = cache_1)
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.name : Aesop.LocalRuleSetMember → Aesop.RuleName
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.instInhabited : {R : Type u} → [Inhabited R] → Inhabited (WeierstrassCurve R)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.aleph0_eq_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 = Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 = c
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `F : C ⥤ Type w` and `C` is locally `w`-small, then `F` identifies to the composition
`shrinkYoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (CategoryOfElements.π F).op ⋙ colim`.  -/
CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      (F : CategoryTheory.Functor C (Type w)) →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape F.Elementsᵒᵖ (Type w)] →
          CategoryTheory.shrinkYoneda.{w, v₁, u₁}.comp
              (((CategoryTheory.Functor.whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj
                    (CategoryTheory.CategoryOfElements.π F).op).comp
                CategoryTheory.Limits.colim) ≅
            F
-- Mathlib.Algebra.Star.MonoidHom
/-- A *star monoid equivalence* is an equivalence preserving multiplication and the star
operation.  -/
StarMulEquiv : (A : Type u_6) → (B : Type u_7) → [Mul A] → [Mul B] → [Star A] → [Star B] → Type (max u_6 u_7)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
/-- A morphism of schemes `f : X ⟶ Y` is locally of finite type if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite type.
 -/
AlgebraicGeometry.LocallyOfFiniteType : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), h.coeff = h.liftPolyₗ { toFun := Polynomial.coeff, map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.yesWithDeltaI.sizeOf_spec : sizeOf Lean.Meta.ProjReductionKind.yesWithDeltaI = 1
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The cowedge corresponding to the explicit coend in `Type`  -/
CategoryTheory.Limits.Types.cowedge : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) → CategoryTheory.Limits.Cowedge F