mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The gluing of two good path objects.  -/
HomotopicalAlgebra.PathObject.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {A : C} →
        [HomotopicalAlgebra.IsFibrant A] →
          HomotopicalAlgebra.PathObject A →
            (P' : HomotopicalAlgebra.PathObject A) → [P'.IsGood] → HomotopicalAlgebra.PathObject A
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKey! k = default
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grindStep : Lean.ParserDescr
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.mk.inj : ∀ {mvarId : Lean.MVarId} {subst : Lean.Meta.FVarSubst} {numNewEqs : ℕ} {mvarId_1 : Lean.MVarId}
  {subst_1 : Lean.Meta.FVarSubst} {numNewEqs_1 : ℕ},
  { mvarId := mvarId, subst := subst, numNewEqs := numNewEqs } =
      { mvarId := mvarId_1, subst := subst_1, numNewEqs := numNewEqs_1 } →
    mvarId = mvarId_1 ∧ subst = subst_1 ∧ numNewEqs = numNewEqs_1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.Context.mk.sizeOf_spec : ∀ (bvars : List Lean.FVarId), sizeOf { bvars := bvars } = 1 + sizeOf bvars
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_whiskerLeft : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y₁ Y₂ : Rep.{u, u, v} k G} (f : Y₁ ⟶ Y₂),
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
    Representation.IntertwiningMap.lTensor X.ρ (Rep.Hom.hom f)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.Pretriangulated.rotCompInvRot = CategoryTheory.Pretriangulated.rotCompInvRot
-- Mathlib.Algebra.Module.Defs
/-- Scalar multiplication distributes over addition from the right.  -/
Module.add_smul : ∀ {R : Type u} {M : Type v} {inst : Semiring R} {inst_1 : AddCommMonoid M} [self : Module R M] (r s : R) (x : M),
  (r + s) • x = r • x + s • x
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) {s : Set (G × ((i : ι) → Em i))}
  {x : G × ((i : ι) → Em i)}, AnalyticWithinAt 𝕜 (fun p => (f p.1) p.2) s x
-- Init.Data.String.Pattern.Basic
/-- Checks whether the slice starts with the pattern. If it does, the slice is returned with the
  prefix removed; otherwise the result is `none`.
   -/
String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? : {ρ : Type} →
  (pat : ρ) → [self : String.Slice.Pattern.ForwardPattern pat] → (s : String.Slice) → s.isEmpty = false → Option s.Pos
-- Mathlib.Logic.Encodable.Basic
Directed.sequence_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] [inst_2 : Preorder β] {f : α → β}
  (hf : Directed (fun x1 x2 => x1 ≤ x2) f), Monotone (f ∘ Directed.sequence f hf)
-- Mathlib.CategoryTheory.Category.Pointed
/-- the underlying map  -/
Pointed.Hom.toFun : {X Y : Pointed} → X.Hom Y → X.X → Y.X
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instSeparableSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [TopologicalSpace.SeparableSpace M], TopologicalSpace.SeparableSpace Mᵈᵐᵃ
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Trivialization.linearEquivAt.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1) [inst_8 : Bundle.Trivialization.IsLinear R e]
  (b : B) (hb : b ∈ e.baseSet),
  Bundle.Trivialization.linearEquivAt R e b hb = Bundle.Trivialization.linearEquivAt R e_1 b ⋯
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.toBitVec_maxValueSealed_eq_intMaxSealed : Int8.maxValueSealed✝.toBitVec = BitVec.Signed.intMaxSealed✝ 8
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mul_right_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (u : M₀ˣ) {a : M₀}, ↑u * a = 0 ↔ a = 0
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_transvection : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : CommRing R]
  [inst_2 : DecidableEq m] {i j : m}, b i ≤ b j → ∀ (c : R), (Matrix.transvection i j c).BlockTriangular b
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Change `n` in `(c : Composition n)` to a propositionally equal value.  -/
Composition.cast : {n m : ℕ} → Composition m → m = n → Composition n
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_eq_zero_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] (f : CauSeq β abv),
  f.lim = 0 ↔ f.LimZero
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNormClass.toSeminormClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} [inst : SeminormedCommRing R] {S : outParam (Type u_3)} [inst_1 : Ring S]
  [inst_2 : Algebra R S] [inst_3 : FunLike F S ℝ] [self : AlgebraNormClass F R S], SeminormClass F R S
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.aedisjoint : ∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsFundamentalDomain._auto_1},
  MeasureTheory.IsFundamentalDomain G s μ → Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g • s)
-- Mathlib.Algebra.Group.ModEq
/-- `a ≡ b [PMOD p]` means that `b` is congruent to `a` modulo `p`.

