mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.coe_toContinuousLinearMap : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ), ⇑↑φ.toContinuousLinearEquiv = ⇑φ
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_pow : ∀ {R : Type u} [inst : CommSemiring R] (p q : ℕ) (f : Polynomial R),
  (Polynomial.expand R (p ^ q)) f = (⇑(Polynomial.expand R p))^[q] f
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.comap_iInf : ∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → MeasureTheory.OuterMeasure β),
  (MeasureTheory.OuterMeasure.comap f) (⨅ i, m i) = ⨅ i, (MeasureTheory.OuterMeasure.comap f) (m i)
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.toNondegenerate : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.HasLines P L],
  Configuration.Nondegenerate P L
-- Mathlib.Condensed.Discrete.Colimit
CompHausLike.LocallyConstant.counitApp.eq_1 : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_3 : CategoryTheory.Limits.PreservesFiniteProducts Y],
  CompHausLike.LocallyConstant.counitApp Y =
    {
      app := fun x =>
        match x with
        | Opposite.op S => CompHausLike.LocallyConstant.counitAppApp S Y,
      naturality := ⋯ }
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instSMul : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → SMul R (M →ₚₗ[R] N)
-- Mathlib.Algebra.Torsor.Basic
Set.Nonempty.one_mem_sdiv_self : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {s : Set P}, s.Nonempty → 1 ∈ s /ₛ s
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_eq_of_inf_eq : ∀ {E : Type v} [inst : Field E] {A B C : Subfield E}, A ⊓ C = B ⊓ C → A.relrank C = B.relrank C
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {h' : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.maxKey h' = t₂.maxKey ⋯
-- Std.Data.String.ToNat
String.Slice.toNat?_eq_none_iff : ∀ {s : String.Slice}, s.toNat? = none ↔ s.isNat = false
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.app_zero_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (s : CategoryTheory.Limits.Trident f) (j : J) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero)
      (CategoryTheory.CategoryStruct.comp (f j) h) =
    CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.one) h
-- Mathlib.Data.Sign.Defs
SignType.pos : SignType
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `IsCompact.exists_infEDist_eq_edist`. -/
IsCompact.exists_infEdist_eq_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α},
  IsCompact s → s.Nonempty → ∀ (x : α), ∃ y ∈ s, Metric.infEDist x s = edist x y
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok a s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 a s
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure.below.step : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {motive : (a : σ) → M.εClosure S a → Prop} (s t : σ)
  (a : t ∈ M.step s none) (a_1 : M.εClosure S s), εNFA.εClosure.below a_1 → motive s a_1 → εNFA.εClosure.below ⋯
-- Mathlib.NumberTheory.Modular
/-- If `z ∈ 𝒟ᵒ`, and `n : ℤ`, then `|z + n| > 1`.  -/
ModularGroup.one_lt_normSq_T_zpow_smul : ∀ {z : UpperHalfPlane}, z ∈ ModularGroup.fdo → ∀ (n : ℤ), 1 < Complex.normSq ↑(ModularGroup.T ^ n • z)
-- Mathlib.Combinatorics.Additive.Dissociation
not_addDissociated : ∀ {α : Type u_1} [inst : AddCommGroup α] {s : Set α},
  ¬AddDissociated s ↔ ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∑ x ∈ t, x = ∑ x ∈ u, x
-- Std.Data.Internal.List.Associative
Std.Internal.List.List.getValueD_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValueD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        Std.Internal.List.getValueD k l₁ fallback
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The cones defined by `coneOfAdj` are limit cones.  -/
CategoryTheory.Limits.isLimitConeOfAdj : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {L : CategoryTheory.Functor (CategoryTheory.Functor J C) C} →
          (adj : CategoryTheory.Functor.const J ⊣ L) →
            (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfAdj adj F)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = false →
      Std.Internal.List.getValueCast? k (List.filter (fun p => !l₂.contains p.fst) l₁) =
        Std.Internal.List.getValueCast? k l₁
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The canonical isomorphism `mappingCone (homOfDegreewiseSplit S σ) ≅ S.X₂⟦(1 : ℤ)⟧`.  -/
CochainComplex.mappingConeHomOfDegreewiseSplitIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ) ≅
              (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₂
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instSetLike.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M], AddSubmonoid.instSetLike = { coe := fun s => s.carrier, coe_injective := ⋯ }
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.fields : Lean.Meta.InductionSubgoal → Array Lean.Expr
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.symmetrify_map : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (φ : U ⥤q V) {X Y : Quiver.Symmetrify U}
  (a : (X ⟶ Y) ⊕ (Y ⟶ X)), φ.symmetrify.map a = Sum.map φ.map φ.map a
