mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Chain
List.IsChain.append : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α},
  List.IsChain R l₁ → List.IsChain R l₂ → (∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y) → List.IsChain R (l₁ ++ l₂)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- `autGalois.π` is surjective for every pointed Galois object.  -/
CategoryTheory.PreGaloisCategory.AutGalois.π_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.AutGalois.π F A)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.const_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a : X} {b : Y}
  (ha : IsOpen {a}) (hb : IsOpen {b}), (OpenPartialHomeomorph.const ha hb).source = {a}
-- Mathlib.Data.Rat.Lemmas
Rat.num_den_mk : ∀ {q : ℚ} {n d : ℤ}, d ≠ 0 → q = Rat.divInt n d → ∃ c, n = c * q.num ∧ d = c * ↑q.den
-- Mathlib.Topology.Order.Compact
/-- A compact set is bounded above  -/
IsCompact.bddAbove : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α] [Nonempty α] {s : Set α},
  IsCompact s → BddAbove s
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.prodMk : ∀ {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} {x : MeasurableSpace β} {x_1 : MeasurableSpace γ}
  {f : α → β} {g : α → γ}, Measurable f → Measurable g → Measurable fun a => (f a, g a)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_uIoc_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.uIoc ↑i ↑j = Set.uIoc i j
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'.congr_simp : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))))
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂ =
    X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂
-- Lean.Elab.Tactic.SimpTrace
Lean.Elab.Tactic.evalSimpAllTrace : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.UniformSpace.Path
Path.uniformContinuous_symm : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X}, UniformContinuous Path.symm
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.toString : Aesop.ScriptGenerated → String
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertList_cons_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {p : (a : α) × β a},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys (p :: l₂) →
      (Std.Internal.List.insertList l₁ (p :: l₂)).Perm
        (Std.Internal.List.insertEntry p.fst p.snd (Std.Internal.List.insertList l₁ l₂))
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.scomp_hasDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F}
  {y : 𝕜'},
  HasDerivWithinAt g₁ g₁' s' y → HasDerivAt h h' x → (∀ (x : 𝕜), h x ∈ s') → y = h x → HasDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib.Tactic.MinImports
/-- `#min_imports in cmd` scans the syntax `cmd` and the declaration obtained by elaborating `cmd`
to find a collection of minimal imports that should be sufficient for `cmd` to work.  -/
Mathlib.Command.MinImports.«command#min_importsIn_» : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Every connected graph on `n` vertices has at least `n-1` edges.  -/
SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one : ∀ {V : Type u_1} {G : SimpleGraph V}, G.Connected → Nat.card V ≤ Nat.card ↑G.edgeSet + 1
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) (a : R),
  ((MvPolynomial.monomial s) a).degrees ≤ Finsupp.toMultiset s
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_add_single_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {m : ℕ} [NeZero m] {n : σ →₀ ℕ} (a : R) (i : σ),
  (MvPowerSeries.coeff (n + fun₀ | i => m)) (MvPowerSeries.C a) = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsAddUnit.multisetSum_iff : ∀ {M : Type u_4} [inst : AddCommMonoid M] {s : Multiset M}, IsAddUnit s.sum ↔ ∀ a ∈ s, IsAddUnit a
-- Init.Data.Vector.Lemmas
/-- The empty vector maps to the empty vector.  -/
Vector.map_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Vector.map f #v[] = #v[]
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(α →₁ₛ[μ] ℝ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.L1.SimpleFunc.posPart f)) =ᵐ[μ]
    ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f).posPart
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.congr_simp : ∀ (R : Type u_1) (G : Type u_2) (V : Type u_3) [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V],
  ContRepresentation R G V = ContRepresentation R G V
