mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_finsetSum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (∑ i ∈ t, f i) x
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- A Gram matrix is Hermitian.  -/
Matrix.isHermitian_gram : ∀ {E : Type u_1} {n : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (v : n → E), (Matrix.gram 𝕜 v).IsHermitian
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_zero_of_exists_eq_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β}, (∃ b, f b = 0) → ∀ [L.LeAtTop], HasProd f 0 L
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
cardinalMk_eq_cardinalMk_field_pow_rank : ∀ (K V : Type u) [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] [Module.Finite K V], Cardinal.mk V = Cardinal.mk K ^ Module.rank K V
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  (F : CategoryTheory.Limits.MonoFactorisation f.hom) (sq : f ⟶ g) [inst_1 : CategoryTheory.IsIso sq],
  (F.ofArrowIso sq).m = CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
Fin.clamp.eq_1 : ∀ (n m : ℕ), Fin.clamp n m = ⟨min n m, ⋯⟩
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_sUnion : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {S : Set (Set P)},
  S.Finite → asymptoticCone k (⋃₀ S) = ⋃ s ∈ S, asymptoticCone k s
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_right : ∀ {n a b : ℕ} (c : ℕ), a ≡ b [MOD n] → a + c ≡ b + c [MOD n]
-- Mathlib.Topology.MetricSpace.Bounded
Metric.cobounded_eq_cocompact : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α], Bornology.cobounded α = Filter.cocompact α
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instDecidableEq : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [DecidableEq R] → [DecidableEq M] → DecidableEq (MonoidAlgebra R M)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_1 : Inhabited (γ k)] (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.get! k = ((t.get? k).bind (f k)).get!
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioc_pred_pred_eq_Ico_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Set.Ioc (Order.pred a) (Order.pred b) = Set.Ico a b
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opFunctorInvolutive_hom_app_toFunctor_map : ∀ (X : CategoryTheory.Cat) {X_1 Y : (↑X)ᵒᵖᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.Cat.opFunctorInvolutive.hom.app X).toFunctor.map f = f.unop.unop
-- Mathlib.Data.Sym.Sym2.Finsupp
Finsupp.sym2_support_eq_preimage_support_mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : CommMonoidWithZero M₀] [NoZeroDivisors M₀] (f : α →₀ M₀),
  ↑f.support.sym2 = Sym2.map ⇑f ⁻¹' Function.support Sym2.mul
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $(r_1 r_2)^m x$, where $m$ is a natural number. This is the special case of
`Module.reflection_mul_reflection_pow_apply` with $z = x$.  -/
Module.reflection_mul_reflection_pow_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_pow_apply_self._auto_1 →
    ((Module.reflection hf * Module.reflection hg) ^ m) x =
      (Polynomial.eval t (Polynomial.Chebyshev.S R ↑m) + Polynomial.eval t (Polynomial.Chebyshev.S R (↑m - 1))) • x +
        (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m - 1)) * -g x) • y
-- Std.Do.Triple.SpecLemmas
/-- Creates a cursor at position `n` in the list `l`.
The prefix contains the first `n` elements, and the suffix contains the remaining elements.
If `n` is larger than the length of the list, the cursor is positioned at the end of the list.
 -/
List.Cursor.at : {α : Type u_1} → (l : List α) → ℕ → l.Cursor
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.transitionMap_ideal_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) (x : R),
  (AdicCompletion.transitionMap I R hmn) ((Ideal.Quotient.mk (I ^ n • ⊤)) x) = (Ideal.Quotient.mk (I ^ m • ⊤)) x
-- Init.Prelude
/-- The typeclass behind the notation `a >> b : γ` where `a : α`, `b : β`.
Because `b` is "lazy" in this notation, it is passed as `Unit → β` to the
implementation so it can decide when to evaluate it.
 -/
HAndThen : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.RingTheory.Trace.Quotient
trace_quotient_eq_trace_localization_quotient : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsMaximal] (Rₚ : Type u_3) (Sₚ : Type u_4) [inst_4 : CommRing Rₚ] [inst_5 : CommRing Sₚ]
  [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization.AtPrime Rₚ p] [inst_8 : IsLocalRing Rₚ] [inst_9 : Algebra S Sₚ]
  [inst_10 : Algebra R Sₚ] [inst_11 : Algebra Rₚ Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (x : S),
  (Algebra.trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ)
          (Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ)))
        ((algebraMap S (Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ))) x))
