mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.FiveLemma
/-- The five lemma in terms of additive groups.
For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {M₅ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7}
  {N₃ : Type u_8} {N₄ : Type u_9} {N₅ : Type u_10} [inst : AddGroup M₁] [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃]
  [inst_3 : AddGroup M₄] [inst_4 : AddGroup M₅] [inst_5 : AddGroup N₁] [inst_6 : AddGroup N₂] [inst_7 : AddGroup N₃]
  [inst_8 : AddGroup N₄] [inst_9 : AddGroup N₅] (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (f₄ : M₄ →+ M₅)
  (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (g₄ : N₄ →+ N₅) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃)
  (i₄ : M₄ →+ N₄) (i₅ : M₅ →+ N₅),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        g₄.comp i₄ = i₅.comp f₄ →
          Function.Exact ⇑f₁ ⇑f₂ →
            Function.Exact ⇑f₂ ⇑f₃ →
              Function.Exact ⇑f₃ ⇑f₄ →
                Function.Exact ⇑g₁ ⇑g₂ →
                  Function.Exact ⇑g₂ ⇑g₃ →
                    Function.Exact ⇑g₃ ⇑g₄ →
                      Function.Surjective ⇑i₁ →
                        Function.Bijective ⇑i₂ →
                          Function.Bijective ⇑i₄ → Function.Injective ⇑i₅ → Function.Bijective ⇑i₃
-- Mathlib.Topology.Algebra.ConstMulAction
AddAction.IsPretransitive.discreteTopology_iff : ∀ {α : Type u_2} (G : Type u_4) [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (x : α) [AddAction.IsPretransitive G α], DiscreteTopology α ↔ IsOpen {x}
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_closedEBall_le`. -/
EMetric.diam_closedBall : ∀ {X : Type u_2} {x : X} [inst : PseudoEMetricSpace X] {r : ENNReal}, Metric.ediam (Metric.closedEBall x r) ≤ 2 * r
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.adjoin_basis_eq_top : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IntermediateField.adjoin F (Set.range ⇑(Field.Emb.Cardinal.wellOrderedBasis F E)) = ⊤
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.enlarge : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S T : Set (Set X)},
  Topology.IsCoherentWith S → (∀ s ∈ S, ∃ t ∈ T, s ⊆ t) → Topology.IsCoherentWith T
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.mk.inj : ∀ {toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams} {textDocument : Lean.Lsp.TextDocumentIdentifier}
  {range : Lean.Lsp.Range} {toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams}
  {textDocument_1 : Lean.Lsp.TextDocumentIdentifier} {range_1 : Lean.Lsp.Range},
  { toWorkDoneProgressParams := toWorkDoneProgressParams, textDocument := textDocument, range := range } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, textDocument := textDocument_1, range := range_1 } →
    toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧ textDocument = textDocument_1 ∧ range = range_1
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) [inst_2 : Inhabited (β a)],
  Std.DHashMap.Internal.AssocList.getCast! a Std.DHashMap.Internal.AssocList.nil =
    panicWithPosWithDecl "Std.Data.DHashMap.Internal.AssocList.Basic" "Std.DHashMap.Internal.AssocList.getCast!" 153 11
      "key is not present in hash table"
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.star_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : StarAddMonoid β]
  [inst_3 : NormedStarGroup β] (f : BoundedContinuousFunction α β) (x : α), (star f) x = star (f x)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_fun_smul : ∀ {𝕜 : 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}
  {x : E} {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      DifferentiableWithinAt 𝕜 f s x →
        fderivWithin 𝕜 (fun y => c y • f y) s x = c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.dfun : ∀ {ι : Type u} {α : ι → Type v} {β : ι → Type w} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → Preorder (β i)]
  (l : (i : ι) → α i → β i) (u : (i : ι) → β i → α i),
  (∀ (i : ι), GaloisConnection (l i) (u i)) → GaloisConnection (fun a i => l i (a i)) fun b i => u i (b i)
-- Init.Data.List.Impl
List.replace.eq_1 : ∀ {α : Type u} [inst : BEq α] (x x_1 : α), [].replace x x_1 = []
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions.resolveProvider? : Lean.Lsp.InlayHintOptions → Option Bool
-- Std.Data.ExtDTreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in descending order.  -/
Std.ExtDTreeMap.foldrM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] →
            [LawfulMonad m] → [Std.TransCmp cmp] → ((a : α) → β a → δ → m δ) → δ → Std.ExtDTreeMap α β cmp → m δ
-- Init.Core
Subtype.instReflBEq : ∀ {α : Type u} {p : α → Prop} [inst : BEq α] [ReflBEq α], ReflBEq { x // p x }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reducePred : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
-- Lean.Elab.Tactic.Omega.Frontend
/-- Construct the linear combination (and its associated proof and new facts) for an atom.  -/
Lean.Elab.Tactic.Omega.mkAtomLinearCombo : Lean.Expr →
  Lean.Elab.Tactic.Omega.OmegaM (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM Lean.Expr × List Lean.Expr)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, max u v} (CategoryTheory.Square C)
-- Init.Data.Ord.Basic
Ordering.isLE_then_iff_or : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE = true ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂.isLE = true
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The covering number of the image of a set under an injective isometry is equal to
the covering number of the set.
See `Isometry.coveringNumber_image'` for the version in a `PseudoEMetricSpace` and not
an `EMetricSpace`, for which an additional injectivity assumption is needed.  -/
Isometry.coveringNumber_image : ∀ {Y : Type u_2} [inst : PseudoEMetricSpace Y] {ε : NNReal} {X : Type u_3} [inst_1 : EMetricSpace X] {f : X → Y},
  Isometry f → ∀ {A : Set X}, Metric.coveringNumber ε (f '' A) = Metric.coveringNumber ε A
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_inner_mul_inner : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x y : E),
  ∑ i, inner 𝕜 x (b i) * inner 𝕜 (b i) y = inner 𝕜 x y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.prod_apply : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) (x : M₁), (f₁.prod f₂) x = (f₁ x, f₂ x)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- The value of the quadratic character at `2`  -/
