mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Module
DirectSum.mker_map : ∀ {ι : Type v} {M : ι → Type w} [inst : (i : ι) → AddCommMonoid (M i)] {N : ι → Type u_1}
  [inst_1 : (i : ι) → AddCommMonoid (N i)] (f : (i : ι) → M i →+ N i),
  AddMonoidHom.mker (DirectSum.map f) =
    AddSubmonoid.comap (DirectSum.coeFnAddMonoidHom M) (AddSubmonoid.pi Set.univ fun i => AddMonoidHom.mker (f i))
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The uniform space structure on `L` induced by the spectral norm.  -/
spectralNorm.uniformSpace : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → UniformSpace L
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_counitIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithTerminal Cᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).counitIso.hom.app X =
    (match X with
      | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x)
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel`.  -/
mul_inv_le_one : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] [ZeroLEOneClass G₀] {a : G₀}, a * a⁻¹ ≤ 1
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- `f` is an effective epimorphism if there exists an `EffectiveEpiStruct` for `f`.  -/
CategoryTheory.EffectiveEpi.effectiveEpi : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X Y : C} {f : Y ⟶ X}
  [self : CategoryTheory.EffectiveEpi f], Nonempty (CategoryTheory.EffectiveEpiStruct f)
-- Init.Data.String.Basic
String.Pos.sliceFrom_ofSliceFrom : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}, p₀.sliceFrom (String.Pos.ofSliceFrom p) ⋯ = p
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  {r : Std.Rcc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Rcc.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Mathlib.LinearAlgebra.TensorProduct.Matrix
/-- `TensorProduct.assoc` corresponds to a permutation of the identity matrix.  -/
TensorProduct.toMatrix_assoc : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {ι : Type u_7} {κ : Type u_8} {τ : Type u_9}
  [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : DecidableEq τ] [inst_3 : Fintype ι] [inst_4 : Fintype κ]
  [inst_5 : Fintype τ] [inst_6 : CommRing R] [inst_7 : AddCommGroup M] [inst_8 : AddCommGroup N]
  [inst_9 : AddCommGroup P] [inst_10 : Module R M] [inst_11 : Module R N] [inst_12 : Module R P]
  (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bP : Module.Basis τ R P),
  (LinearMap.toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)))
      ↑(TensorProduct.assoc R M N P) =
    Matrix.submatrix 1 id ⇑(Equiv.prodAssoc ι κ τ)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_involutive : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x : P),
  Function.Involutive ⇑(AffineIsometryEquiv.pointReflection 𝕜 x)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.embedding_generator' : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete],
  MonoidWithZeroHom.ValueGroup₀.embedding ↑(Valuation.IsRankOneDiscrete.generator' v) =
    ↑(Valuation.IsRankOneDiscrete.generator v)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.descQ.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k k_1 : S.X₂ ⟶ A) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0), h.descQ k hk = h.descQ k_1 ⋯
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.prodMkRight γ κ)
-- Init.Internal.Order.Basic
Lean.Order.admissible_pi : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {β : Sort u_1} (P : α → β → Prop),
  (∀ (y : β), Lean.Order.admissible fun x => P x y) → Lean.Order.admissible fun x => ∀ (y : β), P x y
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mk.sizeOf_spec : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : SizeOf 𝕜] [inst_12 : SizeOf E]
  [inst_13 : SizeOf H] [inst_14 : SizeOf M] [inst_15 : SizeOf F] [inst_16 : (a : M) → SizeOf (V a)]
  (toFun : (x : M) → V x) (contMDiff_toFun : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, toFun x⟩),
  sizeOf { toFun := toFun, contMDiff_toFun := contMDiff_toFun } = 1
-- Mathlib.Order.SymmDiff
Disjoint.le_symmDiff_sup_symmDiff_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Disjoint b c → a ≤ symmDiff a b ⊔ symmDiff a c
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i},
  HasFDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) φ' s x ↔
    HasFDerivWithinAt φ (ContinuousLinearMap.proj 0 ∘SL φ') s x ∧
      HasFDerivWithinAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') s x
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.initial_of_representablyCoflat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [h : CategoryTheory.RepresentablyCoflat F], F.Initial
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.t.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] (j : ι),
  f.t j = CategoryTheory.Limits.Sigma.desc fun c => SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.prodMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {a : α} {b : β} {n : ℕ},
  Function.IsPeriodicPt f n a → Function.IsPeriodicPt g n b → Function.IsPeriodicPt (Prod.map f g) n (a, b)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.coe_restrOpen : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s), ↑(e.restrOpen s hs) = ↑e
-- Mathlib.NumberTheory.FactorisationProperties
/-- `n : ℕ` is a _weird_ number if and only if it is abundant but not pseudoperfect.  -/
Nat.Weird : ℕ → Prop
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_natCast_nonneg : ∀ (v : ℕ → ℕ), 0 ≤ LinearGrowth.linearGrowthInf fun n => ↑(v n)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ext_iff : ∀ {x y : UpperHalfPlane}, x = y ↔ ↑x = ↑y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_apply_map_one : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₂ : Type u_6} [inst_1 : TopologicalSpace M₂] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R₁ M₂] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₂] (c : R₁ →L[R₁] M₂),
  ContinuousLinearMap.toSpanSingleton R₁ (c 1) = c
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike.getProof : {α : Type} → [self : Lean.Meta.Grind.TheoremLike α] → α → Lean.Expr
-- Mathlib.Algebra.Group.Action.Units
/-- Note this has different defeqs than `Units.mulAction'`, but doesn't create a diamond
with it in non-degenerate situations. Indeed, to get a diamond on `MulDistribMulAction G Mˣ`,
we would need both instances to fire. But `Units.mulAction'` assumes `SMulCommClass G M M`,
i.e. `∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = m₁ * g • m₂`), while
`Units.instMulDistribMulActionRight` assumes `MulDistribMulAction G M`,
i.e. `∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = g • m₁ * g • m₂`.
In particular, if `M` is cancellative, then we obtain `∀ (g : G) (m : M), g • m = m`,
i.e. the action is trivial!