-- Mathlib.Topology.Sequences
IsCompact.isSeqCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] {s : Set X}, IsCompact s → IsSeqCompact s
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_iff_of_summable_sub : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f g : β → α}, Summable (fun b => f b - g b) L → (Summable f L ↔ Summable g L)
-- Mathlib.RingTheory.Jacobson.Radical
Module.comap_jacobson_of_bijective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Bijective ⇑f → Submodule.comap f (Module.jacobson R₂ M₂) = Module.jacobson R M
-- Std.Data.ExtTreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in ascending order.  -/
Std.ExtTreeMap.foldlM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] → [LawfulMonad m] → [Std.TransCmp cmp] → (δ → α → β → m δ) → δ → Std.ExtTreeMap α β cmp → m δ
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.triangle_aux₃ : ∀ {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)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X Y : CategoryTheory.LocalizedMonoidal L W ε} {X' Y' : C}
  (e₁ : (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X' ≅ X)
  (e₂ : (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y' ≅ Y),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom e₁.inv ε.inv)
        e₂.inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          (CategoryTheory.MonoidalCategoryStruct.tensorObj
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X')
            (L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          e₂.hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Localization.Monoidal.μ L W ε X' (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
                (CategoryTheory.MonoidalCategoryStruct.rightUnitor X').hom))
            Y)
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight e₁.hom Y)))
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csSup_eq_greatestOfBdd : ∀ {s : Set ℤ} [inst : DecidablePred fun x => x ∈ s] (b : ℤ) (Hb : ∀ z ∈ s, z ≤ b) (Hinh : ∃ z, z ∈ s),
  sSup s = ↑(b.greatestOfBdd Hb Hinh)
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.mk'.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y} [inst_2 : SizeOf C]
  (base' : CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g),
  sizeOf { base' := base' } = 1 + sizeOf base'
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.homAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} [inst_3 : HasDerivedCategory C]
  (α : CategoryTheory.Abelian.Ext X Y n), CategoryTheory.Abelian.Ext.homAddEquiv α = α.hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.hasDimensionLT_of_finite : ∀ (X : SSet) [X.Finite], ∃ d, X.HasDimensionLT d
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.of_subsingleton : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} [Subsingleton ι] {m : ι → MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  [ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.Kernel.iIndep m κ μ
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedAltParamInfo.default : Lean.Meta.Match.AltParamInfo
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The subset of `C` consisting of those elements whose `o`-th entry is `true`.  -/
Profinite.NobelingProof.C1 : {I : Type u} →
  Set (I → Bool) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] → {o : Ordinal.{u}} → (o < Ordinal.type fun x1 x2 => x1 < x2) → Set (I → Bool)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommSemigroup α],
  AddOpposite.instAddCommSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, add_comm := ⋯ }
-- Aesop.Stats.Basic
/-- Total elapsed time of failed applications of a rule.
 -/
Aesop.RuleStatsTotals.elapsedFailed : Aesop.RuleStatsTotals → Aesop.Nanos
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂.eq_2 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f : α₁ → β₁ → Finset γ₁) (g : α₂ → β₂ → Finset γ₂) (val : α₁) (val_1 : β₂),
  Finset.sumLift₂ f g (Sum.inl val) (Sum.inr val_1) = ∅
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filter_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.isEmpty = true ↔
    ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true),
      f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h) = false
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `PComp.add c1 c2 elimVar` creates the result of summing the linear comparisons `c1` and `c2`,
during the process of eliminating the variable `elimVar`.
The computation assumes, but does not enforce, that `elimVar` appears in both `c1` and `c2`
and does not appear in the sum.
Computing the sum of the two comparisons is easy; the complicated details lie in tracking the
additional fields of `PComp`.
* The historical set `pcomp.history` of `c1 + c2` is the union of the two historical sets.
* `vars` is the union of `c1.vars` and `c2.vars`.
* The effectively eliminated variables of `c1 + c2` are the union of the two effective sets,
  with `elim_var` inserted.
* The implicitly eliminated variables of `c1 + c2` are those that appear in
  `vars` but not `c.vars` or `effective`.

