mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Point.Conservative
/-- A site has enough points (relatively to a universe `w`)
if it has a `w`-small conservative family of points.  -/
CategoryTheory.GrothendieckTopology.HasEnoughPoints : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Prop
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.unfold_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x y : α), Mathlib.Tactic.Abel.smulg n x = y → n • x = y
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.iff.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.AndKind.iff = 1
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist_comm : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovEDist μ ν = MeasureTheory.levyProkhorovEDist ν μ
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  {x y : CategoryTheory.Cokleisli U} {f g : x ⟶ y}, f.of = g.of → f = g
-- Plausible.Shrinkable
Plausible.UInt32.shrinkable : Plausible.Shrinkable UInt32
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.ofList.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (Lists α) → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : Lists α) → (l : List (Lists α)) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Mathlib.Tactic.GCongr.Core
/-- Construct a `GCongrLemma` for `gcongr` goals of the form `a ≺ b → c ≺ d`.
This will be tried if there is no other available `@[gcongr]` lemma.
For example, the relation `a ≡ b [ZMOD n]` has an instance of `IsTrans`, so a congruence of the form
`a ≡ b [ZMOD n] → c ≡ d [ZMOD n]` can be solved with `rel_imp_rel`.
 -/
Mathlib.Tactic.GCongr.relImpRelLemma : ℕ → List Mathlib.Tactic.GCongr.GCongrLemma
-- Mathlib.Topology.VectorBundle.Basic
VectorBundle.continuousLinearEquivAt_apply : ∀ (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [inst_9 : VectorBundle R F E] (b : B)
  (y : E b), (VectorBundle.continuousLinearEquivAt R F E b) y = (↑(trivializationAt F E b) ⟨b, y⟩).2
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_right_strictMono : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ},
  n ≠ 0 → StrictMono fun x => n • x
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.sSup_adj : ∀ {V : Type u_2} {a b : V} {s : Set (Digraph V)}, (sSup s).Adj a b ↔ ∃ G ∈ s, G.Adj a b
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} (a_1 : a ⟶ b) {X Y : Opposite.unop a ⟶ x}
  (x_1 : X ⟶ Y),
  ((CategoryTheory.Bicategory.yoneda₀ x).map a_1).toFunctor.map x_1 = CategoryTheory.Bicategory.whiskerLeft a_1.unop x_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F}, WeierstrassCurve.Jacobian.Point.toAffineLift 0 = 0
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.prev.eq_1 : ∀ {ι : Type u_1} (c : ComplexShape ι) (i : ι), c.prev i = if h : ∃ j, c.Rel j i then h.choose else i
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map is compatible with addition.  -/
CategoryTheory.AddModObj.add_vadd : ∀ {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.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.AddMonObj M} (X : D) [self : CategoryTheory.AddModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X)
      CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.AddModObj.vadd)
        CategoryTheory.AddModObj.vadd)
-- Mathlib.Data.Rel
SetRel.image_subset_image_left : ∀ {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} {s : Set α}, R₁ ⊆ R₂ → R₁.image s ⊆ R₂.image s
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom₂.mk.injEq : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} (hom hom_1 : f.hom ⟶ g.hom),
  ({ hom := hom } = { hom := hom_1 }) = (hom = hom_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.neg (u • P) = u • W'.neg P
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_invRev : ∀ {α : Type u_1} [inst : DecidableEq α] {w : List (α × Bool)},
  FreeGroup.reduce (FreeGroup.invRev w) = FreeGroup.invRev (FreeGroup.reduce w)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq)
  {v : β k},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (↑(t.insertMany l ⋯)).get? k' = some (cast ⋯ v)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.inclusion_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S T U : NonUnitalStarSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S),
  (NonUnitalStarSubalgebra.inclusion htu) ((NonUnitalStarSubalgebra.inclusion hst) x) =
    (NonUnitalStarSubalgebra.inclusion ⋯) x
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.vaddAssocClass_addMonoidAlgebra : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] [inst_3 : Algebra R S] [inst_4 : CommSemiring T] [inst_5 : Algebra R T]
  [inst_6 : Algebra S T] [IsScalarTower R S T], IsScalarTower R (AddMonoidAlgebra S M) (AddMonoidAlgebra T M)
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodComm_apply : ∀ (R : Type u_3) (M : Type u_4) (N : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (a : M × N), (LinearEquiv.prodComm R M N) a = a.swap
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.colimit.whiskerLeft_ι_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F) (j : J) {Q Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.desc F c)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (c.ι.app j)) h
-- Mathlib.Algebra.Order.Monoid.NatCast
lt_one_add : ∀ {α : Type u_1} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
  [AddRightStrictMono α] (a : α), a < 1 + a