-- Mathlib.Data.Fin.Tuple.Sort
/-- If `f₀ ≤ f₁ ≤ f₂ ≤ ⋯` is a sorted `n`-tuple of elements of `α`, then for any `j : Fin n` and
`a : α` we have `j < #{i | fᵢ ≤ a}` iff `fⱼ ≤ a`.  -/
Tuple.lt_card_le_iff_apply_le_of_monotone : ∀ {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [inst : Preorder α] {a : α} [inst_1 : DecidableLE α],
  Monotone f → (↑j < {i | f i ≤ a}.card ↔ f j ≤ a)
-- Mathlib.Topology.Bases
/-- The sequence `TopologicalSpace.denseSeq α` has dense range.  -/
TopologicalSpace.denseRange_denseSeq : ∀ (α : Type u) [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α] [inst_1 : Nonempty α],
  DenseRange (TopologicalSpace.denseSeq α)
-- Std.Internal.Do.Order.Basic
Lean.Order.true_le_of_top_le : ∀ (x : Prop), Lean.Order.PartialOrder.rel Lean.Order.top x → Lean.Order.PartialOrder.rel True x
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X - y`
has Gaussian law with mean `μ - y` and variance `v`.  -/
ProbabilityTheory.gaussianReal_sub_const : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (y : ℝ), ProbabilityTheory.HasLaw (fun ω => X ω - y) (ProbabilityTheory.gaussianReal (μ - y) v) P
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` is differentiable on `e.baseSet`, so is its coefficient `b.localFrameCoeff e i` in the
local frame induced by `e`  -/
mdifferentiableOn_baseSet_localFrameCoeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  MDiff[e.baseSet] (T% s) →
    ∀ (i : ι), MDiff[e.baseSet] ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM'.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
/-- A "proxy type" equivalent to `CategoryTheory.Limits.WalkingMultispan` that is constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. See `CategoryTheory.Limits.WalkingMultispan.proxyTypeEquiv` for the equivalence. (Generated by the `proxy_equiv%` elaborator.) -/
CategoryTheory.Limits.WalkingMultispan.proxyType : CategoryTheory.Limits.MultispanShape → Type (max w w')
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence : ∀ {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] (F : CategoryTheory.Functor C D) [F.IsEquivalence]
  [h : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C], CategoryTheory.Limits.HasStrongEpiMonoFactorisations D
-- Mathlib.Data.Set.Countable
/-- A non-empty set is countable iff there exists a surjection from the
natural numbers onto the subtype induced by the set.
 -/
Set.countable_iff_exists_surjective : ∀ {α : Type u} {s : Set α}, s.Nonempty → (s.Countable ↔ ∃ f, Function.Surjective f)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddZeroClass.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y],
  LocallyConstant.instAddZeroClass = Function.Injective.addZeroClass DFunLike.coe ⋯ ⋯ ⋯
-- Batteries.Tactic.GeneralizeProofs
/-- Generalizes the proofs in the type `e` and runs `k` in a local context with these propositions.
This continuation `k` is passed
1. an array of fvars for the propositions
2. an array of proof terms (extracted from `e`) that prove these propositions
3. the generalized `e`, which refers to these fvars

The `propToFVar` map is updated with the new proposition fvars.
 -/
Batteries.Tactic.GeneralizeProofs.withGeneralizedProofs : {α : Type} →
  [Nonempty α] →
    Lean.Expr →
      Option Lean.Expr →
        (Array Lean.Expr → Array Lean.Expr → Lean.Expr → Batteries.Tactic.GeneralizeProofs.MGen α) →
          Batteries.Tactic.GeneralizeProofs.MGen α
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.toCommMonoid.eq_1 : ∀ {M : Type u_5} [inst : CommMonoid M] (S : Submonoid M), S.toCommMonoid = SubmonoidClass.toCommMonoid S
-- Init.Data.Range.Polymorphic.Fin
Fin.instUpwardEnumerable : {n : ℕ} → Std.PRange.UpwardEnumerable (Fin n)
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- The inclusion map from a closed segment to `ℝ` is a smooth immersion  -/
isImmersionOfComplement_subtypeVal_Icc : ∀ {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞},
  Manifold.IsImmersionOfComplement Unit (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) n fun z => ↑z
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The number of side goals created.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey.numGoals : Mathlib.Tactic.ClickSuggestions.GrwKey → ℕ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_biUnion : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ι : Type u_2} (f : ι → Set α) (I : Set ι) (x : α),
  Metric.infEDist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, Metric.infEDist x (f i)
