mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coe_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] [inst_3 : Nontrivial R],
  ↑0 = 0
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.gt → motive Ordering.gt)
  (h_2 : Ordering.lt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.lt = Ordering.lt → motive Ordering.lt),
  (match hkky : Ordering.lt with
    | Ordering.gt => h_1 hkky
    | Ordering.eq => h_2 hkky
    | Ordering.lt => h_3 hkky) =
    h_3 ⋯
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_image_linearEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {s : Set M} {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂),
  Submodule.span R₂ (⇑f '' s) = Submodule.map (↑f) (Submodule.span R s)
-- Mathlib.LinearAlgebra.BilinearMap
/-- `LinearMap.flip` as an isomorphism of modules.  -/
LinearMap.lflip : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S : Type u_3} →
      {S₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : Semiring S] →
              [inst_3 : Semiring S₂] →
                {M : Type u_5} →
                  {N : Type u_7} →
                    {P : Type u_9} →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid N] →
                          [inst_6 : AddCommMonoid P] →
                            [inst_7 : Module R M] →
                              [inst_8 : Module S N] →
                                [inst_9 : Module R₂ P] →
                                  [inst_10 : Module S₂ P] →
                                    [inst_11 : SMulCommClass S₂ R₂ P] →
                                      {ρ₁₂ : R →+* R₂} →
                                        {σ₁₂ : S →+* S₂} →
                                          {R₀ : Type u_14} →
                                            [inst_12 : Semiring R₀] →
                                              [inst_13 : Module R₀ P] →
                                                [inst_14 : SMulCommClass S₂ R₀ P] →
                                                  [inst_15 : SMulCommClass R₂ R₀ P] →
                                                    (M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) ≃ₗ[R₀] N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sphere.eq_1 : ∀ (n d k : ℕ), Behrend.sphere n d k = {x ∈ Behrend.box n d | ∑ i, x i ^ 2 = k}
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart.congr_simp : ∀ (x y : ℝ) [h : Fact (x < y)], IccRightChart x y = IccRightChart x y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Naturality of the `prodComparison` morphism in the right argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B B' : C} (g : B ⟶ B') {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) h)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.integrable_preCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℚ),
  MeasureTheory.Integrable (fun a => (ProbabilityTheory.preCDF ρ x a).toReal) ρ.fst
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.UniversallyClosed f
-- Mathlib.Order.Cover
WCovBy.sup_eq : ∀ {α : Type u_1} [inst : SemilatticeSup α] {a b c : α}, a ⩿ c → b ⩿ c → a ≠ b → a ⊔ b = c
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instVAdd.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α], OrderDual.instVAdd = inst
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X)
  (U : X.Opens) (hU : f (IsLocalRing.closedPoint ↑R) ∈ U) {Z : CommRingCat} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ U (f (IsLocalRing.closedPoint ↑R)) hU)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.stalkClosedPointTo f) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.mapIso (AlgebraicGeometry.Spec R).presheaf (CategoryTheory.eqToIso ⋯).op ≪≫
            AlgebraicGeometry.Scheme.ΓSpecIso R).hom
        h)
-- Mathlib.Algebra.Order.AddGroupWithTop
top_add : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] (a : α), ⊤ + a = ⊤
-- Mathlib.Order.WithBot
WithTop.map_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (WithTop.map f)
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprTZif : Repr Std.Time.TimeZone.TZif.TZif
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- For any infinite place `w'`, the regulator is equal to the absolute value of the determinant
of the matrix with entries `(mult w * log w (fundSystem K i))_i` for `w ≠ w'`.
 -/
NumberField.Units.regulator_eq_det : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w' : NumberField.InfinitePlace K)
  (e : { w // w ≠ w' } ≃ Fin (NumberField.Units.rank K)),
  NumberField.Units.regulator K =
    |(Matrix.of fun i w =>
          ↑(↑w).mult *
            Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.fundSystem K (e i))))).det|
-- Init.Data.UInt.Lemmas
USize.toNat_sub : ∀ (a b : USize), (a - b).toNat = (2 ^ System.Platform.numBits - b.toNat + a.toNat) % 2 ^ System.Platform.numBits
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.medial_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {V₂ : Type u_4} {P₂ : Type u_5} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] [inst_7 : CharZero k] {n : ℕ} [inst_8 : NeZero n] (s : Affine.Simplex k P n)
  (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f), (s.map f hf).medial = s.medial.map f hf
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.zoom.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α)
  (y : α) (b : RBTree.RBNode α) (path : RBTree.RBNode.Path α)
  (h_1 : (path : RBTree.RBNode.Path α) → motive RBTree.RBNode.nil path)
  (h_2 :
    (n : RBTree.RBNode α) →
      (c : RBTree.RBColor) →
        (a : RBTree.RBNode α) →
          (y : α) →
            (b : RBTree.RBNode α) →
              n = RBTree.RBNode.node c a y b →
                (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a y b) path),
  (match RBTree.RBNode.node c a y b, path with
    | RBTree.RBNode.nil, path => h_1 path
    | n@h:(RBTree.RBNode.node c a y b), path => h_2 n c a y b h path) =
    h_2 (RBTree.RBNode.node c a y b) c a y b ⋯ path