This however does create a (propeq) diamond for `MulDistribMulAction (ConjAct Mˣ) Mˣ` with
`ConjAct.unitsMulDistribMulAction` and `ConjAct.instMulDistribMulAction`. Indeed, if we go down
one way then `u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * v⁻¹ * ofConjAct u⁻¹, _, _⟩`,
while the other way is
`u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * (v⁻¹ * ofConjAct u⁻¹), _, _⟩`.  -/
Units.mulDistribMulActionRight : {M : Type u_6} →
  {N : Type u_7} → [inst : Monoid M] → [inst_1 : Monoid N] → [MulDistribMulAction M N] → MulDistribMulAction M Nˣ
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.stronglyMeasurable_poissonPMFReal : ∀ (r : NNReal), MeasureTheory.StronglyMeasurable (ProbabilityTheory.poissonPMFReal r)
-- Mathlib.Algebra.Group.Defs
zpow_negSucc : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G) (n : ℕ), a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
-- Mathlib.Tactic.Polynomial.Core
/-- `polynomial_pre` marks a theorem to be used by the `polynomial` tactic as a preprocessing lemma.
These serve the purpose of removing any definitions specific to polynomials that `algebra` can't
handle. e.g. `Polynomial.C` and `Polynomial.map`  -/
Mathlib.Tactic.Polynomial.polynomialPreExt : Lean.Meta.SimpExtension
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x * a) ⁻¹' Set.Iio b = Set.Iio (b / a)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The canonical map from `List (α × Bool)` to the free group on `α`.  -/
FreeGroup.mk : {α : Type u} → List (α × Bool) → FreeGroup α
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and
the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is continuous at
`a` from the right.  -/
continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  MonotoneOn f s →
    s ∈ nhdsWithin a (Set.Ici a) → f '' s ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
MeromorphicAt.eventually_nhdsSet_eventuallyEq_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f g : 𝕜 → E},
  MeromorphicOn f U →
    MeromorphicOn g U →
      Preperfect U → f =ᶠ[Filter.codiscreteWithin U] g → ∀ᶠ (x : 𝕜) in nhdsSet U, f =ᶠ[nhdsWithin x {x}ᶜ] g