If `a`, `b` are elements of an additive group,
then `a ≡ b [PMOD p]` iff `m • p = b - a` for some `m : ℤ`, see `modEq_iff_zsmul` below.
For additive commutative monoid, the definition is given by `modEq_iff_nsmul`.

Equivalently (as shown in `Algebra.Order.ToIntervalMod`), `b` does not lie in the open interval
`(a, a + p)` modulo `p`, or `toIcoMod hp a` disagrees with `toIocMod hp a` at `b`, or
`toIcoDiv hp a` disagrees with `toIocDiv hp a` at `b`.  -/
AddCommGroup.ModEq : {M : Type u_1} → [AddCommMonoid M] → M → M → M → Prop
-- Init.Data.List.Control
List.findSome?.eq_def : ∀ {α : Type u} {β : Type v} (f : α → Option β) (x : List α),
  List.findSome? f x =
    match x with
    | [] => none
    | a :: as =>
      match f a with
      | some b => some b
      | none => List.findSome? f as
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {a : α}, t.WF → (t.insert a).WF
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedQueryString` from a `ByteArray` with compile-time proofs.
Use this when you have proofs that the byte array is valid.
 -/
Std.Http.URI.EncodedQueryString.new : {r : UInt8 → Bool} →
  (ba : ByteArray) →
    Std.Http.URI.IsAllowedEncodedQueryChars r ba →
      Std.Http.URI.isValidPercentEncoding ba = true → Std.Http.URI.EncodedQueryString r
-- Mathlib.RingTheory.WittVector.Identities
WittVector.verschiebung_frobenius_comm : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p],
  Function.Commute ⇑WittVector.verschiebung ⇑WittVector.frobenius
-- Init.Data.SInt.Lemmas
Int32.ofInt_int8ToInt : ∀ (x : Int8), Int32.ofInt x.toInt = x.toInt32
-- Batteries.Data.AssocList
Batteries.AssocList.beq_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] {l m : Batteries.AssocList α β},
  (l == m) = (l.toList == m.toList)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.extension_unique : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [T0Space β]
  [CompleteSpace β],
  UniformContinuous f →
    ∀ {g : UniformSpace.Completion α → β},
      UniformContinuous g → (∀ (a : α), f a = g ↑a) → UniformSpace.Completion.extension f = g
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_iff_isLittleO : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F},
  HasGradientWithinAt f f' s x ↔ (fun x' => f x' - f x - inner 𝕜 f' (x' - x)) =o[nhdsWithin x s] fun x' => x' - x
-- Mathlib.Topology.Order.AtTopBotIxx
map_coe_Ioi_atBot : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] (a : X),
  autoParam (Order.IsPredPrelimit a) map_coe_Ioi_atBot._auto_1 →
    Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `Config` which calls `intro` on each goal before applying lemmas.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.intros : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } → Lean.Meta.SolveByElim.SolveByElimConfig
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.un.inj : ∀ {w : ℕ} {op : Std.Tactic.BVDecide.BVUnOp} {operand : Std.Tactic.BVDecide.BVExpr w} {op_1 : Std.Tactic.BVDecide.BVUnOp}
  {operand_1 : Std.Tactic.BVDecide.BVExpr w},
  Std.Tactic.BVDecide.BVExpr.un op operand = Std.Tactic.BVDecide.BVExpr.un op_1 operand_1 →
    op = op_1 ∧ operand = operand_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keys.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  t.keys = Std.DTreeMap.Internal.Impl.foldr (fun k x l => k :: l) [] t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : Inhabited α]
  (h : t.WF) {l : List α} {k k' : α},
  compare k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
        k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey! k' = k
-- Init.Data.Nat.Basic
Nat.add_lt_add_right : ∀ {n m : ℕ}, n < m → ∀ (k : ℕ), n + k < m + k
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.coassoc_symm_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A),
  (TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A CoalgebraStruct.comul) (CoalgebraStruct.comul a)) =
    (LinearMap.rTensor A CoalgebraStruct.comul) (CoalgebraStruct.comul a)
-- Init.Data.SInt.Lemmas
Int64.ofInt_eq_ofIntLE_mod : ∀ {a b : ℤ} (ha₁ : Int64.minValue.toInt ≤ a) (ha₂ : a ≤ Int64.maxValue.toInt) (hb₁ : Int64.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int64.maxValue.toInt), Int64.ofInt (a.tmod b) = Int64.ofIntLE a ha₁ ha₂ % Int64.ofIntLE b hb₁ hb₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokens.toJson : Lean.Lsp.SemanticTokens → Lean.Json
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative additive groups preserves limits of
arbitrary size.  -/
AddCommGrpCat.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} AddCommGrpCat.uliftFunctor
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.delete_subset : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (arr : Array ℕ),
  ∀ c ∈ (f.delete arr).toList, c ∈ f.toList
-- Init.Data.Int.DivMod.Lemmas
Int.neg_fdiv_of_dvd : ∀ {a b : ℤ}, b ∣ a → (-a).fdiv b = -a.fdiv b
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
/-- A sequence of measurable functions that are equal to `f` and verify property `p` on the
measurable set `aeSeqSet hf p`.  -/
aeSeq : {ι : Sort u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] →
          {f : ι → α → β} →
            {μ : MeasureTheory.Measure α} → (∀ (i : ι), AEMeasurable (f i) μ) → (α → (ι → β) → Prop) → ι → α → β
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_neg_left : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b : ℤ), IsEllipticNet.atom W (-a) b = IsEllipticNet.atom W a b
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.instModuleR : (σ K : Type u) → [inst : Fintype K] → [inst_1 : CommRing K] → Module K (MvPolynomial.R σ K)
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- `Matrix.mkLiteralQ !![a, b; c, d]` produces the term `q(!![$a, $b; $c, $d])`.  -/
Matrix.mkLiteralQ : {u : Lean.Level} → {α : Q(Type u)} → {m n : ℕ} → Matrix (Fin m) (Fin n) Q(«$α») → Q(Matrix (Fin «$m») (Fin «$n») «$α»)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.isHermitian_degMatrix : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : NonAssocSemiring R] [inst_4 : StarRing R], (SimpleGraph.degMatrix R G).IsHermitian
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_nsmul : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R),
  WittVector.ghostFun✝ (m • x) = m • WittVector.ghostFun✝ x
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instInhabitedDiscreteUnit : Inhabited (AlgebraicGeometry.SheafedSpace (CategoryTheory.Discrete Unit))
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNonUnitalCommRingOfIsTopologicalRing : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalCommRing β] → [IsTopologicalRing β] → NonUnitalCommRing (CompactlySupportedContinuousMap α β)
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.genericPoint_eq_bot_of_affine : ∀ (R : CommRingCat) [inst : IsDomain ↑R], genericPoint ↥(AlgebraicGeometry.Spec R) = ⊥
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.constantCoeff_rename : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] {τ : Type u_6} (f : σ → τ) (φ : MvPolynomial σ R),
  MvPolynomial.constantCoeff ((MvPolynomial.rename f) φ) = MvPolynomial.constantCoeff φ
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set of right differentiability points of a function, with derivative in a given complete
set, is Borel-measurable.  -/
measurableSet_of_differentiableWithinAt_Ici_of_isComplete : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) {K : Set F},
  IsComplete K → MeasurableSet {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K}
-- Mathlib.Algebra.BigOperators.Fin
finSigmaFinEquiv.eq_1 : ∀ (n_2 : Fin 0 → ℕ), finSigmaFinEquiv = Equiv.equivOfIsEmpty ((i : Fin 0) × Fin (n_2 i)) (Fin (∑ i, n_2 i))
-- Mathlib.Data.Real.Pointwise
Real.sInf_smul_of_nonneg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : MulActionWithZero α ℝ]
  [IsOrderedModule α ℝ] {a : α}, 0 ≤ a → ∀ (s : Set ℝ), sInf (a • s) = a • sInf s
-- Mathlib.Order.Heyting.Regular
Heyting.isRegular_bot : ∀ {α : Type u_1} [inst : HeytingAlgebra α], Heyting.IsRegular ⊥
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M},
  ↑((FirstOrder.Language.Substructure.closure L).toFun s) = Set.range (FirstOrder.Language.Term.realize Subtype.val)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq_spec_1 : ∀ (a : Lean.Grind.CommRing.Var) (a_1 : ℕ) (b : Lean.Grind.CommRing.Var) (b_1 : ℕ),
  ({ x := a, k := a_1 } == { x := b, k := b_1 }) = (a == b && a_1 == b_1)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- If `n % 4 = 3`, then `χ₄ n = -1`.  -/
ZMod.χ₄_nat_three_mod_four : ∀ {n : ℕ}, n % 4 = 3 → ZMod.χ₄ ↑n = -1
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat iX],
  AlgebraicGeometry.IsAffineOpen US →
    AlgebraicGeometry.IsAffineOpen UX →
      IsCompact ↑UT → CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Lean.DocString.Types
/-- A sequence of inline elements.
 -/
Lean.Doc.Inline.concat : {i : Type u} → Array (Lean.Doc.Inline i) → Lean.Doc.Inline i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R) (u v : R),
  W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.nondegenerate_toLinearMap₂_iff : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂), ((Matrix.toLinearMap₂ b₁ b₂) M).Nondegenerate ↔ M.Nondegenerate
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosZeta_apply_zero : ∀ (a : UnitAddCircle), HurwitzZeta.cosZeta a 0 = -1 / 2
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instInhabitedTacticParsedSnapshotInner : {α : Type} → Inhabited (Lean.Elab.Tactic.TacticParsedSnapshotInner α)
-- Mathlib.Probability.ProductMeasure
MeasureTheory.integral_infinitePi_of_piFinset : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : DecidableEq ι] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {s : Finset ι} {f : ((i : ι) → X i) → E},
  MeasureTheory.StronglyMeasurable f →
    ∀ (x : (i : ι) → X i),
      ∫ (y : (i : ι) → X i), f y ∂MeasureTheory.Measure.infinitePi μ =
        ∫ (y : (i : ↥s) → X ↑i), f (Function.updateFinset x s y) ∂MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.equiv_functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  CategoryTheory.Functor.equiv.functor.obj F = F.obj { as := PUnit.unit }
-- Mathlib.Probability.Kernel.Disintegration.Basic
/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.

A conditional kernel for `κ : Kernel α (β × Ω)` where `α` is countable and `Ω` is a measurable
space.  -/
ProbabilityTheory.Kernel.condKernelCountable : {α : Type u_1} →
  {β : Type u_2} →
    {Ω : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mΩ : MeasurableSpace Ω} →
            [Countable α] →
              (κCond : α → ProbabilityTheory.Kernel β Ω) →
                (∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) → ProbabilityTheory.Kernel (α × β) Ω
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The underlying space of `Spec (𝒪ₓ(U)/I(U))` is homeomorphic to its image in `X`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjCarrierIso : {X : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) →
    (U : ↑X.affineOpens) → ↑(I.glueDataObj U).toPresheafedSpace ≅ TopCat.of ↑(X.zeroLocus ↑(I.ideal U) ∩ ↑↑U)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer.eq_2 : ∀ (S : Type u) [inst : Semiring S] (n : ℕ),
  ascPochhammer S n.succ = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header : Type
-- Batteries.Recycling.RBTree.Basic
/-- True if `x` is equivalent to an element of `t`.  -/
RBTree.RBSet.Mem : {α : Type u_1} → {cmp : α → α → Ordering} → α → RBTree.RBSet α cmp → Prop
-- Mathlib.Algebra.Group.Basic
mul_div_div_cancel : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), a * b / (a / c) = b * c
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform.vadd_finset_snd_subset_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] {e : α} {x : Finset α × Finset α},
  e +ᵥ (Finset.addDysonETransform e x).2 ⊆ (Finset.addDysonETransform e x).1
-- Mathlib.Order.Circular.ZMod
instCircularOrderZMod : (n : ℕ) → CircularOrder (ZMod n)
-- Mathlib.Algebra.Group.Semiconj.Units
AddSemiconjBy.addUnits_neg_right_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M}, AddSemiconjBy a ↑(-x) ↑(-y) ↔ AddSemiconjBy a ↑x ↑y
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.coe_toInfTopHom : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β),
  ⇑f.toInfTopHom = ⇑f
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.eq_zero_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {l : Filter α}, f'' =Θ[l] g'' → ∀ᶠ (x : α) in l, f'' x = 0 ↔ g'' x = 0
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofSubsingleton_symm_apply : ∀ {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Subsingleton M]
  [inst_6 : Subsingleton M₂] (x : M₂), (LinearEquiv.ofSubsingleton M M₂).symm x = 0
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.casesPatterns.injEq : ∀ (pats pats_1 : Array Aesop.CasesPattern),
  (Aesop.Frontend.BuilderOption.casesPatterns pats = Aesop.Frontend.BuilderOption.casesPatterns pats_1) =
    (pats = pats_1)
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.instIsScalarTowerLocalizationAtPrime : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (p : Ideal (Localization M)) [inst_1 : p.IsPrime],
  IsScalarTower R (Localization M) (Localization.AtPrime p)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_neg : ∀ {M : Type u_1} (s : Set M) [inst : AddGroup M], SimpleGraph.addCayley (-s) = SimpleGraph.addCayley s
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
/-- Asymptotic lower bound on the **Ruzsa-Szemerédi problem**.

There exists a graph with `n` vertices and `Ω((n ^ 2 * exp (-4 * √(log n))))` edges such that
each edge belongs to exactly one triangle.  -/
ruzsaSzemerediNumberNat_asymptotic_lower_bound : (fun n => ↑n ^ 2 * Real.exp (-4 * √(Real.log ↑n))) =O[Filter.atTop] fun n => ↑(ruzsaSzemerediNumberNat n)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.instAssociativeUnion : ∀ {α : Type u_1} [inst : DecidableEq α], Std.Associative fun x1 x2 => x1 ∪ x2
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
NNRealRMK.rieszMeasure.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ Λ_1 : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal),
  Λ = Λ_1 →
    ∀ [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X] [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X],
      NNRealRMK.rieszMeasure Λ = NNRealRMK.rieszMeasure Λ_1