mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- The opposite localizer morphism `LocalizerMorphism W₁.op W₂.op` deduced
from `Φ : LocalizerMorphism W₁ W₂`.  -/
CategoryTheory.LocalizerMorphism.op : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            CategoryTheory.LocalizerMorphism W₁ W₂ → CategoryTheory.LocalizerMorphism W₁.op W₂.op
-- Mathlib.Tactic.Core
/-- Run a tactic on all goals, and always succeeds.

(This is parallel to `Lean.Elab.Tactic.evalAllGoals` in core,
which takes a `Syntax` rather than `TacticM Unit`.
This function could be moved to core and `evalAllGoals` refactored to use it.)
 -/
Lean.Elab.Tactic.allGoals : Lean.Elab.Tactic.TacticM Unit → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Order.Hom.Units
OrderMonoidIso.val_unitsCongr_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : Preorder β] [inst_3 : Monoid β]
  (e : α ≃*o β) (a : βˣ), ↑(e.unitsCongr.symm a) = (↑e).symm ↑a
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iInf_natCast_eq_top`. -/
ENat.iInf_coe_eq_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨅ i, ↑(f i) = ⊤ ↔ IsEmpty ι
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.enum.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.enum = 1
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMaxOrderElemIio : ∀ (α : Type u_1) [inst : Preorder α] [DenselyOrdered α] {x : α}, NoMaxOrder ↑(Set.Iio x)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instPowSubtypeMemInt : {K : Type u} → [inst : DivisionRing K] → (s : Subfield K) → Pow ↥s ℤ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂_mk_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g : β → γ → δ)
  (hg : Continuous (Function.uncurry g)) (f₁ : α → β) (f₂ : α → γ) (hf₁ : MeasureTheory.AEStronglyMeasurable f₁ μ)
  (hf₂ : MeasureTheory.AEStronglyMeasurable f₂ μ),
  MeasureTheory.AEEqFun.comp₂ g hg (MeasureTheory.AEEqFun.mk f₁ hf₁) (MeasureTheory.AEEqFun.mk f₂ hf₂) =
    MeasureTheory.AEEqFun.mk (fun a => g (f₁ a) (f₂ a)) ⋯
-- Mathlib.Data.Nat.GCD.Basic
Nat.dvd_of_lcm_right_dvd : ∀ {a b c : ℕ}, a.lcm b ∣ c → a ∣ c
-- Mathlib.Data.Fin.SuccPred
/-- The range of `p.succAbove` is everything except `p`.  -/
Fin.range_succAbove : ∀ {n : ℕ} (p : Fin (n + 1)), Set.range p.succAbove = {p}ᶜ
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_div : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (a b : Quaternion R),
  Quaternion.normSq (a / b) = Quaternion.normSq a / Quaternion.normSq b
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_dirac' : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} [inst_6 : MeasurableSpace X] [CompleteSpace G] {a : X} {v : F},
  MeasureTheory.StronglyMeasurable f → ∫ᵛ (x : X), f x ∂[B; MeasureTheory.VectorMeasure.dirac a v] = (B (f a)) v
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_neg_apply : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : AdicCompletion I M) (n : ℕ), ↑(-f) n = -↑f n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The composition `inv ≫ hom` is isomorphic to the identity.  -/
CategoryTheory.Bicategory.Equivalence.counit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (self : CategoryTheory.Bicategory.Equivalence a b) →
        CategoryTheory.CategoryStruct.comp self.inv self.hom ≅ CategoryTheory.CategoryStruct.id b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [CommSemigroup M] → CommSemigroup (l.Germ M)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.revSkip?_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.endPos.revSkip? pat = s.skipSuffix? pat
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Bound.0.SzemerediRegularity.Positivity.m_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α → 0 < Fintype.card α / SzemerediRegularity.stepBound P.parts.card
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.min_lexOrder_le : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ ψ : MvPowerSeries σ R}, min φ.lexOrder ψ.lexOrder ≤ (φ + ψ).lexOrder
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey! t.minKey! = t.minKey!
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.subsingleton_eq_refl : ∀ {α : Sort u} [Subsingleton α] (e : Equiv.Perm α), e = Equiv.refl α
-- Init.System.FilePath
System.instHashableFilePath.hash : System.FilePath → UInt64
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- The `star` map in a normed star group is an isometry  -/
star_isometry : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E], Isometry star
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.instMembershipSet.eq_1 : ∀ {G : Type u} [inst : Group G], GroupFilterBasis.instMembershipSet = { mem := fun f s => s ∈ f.sets }
-- Mathlib.CategoryTheory.Galois.Basic
/-- The cardinality of the fiber is preserved under isomorphisms.  -/
CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C}
  (i : X ≅ Y), Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
-- Mathlib.Order.Filter.Partial
/-- One way of taking the inverse map of a filter under a relation. One generalization of
`Filter.comap` to relations. Note that `Rel.core` generalizes `Set.preimage`.  -/
Filter.rcomap : {α : Type u} → {β : Type v} → SetRel α β → Filter β → Filter α
-- Init.Data.Array.Basic
/-- Returns the last element of an array, or panics if the array is empty.

Safer alternatives include `Array.back`, which requires a proof the array is non-empty, and
`Array.back?`, which returns an `Option`.
 -/
Array.back! : {α : Type u} → [Inhabited α] → Array α → α
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.closedBall_subset_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ε : ℝ}
  {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} [inst_5 : CompleteSpace E]
  (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) {b : E},
  0 ≤ ε →
    Metric.closedBall b ε ⊆ s →
      Metric.closedBall (f b) ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * ε) ⊆
        (ApproximatesLinearOn.toOpenPartialHomeomorph f s hf hc hs).target
-- Mathlib.Data.Finset.Lattice.Fold
Finset.mem_sup : ∀ {α : Type u_2} {ι : Type u_5} [inst : DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α},
  a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Given `T : F →L[𝕜] F'`, `postcompLM T` is the `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)`