-- Init.Data.List.Sublist
List.prefix_iff_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ l₁ ++ List.drop l₁.length l₂ = l₂
-- Mathlib.Order.Filter.Interval
/-- A pair of filters `l₁`, `l₂` has `TendstoIxxClass Ixx` property if `Ixx a b` tends to
`l₂.small_sets` as `a` and `b` tend to `l₁`. In all instances `Ixx` is one of `Set.Icc`, `Set.Ico`,
`Set.Ioc`, or `Set.Ioo`. The instances provide the best `l₂` for a given `l₁`. In many cases
`l₁ = l₂` but sometimes we can drop an endpoint from an interval: e.g., we prove
`TendstoIxxClass Set.Ico (𝓟 (Set.Iic a)) (𝓟 (Set.Iio a))`, i.e., if `u₁ n` and `u₂ n` belong
eventually to `Set.Iic a`, then the interval `Set.Ico (u₁ n) (u₂ n)` is eventually included in
`Set.Iio a`.

We mark `l₂` as an `outParam` so that Lean can automatically find an appropriate `l₂` based on
`Ixx` and `l₁`. This way, e.g., `tendsto.Ico h₁ h₂` works without specifying explicitly `l₂`.  -/
Filter.TendstoIxxClass : {α : Type u_1} → (α → α → Set α) → Filter α → outParam (Filter α) → Prop
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `zero_apply`. -/
AddGroupSeminorm.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.isScalarTower : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : Algebra.Extension R S), IsScalarTower R self.Ring S
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.sum_smul_mem : ∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {t : Finset ι} {f : ι → M} (r : ι → R), (∀ c ∈ t, f c ∈ p) → ∑ i ∈ t, r i • f i ∈ p
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitInvAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (x : (j : J) × ↑(F.obj j)),
  GrpCat.FilteredColimits.colimitInvAux F x = GrpCat.FilteredColimits.G.mk F ⟨x.fst, x.snd⁻¹⟩
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_ker_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) {c d : C} (f : c ⟶ d),
  f ∈ (CategoryTheory.Subgroupoid.ker φ).arrows c d ↔ ∃ (h : φ.obj c = φ.obj d), φ.map f = CategoryTheory.eqToHom h
-- Mathlib.Dynamics.Flow
Flow.orbit_restrict : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (s : Set α) (hs : IsInvariant ϕ.toFun s) (x : ↑s), (ϕ.restrict hs).orbit x = Subtype.val ⁻¹' ϕ.orbit ↑x
-- Init.Data.Int.DivMod.Lemmas
Int.eq_fdiv_of_mul_eq_left : ∀ {a b c : ℤ}, b ≠ 0 → a * b = c → a = c.fdiv b
-- Mathlib.Order.Directed
SemilatticeSup.instIsDirectedOrder : ∀ {α : Type u_1} [inst : SemilatticeSup α], IsDirectedOrder α
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_toNonUnitalSubring : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [inst_3 : Star A]
  (S : NonUnitalStarSubalgebra R A), ↑S.toNonUnitalSubring = ↑S
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.equalizerSieve_self_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ}
  (x : CategoryTheory.ToType (F.obj X)), CategoryTheory.Presheaf.equalizerSieve x x = ⊤
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiff.sub : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f g : M → G}, ContMDiff I' I n f → ContMDiff I' I n g → ContMDiff I' I n fun x => f x - g x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postCongr_inv_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F G : CategoryTheory.Functor T D} (e : F ≅ G) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.postCongr e).inv.app X_1).left = e.inv.app X_1.left
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coe_coe : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N] (f : F), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Subobject.Comma
/-- Every quotient of a costructured arrow can be projected to a quotient of the underlying
object.  -/
CategoryTheory.CostructuredArrow.projectQuotient : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          {T : D} →
            [CategoryTheory.Limits.HasFiniteColimits C] →
              [CategoryTheory.Limits.PreservesFiniteColimits S] →
                {A : CategoryTheory.CostructuredArrow S T} →
                  CategoryTheory.Subobject (Opposite.op A) → CategoryTheory.Subobject (Opposite.op A.left)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- Closure of a subsemigroup `S` equals `S`.  -/