-- Mathlib.Analysis.Normed.Ring.Lemmas
Filter.comap_mul_left_cobounded : ∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [NormMulClass α] {a : α},
  a ≠ 0 → Filter.comap (fun x => a * x) (Bornology.cobounded α) = Bornology.cobounded α
-- Mathlib.Algebra.Group.Action.Defs
MulAction.mk : {α : Type u_9} →
  {β : Type u_10} →
    [inst : Monoid α] → [toSemigroupAction : SemigroupAction α β] → (∀ (b : β), 1 • b = b) → MulAction α β
-- Std.Async.System
/-- The user's name.
 -/
Std.Async.System.SystemUser.username : Std.Async.System.SystemUser → String
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- A limit (over a general filter) of measurable `ℝ≥0`-valued functions is measurable.  -/
NNReal.measurable_of_tendsto' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} {f : ι → α → NNReal} {g : α → NNReal} (u : Filter ι) [u.NeBot]
  [u.IsCountablyGenerated], (∀ (i : ι), Measurable (f i)) → Filter.Tendsto f u (nhds g) → Measurable g
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
CFC.monotoneOn_one_sub_one_add_inv_real : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  MonotoneOn (cfcₙ fun x => 1 - (1 + x)⁻¹) (Set.Ici 0)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- Construct a quadratic form on a family of modules from the quadratic form on each module.  -/
QuadraticMap.pi : {ι : Type u_1} →
  {R : Type u_2} →
    {P : Type u_7} →
      {Mᵢ : ι → Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] →
            [inst_2 : AddCommMonoid P] →
              [inst_3 : (i : ι) → Module R (Mᵢ i)] →
                [inst_4 : Module R P] →
                  [Fintype ι] → ((i : ι) → QuadraticMap R (Mᵢ i) P) → QuadraticMap R ((i : ι) → Mᵢ i) P
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.local.injEq : ∀ (wi wi_1 : Lean.Widget.WidgetInstance),
  (Lean.Widget.PanelWidgetsExtEntry.local wi = Lean.Widget.PanelWidgetsExtEntry.local wi_1) = (wi = wi_1)
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofBitVec : ∀ {b : BitVec 8}, { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.h_mem_prod : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂) (i : ι₁), (b₁.h i, b₂.h (eι i)) ∈ LieAlgebra.Basis.prod✝ eι b₁ b₂
-- Mathlib.Data.List.Rotate
List.reverse_rotate : ∀ {α : Type u} (l : List α) (n : ℕ), (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)
-- Mathlib.Algebra.Lie.Basic
/-- The inverse function of an equivalence of Lie algebras is a right inverse of the underlying
function.  -/
LieEquiv.right_inv : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (self : L ≃ₗ⁅R⁆ L'),
  Function.RightInverse self.invFun (↑self.toLieHom).toFun
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_succ' : ∀ {x y : NNReal} {n : ℕ},
  x.agmSequences y (n + 1) =
    (NNReal.sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.zero_update : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (b : M),
  SkewMonoidAlgebra.update 0 a b = SkewMonoidAlgebra.single a b
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_fun_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E}
  (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F),
  UniqueDiffWithinAt 𝕜 s x → extDerivWithin (fun x => c • ω x) s x = c • extDerivWithin ω s x
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_insert : ∀ (x y : ZFSet.{u_1}), x ∈ insert x y
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor D C) {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [G.IsCoverDense J]
  [G.Full] [inst_5 : G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj],
  K.W.inverseImage ((CategoryTheory.Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W
-- Mathlib.LinearAlgebra.Prod
LinearMap.mem_graph_iff : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (x : M × M₂), x ∈ f.graph ↔ x.2 = f x.1
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_zero_left : ∀ (p : ℕ), Nat.divMaxPow 0 p = 0
-- Mathlib.Dynamics.Ergodic.Conservative
/-- If `f` is a conservative map and `s` is a measurable set of nonzero measure, then
for an arbitrarily large `m` a positive measure of points `x ∈ s` returns back to `s`
after `m` iterations of `f`.  -/
MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∀ (N : ℕ), ∃ m > N, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.pow_lt_one_of_lt : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M} {n : ℕ}, a < 1 → n ≠ 0 → a ^ n < 1
-- Mathlib.Combinatorics.HalesJewett
/-- A generalization of Van der Waerden's theorem: if `M` is a finitely colored commutative
monoid, and `S` is a finite subset, then there exists a monochromatic homothetic copy of `S`.  -/
Combinatorics.exists_mono_homothetic_copy : ∀ {M : Type u_5} {κ : Type u_6} [inst : AddCommMonoid M] (S : Finset M) [Finite κ] (C : M → κ),
  ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
-- Mathlib.Tactic.FunProp.Types
/-- Increase depth  -/
Mathlib.Meta.FunProp.Context.increaseTransitionDepth : Mathlib.Meta.FunProp.Context → Mathlib.Meta.FunProp.Context
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.instHasFunctorialFactorizationFunctorFunctorCategory : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.HasFunctorialFactorization W₂] (J : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} J],
  (W₁.functorCategory J).HasFunctorialFactorization (W₂.functorCategory J)
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Submonoid.multiples` of two elements `a, b` of the same additive
order, mapping `i • a` to `i • b`.  -/
multiplesEquivMultiples : {G : Type u_1} →
  [inst : AddLeftCancelMonoid G] →
    [Finite G] → {x y : G} → addOrderOf x = addOrderOf y → ↥(AddSubmonoid.multiples x) ≃ ↥(AddSubmonoid.multiples y)
-- Mathlib.Order.Category.DistLat
DistLat.forget_map : ∀ {X Y : DistLat} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget DistLat).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_eq_get_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List ((a : α) × β a)}
  {h : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.getValueCast a l h = (Std.Internal.List.getValueCast? a l).get ⋯
-- Batteries.Data.Array.Scan
Array.scanl_push : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β} {a : α} {as : Array α},
  Array.scanl f init (as.push a) = (Array.scanl f init as).push (f (Array.foldl f init as) a)
-- Init.Data.Nat.Lemmas
Nat.pos_of_mul_pos_right : ∀ {a b : ℕ}, 0 < a * b → 0 < a
-- Mathlib.Order.CompleteLattice.Defs
instCompleteSemilatticeInfOrderDualOfCompleteSemilatticeSup.eq_1 : ∀ {α : Type u_8} [inst : CompleteSemilatticeSup α],
  instCompleteSemilatticeInfOrderDualOfCompleteSemilatticeSup =
    { toPartialOrder := OrderDual.instPartialOrder α, toInfSet := OrderDual.infSet α, isGLB_sInf := ⋯ }
-- Mathlib.Order.Concept
Concept.extent_ofObjects_of_isExtent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α}, Order.IsExtent r s → (Concept.ofObjects r s).extent = s
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F).inv.app X).hom.left =
    CategoryTheory.CategoryStruct.id X.pt.left
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `rgStop` is the `Position` where the deprecated declaration ends.  -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.rgStop : Mathlib.Tactic.DeprecationInfo✝ → Lean.Position
-- Mathlib.Algebra.Polynomial.UnitTrinomial
/-- A unit trinomial is irreducible if it is coprime with its mirror  -/
Polynomial.IsUnitTrinomial.irreducible_of_isCoprime : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → IsCoprime p p.mirror → Irreducible p
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.refl_mem_dilatransvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  LinearEquiv.refl R V ∈ LinearEquiv.dilatransvections R V
-- Mathlib.Geometry.Manifold.ChartedSpace
prodChartedSpace_chartAt : ∀ {H : Type u} {H' : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H'] [inst_4 : TopologicalSpace M']
  [inst_5 : ChartedSpace H' M'] {x : M × M'}, chartAt (ModelProd H H') x = (chartAt H x.1).prod (chartAt H' x.2)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.mk.injEq : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y)
  (h₀ : autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h = f.map) SSet.RelativeMorphism.Homotopy.h₀._autoParam)
  (h₁ : autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h = g.map) SSet.RelativeMorphism.Homotopy.h₁._autoParam)
  (rel :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) h =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
          (CategoryTheory.CategoryStruct.comp φ B.ι))
      SSet.RelativeMorphism.Homotopy.rel._autoParam)
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y)
  (h₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h_1 = f.map) SSet.RelativeMorphism.Homotopy.h₀._autoParam)
  (h₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h_1 = g.map) SSet.RelativeMorphism.Homotopy.h₁._autoParam)
  (rel_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) h_1 =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
          (CategoryTheory.CategoryStruct.comp φ B.ι))
      SSet.RelativeMorphism.Homotopy.rel._autoParam),
  ({ h := h, h₀ := h₀, h₁ := h₁, rel := rel } = { h := h_1, h₀ := h₀_1, h₁ := h₁_1, rel := rel_1 }) = (h = h_1)
-- ImportGraph.Tools.MinImports
«command#minimize_imports» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.Polarization_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (x : M), P.Polarization x = ∑ i, (P.coroot' i) x • P.coroot i
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.nullMeasurableSet_smul_measure_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {c : ENNReal},
  c ≠ 0 → (MeasureTheory.NullMeasurableSet s (c • μ) ↔ MeasureTheory.NullMeasurableSet s μ)
-- Mathlib.Algebra.Group.ULift
ULift.addCancelCommMonoid.eq_1 : ∀ {α : Type u} [inst : AddCancelCommMonoid α],
  ULift.addCancelCommMonoid = Function.Injective.addCancelCommMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Order.Filter.Basic
/-- **Alias** of the forward direction of `Filter.frequently_inf_principal`. -/
Filter.Frequently.of_inf_principal : ∀ {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop},
  (∃ᶠ (x : α) in f ⊓ Filter.principal s, p x) → ∃ᶠ (x : α) in f, x ∈ s ∧ p x
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instIteratorLoop.loop.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [inst_4 : Monad n] (γ : Type u)
  (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ)
  (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxo.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc next h f =
    WellFounded.extrinsicFix₃
      (InvImage (Std.IteratorLoop.rel (Std.Rxo.Iterator α) Id Pl) fun x =>
        ({ internalState := { next := some x.fst, upperBound := upperBound } }, x.snd.fst))
      (fun next acc h G =>
        if hu : next < upperBound then do
          let __do_lift ← f next h hu acc
          match __do_lift with
            | ⟨ForInStep.yield acc', h'⟩ =>
              match hs : Std.PRange.succ? next with
              | some next' => G next' acc' ⋯ ⋯
              | none => pure acc'
            | ⟨ForInStep.done acc', property⟩ => pure acc'
        else pure acc)
      next acc h
-- Mathlib.Probability.Kernel.Basic
/-- Kernel which to `a` associates the dirac measure at `f a`. This is a Markov kernel.  -/
ProbabilityTheory.Kernel.deterministic : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → (f : α → β) → Measurable f → ProbabilityTheory.Kernel α β
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I),
  (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I) i =
    (NumberField.mixedEmbedding K) ((NumberField.basisOfFractionalIdeal K I) i)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux.eq_2 : ∀ (e a0 a : ONote) (m : ℕ), e.opowAux a0 a 0 m.succ = e.oadd m.succPNat 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.isBasis_preimage_isAffineOpen : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)],
  TopologicalSpace.Opens.IsBasis
    {x | ∃ i V, ∃ (_ : AlgebraicGeometry.IsAffineOpen V), (TopologicalSpace.Opens.map (c.π.app i).base).obj V = x}
-- Mathlib.Algebra.Group.Defs
mul_right_cancel : ∀ {G : Type u_1} [inst : Mul G] [IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.Extension.getEMatchTheorems : Lean.Meta.Grind.Extension → Lean.CoreM Lean.Meta.Grind.EMatchTheorems
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.BoundaryLE.false_of_isTruncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι},
  e.BoundaryLE j → ∀ [e.IsTruncGE], False
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The base change of a standard etale algebra is standard etale.  -/
StandardEtalePresentation.baseChange : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] → StandardEtalePresentation R S → StandardEtalePresentation T (TensorProduct R T S)
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.strongSubRecursion.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) → (x x_1 : ℕ) → ((n m : ℕ) → motive n m) → motive x x_1