mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- An aesop tactic for bulk cases on morphisms in `WidePushoutShape`  -/
CategoryTheory.Limits.WidePullbackShape.evalCasesBash : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [FaithfulSMul R S] [IsDedekindDomain S],
  IsDedekindDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.isoMk_hom_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.isoMk._auto_1)
  (a : E.I₀), (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).hom.s₀ a = s₀ a
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.append_denote : ∀ (ctx : Nat.Internal.Linear.Context) (p₁ p₂ : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (p₁ ++ p₂) =
    Nat.Internal.SOM.Poly.denote ctx p₁ + Nat.Internal.SOM.Poly.denote ctx p₂
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.exists_measurable_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β},
  MeasurableEmbedding f → ∀ {g : α → γ}, Measurable g → (∀ (a : β), Nonempty γ) → ∃ g', Measurable g' ∧ g' ∘ f = g
-- Std.Http.Transport
/-- Receives data, joining all available chunks.
 -/
Std.Http.Internal.Mock.Server.recv? : Std.Http.Internal.Mock.Server → optParam (Option UInt64) none → Std.Async.Async (Option ByteArray)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAtFilter_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {L : Filter (E × E)} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i}
  {φ' : (i : ι) → E →L[𝕜] F' i},
  HasFDerivAtFilter (fun x i => φ i x) (ContinuousLinearMap.pi φ') L ↔ ∀ (i : ι), HasFDerivAtFilter (φ i) (φ' i) L
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If `u` is a superset of `t` with the same (finite) measure (both sets possibly non-measurable),
then for any measurable set `s` one also has `μ (t ∩ s) = μ (u ∩ s)`.  -/
MeasureTheory.Measure.measure_inter_eq_of_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasurableSet s → μ t = μ u → t ⊆ u → μ t ≠ ⊤ → μ (t ∩ s) = μ (u ∩ s)
-- Lean.Util.SCC
Lean.SCC.Data.mk.injEq : ∀ (index? lowlink? : Option ℕ) (onStack : Bool) (index?_1 lowlink?_1 : Option ℕ) (onStack_1 : Bool),
  ({ index? := index?, lowlink? := lowlink?, onStack := onStack } =
      { index? := index?_1, lowlink? := lowlink?_1, onStack := onStack_1 }) =
    (index? = index?_1 ∧ lowlink? = lowlink?_1 ∧ onStack = onStack_1)
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
  Filter.bliminf u f p = sSup {a | ∀ᶠ (x : β) in f, p x → a ≤ u x}
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Function.Embedding.subtype.eq_1 : ∀ {α : Sort u_1} (p : α → Prop), Function.Embedding.subtype p = { toFun := Subtype.val, inj' := ⋯ }
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_inf : ∀ {α : Type u_1} [inst : LE α] (s t : LowerSet α), ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Convenience shortcut for `SemimoduleCat.hom_bijective.injective`.  -/
SemimoduleCat.hom_injective : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R}, Function.Injective SemimoduleCat.Hom.hom
-- Aesop.Search.Main
_private.Aesop.Search.Main.0.Aesop.expandNextGoal.fmt : {Q : Type} →
  [inst : Aesop.Queue Q] →
    Aesop.GoalId →
      Aesop.Percent →
        Lean.MVarId → Lean.Meta.SavedState → Except Lean.Exception Aesop.RuleResult → Aesop.SearchM Q Lean.MessageData
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = none ↔ t.contains k = false
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Γ → σ → σ)
  (q : Turing.TM1.Stmt Γ Λ σ) (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.load a q with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_3 a q
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_iff_neg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddRightStrictMono α] [AddRightReflectLT α] {a : α} (b : α),
  a + b < b ↔ a < 0
-- Init.Data.NeZero
ite.congr_simp : ∀ {α : Sort u} (c c_1 : Prop),
  c = c_1 →
    ∀ {h : Decidable c} [h_1 : Decidable c_1] (t t_1 : α),
      t = t_1 → ∀ (e e_1 : α), e = e_1 → (if c then t else e) = if c_1 then t_1 else e_1