Subsemigroup.closure_eq : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), Subsemigroup.closure ↑S = S
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Criterion for equality in terms of real part and norm. Useful when working with the
geometry of the fundamental domain.  -/
UpperHalfPlane.eq_of_re_of_norm : ∀ {τ τ' : UpperHalfPlane}, τ.re = τ'.re → ‖↑τ‖ = ‖↑τ'‖ → τ = τ'
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). Given a section of `ℱ` on `X`, we can obtain a family of elements valued in `ℱ'`
that is defined on a cover generated by the images of `G`.  -/
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {G : CategoryTheory.Functor C D} →
            {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} →
              {ℱ' : CategoryTheory.Sheaf K (Type v)} →
                (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) →
                  {X : D} →
                    ℱ.obj (Opposite.op X) →
                      CategoryTheory.Presieve.FamilyOfElements ℱ'.obj (CategoryTheory.Presieve.coverByImage G X)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.embeddingConjugateIte_neg : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
  ¬NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding →
    NumberField.InfinitePlace.embeddingConjugateIte✝ v w = NumberField.ComplexEmbedding.conjugate w.embedding
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup (WithZero α)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskering_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.whiskering E).obj c = CategoryTheory.Limits.Cocone.whisker E c
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α α_1 : LieModule.Weight K (↥H) L),
  α = α_1 →
    ∀ (β β_1 : LieModule.Weight K (↥H) L),
      β = β_1 → LieAlgebra.IsKilling.chainLength α β = LieAlgebra.IsKilling.chainLength α_1 β_1
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy : Type → Type → Type
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.centroid_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] [CharZero k] {V₂ : Type u_4} {P₂ : Type u_5} [inst_5 : AddCommGroup V₂]
  [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂)
  (hf : Function.Injective ⇑f), (s.map f hf).centroid = f s.centroid
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.assoc_tmul : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R P] [inst_9 : Module S M]
  [inst_10 : IsScalarTower R S M] [inst_11 : Coalgebra S M] [inst_12 : Module S N] [inst_13 : IsScalarTower R S N]
  [inst_14 : Coalgebra S N] [inst_15 : Coalgebra R P] (x : M) (y : N) (z : P),
  (Coalgebra.TensorProduct.assoc R S M N P) (x ⊗ₜ[S] y ⊗ₜ[R] z) = x ⊗ₜ[S] (y ⊗ₜ[R] z)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topCat_hasColimits : CategoryTheory.Limits.HasColimits TopCat
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCast_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  {h : Std.DHashMap.Internal.AssocList.contains a l = true},
  Std.DHashMap.Internal.AssocList.getCast a l h = Std.Internal.List.getValueCast a l.toList ⋯
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Runs a `DSimpM` computation with the given methods and configuration.  -/
Lean.Meta.Sym.DSimp.DSimpM.run' : {α : Type} →
  Lean.Meta.Sym.DSimp.DSimpM α →
    optParam Lean.Meta.Sym.DSimp.Methods { } → optParam Lean.Meta.Sym.DSimp.Config { } → Lean.Meta.Sym.SymM α
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
the family by another vector while retaining linear independence.  -/
exists_linearIndependent_snoc_of_lt_rank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {n : ℕ} {v : Fin n → M},
  LinearIndependent R v → ↑n < Module.rank R M → ∃ x, LinearIndependent R (Fin.snoc v x)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.mk.injEq : ∀ (p : Lean.Grind.CommRing.Poly) (strict : Bool) (h : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof)
  (p_1 : Lean.Grind.CommRing.Poly) (strict_1 : Bool) (h_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof),
  ({ p := p, strict := strict, h := h } = { p := p_1, strict := strict_1, h := h_1 }) =
    (p = p_1 ∧ strict = strict_1 ∧ h = h_1)