quadraticChar_two : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → (quadraticChar F) 2 = ZMod.χ₈ ↑(Fintype.card F)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_preimage_le : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Set L),
  Subfield.closure (⇑f ⁻¹' s) ≤ Subfield.comap f (Subfield.closure s)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Positive part of a simple function.  -/
MeasureTheory.SimpleFunc.posPart : {α : Type u_1} →
  {E : Type u_2} →
    [LinearOrder E] →
      [Zero E] → [inst : MeasurableSpace α] → MeasureTheory.SimpleFunc α E → MeasureTheory.SimpleFunc α E
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : LowerSet α) (t₁ t₂ : LowerSet β),
  s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A pullback cone is just a cone on the cospan formed by two morphisms `f : X ⟶ Z` and
`g : Y ⟶ Z`.  -/
CategoryTheory.Limits.PullbackCone : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : C} → (X ⟶ Z) → (Y ⟶ Z) → Type (max (max 0 u) v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k fallback : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKeyD k fallback = fallback
-- Mathlib.Order.Filter.Cofinite
Filter.Tendsto.exists_within_forall_ge : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder β] {s : Set α},
  s.Nonempty → ∀ {f : α → β}, Filter.Tendsto f Filter.cofinite Filter.atBot → ∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_union_le_size_add_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- If `f ∈ A` is a homogeneous element of positive degree, then the projective spectrum restricted to
`D(f)` as a locally ringed space is isomorphic to `Spec A⁰_f`.
 -/
AlgebraicGeometry.projIsoSpec : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯ ≅
                        AlgebraicGeometry.Spec.locallyRingedSpaceObj
                          (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)))
-- Mathlib.Order.Bounds.Defs
lowerBounds.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), lowerBounds s = {x | ∀ ⦃a : α⦄, a ∈ s → x ≤ a}
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.generator'.congr_simp : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete], Valuation.IsRankOneDiscrete.generator' v = Valuation.IsRankOneDiscrete.generator' v
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_comm' : ∀ {α : Type u} [inst : TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x y : Option α), edist x y = edist y x
-- Lean.DocString.Links
/-- Constructs a link to the manual.
 -/