to `T ∘ f` as an element of `𝓓^{n}_{K}(E, F')`.

This is subsumed by `postcompCLM T`, which also bundles the continuity.  -/
ContDiffMapSupportedIn.postcompLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {F' : Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    [inst_6 : SMulCommClass ℝ 𝕜 F] →
                      [inst_7 : NormedAddCommGroup F'] →
                        [inst_8 : NormedSpace ℝ F'] →
                          [inst_9 : NormedSpace 𝕜 F'] →
                            [inst_10 : SMulCommClass ℝ 𝕜 F'] →
                              {n : ℕ∞} →
                                {K : TopologicalSpace.Compacts E} →
                                  [LinearMap.CompatibleSMul F F' ℝ 𝕜] →
                                    (F →L[𝕜] F') → ContDiffMapSupportedIn E F n K →ₗ[𝕜] ContDiffMapSupportedIn E F' n K
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformlyOn.sub : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn G g l s → TendstoLocallyUniformlyOn (F - G) (f - g) l s
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.halt.sizeOf_spec : ∀ (a : List ℕ), sizeOf (Turing.ToPartrec.Cfg.halt a) = 1 + sizeOf a
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.inf_mem_subalgebra_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f g : ↥A),
  ↑f ⊓ ↑g ∈ A.topologicalClosure
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivWithinAt_comp_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (a : E),
  HasFDerivWithinAt (fun x => f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h i : b ⟶ c} {j : a ⟶ c}
  {k : c ⟶ d} {α : g ≅ CategoryTheory.CategoryStruct.comp f h} {η : h ⟶ i}
  {ηs : CategoryTheory.CategoryStruct.comp f i ⟶ j}
  {η₁ : CategoryTheory.CategoryStruct.comp h k ⟶ CategoryTheory.CategoryStruct.comp i k}
  {η₂ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i k)}
  {ηs₁ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) k ⟶
      CategoryTheory.CategoryStruct.comp j k}
  {ηs₂ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i k) ⟶
      CategoryTheory.CategoryStruct.comp j k}
  {η₃ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶
      CategoryTheory.CategoryStruct.comp j k}
  {η₄ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) k ⟶
      CategoryTheory.CategoryStruct.comp j k}
  {η₅ : CategoryTheory.CategoryStruct.comp g k ⟶ CategoryTheory.CategoryStruct.comp j k},
  CategoryTheory.Bicategory.whiskerRight
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl h).hom
          (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl i).hom))
        k =
      η₁ →
    CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂ →
      CategoryTheory.Bicategory.whiskerRight ηs k = ηs₁ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f i k).inv ηs₁ = ηs₂ →
          CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃ →
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f h k).hom η₃ = η₄ →
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRightIso α k).hom η₄ = η₅ →
                CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.CategoryStruct.comp α.hom
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) ηs))
                    k =
                  η₅
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.addFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Init.Data.Option.Lemmas
Option.some_get! : ∀ {α : Type u_1} [inst : Inhabited α] (o : Option α), o.isSome = true → some o.get! = o
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_one_le_add_one_iff : ∀ {α β : Cardinal.{u_1}}, α + 1 ≤ β + 1 ↔ α ≤ β
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_mul_noncomm : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  (∀ (k : ℕ), Commute (f (q.coeff k)) x) →
    Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.div_isBoundedUnder_of_isBigO : ∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜},
  f =O[l] g → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x / g x‖
-- Mathlib.Data.Real.ENatENNReal
ENat.hasCoeENNReal : CoeTC ℕ∞ ENNReal
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE : ∀ (p : ℤ), (ComplexShape.embeddingUpIntLE p).IsRelIff
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.congr_simp : ∀ (ι ι_1 : Type u_1) (e_ι : ι = ι_1) {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : LieRing L] [inst_3 : LieAlgebra R L] (H H_1 : LieSubalgebra R L),
  H = H_1 → LieAlgebra.Basis ι H = LieAlgebra.Basis ι_1 H_1