-- Aesop.Builder.Basic
Aesop.instInhabitedRuleBuilderOptions : Inhabited Aesop.RuleBuilderOptions
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.comp_def : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {X Y Z : CategoryTheory.ShrinkHoms.{u} C} (f : Shrink.{w, v} (X.fromShrinkHoms ⟶ Y.fromShrinkHoms))
  (g : Shrink.{w, v} (Y.fromShrinkHoms ⟶ Z.fromShrinkHoms)),
  CategoryTheory.CategoryStruct.comp f g =
    (equivShrink (X.fromShrinkHoms ⟶ Z.fromShrinkHoms))
      (CategoryTheory.CategoryStruct.comp ((equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f)
        ((equivShrink (Y.fromShrinkHoms ⟶ Z.fromShrinkHoms)).symm g))
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.union : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s₂ s' : Set (Set Ω)},
  ProbabilityTheory.IndepSets s₁ s' μ → ProbabilityTheory.IndepSets s₂ s' μ → ProbabilityTheory.IndepSets (s₁ ∪ s₂) s' μ
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.eval_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (F : CategoryTheory.Functor C A)
  (X : CategoryTheory.Limits.FormalCoproduct C),
  ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).obj X = ∐ fun i => F.obj (X.obj i)
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isPreconnected_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → IsPreconnected {K | ↑K ⊆ s}
-- Init.Data.List.Lemmas
List.tail_append_of_ne_nil : ∀ {α : Type u_1} {xs ys : List α}, xs ≠ [] → (xs ++ ys).tail = xs.tail ++ ys
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.instCoeFunForallSet : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} →
        {s : Set X} → {p : Set X → Prop} → CoeFun (ShrinkingLemma.PartialRefinement u s p) fun x => ι → Set X
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Adds an E-matching theorem to the environment.
See `mkEMatchTheorem`.
 -/
Lean.Meta.Grind.Extension.addEMatchTheorem : Lean.Meta.Grind.Extension →
  Lean.Name →
    ℕ →
      List Lean.Expr →
        Lean.Meta.Grind.EMatchTheoremKind →
          Bool →
            optParam Lean.AttributeKind Lean.AttributeKind.global →
              List Lean.Meta.Grind.EMatchTheoremConstraint → Lean.MetaM Unit
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.haveLebesgueDecomposition_neg : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ], (-s).HaveLebesgueDecomposition μ
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_eq_iff : ∀ {α : Sort u_1} [inst : DecidableEq α] {x y z w : α}, (Equiv.swap x y) z = w ↔ z = (Equiv.swap x y) w
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Compacts.lipschitz_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : EMetricSpace α] [inst_1 : EMetricSpace β], LipschitzWith 1 fun p => p.1 ×ˢ p.2
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonnegative.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα : Q(PartialOrder «$α»)}
  (pf pf_1 : Q(0 ≤ «$e»)),
  (Mathlib.Meta.Positivity.Strictness.nonnegative pf = Mathlib.Meta.Positivity.Strictness.nonnegative pf_1) =
    (pf = pf_1)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.TheoremForm.comp : Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.Order.Antichain
IsAntichain.preimage_relIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β},
  IsAntichain r' t → ∀ (φ : r ≃r r'), IsAntichain r (⇑φ ⁻¹' t)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_sub : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (s t : NonemptyInterval α), (s - t).toProd.1 = s.toProd.1 - t.toProd.2
-- Mathlib.Analysis.Convex.Extreme
Set.extremePoints_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] [Subsingleton E] (A : Set E), Set.extremePoints 𝕜 A = A
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- If a unit `u` is congruent to an integer modulo `λ ^ 2`, then `u = 1` or `u = -1`.

