mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_pos : ∀ {x y : NNReal}, 0 < x → 0 < y → 0 < x.agm y
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_add_one : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  f x ≤ x → ∀ (a : Ordinal.{u}), OrdinalApprox.gfpApprox f x (a + 1) = f (OrdinalApprox.gfpApprox f x a)
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of indexed supremum on function lattices.  -/
Lean.Order.iSup_apply : ∀ {ι : Type v} {σ : Type w} {β : Type u} [inst : Lean.Order.CompleteLattice β] (f : ι → σ → β) (s : σ),
  Lean.Order.iSup f s = Lean.Order.iSup fun i => f i s
-- Init.Data.Fin.Lemmas
Fin.one_pos : ∀ {n : ℕ}, 0 < 1
-- Lean.Expr
Lean.mkMVarEx : Lean.MVarId → Lean.Expr
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrows_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ)
  (F : CategoryTheory.Functor (Fin (n + 1)) C) {X Y : Fin (n + 1)} (f : X ⟶ Y),
  ((G.mapComposableArrows n).obj F).map f = G.map (F.map f)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_1 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.id x) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.FreeMonoidalCategory.projectObj f x)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.isUnit_resultant_iff_isCoprime : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R}, f.Monic → (IsUnit (f.resultant g) ↔ IsCoprime f g)
-- Mathlib.Computability.DFA
DFA.evalFrom_append_singleton : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (x : List α) (a : α),
  M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
