mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.DeriveCountable
/-- Constructs a proof that the functions created by `mkToNatFuns` are injective.  -/
Mathlib.Deriving.Countable.mkInjThms : Lean.Elab.Deriving.Context → Array Lean.Name → Lean.Elab.TermElabM (Lean.TSyntax `command)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Stability under pullback. Use `GrothendieckTopology.pullback_stable`.  -/
CategoryTheory.GrothendieckTopology.pullback_stable' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X Y : C⦄
  ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ self.sieves X → CategoryTheory.Sieve.pullback f S ∈ self.sieves Y
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.exp_half_dist : ∀ (z w : UpperHalfPlane), Real.exp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.linear_ne_zero_of_im : ∀ {cd : Fin 2 → ℝ} {z : ℂ}, z.im ≠ 0 → cd ≠ 0 → ↑(cd 0) * z + ↑(cd 1) ≠ 0
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.Model.split.congr_simp : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice}
  (firstRejected firstRejected_1 : s.Pos) (e_firstRejected : firstRejected = firstRejected_1) (curr curr_1 : s.Pos)
  (e_curr : curr = curr_1) (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    String.Slice.Pattern.Model.split pat firstRejected_1 curr_1 ⋯
-- Init.Data.UInt.Lemmas
UInt16.neg_zero : -0 = 0
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingAddSubgroup_compl_iff_movedBy_subset : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {m : M},
  m ∈ fixingAddSubgroup M sᶜ ↔ (AddAction.fixedBy α m)ᶜ ⊆ s
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.graph.eq_1 : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α),
  Tuple.graph f = Finset.image (fun i => (f i, i)) Finset.univ
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct a morphism `A ⟶ B` of `AddGrp C` from a map `f : A.X ⟶ A.X` and a `IsAddMonHom f`
instance. -/
CategoryTheory.AddGrp.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : CategoryTheory.AddGrp C} → (f : A.X ⟶ B.X) → [CategoryTheory.IsAddMonHom f] → A ⟶ B
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.comp_apply : ∀ {X Y Z : TopCat} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : TopCat.Homotopy g₀ g₁) (F : TopCat.Homotopy f₀ f₁)
  (x : ↑unitInterval × ↑X), (G.comp F) x = G (x.1, F x)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_neg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Set α), ⇑f '' (-s) = -⇑f '' s
-- Std.Data.DTreeMap.Internal.WF.Defs
_private.Std.Data.DTreeMap.Internal.WF.Defs.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.isLocalizedModule : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  (p : Submonoid R) [IsLocalization p S] [IsLocalization (Algebra.algebraMapSubmonoid A p) B],
  IsLocalizedModule p (↑R (KaehlerDifferential.map R S A B))
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The cokernel of `f.op` is the opposite of `kernel f`.  -/
CategoryTheory.cokernelOpOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.cokernel f.op ≅ Opposite.op (CategoryTheory.Limits.kernel f)
-- Mathlib.Combinatorics.Colex
Finset.Colex.initSeg.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Fintype α] (s : Finset α),
  Finset.Colex.initSeg s = {t | s.card = t.card ∧ toColex t ≤ toColex s}
-- Mathlib.Topology.Order.ExtrClosure
IsMinOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y]
  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X},
  IsMinOn f s a → ContinuousOn f (closure s) → IsMinOn f (closure s) a
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivisionMonoid : {α : Type u_1} → [DivisionMonoid α] → DivisionMonoid (Colex α)
-- Mathlib.Topology.Algebra.MulAction
continuousSMul_iInf : ∀ {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : SMul M X]
  {ts' : ι → TopologicalSpace X}, (∀ (i : ι), ContinuousSMul M X) → ContinuousSMul M X
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An inequality of subobjects is witnessed by some morphism between the corresponding objects.  -/
CategoryTheory.Subobject.ofLEMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A : C} →
      (X : CategoryTheory.Subobject B) →
        (f : A ⟶ B) →
          [inst_1 : CategoryTheory.Mono f] →
            X ≤ CategoryTheory.Subobject.mk f → (CategoryTheory.Subobject.underlying.obj X ⟶ A)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_left_of_integrable_add_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    0 ≤ᵐ[μ] f → 0 ≤ᵐ[μ] g → MeasureTheory.Integrable (f + g) μ → MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso],
  P.op.RespectsIso
-- Mathlib.Order.Category.Lat
Lat.dualEquiv_functor : Lat.dualEquiv.functor = Lat.dual
-- Aesop.Rule
Aesop.NormRuleInfo.penalty : Aesop.NormRuleInfo → ℤ
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
/-- A Zariski-`1`-hypercover of a scheme where all components are affine.  -/
AlgebraicGeometry.Scheme.affineOneHypercover : (X : AlgebraicGeometry.Scheme) → AlgebraicGeometry.Scheme.zariskiTopology.OneHypercover X
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse : ∀ {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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.η e.inverse)) =
    CategoryTheory.Functor.LaxMonoidal.ε e.functor
-- Std.Http.Data.Headers.Value
Std.Http.Header.instBEqValue.beq : Std.Http.Header.Value → Std.Http.Header.Value → Bool
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.of_fst : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  (CategoryTheory.AdditiveFunctor.of F).obj = F
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.le_sSupFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {c : Set (HahnEmbedding.Partial seed)} (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c) {f : HahnEmbedding.Partial seed},
  f ∈ c → ↑f ≤ HahnEmbedding.Partial.sSupFun hc
-- Mathlib.RingTheory.Smooth.StandardSmooth
/-- An `R`-algebra `S` is called standard smooth of relative dimension `n`, if there exists
a submersive presentation of dimension `n`.
 -/
Algebra.IsStandardSmoothOfRelativeDimension : ℕ → (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftPath_lifts : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) (γ : C(↑unitInterval, X)) (e : E) (γ_0 : γ 0 = p e), p ∘ ⇑(cov.liftPath γ e γ_0) = ⇑γ
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.sub_const : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableSub G], AEMeasurable f μ → ∀ (c : G), AEMeasurable (fun x => f x - c) μ
-- Batteries.Data.List.Basic
/-- `getRest l l₁` returns `some l₂` if `l = l₁ ++ l₂`.
If `l₁` is not a prefix of `l`, returns `none`  -/
List.getRest : {α : Type u_1} → [DecidableEq α] → List α → List α → Option (List α)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_sUnion : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set (Set R)),
  Subsemiring.closure (⋃₀ s) = ⨆ t ∈ s, Subsemiring.closure t
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.bot_lt_toWithBotSyn_apply_iff : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : WithBot (σ →₀ ℕ)), ⊥ < m.toWithBotSyn a ↔ ⊥ < a
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
AlgebraicIndependent.integralClosure : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x → ∀ [NoZeroDivisors A], AlgebraicIndependent (↥(integralClosure R A)) x
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.isBasis_insert_sdiff_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} {B : Set α},
  M.IsBasis B X → e ∈ M.closure (insert f B \ {e}) → e ∈ insert f B → f ∈ X → M.IsBasis (insert f B \ {e}) X
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → (AlgebraicGeometry.Spec (X.presheaf.stalk x)).Over X
-- Lean.Meta.Tactic.Grind.Ctor
_private.Lean.Meta.Tactic.Grind.Ctor.0.Lean.Meta.Grind.propagateInjEqs : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.M : (Type → Type) → Type → Type
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getElem?_filter` when `LawfulBEq` is available.  -/
Std.HashMap.getElem?_filter' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {f : α → β → Bool}
  {k : α}, (Std.HashMap.filter f m)[k]? = Option.filter (f k) m[k]?
-- Mathlib.ModelTheory.Syntax
/-- The sentence indicating that a basic relation symbol is reflexive.  -/
FirstOrder.Language.Relations.reflexive : {L : FirstOrder.Language} → L.Relations 2 → L.Sentence
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.mul_inv_mul_mul_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.mk.inj : ∀ {α β σ : Type} {name : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam} {mkInitial : IO σ}
  {ofOLeanEntry : σ → α → Lean.ImportM β} {toOLeanEntry : β → α} {addEntry : σ → β → σ} {finalizeImport : σ → σ}
  {exportEntry? : Lean.Environment → α → Lean.OLeanEntries (Option α)}
  {name_1 : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam} {mkInitial_1 : IO σ}
  {ofOLeanEntry_1 : σ → α → Lean.ImportM β} {toOLeanEntry_1 : β → α} {addEntry_1 : σ → β → σ} {finalizeImport_1 : σ → σ}
  {exportEntry?_1 : Lean.Environment → α → Lean.OLeanEntries (Option α)},
  { name := name, mkInitial := mkInitial, ofOLeanEntry := ofOLeanEntry, toOLeanEntry := toOLeanEntry,
        addEntry := addEntry, finalizeImport := finalizeImport, exportEntry? := exportEntry? } =
      { name := name_1, mkInitial := mkInitial_1, ofOLeanEntry := ofOLeanEntry_1, toOLeanEntry := toOLeanEntry_1,
        addEntry := addEntry_1, finalizeImport := finalizeImport_1, exportEntry? := exportEntry?_1 } →
    name = name_1 ∧
      mkInitial = mkInitial_1 ∧
        ofOLeanEntry = ofOLeanEntry_1 ∧
          toOLeanEntry = toOLeanEntry_1 ∧
            addEntry = addEntry_1 ∧ finalizeImport = finalizeImport_1 ∧ exportEntry? = exportEntry?_1
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.mono_simpleSubobjectArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} [inst_3 : CategoryTheory.IsArtinianObject X]
  (h : ¬CategoryTheory.Limits.IsZero X), CategoryTheory.Mono (CategoryTheory.simpleSubobjectArrow h)
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
NNReal.tendsto_rpow_atTop : ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => x ^ y) Filter.atTop Filter.atTop
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m),
  (Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun x => x ≠ k) True = M k k • 1
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `Prod.snd` as a bundled `MulActionHom`.  -/
MulActionHom.snd : (M : Type u_1) → (α : Type u_2) → (β : Type u_3) → [inst : SMul M α] → [inst_1 : SMul M β] → α × β →ₑ[id] β
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mrange_eq : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : Monoid.Coprod M N →* P),
  MonoidHom.mrange f = MonoidHom.mrange (f.comp Monoid.Coprod.inl) ⊔ MonoidHom.mrange (f.comp Monoid.Coprod.inr)
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F` preserves finite coproducts (G5).  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteCoproducts : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.PreGaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.PreservesFiniteCoproducts F
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.eventuallyLE : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g → ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
-- Std.Time.Duration
Std.Time.instTransOrdDuration : Std.TransOrd Std.Time.Duration
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix; this is the basis for `S`. See
* `Ideal.selfBasis` for the basis on `I`,
* `Ideal.smithCoeffs` for the entries of the diagonal matrix
* `Ideal.selfBasis_def` for the proof that the inclusion map forms a square diagonal matrix.
 -/
Ideal.ringBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [IsDomain R] →
        [IsPrincipalIdealRing R] →
          {S : Type u_4} →
            [inst_3 : CommRing S] →
              [IsDomain S] →
                [inst_5 : Algebra R S] → [Finite ι] → Module.Basis ι R S → (I : Ideal S) → I ≠ ⊥ → Module.Basis ι R S
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_3.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.IterM Id ((a : α) × β a) → Sort u_3) (k : α) (v : β k)
  (l : Std.DHashMap.Internal.AssocList α β)
  (h_1 : Unit → motive { internalState := { l := Std.DHashMap.Internal.AssocList.nil } })
  (h_2 :
    (k : α) →
      (v : β k) →
        (l : Std.DHashMap.Internal.AssocList α β) →
          motive { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } }),
  (match { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } } with
    | { internalState := { l := Std.DHashMap.Internal.AssocList.nil } } => h_1 ()
    | { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } } => h_2 k v l) =
    h_2 k v l
-- Lean.Meta.Check
/-- Throw an exception if `e` cannot be type checked using the kernel.
This function is used for debugging purposes only.
Be sure to share common expressions in `e` before calling this function for good performance.
 -/
Lean.Meta.checkWithKernel : Lean.Expr → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.CommSq.cocone_inl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} (s : CategoryTheory.CommSq f g h i), s.cocone.inl = h
-- Lean.Elab.Coinductive
/-- Generates `casesOn` eliminators for coinductive predicates.
These eliminators allow pattern matching on coinductive predicates,
enabling case analysis in proofs.
 -/
_private.Lean.Elab.Coinductive.0.Lean.Elab.Command.mkCasesOnCoinductive : Array Lean.InductiveVal → Lean.MetaM Unit
-- Mathlib.Data.Finset.Sups
Finset.diffs_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s : Finset α}, s.diffs ∅ = ∅
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.M.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommMonCat),
  CommMonCat.FilteredColimits.M F = MonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is absolutely continuous on `uIcc a b`, then `f` is continuous on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.continuousOn : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → ContinuousOn f (Set.uIcc a b)
-- Mathlib.Topology.Constructions
Continuous.subtype_coind : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
  Continuous f → ∀ (hp : ∀ (x : Y), p (f x)), Continuous (Subtype.coind f hp)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_dist_eq_diam : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], ∃ u v, G.dist u v = G.diam
-- Mathlib.Topology.Category.TopPair
/-- Constructor for a topological pair (X, A) where A ⊆ X.  -/
TopPair.ofSubset : {X : TopCat} → Set ↑X → TopPair
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- `ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`,
for idempotent `f`.  -/
ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → ((↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = f ∘SL T)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorizationEquiv_apply : ∀ (x : ℕ+),
  Nat.factorizationEquiv x =
    match x with
    | ⟨n, property⟩ => ⟨n.factorization, ⋯⟩
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp k ((t.insert k v).maxKey ⋯)).isLE = true
-- Lean.Elab.Tactic.Simp
/-- Elaborate extra simp theorems provided to `simp`. `stx` is of the form `"[" simpTheorem,* "]"`
If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
this option only makes sense for `simp_all` or `*` is used.
When `recover := true`, try to recover from errors as much as possible so that users keep seeing
the current goal.
 -/
Lean.Elab.Tactic.elabSimpArgs : Lean.Syntax →
  Lean.Meta.Simp.Context →
    Lean.Meta.Simp.SimprocsArray →
      Bool →
        Lean.Elab.Tactic.SimpKind → optParam Bool false → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.ElabSimpArgsResult
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv_unitIso : ∀ {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.coneOpEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
-- Mathlib.RingTheory.Multiplicity
multiplicity_pos_of_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → 0 < multiplicity a b
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The non-unital subsemiring generated by a set includes the set.  -/
NonUnitalSubsemiring.subset_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R}, s ⊆ ↑(NonUnitalSubsemiring.closure s)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_mem_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α} {a b : α}, a ∈ s → b ∈ t → a * b ∈ s * t
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.beq.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (h_1 : Unit → motive [] [])
  (h_2 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs))
  (h_3 : (x x_1 : List α) → motive x x_1),
  (match [], [] with
    | [], [] => h_1 ()
    | a :: as, b :: bs => h_2 a as b bs
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.liftPropWithinAt_iff' : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M')
  (s : Set M) (x : M),
  ChartedSpace.LiftPropWithinAt P f s x ↔
    ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
-- Mathlib.LinearAlgebra.Isomorphisms
/-- Second Isomorphism Law : the canonical map from `p/(p ∩ p')` to `(p+p')/p'` as a linear isomorphism.

Note that in the following declaration the type of the domain is expressed using
`comap p.subtype p ⊓ comap p.subtype p'`
instead of
`comap p.subtype (p ⊓ p')`
because the former is the simp normal form (see also `Submodule.comap_inf`).  -/
LinearMap.quotientInfEquivSupQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (p p' : Submodule R M) →
            (↥p ⧸ Submodule.comap p.subtype p ⊓ Submodule.comap p.subtype p') ≃ₗ[R]
              ↥(p ⊔ p') ⧸ Submodule.comap (p ⊔ p').subtype p'
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
rel_iff_cov : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) [CovariantClass M N μ r] [ContravariantClass M N μ r]
  (m : M) {a b : N}, r (μ m a) (μ m b) ↔ r a b
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_pos : ∀ {α : Type u_1} [Finite α] [h : Nonempty α], 0 < Nat.card α