mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.range_inclusion : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖),
  Set.range (RestrictedProduct.inclusion R A h) = {x | ∀ᶠ (i : ι) in 𝓖, x i ∈ A i}
-- Mathlib.Order.Interval.Basic
/-- Canonical coercion from nonempty intervals to intervals  -/
Interval.coe : {α : Type u_1} → [inst : LE α] → NonemptyInterval α → Interval α
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set `A f L r ε` is the set of points `x` around which the function `f` is well approximated
at scale `r` by the linear map `L`, up to an error `ε`. We tweak the definition to make sure that
this is an open set.  -/
FDerivMeasurableAux.A : {𝕜 : 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] → (E → F) → (E →L[𝕜] F) → ℝ → ℝ → Set E
-- Mathlib.Order.Partition.Finpartition
Finpartition.instMin : {α : Type u_1} → [inst : DistribLattice α] → [inst_1 : OrderBot α] → [DecidableEq α] → {a : α} → Min (Finpartition a)
-- Mathlib.Order.Comparable
incompRel_compl_apply : ∀ {α : Type u_1} {a b : α} (r : α → α → Prop), IncompRel rᶜ a b ↔ AntisymmRel r a b
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.instLinearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (Topology.WithUpper α)
-- Mathlib.MeasureTheory.Group.IntegralConvolution
MeasureTheory.integrable_conv_iff : ∀ {M : Type u_1} {F : Type u_2} [inst : AddMonoid M] {mM : MeasurableSpace M} [MeasurableAdd₂ M]
  [inst_2 : NormedAddCommGroup F] {μ ν : MeasureTheory.Measure M} {f : M → F} [MeasureTheory.SFinite ν],
  MeasureTheory.AEStronglyMeasurable f (μ.conv ν) →
    (MeasureTheory.Integrable f (μ.conv ν) ↔
      (∀ᵐ (x : M) ∂μ, MeasureTheory.Integrable (fun y => f (x + y)) ν) ∧
        MeasureTheory.Integrable (fun x => ∫ (y : M), ‖f (x + y)‖ ∂ν) μ)
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The antipodal map is analytic.  -/
contMDiff_neg_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {m : WithTop ℕ∞} {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)],
  ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) m
    fun x => -x
-- Mathlib.Algebra.Group.Irreducible.Lemmas
/-- Irreducibility is preserved by additive equivalences.  -/
AddIrreducible.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] {x : M}
  [inst_2 : EquivLike F M N] [AddEquivClass F M N] (f : F), AddIrreducible x → AddIrreducible (f x)
-- Init.Notation
/-- Sequences the effects of two terms, discarding the value of the first. This function is usually
invoked via the `*>` operator.

Given `x : f α` and `y : f β`, `x *> y` runs `x`, then runs `y`, and finally returns the result of
`y`.

The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.


Conventions for notations in identifiers:

 * The recommended spelling of `*>` in identifiers is `seqRight`. -/
«term_*>_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Units.Hom
Units.coeHom_apply : ∀ {M : Type u} [inst : Monoid M] (x : Mˣ), (Units.coeHom M) x = ↑x
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNegEquiv_symm_eq_neg : ∀ {M : Type u_1} [inst : AddCommGroup M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S),
  ↑((S.leftNegEquiv hS).symm x) = -↑x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_rat : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun r => 0 < r) fun r => {p | dist p.1 p.2 < ↑r}
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
tendsto_iff_dist_tendsto_zero : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {x : Filter β} {a : α},
  Filter.Tendsto f x (nhds a) ↔ Filter.Tendsto (fun b => dist (f b) a) x (nhds 0)
-- Mathlib.Topology.WithTopology
WithTopology.instDecidableEq.decEq : {X : Type u_2} → {t : TopologicalSpace X} → [DecidableEq X] → (x x_1 : WithTopology X t) → Decidable (x = x_1)
-- Init.Omega.Int
Lean.Omega.Int.add_le_iff_le_sub : ∀ {a b c : ℤ}, a + b ≤ c ↔ a ≤ c - b
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.discr'`.

---

