mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.comp_whisker_right : ∀ {B : Type u} [inst : Quiver B] {a b c : B} {f g h : CategoryTheory.FreeBicategory.Hom a b}
  (i : CategoryTheory.FreeBicategory.Hom b c) (η : CategoryTheory.FreeBicategory.Hom₂ f g)
  (θ : CategoryTheory.FreeBicategory.Hom₂ g h),
  CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right i (η.vcomp θ))
    ((CategoryTheory.FreeBicategory.Hom₂.whisker_right i η).vcomp
      (CategoryTheory.FreeBicategory.Hom₂.whisker_right i θ))
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.update_mem_cylinder : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ) (y : E n), Function.update x n y ∈ PiNat.cylinder x n
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principalsKanExtension.congr_simp : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] [inst_4 : CategoryTheory.Limits.HasLimits C]
  (F F_1 : CategoryTheory.Functor X C),
  F = F_1 → Alexandrov.principalsKanExtension F = Alexandrov.principalsKanExtension F_1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instSMul : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {S : Type u_10} →
                    [inst_5 : Monoid S] →
                      [inst_6 : DistribMulAction S N] → [SMulCommClass R S N] → SMul S (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Topology.Path
Path.truncate.eq_1 : ∀ {X : Type u_4} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ),
  γ.truncate t₀ t₁ =
    { toFun := fun s => γ.extend (min (max (↑s) t₀) t₁), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Mathlib.Topology.Order.LowerUpperTopology
OrderDual.instIsLower : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α], Topology.IsLower αᵒᵈ
-- Lean.Expr
Lean.FVarIdSet.ofList : List Lean.FVarId → Lean.FVarIdSet
-- Aesop.Frontend.Saturate
Aesop.Frontend.elabForwardRuleSetCore : Array Lean.Ident →
  Array (Lean.TSyntax `Aesop.Frontend.Parser.additionalRule) → Aesop.Options' → Aesop.ElabM Aesop.LocalRuleSet
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp' : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p]
  [ContinuousMap.UniqueHom R A] (g f : R → R) (a : A),
  autoParam (ContinuousOn g (f '' spectrum R a)) cfc_comp'._auto_1 →
    autoParam (ContinuousOn f (spectrum R a)) cfc_comp'._auto_3 →
      autoParam (p a) cfc_comp'._auto_5 → cfc (fun x => g (f x)) a = cfc g (cfc f a)
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt64HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_one_lt_nnnorm : ∀ (α : Type u_2) [inst : NontriviallyNormedField α], ∃ x, 1 < ‖x‖₊
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.toEmbedding_toHom : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N), f.toEmbedding.toHom = f.toHom
-- Lean.Server.CodeActions.Attr
/-- A command code action extension.  -/
Lean.CodeAction.CommandCodeAction : Type
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.coe_injective : ∀ {X : Type u_1}, Function.Injective OnePoint.some
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `VectorMeasure.map` as a linear map.  -/
MeasureTheory.VectorMeasure.mapₗ : {α : Type u_1} →
  {β : Type u_2} →
    {m : MeasurableSpace α} →
      [inst : MeasurableSpace β] →
        {M : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : TopologicalSpace M] →
              {R : Type u_4} →
                [inst_3 : Semiring R] →
                  [inst_4 : Module R M] →
                    [inst_5 : ContinuousConstSMul R M] →
                      [inst_6 : ContinuousAdd M] →
                        (α → β) → MeasureTheory.VectorMeasure α M →ₗ[R] MeasureTheory.VectorMeasure β M
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf_of_finite : ∀ {ι : Sort u_2} [Finite ι] {α : Type u_3} {f : ι → Filter α} (s : Set α),
  s ∈ ⨅ i, f i ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.IndepFun.mgf_add' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ →
        ProbabilityTheory.mgf (X + Y) μ t = ProbabilityTheory.mgf X μ t * ProbabilityTheory.mgf Y μ t
-- Mathlib.Geometry.Manifold.StructureGroupoid
instInhabitedPregroupoid : (H : Type u_2) → [inst : TopologicalSpace H] → Inhabited (Pregroupoid H)
-- Mathlib.Order.Interval.Multiset
Multiset.Icc_eq_zero_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, Multiset.Icc a b = 0 ↔ ¬a ≤ b
-- Mathlib.Topology.Filter
Filter.nhds_eq' : ∀ {α : Type u_2} (l : Filter α), nhds l = l.lift' fun s => {l' | s ∈ l'}
-- Mathlib.RingTheory.Spectrum.Prime.Module
IsLocalRing.closedPoint_mem_support : ∀ (R : Type u_1) (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Nontrivial M], IsLocalRing.closedPoint R ∈ Module.support R M
-- Lean.Server.Requests
Lean.Server.parseRequestParams : (paramType : Type) → [Lean.FromJson paramType] → Lean.Json → Except Lean.Server.RequestError paramType
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- The tensor product of `M` and `ι →₀ R` is linearly equivalent to `ι →₀ M`  -/
TensorProduct.finsuppScalarRight : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (ι : Type u_5) → [DecidableEq ι] → TensorProduct R M (ι →₀ R) ≃ₗ[S] ι →₀ M
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isMaximumClique_iff : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] {s : Finset α},
  G.IsMaximumClique s ↔ G.IsClique ↑s ∧ ∀ (t : Finset α), G.IsClique ↑t → t.card ≤ s.card
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.mk_inj : ∀ {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1), Complex.UnitDisc.mk z hz = Complex.UnitDisc.mk w hw ↔ z = w
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_iUnion : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VAdd α β] (s : Set α) (t : ι → Set β),
  s +ᵥ ⋃ i, t i = ⋃ i, s +ᵥ t i
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_sub : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x y : M), Q (x - y) = Q (y - x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.max! ∈ t
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.eq_1 : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass M = Antisymmetrization (MulArchimedeanOrder M) fun x1 x2 => x1 ≤ x2
-- Lean.Expr
Lean.Expr.isBoolFalse : Lean.Expr → Bool
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Triangle.eulerPoint_eq_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : Affine.Triangle ℝ P) (i : Fin 3),
  Affine.Simplex.eulerPoint s i = midpoint ℝ s.orthocenter (s.points i)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.iso_inv : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y),
  (CategoryTheory.PreservesImage.iso L f).inv =
    { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯,
            e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯, e_strong_epi := ⋯ }.toMonoIsImage.lift
      (CategoryTheory.Limits.Image.monoFactorisation (L.map f))
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newDepHyp.inj : ∀ {goal goal_1 : Lean.Meta.Grind.Goal},
  Lean.Meta.Grind.IntroResult.newDepHyp✝ goal = Lean.Meta.Grind.IntroResult.newDepHyp✝ goal_1 → goal = goal_1
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.symmetry₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp p₂ h) =
    CategoryTheory.CategoryStruct.comp p₁ h
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.pmap_eq_pmapImpl.go : ∀ (α : Type u_2) (β : Type u_1) (p : α → Prop) (f : (a : α) → p a → β) (l' : List α) (hL' : ∀ ⦃x : α⦄, x ∈ l' → p x),
  List.pmap f l' hL' =
    List.map
      (fun x =>
        match x with
        | ⟨x, hx⟩ => f x hx)
      (List.pmap Subtype.mk l' hL')
-- Mathlib.Order.SuccPred.InitialSeg
InitialSeg.map_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : SuccOrder α] [NoMaxOrder α]
  [inst_4 : SuccOrder β] (f : α ≤i β) (a : α), f (Order.succ a) = Order.succ (f a)
-- LeanSearchClient.Syntax
LeanSearchClient.instInhabitedSearchServer : Inhabited LeanSearchClient.SearchServer
-- Mathlib.Data.Finset.Defs
/-- Coercion to `Set α` as an `OrderEmbedding`.  -/
Finset.coeEmb : {α : Type u_1} → Finset α ↪o Set α
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Multiset.Ioc a b ↔ a < x ∧ x ≤ b
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.RepToAction_obj : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (X : Rep.{w, u, v} k G),
  (Rep.RepToAction k G).obj X =
    { V := ModuleCat.of k ↑X, ρ := (ModuleCat.of k ↑X).endRingEquiv.symm.toMonoidHom.comp X.ρ }
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
NNReal.continuousAt_rpow : ∀ {x : NNReal} {y : ℝ}, x ≠ 0 ∨ 0 < y → ContinuousAt (fun p => p.1 ^ p.2) (x, y)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsLeftAdjointTopCatFree : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R], (TopModuleCat.free R).IsLeftAdjoint
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- If `U ≤ V`, then projecting on `V` and then on `U` is the same as projecting on `U`.  -/
Submodule.orthogonalProjectionOnto_starProjection_of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U ≤ V → ∀ (x : E), U.orthogonalProjectionOnto (V.starProjection x) = U.orthogonalProjectionOnto x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_nonpos_of_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f : α → E}, f ≤ᵐ[μ] 0 → ∫ (x : α), f x ∂μ ≤ 0
-- Mathlib.Logic.Equiv.Bool
Bool.not_injective : Function.Injective not
-- Aesop.Forward.SlotIndex
Aesop.SlotIndex.mk : ℕ → Aesop.SlotIndex
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasFDerivAtFilter.of_comp_of_leftInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G}
  {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {lE : Filter (E × E)} {lF : Filter (F × F)},
  Filter.Tendsto (Prod.map g g) lE lF →
    HasFDerivAtFilter f f' lF →
      HasFDerivAtFilter h h' lE →
        Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h →
          Function.LeftInverse ⇑f'symm ⇑f' → HasFDerivAtFilter g (f'symm ∘SL h') lE
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addMap_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 → W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_Option : ∀ {α : Type} {e : PUnit.{1}} {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{1} Std.Do.PostShape.pure)},
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = Q.2.1 e
-- Mathlib.Topology.LocallyConstant.Basic
/-- A (bundled) locally constant function from a topological space `X` to a type `Y`.  -/
LocallyConstant : (X : Type u_5) → Type u_6 → [TopologicalSpace X] → Type (max u_5 u_6)
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.iInter₂ : ∀ {R : Type u_1} {X : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] {x : X} {s : (i : ι) → κ i → Set X},
  (∀ (i : ι) (j : κ i), Convexity.IsStarConvexSet R x (s i j)) → Convexity.IsStarConvexSet R x (⋂ i, ⋂ j, s i j)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeToSubmodule_inj : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P}, ↑I = ↑J ↔ I = J
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The invariant vector field associated to the value at zero of the Lie
bracket of two invariant vector fields, is everywhere the Lie bracket of the invariant vector
fields.  -/
addInvariantVector_mlieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G]
  [CompleteSpace E] (v w : AddGroupLieAlgebra I G),
  addInvariantVectorField (VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0) =
    VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w)
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindRing.mk : ∀ {A : Type u_2} [inst : CommRing A] [toIsNoetherian : IsNoetherian A A] [toDimensionLEOne : Ring.DimensionLEOne A]
  [toIsIntegralClosure : IsIntegralClosure A A (FractionRing A)], IsDedekindRing A
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.defEq.sizeOf_spec : ∀ (lhs : ℕ) (rhs : Lean.Meta.Grind.CnstrRHS),
  sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.defEq lhs rhs) = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableAt_iff_source_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} [IsManifold I 1 M]
  {x' : M},
  x' ∈ (chartAt H x).source → (MDiffAt f x' ↔ MDiffAt[Set.range ↑I] (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x'))
-- Mathlib.Algebra.Group.Ext
AddCommMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : AddCommMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Mathlib.Order.Interval.Basic
NonemptyInterval.fst_sup : ∀ {α : Type u_1} [inst : Lattice α] (s t : NonemptyInterval α), (s ⊔ t).toProd.1 = s.toProd.1 ⊓ t.toProd.1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has locally bounded variation, then the variation on
small closed intervals to the left of this point tends to the contribution of the point, i.e.,
the distance between the left limit and the value at the point  -/
LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_left : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {l : E},
  LocallyBoundedVariationOn f s →
    ∀ {x : α},
      Filter.Tendsto f (nhdsWithin x (s ∩ Set.Iio x)) (nhds l) →
        x ∈ s →
          Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc y x)) (nhdsWithin x (s ∩ Set.Iio x))
            (nhds (edist (f x) l))
-- Init.Data.SInt.Basic
instModInt64 : Mod Int64
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a b : QuaternionAlgebra R c₁ c₂ c₃) [inst : AddGroup R], (a - b).im = a.im - b.im
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid.merge : ∀ {α : Type u_1} [inst : Preorder α] {l r : Ordnode α},
  l.Valid → r.Valid → Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l → (l.merge r).Valid
-- Mathlib.Algebra.Algebra.Hom
AlgHom.instRingHomCompTripleComp : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {φ₁ : B →ₐ[R] C} {φ₂ : A →ₐ[R] B}, RingHomCompTriple φ₂.toRingHom φ₁.toRingHom (φ₁.comp φ₂).toRingHom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α fun x => β) (k : α) (v : β)
  (ht : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? t k v ht =
    match Std.DTreeMap.Internal.Impl.Const.get? t k with
    | none => (none, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ht).impl)
    | some b => (some b, t)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale.eq_1 : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (a : σ → R),
  MvPowerSeries.rescale a =
    { toFun := fun f n => (n.prod fun s m => a s ^ m) * (MvPowerSeries.coeff n) f, map_one' := ⋯, map_mul' := ⋯,
      map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- Every algebra is Lie-admissible.
See note [reducible non-instances].  -/
Algebra.instLieAdmissibleAlgebra : {R : Type u_1} → {L : Type u_2} → [inst : CommRing R] → [inst_1 : Ring L] → [Algebra R L] → LieAdmissibleAlgebra R L
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_fst_assoc : ∀ (X : SSet) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj { len := 1 })) h) =
    h
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toAddSubgroup_eq_top : ∀ {R : Type u} [inst : NonAssocRing R] {S : Subring R}, S.toAddSubgroup = ⊤ ↔ S = ⊤
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsMultiplicative]
  [AlgebraicGeometry.IsZariskiLocalAtSource P],
  AlgebraicGeometry.Scheme.zariskiTopology ≤ AlgebraicGeometry.Scheme.propQCTopology P
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistance of a set to itself vanishes.  -/
Metric.hausdorffEDist_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Metric.hausdorffEDist s s = 0
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `StrongDual.extendRCLike_apply`. -/
ContinuousLinearMap.extendTo𝕜'_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (fr : StrongDual ℝ F) (x : F), fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_id' : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α), (M.map fun x => x) = M
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.vaddCommClass_left : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G β] [inst_2 : VAdd α β]
  [VAddCommClass G α β] (S : AddSubgroup G), VAddCommClass (↥S) α β
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorHom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X₂ Y₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X₁ Y₁)
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.AEEqFun.compMeasurePreserving_mem_Lp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  {g : β →ₘ[μb] E},
  g ∈ MeasureTheory.Lp E p μb →
    ∀ {f : α → β} (hf : MeasureTheory.MeasurePreserving f μ μb), g.compMeasurePreserving f hf ∈ MeasureTheory.Lp E p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multicofork for `I : MultispanIndex (.prod ι) C` deduced from
a multicofork for `I.toLinearOrder` when `ι` is linearly ordered
and `I` is symmetric.  -/
CategoryTheory.Limits.Multicofork.ofLinearOrder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      [inst_1 : LinearOrder ι] →
        {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
          CategoryTheory.Limits.Multicofork I.toLinearOrder → I.SymmStruct → CategoryTheory.Limits.Multicofork I
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.mapGrindM : {m : Type → Type u_1} →
  [MonadControlT Lean.Meta.Grind.GrindM m] →
    [Monad m] → ({α : Type} → Lean.Meta.Grind.GrindM α → Lean.Meta.Grind.GrindM α) → {α : Type} → m α → m α
-- Lean.Parser.Command
Lean.Parser.Command.set_option.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a b : α} (hab : cmp a b = Ordering.eq) {h' : a ∈ t}, Std.DTreeMap.Const.get t a h' = Std.DTreeMap.Const.get t b ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_alter_eq_sub_one : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF →
    k ∈ m → (f (Std.DHashMap.Raw.Const.get? m k)).isNone = true → (Std.DHashMap.Raw.Const.alter m k f).size = m.size - 1