-- Mathlib.Algebra.Ring.Prod
/-- Product of two `NonUnitalSemiring`s is a `NonUnitalSemiring`.  -/
Prod.instNonUnitalSemiring : {R : Type u_1} → {S : Type u_3} → [NonUnitalSemiring R] → [NonUnitalSemiring S] → NonUnitalSemiring (R × S)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postAdjunctionRight_unit_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {Y : D} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  (A : CategoryTheory.Over (G.obj Y)),
  (CategoryTheory.Over.postAdjunctionRight a).unit.app A = CategoryTheory.Over.homMk (a.unit.app A.left) ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ₄.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.preΨ₄ =
    2 * Polynomial.X ^ 6 + Polynomial.C W.b₂ * Polynomial.X ^ 5 + 5 * Polynomial.C W.b₄ * Polynomial.X ^ 4 +
            10 * Polynomial.C W.b₆ * Polynomial.X ^ 3 +
          10 * Polynomial.C W.b₈ * Polynomial.X ^ 2 +
        Polynomial.C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * Polynomial.X +
      Polynomial.C (W.b₄ * W.b₈ - W.b₆ ^ 2)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coeToAddHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N],
  AddMonoidHom.coeToAddHom = { coe := AddMonoidHom.toAddHom }
-- Mathlib.Order.WithBot
WithTop.le_coe : ∀ {α : Type u_1} {a b : α} [inst : LE α] {o : Option α}, b ∈ o → (o ≤ ↑a ↔ b ≤ a)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The product of the sections of a presheaf over a family of open sets.  -/
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} → TopCat.Presheaf C X → {ι : Type v'} → (ι → TopologicalSpace.Opens ↑X) → C
-- Mathlib.Tactic.TermCongr
/-- Given the pattern `t` in `congr(t)`, elaborate it for the given side
by replacing antiquotations with `cHole%` terms, and ensure the elaborated term
is of the expected type.  -/
Mathlib.Tactic.TermCongr.elaboratePattern : Lean.Term → Option Lean.Expr → Bool → Lean.Elab.TermElabM Lean.Expr
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev_ensureTermination_eq_toListRev : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] {it : Std.IterM m β}, it.ensureTermination.toListRev = it.toListRev
-- Std.Time.Date.Unit.Month
Std.Time.Month.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Month.Offset n
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `antivary_iff_exists_monotone_antitone`. -/
Antivary.exists_monotone_antitone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Antivary f g → ∃ x, Monotone f ∧ Antitone g
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_sdiff_cancel_left`. -/
Set.diff_diff_cancel_left : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → t \ (t \ s) = s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getEntryLE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match hkky : compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryLED k r ⟨ky, y⟩
      | Ordering.eq => ⟨ky, y⟩
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryLE k l ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rci α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.CategoryTheory.Category.PartialFun
/-- The equivalence induced by `PartialFunToPointed` and `PointedToPartialFun`.
`Part.equivOption` made functorial.  -/
partialFunEquivPointed : PartialFun ≌ Pointed
-- Init.Data.String.Lemmas.FindPos
String.posGT_eq_posGT_toSlice : ∀ {s : String} {p : String.Pos.Raw} (h : p < s.rawEndPos), s.posGT p h = String.Pos.ofToSlice (s.toSlice.posGT p ⋯)
-- Lean.Elab.InfoTree.Types
/-- Whether info trees should be recorded.  -/
Lean.Elab.InfoState.enabled : Lean.Elab.InfoState → Bool
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsClosedBelow.iInter : ∀ {ι : Type u} {f : ι → Set Ordinal.{u_1}} {o : Ordinal.{u_1}},
  (∀ (i : ι), Ordinal.IsClosedBelow (f i) o) → Ordinal.IsClosedBelow (⋂ i, f i) o
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.eq_of_eqOn_set_dense : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {s : Set R},
  NonUnitalSubring.closure s = ⊤ → ∀ {f g : R →ₙ+* S}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Lean.Parser.Types
Lean.Parser.instBEqCacheableParserContext.beq : Lean.Parser.CacheableParserContext → Lean.Parser.CacheableParserContext → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Boolean substructure of problems involving predicates on BitVec as atoms.
 -/
Std.Tactic.BVDecide.BVLogicalExpr : Type
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_nodal : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} {x : R},
  Polynomial.eval x (Lagrange.nodal s v) = ∏ i ∈ s, (x - v i)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- The canonical isomorphism `F.shift 0 ≅ F`.  -/
CategoryTheory.Functor.isoShiftZero : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        (F : CategoryTheory.Functor C A) →
          (M : Type u_4) →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] → [inst_4 : F.ShiftSequence M] → F.shift 0 ≅ F
-- Lean.Elab.Do.InferControlInfo
/-- The left identity of `ControlInfo.sequence`: a `ControlInfo` describing an element that always
falls through normally with a single regular exit.
 -/
Lean.Elab.Do.ControlInfo.pure : Lean.Elab.Do.ControlInfo
-- Mathlib.Topology.Algebra.ConstMulAction
MulOpposite.continuousConstSMul : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α],
  ContinuousConstSMul M αᵐᵒᵖ
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- Whiskering commutes with the enriched composition.  -/
CategoryTheory.eComp_eHomWhiskerRight : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' : C}
  (f : X ⟶ X') (Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X' Y Z) (CategoryTheory.eHomWhiskerRight V f Z) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerRight V f Y) (Y ⟶[V] Z))
      (CategoryTheory.eComp V X Y Z)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The canonical isomorphism `S.cycles ≅ kernel S.g`.  -/
CategoryTheory.ShortComplex.cyclesIsoKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasLeftHomology] →
          [inst_3 : CategoryTheory.Limits.HasKernel S.g] → S.cycles ≅ CategoryTheory.Limits.kernel S.g
-- Mathlib.Topology.Algebra.UniformConvergence
instGroupUniformFun : {α : Type u_1} → {β : Type u_2} → [Group β] → Group (UniformFun α β)
-- Batteries.Control.AlternativeMonad
ReaderT.instLawfulAlternative : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : AlternativeMonad m] [LawfulAlternative m],
  LawfulAlternative (ReaderT ρ m)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.postcomposeInvEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G) (c : CategoryTheory.Limits.Cone G),
  CategoryTheory.Limits.IsLimit.postcomposeInvEquiv α c = CategoryTheory.Limits.IsLimit.postcomposeHomEquiv α.symm c
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_toSubgroup : ∀ {G : Type u_3} [inst : AddGroup G] (H K : AddSubgroup G),
  (AddSubgroup.toSubgroup H).relIndex (AddSubgroup.toSubgroup K) = H.relIndex K
-- Init.Data.SInt.Lemmas
Int16.toInt_toBitVec : ∀ (x : Int16), x.toBitVec.toInt = x.toInt
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the maximum number of instances has been reached.  -/
Lean.Meta.Grind.checkMaxInstancesExceeded : Lean.Meta.Grind.GoalM Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1`, then `smoothingFun μ 1 ≤ 1`.  -/
smoothingFun_one_le : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R), μ 1 ≤ 1 → smoothingFun μ 1 ≤ 1
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.Label.move.sizeOf_spec : sizeOf Lean.Meta.NormCast.Label.move = 1
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- `R` consists of a single epimorphism.  -/
CategoryTheory.Presieve.regular.single_epi : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : C} {R : CategoryTheory.Presieve X}
  [self : R.regular],
  ∃ Y f, (R = CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) ∧ CategoryTheory.EffectiveEpi f
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.coe_centralizer : ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], ↑(Submonoid.centralizer S) = S.centralizer
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.activateInjectiveTheorems : Lean.Name → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictScalars_restrictSupportIdeal : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (s : Set (σ →₀ ℕ)) (hs : IsUpperSet s),
  Submodule.restrictScalars R (MvPolynomial.restrictSupportIdeal R s hs) = MvPolynomial.restrictSupport R s