This is a special case of the so-called *Kummer's lemma*.  -/
IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K], (∃ n, (hζ.toInteger - 1) ^ 2 ∣ ↑u - ↑n) → u = 1 ∨ u = -1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_monomial : ∀ {R : Type u_1} [inst : Semiring R] (f : SkewPolynomial R), (f.sum fun a => ⇑(SkewPolynomial.monomial a)) = f
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.hasSum_symmetricIcc_iff : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasSum f a (SummationFilter.symmetricIcc ℤ) ↔
    Filter.Tendsto (fun N => ∑ n ∈ Finset.Icc (-↑N) ↑N, f n) Filter.atTop (nhds a)
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.mk : Array Lean.Elab.InlayHintInfo → ℕ → Option ℕ → Bool → Lean.Server.FileWorker.InlayHintState
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_reindex : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : m ≃ l) (f : n ≃ o),
  ((Matrix.reindex e f) A).updateRow i r = (Matrix.reindex e f) (A.updateRow (e.symm i) fun j => r (f j))
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_zero_iff_subsingleton' : ∀ {R : Type u} [inst : Semiring R], Polynomial.Monic 0 ↔ (∀ (f g : Polynomial R), f = g) ∧ ∀ (a b : R), a = b
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualCoannihilator_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊥.dualCoannihilator = ⊤
-- Mathlib.Order.Filter.Pointwise
Filter.add_bot : ∀ {α : Type u_2} [inst : Add α] {f : Filter α}, f + ⊥ = ⊥
-- Mathlib.Dynamics.Ergodic.Ergodic
MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_semiconj : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {β : Type u_2}
  {m' : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ μ' → PreErgodic f μ → ∀ {f' : β → β}, Function.Semiconj g f f' → PreErgodic f' μ'
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.postcomp_h : ∀ {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (h : f.Homotopy g) (f' : SSet.RelativeMorphism B C ψ)
  {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ),
  (h.postcomp f' fac).h = CategoryTheory.CategoryStruct.comp h.h f'.map
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.of_constant : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y), (∀ (x y : X), f x = f y) → IsLocallyConstant f
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.eq_domRestrict_iff`. -/
Set.eq_restrict_iff : ∀ {α : Type u_1} {π : α → Type u_6} {s : Set α} {f : (a : ↑s) → π ↑a} {g : (a : α) → π a},
  f = s.domRestrict g ↔ ∀ (a : α) (ha : a ∈ s), f ⟨a, ha⟩ = g a
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F]
  {X Y : D} (f : X ⟶ Y),
  CategoryTheory.Limits.HasColimit
    (((CategoryTheory.CostructuredArrow.functor L).map f).toFunctor.comp
      ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) Y).comp
        ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F)))
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_iff_comp_const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (b - x)) (b - a)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.id_apply : ∀ (M : AddMonCat) (x : ↑M), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.Algebra.Algebra.Equiv
/-- [Stacks Tag 09HR](https://stacks.math.columbia.edu/tag/09HR) -/
AlgEquiv.aut : {R : Type uR} →
  {A₁ : Type uA₁} → [inst : CommSemiring R] → [inst_1 : Semiring A₁] → [inst_2 : Algebra R A₁] → Group (A₁ ≃ₐ[R] A₁)
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.mk.sizeOf_spec : ∀ {Ω : Type w} [inst : SizeOf Ω] (obj : Set Ω) (hom : ↑obj → ↑obj → Set Ω) (id : (X : ↑obj) → ↑(hom X X))
  (comp : {X Y Z : ↑obj} → ↑(hom X Y) → ↑(hom Y Z) → ↑(hom X Z))
  (id_comp :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp (id X) f = f) CategoryTheory.SmallCategoryOfSet.id_comp._autoParam)
  (comp_id :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp f (id Y) = f) CategoryTheory.SmallCategoryOfSet.comp_id._autoParam)
  (assoc :
    autoParam
      (∀ {X Y Z T : ↑obj} (f : ↑(hom X Y)) (g : ↑(hom Y Z)) (h : ↑(hom Z T)), comp (comp f g) h = comp f (comp g h))
      CategoryTheory.SmallCategoryOfSet.assoc._autoParam),
  sizeOf { obj := obj, hom := hom, id := id, comp := comp, id_comp := id_comp, comp_id := comp_id, assoc := assoc } = 1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_vsub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, (s -ᵥ t).Nonempty → t.Nonempty
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type u_6} {f : β → γ} {g : α → Part β},
  OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous fun x => f <$> g x
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a / b
-- Lean.Meta.Canonicalizer
/-- State for the `CanonM` monad.
 -/
Lean.Meta.Canonicalizer.State : Type