-- Mathlib.Data.Set.Basic
Set.inter_ssubset_right_iff : ∀ {α : Type u} {s t : Set α}, s ∩ t ⊂ t ↔ ¬t ⊆ s
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop : ∀ {α : Type u_1} {G : SimpleGraph α} {u : α} (p : G.Walk u u), Odd p.length → 3 ≤ G.chromaticNumber
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_mor₃_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃)
  (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g'),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯)
      (CochainComplex.mappingConeCompTriangle f' g').mor₃ =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯))
-- Mathlib.Data.Finmap
Finmap.lookup_insert_of_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b : β a} (s : Finmap β),
  a' ≠ a → Finmap.lookup a' (Finmap.insert a b s) = Finmap.lookup a' s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {s : Set (NumberField.mixedEmbedding.realSpace K)},
  MeasurableSet s →
    ∀ {f : (NumberField.InfinitePlace K → ℝ) → ENNReal},
      Measurable f →
        ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' s,
            f x =
          2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ENNReal.ofReal (NumberField.Units.regulator K) *
              ↑(Module.finrank ℚ K) *
            ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in s,
              ENNReal.ofReal (Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))) *
                  (∏ i, ENNReal.ofReal (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis (fun w => x w) ↑i))⁻¹ *
                f (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x)
-- Mathlib.Analysis.Normed.Operator.Extend
/-- Extension of a continuous linear map `f : E →SL[σ₁₂] F`, with `E` a normed space and `F` a
complete normed space, along a uniform and dense embedding `e : E →L[𝕜] Eₗ`.  -/
ContinuousLinearMap.extend : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          [inst : AddCommGroup E] →
            [inst_1 : UniformSpace E] →
              [IsUniformAddGroup E] →
                [inst_3 : AddCommGroup F] →
                  [inst_4 : UniformSpace F] →
                    [IsUniformAddGroup F] →
                      [T0Space F] →
                        [inst_7 : AddCommMonoid Eₗ] →
                          [inst_8 : UniformSpace Eₗ] →
                            [ContinuousAdd Eₗ] →
                              [inst_10 : Semiring 𝕜] →
                                [inst_11 : Semiring 𝕜₂] →
                                  [inst_12 : Module 𝕜 E] →
                                    [inst_13 : Module 𝕜₂ F] →
                                      [inst_14 : Module 𝕜 Eₗ] →
                                        [ContinuousConstSMul 𝕜 Eₗ] →
                                          [ContinuousConstSMul 𝕜₂ F] →
                                            {σ₁₂ : 𝕜 →+* 𝕜₂} →
                                              (E →SL[σ₁₂] F) → [CompleteSpace F] → (E →L[𝕜] Eₗ) → Eₗ →SL[σ₁₂] F
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (f * g) s x
-- Mathlib.Topology.MetricSpace.HausdorffDistance
IsCompact.exists_infDist_eq_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  IsCompact s → s.Nonempty → ∀ (x : α), ∃ y ∈ s, Metric.infDist x s = dist x y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerLeft_left_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom T.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom S.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) h)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coeff_zero_eq_aeval_zero : ∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R), p.coeff 0 = (Polynomial.aeval 0) p
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousAt.upperHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  (s : Set α), UpperHemicontinuousAt f x → UpperHemicontinuousWithinAt f s x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr},
  Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm c = Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm c_1 →
    c = c_1
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk.injEq : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (hom' hom'_1 : ↑M →ₗ[R] ↑N),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Topology.Constructions.SumProd
IsClosedMap.sumMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace W] [inst_3 : TopologicalSpace Z] {f : X → Y} {g : Z → W},
  IsClosedMap f → IsClosedMap g → IsClosedMap (Sum.map f g)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.self_le_maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β}, (cmp k (t.insert k v).maxKey!).isLE = true
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_unique : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Unique β] (f : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop], HasProd f (f default) L
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonMessageDirection.fromJson : Lean.Json → Except String Lean.JsonRpc.MessageDirection
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.injective_of_source_eq_univ : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.source = Set.univ → Function.Injective ↑e
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.recv : {α : Type} → Std.CloseableChannel.Zero✝ α → BaseIO (Task (Option α))
-- Mathlib.Data.Multiset.Bind
Multiset.card_sigma : ∀ {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)),
  (s.sigma t).card = (Multiset.map (fun a => (t a).card) s).sum
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)],
  (E.pullbackCoverOfRight f g).I₀ = E.I₀
-- Mathlib.Algebra.Ring.NegOnePow
/-- The map `ℤ → ℤˣ` which sends `n` to `(-1 : ℤˣ) ^ n`.  -/
Int.negOnePow : ℤ → ℤˣ
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2}, Height.mulHeight 1 = 1
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then for any submodule `N` of the same rank,
we can find basis for `M` and `N` with the same indexing such that the inclusion map
is a square diagonal matrix.