(Note that the description of the implicitly eliminated variables of `c1 + c2` in the algorithm
described in Section 6 of https://doi.org/10.1016/B978-0-444-88771-9.50019-2 seems to be wrong:
that says it should be `(c1.implicit.union' c2.implicit).sdiff explicit`.
Since the implicitly eliminated sets start off empty for the assumption,
this formula would leave them always empty.)
 -/
Mathlib.Tactic.Linarith.PComp.add : Mathlib.Tactic.Linarith.PComp → Mathlib.Tactic.Linarith.PComp → ℕ → Mathlib.Tactic.Linarith.PComp
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.pair_eq_singleton_iff : ∀ {x y z : ZFSet.{u_1}}, {x, y} = {z} ↔ x = z ∧ y = z
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAddMonoid.eq_1 : ∀ {α : Type u} [inst : AddSemigroup α],
  WithZero.instAddMonoid =
    { toAdd := WithZero.instAddZeroClass.toAdd, add_assoc := ⋯, toZero := WithZero.instAddZeroClass.toZero,
      zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- If `ι.obj X₁ ⟶ ι.obj X₂ ⟶ ι.obj X₃ ⟶ ...` is a distinguished triangle,
then `X₁` is a kernel of `X₂ ⟶ X₃`.  -/
CategoryTheory.Triangulated.AbelianSubcategory.isLimitKernelForkOfDistTriang : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : CategoryTheory.Category.{v_2, u_2} A] →
                  {ι : CategoryTheory.Functor A C} →
                    (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)),
                        n < 0 → f = 0) →
                      [inst_7 : CategoryTheory.Preadditive A] →
                        [ι.Full] →
                          [inst_9 : ι.Faithful] →
                            [CategoryTheory.Limits.HasFiniteProducts A] →
                              [inst_11 : ι.Additive] →
                                {X₁ X₂ X₃ : A} →
                                  (f₁ : X₁ ⟶ X₂) →
                                    (f₂ : X₂ ⟶ X₃) →
                                      (f₃ : ι.obj X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)) →
                                        (hT :
                                            CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f₁ ⋯)
-- Mathlib.Data.Quot
Quotient.lift₂_mk : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {x : Setoid α} {x_1 : Setoid β} (f : α → β → γ)
  (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β),
  Quotient.lift₂ f h ⟦a⟧ ⟦b⟧ = f a b
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] [inst_2 : DecidableEq α] (a : α) (x : M),
  AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq a x =
    AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq._aux_1 a x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.monic_polynomial : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R}, W.polynomial.Monic
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.one_lt_ofNat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ} [inst_5 : n.AtLeastTwo], 1 < OfNat.ofNat n
-- Mathlib.Topology.Homotopy.Basic
/-- Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic with respect to the
predicate `P` if there exists a `HomotopyWith f₀ f₁ P`.
 -/
ContinuousMap.HomotopicWith : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → (C(X, Y) → Prop) → Prop
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.map.eq_1 : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G)
  (e : G ≃+ H), b.map e = { repr := e.symm.trans b.repr }
-- Init.Meta.Defs
/-- Syntax that represents a scientific numeric literal that may have decimal and exponential parts.
 -/
Lean.Syntax.ScientificLit : Type
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- Given a vertex, returns the unique edge of the matching it is incident to.  -/
SimpleGraph.Subgraph.IsMatching.toEdge : {V : Type u_1} → {G : SimpleGraph V} → {M : G.Subgraph} → M.IsMatching → ↑M.verts → ↑M.edgeSet
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableSymbolTag.hash : Lean.Lsp.SymbolTag → UInt64
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionsResult.subgoal.injEq : ∀ (mvarId : Lean.MVarId) (remainingNames : List Lean.Name) (forbidden : Lean.FVarIdSet) (mvarId_1 : Lean.MVarId)
  (remainingNames_1 : List Lean.Name) (forbidden_1 : Lean.FVarIdSet),
  (Lean.Meta.InjectionsResult.subgoal mvarId remainingNames forbidden =
      Lean.Meta.InjectionsResult.subgoal mvarId_1 remainingNames_1 forbidden_1) =
    (mvarId = mvarId_1 ∧ remainingNames = remainingNames_1 ∧ forbidden = forbidden_1)