-- Lean.Meta.Tactic.Grind.Types
/-- New raw fact to be preprocessed, and then asserted.  -/
Lean.Meta.Grind.NewRawFact : Type
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_lt : ∀ (x : Ordinal.{u_1}), x.invVeblen₂ < Ordinal.omega0 ^ x
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.map_fst : ∀ {X Y : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y'), (e₁.tensor e₂).map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) = e₁
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.convs'Aux.match_1.eq_2 : ∀ {K : Type u_1} (motive : Stream'.Seq (GenContFract.Pair K) → ℕ → Sort u_2) (s : Stream'.Seq (GenContFract.Pair K))
  (n : ℕ) (h_1 : (x : Stream'.Seq (GenContFract.Pair K)) → motive x 0)
  (h_2 : (s : Stream'.Seq (GenContFract.Pair K)) → (n : ℕ) → motive s n.succ),
  (match s, n.succ with
    | x, 0 => h_1 x
    | s, n.succ => h_2 s n) =
    h_2 s n
-- Init.Grind.ToInt
/-- The embedding into the integers takes subtraction to subtraction, wrapped into the range interval.
 -/
Lean.Grind.ToInt.Sub : (α : Type u) → [Sub α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Order.Restriction
Preorder.dependsOn_frestrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] (a : α),
  DependsOn (Preorder.frestrictLe a) (Set.Iic a)
-- Mathlib.Order.Filter.Bases.Basic
/-- There exists at least one `i` that satisfies `p`.  -/
Filter.IsBasis.nonempty : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α}, Filter.IsBasis p s → ∃ i, p i
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mulInvariantVectorField_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] (c : 𝕜) (v : GroupLieAlgebra I G),
  mulInvariantVectorField (c • v) = c • mulInvariantVectorField v
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_m_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j) {Z : SSet} (h : f.sigmaStdSimplex j ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (CategoryTheory.CategoryStruct.comp (f.m j) h) =
    CategoryTheory.CategoryStruct.comp c.horn.ι (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.keyAtIdx!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {i : ℕ} [inst : Inhabited α], t₁.keyAtIdx! i = t₂.keyAtIdx! i
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- A fundamental sequence for `o` has cofinal range, i.e. its least strict upper bound equals the
ordinal `o`. See `IsFundamentalSeq.iSup_add_one_eq` and `IsFundamentalSeq.iSup_eq`.  -/
Ordinal.IsFundamentalSeq.isCofinal_range : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → IsCofinal (Set.range f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.ofCone_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.PullbackCone.ofCone t).π =
    CategoryTheory.CategoryStruct.comp t.π (CategoryTheory.Limits.diagramIsoCospan F).hom
-- Init.Data.Fin.Lemmas
Fin.mk_one : ∀ {n : ℕ}, ⟨1, ⋯⟩ = 1
-- Mathlib.Order.Filter.CountableInter
Filter.countableInter_ofCountableUnion : ∀ {α : Type u_2} (l : Set (Set α)) (h₁ : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l)
  (h₂ : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l), CountableInterFilter (Filter.ofCountableUnion l h₁ h₂)
-- Mathlib.Analysis.Complex.Norm
Complex.im_le_norm : ∀ (z : ℂ), z.im ≤ ‖z‖
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injective_iff_hasInjectiveDimensionLT_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C},
  CategoryTheory.Injective X ↔ CategoryTheory.HasInjectiveDimensionLT X 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Order.Filter.Pointwise
Filter.nsmul_top : ∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ}, n ≠ 0 → n • ⊤ = ⊤
-- Init.Data.Hashable
instHashableNat : Hashable ℕ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles._auto_3) {Z : C}
  (h : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.rightRel_eq_top : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G}, QuotientGroup.rightRel N = ⊤ ↔ N = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.wf_ancestralRel : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [WellFoundedLT α] [P.IsProper]
  (f : P.WeakRankFunction α), WellFounded P.AncestralRel
-- Mathlib.RingTheory.Etale.StandardEtale
/-- An isomorphism to the standard etale algebra of a standard etale pair.  -/
StandardEtalePresentation : (R : Type u_4) → (S : Type u_5) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max u_4 u_5)
-- Mathlib.CategoryTheory.Countable
CategoryTheory.countableCategoryDiscreteOfCountable : ∀ (J : Type u_1) [Countable J], CategoryTheory.CountableCategory (CategoryTheory.Discrete J)
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instLEOrdinal : LE Std.Time.Minute.Ordinal
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {s : Set E} {x : E}, MDiffAt[s] ⇑f x
-- Init.SimpLemmas
beq_self_eq_true : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] (a : α), (a == a) = true
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.discrs : Lean.Meta.MatcherApp → Array Lean.Expr
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.types_id : ∀ (X : Type u), ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.toSubmersivePresentation_jacobian : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S),
  P.toSubmersivePresentation.jacobian = (Polynomial.aeval P.x) (Polynomial.derivative P.f) * (Polynomial.aeval P.x) P.g