MulOpposite.dist_op : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : α), dist (MulOpposite.op x) (MulOpposite.op y) = dist x y
-- Mathlib.Order.Antisymmetrization
AntisymmRel.refl : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Refl r] (a : α), AntisymmRel r a a
-- Mathlib.CategoryTheory.Galois.Examples
/-- The forgetful functor from finite `G`-sets to sets is a `FiberFunctor`.  -/
CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget : ∀ (G : Type u) [inst : Group G], CategoryTheory.PreGaloisCategory.FiberFunctor (Action.forget FintypeCat G)
-- Lean.MetavarContext
Lean.instantiateMVarsCore : Lean.MetavarContext → Lean.Expr → Lean.Expr × Lean.MetavarContext
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.counitAlgHom_comp_mapRingHom : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] (f : R →+* S),
  (Bialgebra.counitAlgHom S (AddMonoidAlgebra S M)).comp (AddMonoidAlgebra.mapRingHom M f) =
    f.comp (Bialgebra.counitAlgHom R (AddMonoidAlgebra R M)).toRingHom
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimits.eq_1 : AddMonCat.forget_createsLimits = AddMonCat.forget_createsLimitsOfSize
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (j j' : J),
  (K₁.mapBifunctor K₂ F c).d j j' =
    HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j' + HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j'
-- Std.Do.SPred.Laws
Std.Do.SPred.pure_intro : ∀ {σs : List (Type u)} {φ : Prop} {P : Std.Do.SPred σs}, φ → P ⊢ₛ ⌜φ⌝
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right-residuation operators on a quantale are similar to the Heyting
operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ₗ z ↔ x * y ≤ z` or alternatively `x ⇨ₗ y = sSup { z | z * x ≤ y }`.
 -/
Quantale.leftMulResiduation : {α : Type u_1} → [Semigroup α] → [CompleteLattice α] → α → α → α
-- Lean.Parser.Command
Lean.Parser.Command.optNamedPrio : Lean.Parser.Parser
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.isomorphisms_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), CategoryTheory.MorphismProperty.isomorphisms D ≤ F.relativelyRepresentable
-- Mathlib.AlgebraicGeometry.EllipticCurve.LFunction
/-- The local power series associated to a Weierstrass curve over a nonarchimedean local field.  -/
WeierstrassCurve.localPowerSeries : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → PowerSeries ℤ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_notMem_neg_add_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, 0 ∉ -t + s ↔ Disjoint s t
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X),
  ((hf.autMulEquivOfFullyFaithful X).symm e).hom = hf.preimage e.hom
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LocalTimeType.mk : ℤ → Bool → UInt8 → Std.Time.TimeZone.TZif.LocalTimeType
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
/-- The function `tanh` is meromorphic at any `z`.  -/
Complex.meromorphicAt_tanh : ∀ (z : ℂ), MeromorphicAt Complex.tanh z
-- Lean.Util.ForEachExprWhere
_private.Lean.Util.ForEachExprWhere.0.Lean.ForEachExprWhere.notAnExpr : Unit × Unit
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_sin : ∀ (x : ℝ), ↑(Real.sin x) = Complex.sin ↑x
-- Mathlib.Data.Complex.Basic
Complex.smul_im : ∀ {R : Type u_1} [inst : SMul R ℝ] (r : R) (z : ℂ), (r • z).im = r • z.im
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- Given a function on `𝕜`, return the unique function on `AddCircle p` agreeing with `f` on
`(a, a + p]`.  -/
AddCircle.liftIoc : {𝕜 : Type u_1} →
  {B : Type u_2} →
    [inst : AddCommGroup 𝕜] →
      (p : 𝕜) →
        [inst_1 : LinearOrder 𝕜] →
          [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → 𝕜 → [Archimedean 𝕜] → (𝕜 → B) → AddCircle p → B
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mul_def : ∀ {K : Type u_1} [inst : CommRing K] (x x_1 : RatFunc K),
  x.mul x_1 =
    match x, x_1 with
    | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_union!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union! m₂) k h' = Std.DTreeMap.Internal.Impl.Const.get m₂ k ⋯
-- Std.Data.HashMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.getKey : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → (m : Std.HashMap α β) → (a : α) → a ∈ m → α
-- Std.Sat.AIG.Basic
/-- Contains the index of `decl` in `decls` along with a proof that the index is indeed correct.
 -/
Std.Sat.AIG.CacheHit : {α : Type} → Array (Std.Sat.AIG.Decl α) → Std.Sat.AIG.Decl α → Type
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_Ioi : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.map (Fin.natAddEmb m) (Finset.Ioi i) = Finset.Ioi (Fin.natAdd m i)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*` and `1`.  -/
AbsoluteValue.toMonoidHom : {R : Type u_5} →
  {S : Type u_6} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → [IsDomain S] → [Nontrivial R] → R →* S
-- Init.Data.Vector.Lemmas
Vector.all_eq_true : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = true ↔ ∀ (i : ℕ) (x : i < n), p xs[i] = true
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_mono_null : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, s ⊆ t → μ t = 0 → μ s = 0
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_mul_add : ∀ {R : Type u_1} [inst : Semiring R] (x : R) (n : ℕ), (∑ i ∈ Finset.range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
-- Mathlib.Data.Fin.SuccPred
Fin.pred_lt_castPred : ∀ {n : ℕ} {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ Fin.last n), a.pred h₁ < a.castPred h₂
-- Mathlib.Algebra.Ring.Prod
RingEquiv.fst_comp_coe_prodComm : ∀ {R : Type u_1} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  (RingHom.fst S R).comp ↑RingEquiv.prodComm = RingHom.snd R S
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.finTwoArrow_symm_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α],
  ⇑MeasurableEquiv.finTwoArrow.symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_le : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I : Submodule R A} {N P : Submodule R M}, I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.find?_eq_zoom : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α}
  (p : optParam (RBTree.RBNode.Path α) RBTree.RBNode.Path.root),
  RBTree.RBNode.find? cut t = (RBTree.RBNode.zoom cut t p).1.root?
-- Mathlib.Data.Multiset.Bind
Multiset.product_add : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- `g` is in fact presented by `ψ`.  -/
CategoryTheory.IndParallelPairPresentation.hg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  (self : CategoryTheory.IndParallelPairPresentation f g),
  g = self.isColimit₁.map { pt := B, ι := self.ι₂ } (CategoryTheory.Functor.whiskerRight self.ψ CategoryTheory.yoneda)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ioi a)) (nhdsWithin (-a) (Set.Iio (-a)))
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_insert_of_ne : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq ι] {i j : ι} [inst_2 : (i : ι) → Decidable (i ∈ insert j s)],
  i ≠ j → (insert j s).piecewise f g i = s.piecewise f g i
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- Gradient of `f` at the point `x`, if it exists.  Zero otherwise.
Denoted as `∇` within the Gradient namespace.