The discriminant of a quadratic form `Q : QuadraticForm R (n → R)` generalizes the discriminant
of a quadratic polynomial.  -/
QuadraticForm.QuadraticMap.discr : {R : Type u_3} →
  {n : Type w} → [Fintype n] → [DecidableEq n] → [inst : CommRing R] → [Invertible 2] → QuadraticForm R (n → R) → R
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddSubgroup.isUniformAddGroup : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (S : AddSubgroup α),
  IsUniformAddGroup ↥S
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.append_take_drop_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).append (p.drop n) = p
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.IsGLPos.instSMul : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} → {α : Type u_2} → [inst : SMul α ℂ] → [IsScalarTower α ℂ ℂ] → [Γ.HasDetOne] → SMul α (CuspForm Γ k)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A morphism of `FiniteAddGrp` induces a morphism of the associated profinite
additive groups.  -/
ProfiniteAddGrp.ofFiniteAddGrpHom : {G H : FiniteAddGrp.{u}} → (G ⟶ H) → (ProfiniteAddGrp.ofFiniteAddGrp G ⟶ ProfiniteAddGrp.ofFiniteAddGrp H)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_9 : ∀ {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 9).eval
      (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) =
    a9
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasStrictFDerivAt_add_const_iff`. -/
HasStrictFDerivAt.add_const : ∀ {𝕜 : 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} (c : F), HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => f x + c) f' x
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.on : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α},
  IsLocalMin f a → ∀ (s : Set α), IsLocalMinOn f s a
-- Lean.Meta.LetToHave
/-- The type of `expr`, if it has been computed.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.type? : Lean.Meta.LetToHave.Result✝ → Option Lean.Expr
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.private.sizeOf_spec : sizeOf Lean.Elab.Visibility.private = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.mk.injEq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R}
  {point : WeierstrassCurve.Projective.PointClass R} (nonsingular : W'.NonsingularLift point)
  (point_1 : WeierstrassCurve.Projective.PointClass R) (nonsingular_1 : W'.NonsingularLift point_1),
  ({ point := point, nonsingular := nonsingular } = { point := point_1, nonsingular := nonsingular_1 }) =
    (point = point_1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).obj Y).right =
    CategoryTheory.StructuredArrow.mk Y.hom.right
-- Mathlib.Computability.PartrecCode
/-- The `Nat.Partrec.Code.evaln` function is primitive recursive.  -/
Nat.Partrec.Code.primrec_evaln : Primrec fun a => Nat.Partrec.Code.evaln a.1.1 a.1.2 a.2
-- Mathlib.NumberTheory.ZetaValues
hasSum_one_div_nat_pow_mul_fourier : ∀ {k : ℕ},
  2 ≤ k →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x))
          (-(2 * ↑Real.pi * Complex.I) ^ k / ↑k.factorial * ↑(bernoulliFun k x))
-- Init.Data.Option.Basic
Option.sequence_none : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative m], none.sequence = pure none
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSuppLTAddSubgroup.congr_simp : ∀ (Γ : Type u_1) (R : Type u_2) (κ κ_1 : Cardinal.{u_1}) (e_κ : κ = κ_1) [inst : PartialOrder Γ] [inst_1 : AddGroup R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)], HahnSeries.cardSuppLTAddSubgroup Γ R κ = HahnSeries.cardSuppLTAddSubgroup Γ R κ_1
-- Mathlib.Combinatorics.SimpleGraph.Trails
/-- The edges of a trail as a finset, since each edge in a trail appears exactly once.  -/
SimpleGraph.Walk.IsTrail.edgesFinset : {V : Type u_1} → {G : SimpleGraph V} → {u v : V} → {p : G.Walk u v} → p.IsTrail → Finset (Sym2 V)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.congrHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Y} {g₁ g₂ : X ⟶ Z} (h₁ : f₁ = f₂)
  (h₂ : g₁ = g₂) [inst_1 : CategoryTheory.Limits.HasPushout f₁ g₁] [inst_2 : CategoryTheory.Limits.HasPushout f₂ g₂],
  CategoryTheory.Limits.pushout.congrHom h₁ h₂ = CategoryTheory.Limits.pushout.congrHom h₁ h₂
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sumSet.congr_simp : ∀ {α : Type u_1} {s t : Set α} (h : Disjoint s t), Function.Embedding.sumSet h = Function.Embedding.sumSet h
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Rep.Tor_obj : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ) (X : Rep.{u, u, u} k G),
  (Rep.Tor k G n).obj X = ((Rep.coinvariantsTensor k G).obj X).leftDerived n
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Assume that `p q : Submodule 𝕜 E` are algebraic complements. If `p` is closed and `q`
has finite dimension, then they are in fact topological complements.

Note that this theorem does not help you to build a closed complement to a finite dimensional
subspace. That requires the Hahn-Banach theorem, and you don't get much control over what the
complement is. See `Submodule.ClosedComplemented.of_finiteDimensional`.  -/
Submodule.IsCompl.isTopCompl_of_isClosed_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {p q : Submodule 𝕜 E}, IsCompl p q → IsClosed ↑p → ∀ [hq : FiniteDimensional 𝕜 ↥q], Submodule.IsTopCompl p q
-- Batteries.Classes.Order
Std.instOrientedCmpFlipOrdering_batteries : ∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : Std.OrientedCmp cmp], Std.OrientedCmp (flip cmp)
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.precompose_isIso : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.IsIso α] {c : CategoryTheory.Limits.Cocone G},
  CategoryTheory.IsVanKampenColimit c →
    CategoryTheory.IsVanKampenColimit ((CategoryTheory.Limits.Cocone.precompose α).obj c)
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
cthickening_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 ≤ ε → 0 < δ → ∀ (x : E), Metric.cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.mk.sizeOf_spec : ∀ (keys : Array Lean.Meta.InstanceKey) (val : Lean.Expr) (priority : ℕ) (globalName? : Option Lean.Name)
  (synthOrder : Array ℕ) (attrKind : Lean.AttributeKind),
  sizeOf
      { keys := keys, val := val, priority := priority, globalName? := globalName?, synthOrder := synthOrder,
        attrKind := attrKind } =
    1 + sizeOf keys + sizeOf val + sizeOf priority + sizeOf globalName? + sizeOf synthOrder + sizeOf attrKind
-- Mathlib.Order.CompleteLattice.Lemmas
sup_iSup_nat_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α), u 0 ⊔ ⨆ i, u (i + 1) = ⨆ i, u i
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.evalNode : {α : Type} →
  Lean.Meta.LazyDiscrTree.TrieIndex →
    Lean.Meta.LazyDiscrTree.MatchM α
      (Array α ×
        Lean.Meta.LazyDiscrTree.TrieIndex × Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.congr_of_eventuallyEq_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → HasDerivWithinAt f₁ f' s x
-- Init.Data.Array.Nat
Array.sum_le_max_mul_length_nat : ∀ {xs : Array ℕ} (h : xs ≠ #[]), xs.sum ≤ xs.max h * xs.size
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (I : Ideal S), Ideal.spanNorm R I = Ideal.map (Algebra.intNorm R S) I
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiable_zeroSection : ∀ (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E],
  MDiff (Bundle.zeroSection F E)
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The natural isomorphism between the pullback of `F ⋙ G` and the
composition of the pullbacks of `F` and `G`.
 -/
CategoryTheory.NatTrans.PullbackShift.natIsoComp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                {D : Type u_4} →
                  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] →
                    [inst_5 : CategoryTheory.HasShift D B] →
                      (F : CategoryTheory.Functor C D) →
                        {E : Type u_5} →
                          [inst_6 : CategoryTheory.Category.{v_3, u_5} E] →
                            [inst_7 : CategoryTheory.HasShift E B] →
                              (G : CategoryTheory.Functor D E) →
                                CategoryTheory.PullbackShift.functor φ (F.comp G) ≅
                                  (CategoryTheory.PullbackShift.functor φ F).comp
                                    (CategoryTheory.PullbackShift.functor φ G)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.trivial_mon_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Batteries.Data.Char.AsciiCasing
Char.toLower_toUpper_eq_toLower : ∀ (c : Char), c.toUpper.toLower = c.toLower
-- Mathlib.Order.Sublattice
Sublattice.mk_inf_mk : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} (a b : α) (ha : a ∈ L) (hb : b ∈ L),
  ⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiffOn.comp_contMDiff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {n : WithTop ℕ∞} {t : Set M'} {g : M' → M''},
  ContMDiffOn I' I'' n g t → ContMDiff I I' n f → (∀ (x : M), f x ∈ t) → ContMDiff I I'' n (g ∘ f)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.IsCycle.forall_commute_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (g z : Equiv.Perm α),
  (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
    ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), Equiv.Perm.ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionSemiHomClass.toMulActionSemiHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {φ : outParam (M → N)}
  {A : outParam (Type u_13)} {B : outParam (Type u_14)} {inst : Monoid M} {inst_1 : Monoid N} {inst_2 : AddMonoid A}
  {inst_3 : AddMonoid B} {inst_4 : DistribMulAction M A} {inst_5 : DistribMulAction N B} {inst_6 : FunLike F A B}
  [self : DistribMulActionSemiHomClass F φ A B], MulActionSemiHomClass F φ A B
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.IsClosedUnderLimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderColimitsOfShape J
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isConj_one_iff : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsConj φ 1 ↔ NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_obj : ∀ (self : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.obj self = self.toLocallyRingedSpace
-- Mathlib.Order.SuccPred.Archimedean
StrictMono.not_bddBelow_range_of_isPredArchimedean : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [inst_2 : Preorder β] {f : α → β} [NoMinOrder α]
  [inst_4 : PredOrder β] [IsPredArchimedean β], StrictMono f → ¬BddBelow (Set.range f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.ofRepresentableBy_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X),
  CategoryTheory.MonObj.mul =
    α.homEquiv'.symm
      (α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) *
        α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.snd X X))
-- Mathlib.Algebra.Category.Grp.Basic
/-- Universe lift functor for groups.  -/
GrpCat.uliftFunctor : CategoryTheory.Functor GrpCat GrpCat
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_uIcc : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.uIcc a b)],
  Fintype.card ↑(Set.uIcc a b) = (Finset.uIcc a b).card
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.eq_1 : ∀ (α : Type u), FreeAddGroup α = Quot FreeAddGroup.Red.Step
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'.go.eq_3 : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (r : α) (k : ℤ)
  (v : Lean.Grind.Linarith.Var) (p_2 : Lean.Grind.Linarith.Poly),
  (k = 1 → False) →
    Lean.Grind.Linarith.Poly.denote'.go ctx r (Lean.Grind.Linarith.Poly.add k v p_2) =
      Lean.Grind.Linarith.Poly.denote'.go ctx (r + k • Lean.Grind.Linarith.Var.denote ctx v) p_2
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.coe_projectionOntoL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q),
  ⇑(p.projectionOntoL q h) = ⇑(p.projectionOnto q ⋯)
-- Mathlib.Computability.TuringMachine.Computable
/-- the underlying bundled TM2  -/
Turing.TM2ComputableAux.tm : {Γ₀ Γ₁ : Type} → Turing.TM2ComputableAux Γ₀ Γ₁ → Turing.FinTM2
-- Mathlib.Algebra.Order.Group.Cone
/-- A (positive) cone in an abelian group is a submonoid that
does not contain both `a` and `a⁻¹` for any non-identity `a`.
This is equivalent to being the set of elements that are at least 1 in
some order making the group into a partially ordered group.  -/
GroupCone : (G : Type u_1) → [CommGroup G] → Type u_1
-- Std.Data.TreeMap.Raw.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.TreeMap.Raw.toList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → List (α × β)
-- Lean.Meta.Tactic.Grind.Extension
/-- Constraints of the form `is_ground x`. Instantiates the theorem only if
`x` is ground term.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.isGround : ℕ → Lean.Meta.Grind.EMatchTheoremConstraint
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_modifyₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ {a : α} {f : β a → β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.modifyₘ a f)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.length_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Order.ModularLattice
Codisjoint.codisjoint_inf_right_of_codisjoint_inf_left : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : OrderTop α] [IsModularLattice α],
  Codisjoint a b → Codisjoint (a ⊓ b) c → Codisjoint a (b ⊓ c)