-- Init.Data.Range.Polymorphic.PRange
/-- A full range of all elements of `α`. Its only inhabitant is the range `*...*`, which is
notation for `Rii.mk`.
 -/
Std.Rii : Type u → Type
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_roi : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_roi._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun e => (cmp e.fst bound).isGT) t.toList
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_scomp_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {x : 𝕜},
  ContDiffAt 𝕜 2 g (f x) →
    ContDiffAt 𝕜 2 f x →
      iteratedDeriv 2 (g ∘ f) x = deriv f x ^ 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
StrongDual.toWeakDual_inj : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x' y' : StrongDual 𝕜 E), StrongDual.toWeakDual x' = StrongDual.toWeakDual y' ↔ x' = y'
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is differentiable and `f'` is monotone on `ℝ` then `f` is convex.  -/
Monotone.convexOn_univ_of_deriv : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → Monotone (deriv f) → ConvexOn ℝ Set.univ f
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- The natural category equivalence between `R`-coalgebras and comonoid objects in the
category of `R`-modules.  -/
CoalgCat.comonEquivalence : (R : Type u) → [inst : CommRing R] → CoalgCat R ≌ CategoryTheory.Comon (ModuleCat R)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_intCast_eq_padic_norm : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ), ‖↑z‖ = ‖↑z‖
-- Batteries.Data.Array.Match
/-- Find next match from a given stream

Runs the stream until it reads a sequence that matches the sought pattern, then returns the stream
state at that point and an updated matcher state.
 -/
Array.Matcher.next? : {α : Type u_1} → {σ : Type u_2} → [BEq α] → [Std.Stream σ α] → Array.Matcher α → σ → Option (σ × Array.Matcher α)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.instIsLeftDerivedFunctorLiftHomFac : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] (hF : W.IsInvertedBy F),
  (CategoryTheory.Localization.lift F hF L).IsLeftDerivedFunctor (CategoryTheory.Localization.fac F hF L).hom W
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.f_pOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.f S.pOpcycles = 0
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ‖f'‖` the ratio
`(‖f z‖ - ‖f x‖) / (z - x)` is frequently less than `r` as `z → x+0`.
In other words, the limit inferior of this ratio as `z` tends to `x+0`
is less than or equal to `‖f'‖`.

See also

* `HasDerivWithinAt.limsup_norm_slope_le` for a stronger version using
  limit superior and any set `s`;
* `HasDerivWithinAt.liminf_right_norm_slope_le` for a stronger version using
  `‖f z - f xp‖` instead of `‖f z‖ - ‖f x‖`.  -/
HasDerivWithinAt.liminf_right_slope_norm_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ},
  HasDerivWithinAt f f' (Set.Ici x) x →
    ‖f'‖ < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
-- Mathlib.Analysis.Seminorm
/-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
the rescaling element that shows up in applications.  -/
rescale_to_shell_semi_normed : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, ‖x‖ ≠ 0 → ∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.maximal_normal_subgroupOf_normalizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, Maximal (fun x => (H.subgroupOf x).Normal) (Subgroup.normalizer ↑H)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.one_le_negOnePow_mul_eval_T_real : ∀ (n : ℤ) {x : ℝ}, x ≤ -1 → 1 ≤ ↑↑n.negOnePow * Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.tensor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {W X Y Z : C} →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj W] →
          [inst_3 : Mathlib.Tactic.Coherence.LiftObj X] →
            [inst_4 : Mathlib.Tactic.Coherence.LiftObj Y] →
              [inst_5 : Mathlib.Tactic.Coherence.LiftObj Z] →
                (f : W ⟶ X) →
                  (g : Y ⟶ Z) →
                    [Mathlib.Tactic.Coherence.LiftHom f] →
                      [Mathlib.Tactic.Coherence.LiftHom g] →
                        Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)