-- Mathlib.Data.Bool.Basic
Bool.dichotomy : ∀ (b : Bool), b = false ∨ b = true
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.sup_carrier_def : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J J' : hI.SubDPIdeal),
  (J ⊔ J').carrier = ↑⟨(J ⊔ J').carrier, ⋯⟩
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.TypeToCharPResult.intLike : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n : Q(ℕ)) → (instRing : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Tactic.ReduceModChar.TypeToCharPResult α
-- Mathlib.Order.Monotone.Monovary
Antivary.eq_1 : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (g : ι → β),
  Antivary f g = ∀ ⦃i j : ι⦄, g i < g j → f j ≤ f i
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_forget₂_map : ∀ {X Y : AddCommMonCat} (f : X ⟶ Y),
  AddMonCat.Hom.hom ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).map f) = AddCommMonCat.Hom.hom f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_alter_of_not_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ k' ∈ t)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coeLM_apply : ∀ {R : Type u_1} (S : Type u_4) [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_6} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N₃ : Type u_10} [inst_5 : TopologicalSpace N₃]
  [inst_6 : AddCommMonoid N₃] [inst_7 : Module R N₃] [inst_8 : Module S N₃] [inst_9 : SMulCommClass R S N₃]
  [inst_10 : ContinuousConstSMul S N₃] [inst_11 : ContinuousAdd N₃] (self : M →L[R] N₃),
  (ContinuousLinearMap.coeLM S) self = ↑self
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.map_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C)
  [CategoryTheory.IsIso T.μ], T.map (T.η.app X) = T.η.app (T.obj X)
-- Init.Data.List.Lemmas
List.head?_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, (List.map f l).head? = Option.map f l.head?
-- Mathlib.Topology.MetricSpace.CauSeqFilter
CauSeq.tendsto_limit : ∀ {β : Type v} [inst : NormedRing β] [hn : IsAbsoluteValue norm] (f : CauSeq β norm)
  [inst_1 : CauSeq.IsComplete β norm], Filter.Tendsto (↑f) Filter.atTop (nhds f.lim)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
bddBelow_inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G},
  BddBelow s⁻¹ ↔ BddAbove s
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_zero : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂),
  MvPolynomial.eval₂Hom f 0 = f.comp MvPolynomial.constantCoeff
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₂_eq_some_of_toBitVec : ∀ {w x : UInt8},
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = false →
    ∀ {c : Char},
      128 ≤ c.val →
        c.val.toBitVec = BitVec.setWidth 32 (BitVec.setWidth 5 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec) →
          ByteArray.utf8DecodeChar?.assemble₂ w x = some c
-- Mathlib.Analysis.Fourier.Inversion
Real.tendsto_integral_gaussian_smul : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
      ∀ (v : V),
        Filter.Tendsto
          (fun c =>
            ∫ (w : V),
              ((↑Real.pi * ↑c) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w)
          Filter.atTop (nhds (FourierTransformInv.fourierInv (FourierTransform.fourier f) v))
-- Lean.Parser.Term
/-- Defines a coinductive predicate using lattice theory, based on the Knaster-Tarski fixpoint theorem.

This feature constructs coinductive predicates by leveraging the lattice structure on `Prop`
and ensures correctness through monotonicity.

The coinductive predicate is defined as the greatest fixed point of a monotone function on `Prop`.

By default, monotonicity is verified automatically. However, users can provide custom proofs
of monotonicity if needed.
 -/
Lean.Parser.Termination.coinductiveFixpoint : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_subset_sub_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s t : Finset α}, 0 ∈ s → -t ⊆ s - t
-- Init.Data.UInt.Lemmas
UInt16.ofNat_uInt8ToNat : ∀ (n : UInt8), UInt16.ofNat n.toNat = n.toUInt16
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pow_lt_of_lt_log : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n
-- Mathlib.Order.RelIso.Basic
Function.Surjective.wellFounded_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α → β},
  Function.Surjective f → (∀ {a b : α}, r a b ↔ s (f a) (f b)) → (WellFounded r ↔ WellFounded s)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.hₚFunctor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (i : ι) {X Y : TopPair.HomologyPretheory C c} (f : X ⟶ Y),
  (TopPair.HomologyPretheory.hₚFunctor i).map f = f.homₚ i
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_sdiff_singleton_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R (s \ {0}) = Submodule.span R s
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_ne_bot_of_ne_bot : ∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] [FaithfulSMul R S]
  {I : Ideal R}, I ≠ ⊥ → Ideal.map (algebraMap R S) I ≠ ⊥
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.mk : {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.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] → (X : D) → [mod : CategoryTheory.ModObj A X] → CategoryTheory.Mod D A
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_of_Ici : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α},
  (∀ (x : α), MeasurableSet (f ⁻¹' Set.Ici x)) → Measurable f
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico b a ⊆ Set.Ici b
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.trans_toAlgEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Semiring C]
  [inst_6 : TopologicalSpace C] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] (e₁ : A ≃A[R] B)
  (e₂ : B ≃A[R] C), (e₁.trans e₂).toAlgEquiv = e₁.trans e₂.toAlgEquiv
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_filter : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1} [inst_1 : Monad n]
  [LawfulMonad n] [inst_3 : Std.Do.WPMonad n ps] [Std.Iterators.Finite α Id] [inst_5 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄ forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filter f it) init g ⦃Q⦄