-- Mathlib.Analysis.Quaternion
Quaternion.normSq_eq_norm_mul_self : ∀ (a : Quaternion ℝ), Quaternion.normSq a = ‖a‖ * ‖a‖
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.MemLp (fun x => 0) p μ
-- Mathlib.Algebra.Group.Prod
Prod.instCommSemigroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : CommSemigroup G] [inst_1 : CommSemigroup H],
  Prod.instCommSemigroup = { toSemigroup := Prod.instSemigroup, mul_comm := ⋯ }
-- Init.Data.Nat.Lemmas
Nat.pred_min_pred : ∀ (x y : ℕ), min x.pred y.pred = (min x y).pred
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).getKey? k' =
        if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then some k else none else t.getKey? k'
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.norm_comm_assoc : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] {A B : Rep.{u_1, u, v} k G}
  (f : A ⟶ B) {Z : Rep.{u_1, u, v} k G} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp B.norm h) =
    CategoryTheory.CategoryStruct.comp A.norm (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ) (f : A ⟶ B),
  (CategoryTheory.opEquiv A B) f = f.unop
-- Mathlib.Topology.ContinuousOn
continuousOn_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α},
  Set.EqOn g f s → (ContinuousOn g s ↔ ContinuousOn f s)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_mul_right : ∀ {m n : ℕ}, n ≠ 0 → (m * n).choose n = m * (m * n - 1).choose (n - 1)
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by applying the emod operation constraining the lower bound to 0 and
the upper bound to the value.
 -/
Std.Time.Internal.Bounded.LE.emod : {n num : ℤ} → Std.Time.Internal.Bounded.LE n num → (num : ℤ) → 0 < num → Std.Time.Internal.Bounded.LE 0 (num - 1)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_smul : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {R : Type u_14} [inst : SMul R α] (x : R)
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α), (x • M).blockDiag' = x • M.blockDiag'
-- Std.Http.Data.Response
/-- Adds a single header to the response being built.
Returns `none` if the header name or value is invalid.
 -/
Std.Http.Response.Builder.header? : Std.Http.Response.Builder → String → String → Option Std.Http.Response.Builder
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.semigroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Semigroup G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffMul I' n G] → Semigroup (ContMDiffMap I I' N G n)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.domRestrict_comp_codRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (g : L.Hom N P) (f : L.Hom M N) (p : L.Substructure N) (h : ∀ (b : M), f b ∈ p),
  (g.domRestrict p).comp (FirstOrder.Language.Hom.codRestrict p f h) = g.comp f
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.surjective : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), Function.Surjective ⇑e
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGEMap_comp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'] [inst_6 : CategoryTheory.Limits.HasZeroObject C],
  HomologicalComplex.truncGEMap (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ e) (HomologicalComplex.truncGEMap φ' e)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.insert.eq_2 : ∀ (k : ℕ) (v : Nat.Internal.Linear.Var) (k_1 : ℕ) (v_1 : Nat.Internal.Linear.Var)
  (p_2 : List (ℕ × Nat.Internal.Linear.Var)),
  Nat.Internal.Linear.Poly.insert k v ((k_1, v_1) :: p_2) =
    bif Nat.blt v v_1 then (k, v) :: (k_1, v_1) :: p_2
    else bif Nat.beq v v_1 then (k + k_1, v_1) :: p_2 else (k_1, v_1) :: Nat.Internal.Linear.Poly.insert k v p_2
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_le_iff : ∀ {M : Type u_2} [inst : MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω),
  μ ≠ 0 → ↑μ.normalize = μ.mass⁻¹ • ↑μ
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.phase.inj : ∀ {p p_1 : Aesop.PhaseName}, Aesop.Frontend.Feature.phase p = Aesop.Frontend.Feature.phase p_1 → p = p_1
-- Mathlib.Order.Cover
WCovBy.Ico_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → Set.Ico a b ⊆ {a}
-- Lean.Parser.Command
Lean.Parser.Command.export.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_roi : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LT α] [DecidableLT α] [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.Rxi.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roi α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_right_Icc : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  a ≤ b → 0 ≤ c → (fun x => x * c) '' Set.Icc a b = Set.Icc (a * c) (b * c)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A difference is equal to its expansion by a summand from `S`.  -/
AddOreLocalization.expand' : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r : X) (s s' : ↥S), r -ₒ s = (s' +ᵥ r) -ₒ (s' + s)
-- Init.Data.String.TakeDrop
/-- Checks whether the first string \(`s`\) begins with the pattern \(`pat`\).

`String.isPrefixOf` is a version that takes the
potential prefix before the string.

Examples:

* `"red green blue".startsWith "red" = true`

* `"red green blue".startsWith "green" = false`

* `"red green blue".startsWith "" = true`

* `"red green blue".startsWith 'r' = true`

* `"red green blue".startsWith Char.isLower = true`
 -/
String.startsWith : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Bool
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.isConnected_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
  IsConnected (⇑h ⁻¹' s) ↔ IsConnected s
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instIsStableUnderRetractsOppositeCofibrationsOfFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts], (HomotopicalAlgebra.cofibrations Cᵒᵖ).IsStableUnderRetracts