Lean.manualLink : String → String → Except String String
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.map_le_dualAnnihilator_dualAnnihilator : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V),
  Submodule.map (Module.Dual.eval K V) W ≤ (Submodule.dualAnnihilator W).dualAnnihilator
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
deriv_const_rpow : ∀ {f : ℝ → ℝ} {x a : ℝ}, 0 < a → DifferentiableAt ℝ f x → deriv (fun x => a ^ f x) x = Real.log a * deriv f x * a ^ f x
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`.  -/
AbsoluteValue.apply_nat_le_self : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) [IsDomain S] [IsOrderedRing S] (n : ℕ), abv ↑n ≤ ↑n
-- Mathlib.Topology.MetricSpace.Polish
/-- A type synonym for a subset `s` of a metric space, on which we will construct another metric
for which it will be complete.  -/
TopologicalSpace.Opens.CompleteCopy : {α : Type u_3} → [inst : MetricSpace α] → TopologicalSpace.Opens α → Type u_3
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instBalanced : CategoryTheory.Balanced SimplexCategory
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.List.toByteArray.match_1.eq_1 : ∀ (motive : List UInt8 → ByteArray → Sort u_1) (r : ByteArray) (h_1 : (r : ByteArray) → motive [] r)
  (h_2 : (b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r),
  (match [], r with
    | [], r => h_1 r
    | b :: bs, r => h_2 b bs r) =
    h_1 r
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.PresheafHom.IsSheafFor.app_cond : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X}
  (hG :
    ⦃Y : C⦄ →
      (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op))
  (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible)
  (g : Y ⟶ X) {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryTheory.CategoryStruct.comp p g)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PresheafHom.IsSheafFor.app hG x hx g) (G.map p.op) =
    CategoryTheory.CategoryStruct.comp (F.map p.op)
      ((x (CategoryTheory.CategoryStruct.comp p g) hp).app
        (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Z))))
-- Mathlib.RingTheory.Congruence.Basic
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
under the map to the underlying equivalence relation.  -/
RingCon.sInf_toSetoid : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)),
  (sInf S).toSetoid = sInf ((fun x => x.toSetoid) '' S)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.rfl : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous μ
-- Mathlib.Topology.Compactness.Compact
Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s K : Set X},
  s.Infinite → IsCompact K → s ⊆ K → ∃ x ∈ K, AccPt x (Filter.cofinite ⊓ Filter.principal s)
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.contains.loop.eq_def : ∀ (s : ByteSlice) (byte : UInt8) (i : ℕ),
  ByteSlice.contains.loop✝ s byte i =
    if h : i < s.size then if (s[i] == byte) = true then true else ByteSlice.contains.loop✝ s byte (i + 1) else false
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_max : ∀ (m n : ℕ∞), ↑(max m n) = max ↑m ↑n
-- Init.Sym.Lemmas
Lean.Sym.Int32.le_eq_true : ∀ (a b : Int32), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Topology.Separation.Basic
T0Space.of_cover : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s) → T0Space X
-- Mathlib.Order.GaloisConnection.Basic
OrderIso.bddBelow_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
  BddBelow (⇑e '' s) ↔ BddBelow s
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.type : Lean.Meta.Grind.Arith.FieldNormNum.Context✝ → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons_map_snd_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), u :: List.map (fun x => x.toProd.2) p.darts = p.support
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F}
  {γbc : Path b c} (γab : Path a b),
  CurveIntegrable ω γbc → IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) MeasureTheory.volume (1 / 2) 1
-- Lean.Util.HasConstCache
Lean.HasConstCache.mk.sizeOf_spec : ∀ {declNames : Array Lean.Name} (cache : Std.HashMap.Raw Lean.Expr Bool), sizeOf { cache := cache } = 1 + sizeOf cache
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The map `R[X][Y]/⟨f, Yg-1⟩ →ₐ[R] S` sending `X` to `x`, given `P.HasMap x`.  -/
StandardEtalePair.lift : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : StandardEtalePair R) → (x : S) → P.HasMap x → P.Ring →ₐ[R] S
-- Mathlib.FieldTheory.Normal.Closure
/-- [Stacks Tag 0BMG](https://stacks.math.columbia.edu/tag/0BMG) ((1) normality.) -/
normalClosure.normal : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [h : Normal F L], Normal F ↥(IntermediateField.normalClosure F K L)
-- Mathlib.Order.Heyting.Hom
HeytingHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  [inst_2 : HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.norm_toBoundedContinuousFunction : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [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] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  ‖{ toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }‖ = (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0) f
-- Batteries.Data.List.Lemmas
List.replaceF_of_forall_none : ∀ {α : Type u_1} {p : α → Option α} {l : List α}, (∀ a ∈ l, p a = none) → List.replaceF p l = l
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hyp.sizeOf_spec : ∀ (a : Lean.FVarId), sizeOf (Lean.SubExpr.GoalLocation.hyp a) = 1 + sizeOf a
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.constSMul_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} {M : Type u_7} [inst : Zero 𝕜] [inst_1 : LE α] [inst_2 : SMulZeroClass M 𝕜] (c : M)
  (f : IncidenceAlgebra 𝕜 α) (a b : α), (c • f) a b = c • f a b
-- Init.Data.Option.Lemmas
Option.elim_filter : ∀ {α : Type u_1} {β : Sort u_2} {p : α → Bool} {f : α → β} {o : Option α} {b : β},
  (Option.filter p o).elim b f = o.elim b fun a => if p a = true then f a else b
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) {I : Type u_1} {S : C} {X : I → C} (f : (i : I) → X i ⟶ S)
  (hf : CategoryTheory.Sieve.ofArrows X f ∈ J S) {E : A} (x : (i : I) → E ⟶ P.obj (Opposite.op (X i)))
  (hx :
    ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
      CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) →
        CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op))
  (i : I) {Z : A} (h : P.obj (Opposite.op (X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx)
      (CategoryTheory.CategoryStruct.comp (P.map (f i).op) h) =
    CategoryTheory.CategoryStruct.comp (x i) h
-- Lean.Elab.Command
Lean.Elab.Command.instMonadResolveNameCommandElabM : Lean.MonadResolveName Lean.Elab.Command.CommandElabM
-- Init.Data.String.Modify
String.remainingBytes_pastSet : ∀ {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos}, (p.pastSet c hp).remainingBytes = (p.next hp).remainingBytes
-- Mathlib.Topology.Algebra.Module.Star
selfAdjointPartL_apply_coe : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [inst_9 : ContinuousAdd A] [inst_10 : ContinuousStar A]
  [inst_11 : ContinuousConstSMul R A] (x : A), ↑((selfAdjointPartL R A) x) = ⅟2 • x + ⅟2 • star x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.isIso_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {A : C},
  CategoryTheory.IsIso (CategoryTheory.NonPreadditiveAbelian.r A)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- For any closed ball around `x`, there exists a set of the family contained in this ball.  -/
VitaliFamily.nontrivial : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (self : VitaliFamily μ) (x : X), ∀ ε > 0, ∃ s ∈ self.setsAt x, s ⊆ Metric.closedBall x ε
-- Mathlib.Data.Nat.Choose.Basic
Nat.factorial_mul_factorial_dvd_factorial_add : ∀ (i j : ℕ), i.factorial * j.factorial ∣ (i + j).factorial
-- Mathlib.MeasureTheory.Integral.CircleIntegral
CircleIntegrable.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (c : ℂ) (R : ℝ),
  CircleIntegrable f c R = IntervalIntegrable (fun θ => f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.instSymmetricCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.SymmetricCategory (CategoryTheory.Dial C)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.equiv.congr_simp : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f f_1 : M →ₗ[R] N} (e_f : f = f_1) (h : IsBaseChange S f),
  h.equiv = ⋯.equiv
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedCaseTrace : Inhabited Lean.Meta.Grind.CaseTrace
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.tendsto_antidiagonal : ∀ {M : Type u_3} {S : Type u_4} [inst : AddMonoid M] [inst_1 : Finset.HasAntidiagonal M] [inst_2 : NormedRing S]
  [IsUltrametricDist S] {C : M → ℝ},
  (∀ (a b : M), C (a + b) = C a * C b) →
    ∀ {f g : M → S},
      Filter.Tendsto (fun i => ‖f i‖ * C i) Filter.cofinite (nhds 0) →
        Filter.Tendsto (fun i => ‖g i‖ * C i) Filter.cofinite (nhds 0) →
          Filter.Tendsto (fun a => ‖∑ p ∈ Finset.HasAntidiagonal.antidiagonal a, f p.1 * g p.2‖ * C a) Filter.cofinite
            (nhds 0)