-- Mathlib.Topology.Homotopy.Basic
/-- Deprecated. Use `map_continuous` instead.  -/
ContinuousMap.Homotopy.continuous : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), Continuous ⇑F
-- Mathlib.Order.Bounds.Basic
BddAbove.exists_ge : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] {s : Set γ}, BddAbove s → ∀ (x₀ : γ), ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_one : ∀ {R : Type u_1} {a b : R} [inst : Zero R] [inst_1 : One R], QuadraticAlgebra.C 1 = 1
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.vecMul_self_mul_conjTranspose_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R)
  (v : m → R), Matrix.vecMul v (A * A.conjTranspose) = 0 ↔ Matrix.vecMul v A = 0
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMulGroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : HNNExtension.NormalWord.TransversalPair G A B)
  (u : ℤˣ) (g : G),
  HNNExtension.NormalWord.unitsSMulGroup φ d u g = ((HNNExtension.toSubgroupEquiv φ u) (⋯.equiv g).1, (⋯.equiv g).2)
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.pushKind : Lean.Json.CompressWorkItemQueue✝ → Lean.Json.CompressWorkItemKind✝ → Lean.Json.CompressWorkItemQueue✝
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∏ᶜ I.left ⟶ ∏ᶜ I.right` via `I.snd` for limiting fans.  -/
CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        (c : CategoryTheory.Limits.Fan I.left) →
          {d : CategoryTheory.Limits.Fan I.right} → CategoryTheory.Limits.IsLimit d → (c.pt ⟶ d.pt)
-- Mathlib.Util.CompileInductive
/-- Generate compiled code for the recursor for `iv`, excluding the `sizeOf` function.
 -/
Mathlib.Util.compileInductiveOnly : Lean.InductiveVal → Lean.RecursorVal → optParam Bool true → Lean.MetaM Unit
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.inv_split : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α), if a = 0 then a⁻¹ = 0 else a * a⁻¹ = 1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A], NonUnitalSubsemiringClass (NonUnitalStarSubalgebra R A) A
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCallHierarchyItem : Hashable Lean.Lsp.CallHierarchyItem
-- Mathlib.Data.Sym.Sym2
Sym2.mk_surjective : ∀ {α : Type u_1}, Function.Surjective (Function.uncurry Sym2.mk)
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- A bundled version of `S.asLimitCone'` and `S.asLimit'`.  -/
LightProfinite.lim' : (S : LightProfinite) → CategoryTheory.Limits.LimitCone S.diagram'
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.continuousLinearMapAt_trivialization : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (x : B),
  Bundle.Trivialization.continuousLinearMapAt 𝕜 (Bundle.Trivial.trivialization B F) x = ContinuousLinearMap.id 𝕜 F
-- Lean.Meta.Basic
Lean.Meta.SavedState.meta : Lean.Meta.SavedState → Lean.Meta.State
-- Mathlib.Order.Filter.Map
/-- RHS form is used, e.g., in the definition of `UniformSpace`.  -/
Filter.mem_comap_prodMk : ∀ {α : Type u_1} {β : Type u_2} {x : α} {s : Set β} {F : Filter (α × β)},
  s ∈ Filter.comap (Prod.mk x) F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapMapIso_unitIso : ∀ {X Y : TopCat} (H : X ≅ Y),
  (TopologicalSpace.Opens.mapMapIso H).unitIso =
    CategoryTheory.NatIso.ofComponents (fun U => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.Order.Monotone.Defs
/-- **Alias** of the forward direction of `antitone_iff_apply₂`. -/
Antitone.apply₂ : ∀ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [inst : (i : ι) → Preorder (β i)] [inst_1 : Preorder α]
  {f : α → (i : ι) → β i}, Antitone f → ∀ (i : ι), Antitone fun x => f x i
-- Mathlib.Data.FinEnum.Option
/-- A recursor principle for finite-and-enumerable types, analogous to `Nat.recOn`.
It effectively says that every `FinEnum` is either `Empty` or `Option α`, up to an `Equiv` mediated
by `Fin`s of equal cardinality.
In contrast to the `Fintype` case, data can be transported along such an `Equiv`.
Also, since order matters, the choice of element that gets replaced by `Option.none` has
to be provided for every step.
 -/
FinEnum.recOnEmptyOption : {P : Type u → Sort v} →
  {α : Type u} →
    FinEnum α →
      ((n : ℕ) → Fin (n + 1)) →
        ({α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β) →
          P PEmpty.{u + 1} → ({α : Type u} → FinEnum α → P α → P (Option α)) → P α
-- Init.Data.Int.Gcd
Int.dvd_gcd_mul_gcd_iff_dvd_mul : ∀ {k n m : ℤ}, k ∣ ↑(k.gcd n) * ↑(k.gcd m) ↔ k ∣ n * m
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.map_app' : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (self : Q₁.IsometryEquiv Q₂) (m : M₁),
  Q₂ ((↑self.toLinearEquiv).toFun m) = Q₁ m
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The naturality condition.  -/
CategoryTheory.Lax.LaxTrans.Modification.naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Lax.LaxTrans.Modification η θ) {a b : B}
  (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (F.map f) (θ.app b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))
      (CategoryTheory.CategoryStruct.comp (θ.naturality f) h) =
    CategoryTheory.CategoryStruct.comp (η.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b)) h)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (QuadraticModuleCat R) (Type v)
-- Mathlib.Data.Num.Lemmas
PosNum.size.eq_1 : PosNum.one.size = 1
-- Mathlib.Data.Prod.Lex
Prod.Lex.instTransOrdLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β] [Std.TransOrd α] [Std.TransOrd β],
  Std.TransOrd (Lex (α × β))
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_nonempty : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet], G.edgeFinset.Nonempty ↔ G ≠ ⊥