If the derivative exists (i.e., `∃ f', HasGradientAt f f' x`), then
`f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` where `x'` converges to `x`.  -/
Gradient.«term∇» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.exists_simple_subobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.IsArtinianObject X],
  ¬CategoryTheory.Limits.IsZero X → ∃ Y, CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.map_subtype_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) {x : ↥s},
  ↑x ∈ e.source → ↑e ↑x ∈ (e.subtypeRestr hs).target
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.fromCostructuredArrow_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F}
  (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).map f).hom = f.left
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonMessage : Lean.ToJson Lean.JsonRpc.Message
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) identifying `Spec(Γ(X, U)/I(U))` with its image in `Spec(𝒪ₓ/I)`.  -/
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso : {X : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) →
    (U : ↑X.affineOpens) → I.glueDataObj U ≅ ↑((TopologicalSpace.Opens.map I.gluedTo.base).obj ↑U)
-- Mathlib.Order.Bounded
Set.bounded_gt_Ioo : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 > x2) (Set.Ioo a b)
-- Mathlib.Order.Lattice
ULift.instSemilatticeSup : {α : Type u} → [SemilatticeSup α] → SemilatticeSup (ULift.{v, u} α)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_map_algebraMap_iff : ∀ {R : Type u_1} (S : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M] (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M (List.map (⇑(algebraMap R S)) rs) ↔ RingTheory.Sequence.IsWeaklyRegular M rs
-- Init.Data.Array.Lemmas
Array.push_empty : ∀ {α : Type u_1} {x : α}, #[].push x = #[x]
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Split the set into those satisfying and not satisfying the predicate `p`.
`p` is required to be antitone, that is, `x < y → p y → p x`.

```
span (fun x ↦ x < 4) {1, 2, 3, 4, 5} = ({1, 2, 3}, {4, 5})
span (fun x ↦ x > 4) {1, 2, 3, 4, 5} = precondition violation
```  -/
Ordnode.span : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Ordnode α → Ordnode α × Ordnode α
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.transpose_empty_rows : ∀ {α : Type u} {m' : Type uₘ} (A : Matrix m' (Fin 0) α), A.transpose = Matrix.of ![]
-- Mathlib.CategoryTheory.Monoidal.Closed.Transport
CategoryTheory.MonoidalClosed.instTransported : {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] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [CategoryTheory.MonoidalClosed C] → CategoryTheory.MonoidalClosed (CategoryTheory.Monoidal.Transported e)
-- Lean.Compiler.IR.CompilerM
Lean.IR.logMessageIf : {α : Type} → [Std.ToFormat α] → Lean.Name → α → Lean.IR.CompilerM Unit
-- Mathlib.Order.MinMax
le_of_max_le_right : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b ≤ c → b ≤ c
-- Mathlib.Topology.Order
/-- **Alias** of `TopologicalSpace.setOfPred_isOpen_injective`. -/
TopologicalSpace.setOf_isOpen_injective : ∀ {α : Type u}, Function.Injective fun t => {s | IsOpen s}
-- Mathlib.Algebra.Group.NatPowAssoc
npow_zero : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (x : M), x ^ 0 = 1
-- Lean.Parser.Syntax
Lean.Parser.Command.elabArg : Lean.Parser.Parser
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mk_coe : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b),
  { toFun := ⇑f, map_add_const' := ⋯ } = f
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_swap_sub : ∀ {α : Type u_2} [inst : Sub α],
  CovariantClass (Filter α) (Filter α) (Function.swap fun x1 x2 => x1 - x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ioc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (b : α i), Function.update f i '' Set.Ioc (f i) b = Set.Ioc f (Function.update f i b)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCustomInfo : Lean.Elab.CustomInfo → Lean.Elab.Info
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientEquivProdOfLE'_symm_apply : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t),
  (Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.map_comp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {C : Type u_6} {ψ : Type u_7}
  [inst_10 : CommRing C] [inst_11 : SetLike ψ C] [inst_12 : AddSubgroupClass ψ C] {𝒞 : ι → ψ} [inst_13 : GradedRing 𝒞]
  {f : 𝒜 →+*ᵍ ℬ} {g : ℬ →+*ᵍ 𝒞} {P : Submonoid A} {Q : Submonoid B} {R : Submonoid C} (hpq : P ≤ Submonoid.comap f Q)
  (hqr : Q ≤ Submonoid.comap g R),
  HomogeneousLocalization.map (g.comp f) ⋯ =
    (HomogeneousLocalization.map g hqr).comp (HomogeneousLocalization.map f hpq)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.measurableSet : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ∀ (i : ι), MeasurableSet (φ i)
-- Init.Data.Option.Lemmas
Option.all_merge : ∀ {α : Type u_1} {p : α → Bool} {f : α → α → α},
  (∀ (a b : α), p (f a b) = (p a && p b)) →
    ∀ {o o' : Option α}, Option.all p (Option.merge f o o') = (Option.all p o && Option.all p o')
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysArray.size = m.size
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_rio : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi (Std.Slice.size xs)
-- Mathlib.Data.Rel
SetRel.subset_symmetrize : ∀ {α : Type u_1} {R S : SetRel α α}, S ⊆ R.symmetrize ↔ S ⊆ R ∧ S ⊆ R.inv
-- Mathlib.Algebra.Order.IsBotOne
max_eq_one : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : One α] [IsBotOneClass α] {a b : α}, max a b = 1 ↔ a = 1 ∧ b = 1
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `p` be the minimal polynomial of an integral element `x`. Then `y` is a conjugate root of `x`
if and only if `p y = 0`.
 -/
isConjRoot_iff_aeval_eq_zero : ∀ {K : Type u_2} {A : Type u_5} [inst : Ring A] [inst_1 : Field K] [inst_2 : Algebra K A] [IsDomain A] {x y : A},
  IsIntegral K x → (IsConjRoot K x y ↔ (Polynomial.aeval y) (minpoly K x) = 0)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Submodule.exists_isCompl : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (p : Submodule K V), ∃ q, IsCompl p q
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α),
  MeasurableSet (κ.mutuallySingularSetSlice η a)
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.of_toLex_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k l : ℕ} {α β : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → toLex (l, β) ≤ toLex (k, α) → ContDiffPointwiseHolderAt l β f a
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- A type class for topological spaces in which the indicator functions of closed sets can be
approximated pointwise from above by a sequence of bounded continuous functions.  -/
HasOuterApproxClosed : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [Quiver.IsThin 𝒰.I₀], (d.functor.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.self_le_maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k fallback : α}, (cmp k ((t.insert k).maxD fallback)).isLE = true
-- Init.Grind.Offset
Lean.Grind.Nat.ro_eq_true_of_lo : ∀ (u v k₁ k₂ : ℕ), u + k₁ ≤ v → (u ≤ v + k₂) = True
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₂_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_245✝ ⟶ g.obj' 0 _proof_245✝) (app₁ : f.obj' 1 _proof_246✝ ⟶ g.obj' 1 _proof_246✝)
  (app₂ : f.obj' 2 _proof_247✝ ⟶ g.obj' 2 _proof_247✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
      _auto_256✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_247✝))
      _auto_258✝),
  (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_startPos : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, String.Slice.Pos.ofSlice (s.slice p₀ p₁ h).startPos = p₀
-- Mathlib.Algebra.Order.Group.PosPart
Pi.oneLePart_def : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → Group (α i)]
  (f : (i : ι) → α i), f⁺ᵐ = fun i => (f i)⁺ᵐ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight h Z) =
    CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f h) g