See `Submodule.exists_smith_normal_form_of_rank_eq` for a version that states the
existence of the basis.
 -/
Submodule.smithNormalFormOfRankEq : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                {N : Submodule R M} →
                  [inst_5 : Fintype ι] →
                    Module.Basis ι R M →
                      Module.finrank R ↥N = Module.finrank R M → Module.Basis.SmithNormalForm N ι (Fintype.card ι)
-- Lean.DocString.Markdown
Lean.Doc.instMarkdownBlockElabInlineElabBlock : Lean.Doc.MarkdownBlock Lean.ElabInline Lean.ElabBlock
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiff.clm_comp : ∀ {𝕜 : 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] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁},
  ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g →
    ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f →
      ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n fun x => g x ∘SL f x
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanIso_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanIso 0 A B f ↔ Set.BijOn f A B
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.isClosed_range : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ}, IsCoercive B → IsClosed ↑(↑(InnerProductSpace.continuousLinearMapOfBilin B)).range
-- Mathlib.Algebra.Group.Units.Defs
/-- Addition of a `u : AddUnits M` on the left doesn't affect `IsAddUnit`.  -/
AddUnits.isAddUnit_addUnits_add : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M) (a : M), IsAddUnit (↑u + a) ↔ IsAddUnit a
-- Mathlib.Dynamics.OmegaLimit
eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [T2Space β] {c : Set β},
  IsCompact c →
    (∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) →
      ∀ {n : Set β}, IsOpen n → omegaLimit f ϕ s ⊆ n → ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s n
-- Mathlib.RingTheory.Spectrum.Prime.Chevalley
/-- [Stacks Tag 037G](https://stacks.math.columbia.edu/tag/037G) -/
PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field : ∀ {K : Type u_3} {A : Type u_4} {B : Type u_5} [inst : Field K] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra K A] [inst_4 : Algebra K B], IsOpenMap (PrimeSpectrum.comap (algebraMap A (TensorProduct K A B)))
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.tryClearS.tacticBuilder : Lean.MVarId → Lean.FVarId → Lean.MVarId → Aesop.Script.TacticBuilder
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
UpgradedStandardBorel.toBorelSpace : ∀ {α : Type u_1} [self : UpgradedStandardBorel α], BorelSpace α
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `sum_apply`. -/
UniformConvergenceCLM.sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.mk.inj : ∀ {len len_1 : ℕ}, { len := len } = { len := len_1 } → len = len_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_natCast : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ↑↑n = ↑n
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.of_isImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsImmersion f]
  [AlgebraicGeometry.IsLocallyArtinian Y], AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isBoundedUnder_abs_atBot_iff : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atBot fun x => |Polynomial.eval x P|) ↔ P.degree ≤ 0
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  Filter.Tendsto (⇑e) Filter.atBot Filter.atBot
-- Mathlib.Order.Heyting.Hom
CoheytingHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : CoheytingAlgebra α] →
      [inst_1 : CoheytingAlgebra β] →
        (toLatticeHom : LatticeHom α β) →
          toLatticeHom.toFun ⊤ = ⊤ →
            (∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b) → CoheytingHom α β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_inter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.roots_U_real : ∀ (n : ℕ),
  (Polynomial.Chebyshev.U ℝ ↑n).roots =
    (Finset.image (fun k => Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (Finset.range n)).val
-- Mathlib.Algebra.Module.Presentation.Free
Module.presentationFinsupp_G : ∀ (A : Type u) [inst : Ring A] (G : Type w₀), (Module.presentationFinsupp A G).G = G
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_isLongestRevMatchAt : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  pat ≠ "" →
    (String.Slice.Pattern.Model.RevMatchesAt pat pos ↔
      ∃ (h : String.Pos.Raw.IsValidForSlice s (pos.offset.decreaseBy pat.utf8ByteSize)),
        String.Slice.Pattern.Model.IsLongestRevMatchAt pat (s.pos (pos.offset.decreaseBy pat.utf8ByteSize) h) pos)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.extraFacts : Lean.Meta.Grind.Params → Lean.PArray Lean.Expr
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.pow_dvd_pow_of_sub_pow_eq_zero : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Ring R], n + m ≤ p + 1 → Commute x y → (x - y) ^ n = 0 → x ^ m ∣ y ^ p
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_symm_lt_iff_ne_zero : ∀ {n : ℕ} [inst : NeZero n] (i : Fin n), (Equiv.symm (finRotate n)) i < i ↔ i ≠ 0
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- If `f : ℂ → E` is complex differentiable on some open set `s`, then it is continuously
differentiable on `s`.  -/
DifferentiableOn.contDiffOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {s : Set ℂ} {f : ℂ → E}
  {n : WithTop ℕ∞}, DifferentiableOn ℂ f s → IsOpen s → ContDiffOn ℂ n f s