mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- **Alias** of the reverse direction of `SmoothBumpCovering.isSubordinate_toBumpCovering`. -/
SmoothBumpCovering.IsSubordinate.toBumpCovering : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} [inst_6 : T2Space M]
  [inst_7 : IsManifold I (↑⊤) M] {f : SmoothBumpCovering ι I M s} {U : M → Set M},
  f.IsSubordinate U → f.toBumpCovering.IsSubordinate fun i => U (f.c i)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.δ_objMk₁_of_le : ∀ {n : ℕ} (i : Fin (n + 3)) (j : Fin (n + 2)) (h : i ≤ j.castSucc),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (SSet.stdSimplex.obj { len := 1 }) j))
      (SSet.stdSimplex.objMk₁ i) =
    SSet.stdSimplex.objMk₁ (i.castPred ⋯)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.left_invariant'' : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (self : LeftInvariantDerivation I G) (g : G),
  (hfdifferential ⋯) ((Derivation.evalAt 1) ↑self) = (Derivation.evalAt g) ↑self
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Matrix.isIntegral : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  IsIntegral R M
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {T : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} T] (L : CategoryTheory.Functor A T)
  {W : CategoryTheory.MorphismProperty T} {X : T} [W.RespectsIso],
  (CategoryTheory.MorphismProperty.costructuredArrowObj L W).IsClosedUnderIsomorphisms
-- Lean.Parser.Extra
Lean.Parser.ident.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.PredTrans.pushOption.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMapAlgHom_apply_apply : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂)) (i : M × M₂),
  ((LinearMap.prodMapAlgHom R M M₂) f) i = (f.1 i.1, f.2 i.2)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.fullChange.sizeOf_spec : ∀ (text : String), sizeOf (Lean.Lsp.TextDocumentContentChangeEvent.fullChange text) = 1 + sizeOf text
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : (F.leftDerived 0).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X)
      (CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) h) =
    h
-- Mathlib.Analysis.Meromorphic.Order
meromorphicOrderAt_mul_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {g f : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → g x ≠ 0 → meromorphicOrderAt (g * f) x = meromorphicOrderAt f x
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.PredTrans.pushExcept.match_1.eq_1 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_pos_of_nonneg_of_pos`.  -/
add_pos_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  0 ≤ a → 0 < b → 0 < a + b
-- Mathlib.Topology.Piecewise
Continuous.if_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} (p : Prop)
  [inst_2 : Decidable p], Continuous f → Continuous g → Continuous fun a => if p then f a else g a
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The category of multicoforks is equivalent to the category of coforks over `∐ I.left ⇉ ∐ I.right`.
It then follows from `CategoryTheory.IsColimit.ofPreservesCoconeInitial` (or `reflects`) that
it preserves and reflects colimit cocones.
 -/
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            {d : CategoryTheory.Limits.Cofan I.right} →
              CategoryTheory.Limits.IsColimit d →
                (CategoryTheory.Limits.Multicofork I ≌
                  CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.mk.congr_simp : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (c c_1 : Fin N.succ → α) (e_c : c = c_1)
  (r r_1 : Fin N.succ → ℝ) (e_r : r = r_1) (rpos : ∀ (i : Fin N.succ), 0 < r i)
  (h : Pairwise fun i j => r i ≤ dist (c i) (c j) ∧ r j ≤ τ * r i ∨ r j ≤ dist (c j) (c i) ∧ r i ≤ τ * r j)
  (hlast : ∀ i < Fin.last N, r i ≤ dist (c i) (c (Fin.last N)) ∧ r (Fin.last N) ≤ τ * r i)
  (inter : ∀ i < Fin.last N, dist (c i) (c (Fin.last N)) ≤ r i + r (Fin.last N)),
  { c := c, r := r, rpos := rpos, h := h, hlast := hlast, inter := inter } =
    { c := c_1, r := r_1, rpos := ⋯, h := ⋯, hlast := ⋯, inter := ⋯ }
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.symm_toPartialEquiv : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n),
  Φ.symm.toPartialEquiv = Φ.symm
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.closure_def' : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, ¬f.IsClosable → f.closure = f
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.allM.eq_def : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool) (x : List α),
  List.allM p x =
    match x with
    | [] => pure true
    | a :: as => do
      let __do_lift ← p a
      match __do_lift with
        | true => List.allM p as
        | false => pure false
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.add_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂), (φ + φ').τ₃ = φ.τ₃ + φ'.τ₃
-- Mathlib.RingTheory.LocalRing.Pullback
/-- The subring of pairs `(r, s) : R × S` such that `f r = g s`, i.e.,
the pullback of `f : R →+* T` and `g : S →+* T` as a subring of `R × S`.  -/
RingHom.pullback : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Ring R] → [inst_1 : Ring S] → [inst_2 : Semiring T] → (R →+* T) → (S →+* T) → Subring (R × S)
-- Mathlib.Algebra.Group.Action.Defs
SemigroupAction.ext_iff : ∀ {α : Type u_9} {β : Type u_10} {inst : Semigroup α} {x y : SemigroupAction α β}, x = y ↔ SMul.smul = SMul.smul
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.mk.inj : ∀ {ngen : Lean.NameGenerator} {core : Lean.Core.Cache} {«meta» : Lean.Meta.Cache} {ngen_1 : Lean.NameGenerator}
  {core_1 : Lean.Core.Cache} {meta_1 : Lean.Meta.Cache},
  { ngen := ngen, core := core, «meta» := «meta» } = { ngen := ngen_1, core := core_1, «meta» := meta_1 } →
    ngen = ngen_1 ∧ core = core_1 ∧ «meta» = meta_1
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_eq_iInf : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ (s : Set α), (MeasureTheory.inducedOuterMeasure m P0 m0) s = ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
-- Mathlib.CategoryTheory.Products.Bifunctor
CategoryTheory.Bifunctor.diagonal' : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor (C × D) E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y)))
      (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X') g)) =
    F.map (CategoryTheory.Prod.mkHom f g)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a singleton is the distance to the unique point in this singleton.  -/
Metric.infDist_singleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Metric.infDist x {y} = dist x y
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.comp_ι_eq : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  (f g : NormedAddGroupHom V W), f.comp (NormedAddGroupHom.Equalizer.ι f g) = g.comp (NormedAddGroupHom.Equalizer.ι f g)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.add_mem_sup : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} {x y : M}, x ∈ S → y ∈ T → x + y ∈ S ⊔ T
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_hom_ext_iff : ∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R} {f g : (ModuleCat.free R).obj X ⟶ M},
  f = g ↔
    ∀ (x : X),
      (CategoryTheory.ConcreteCategory.hom f) (ModuleCat.freeMk x) =
        (CategoryTheory.ConcreteCategory.hom g) (ModuleCat.freeMk x)
-- Mathlib.RingTheory.PowerSeries.Order
/-- `PowerSeries.order` as a `MonoidHom`.  -/
PowerSeries.orderHom : {R : Type u_1} → [inst : Semiring R] → [NoZeroDivisors R] → [Nontrivial R] → PowerSeries R →* Multiplicative ℕ∞
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_le_set_inter : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s ≤ᵐ[μ] t → s' ≤ᵐ[μ] t' → s ∩ s' ≤ᵐ[μ] t ∩ t'
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on an open disc and is
continuous on its closure, then for any `w` in this open ball we have
$\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.  -/
DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E},
  DiffContOnCl ℂ f (Metric.ball c R) →
    w ∈ Metric.ball c R → (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `mdifferentiableAt_iff_differentiableAt`.

---

For maps between vector spaces, `MDifferentiableAt` and `DifferentiableAt` coincide  -/
DifferentiableAt.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E}, DifferentiableAt 𝕜 f x → MDiffAt f x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- `bound` lemma for branching on `1 ≤ a ∨ a ≤ 1` when proving `a ^ n ≤ a ^ m`  -/
Bound.pow_le_pow_right_of_le_one_or_one_le : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} {m n : ℕ} [ZeroLEOneClass M₀]
  [PosMulMono M₀], 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n → a ^ n ≤ a ^ m
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] (f : MeasureTheory.SimpleFunc α E), MeasureTheory.Integrable (⇑f) μ
-- Mathlib.MeasureTheory.Measure.Regular
IsCompact.exists_isOpen_lt_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α},
  IsCompact K → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < μ K + ε
-- Mathlib.Data.Seq.Defs
/-- Translate a sequence into a `MLList`.  -/
Stream'.Seq.toMLList : {α : Type u} → Stream'.Seq α → MLList Id α
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.op_smul_inter_nonempty_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α} {x : αᵐᵒᵖ},
  (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocallyArtinian X] (U : ↑X.affineOpens),
  IsArtinianRing ↑(X.presheaf.obj (Opposite.op ↑U))
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExists.eq_1 : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E'),
  DiscreteConvolution.ConvolutionExists L f g = ∀ (x : M), DiscreteConvolution.ConvolutionExistsAt L f g x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.equation_iff_variableChange : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  W.Equation x y ↔ (WeierstrassCurve.toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0
-- Std.Time.Format.Modifier
Std.Time.Modifier.c.sizeOf_spec : ∀ (presentation : Std.Time.Number ⊕ Std.Time.Text), sizeOf (Std.Time.Modifier.c presentation) = 1 + sizeOf presentation
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.hasInjectiveDimensionLT_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X X' : C} (e : X ≅ X')
  (n : ℕ) [CategoryTheory.HasInjectiveDimensionLT X n], CategoryTheory.HasInjectiveDimensionLT X' n
-- Init.Data.Int.DivMod.Lemmas
Int.add_ediv_of_pos : ∀ {a b c : ℤ}, 0 < c → (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.instInhabitedState : Inhabited Lean.Elab.Term.CollectPatternVars.State
-- Mathlib.Control.Functor
Functor.of_mem_supp : ∀ {F : Type u → Type v} [inst : Functor F] {α : Type u} {x : F α} {p : α → Prop},
  Functor.Liftp p x → ∀ y ∈ Functor.supp x, p y
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_three_of_utf8Size_eq_four : ∀ {c : Char} (h : c.utf8Size = 4), (String.utf8EncodeChar c)[3].toBitVec = 2#2 ++ BitVec.extractLsb' 0 6 c.val.toBitVec
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprConfigInteractive.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.ConfigInteractive
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.preconnected_iff : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H), G.Preconnected ↔ H.Preconnected
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.inv : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α} {a : α}, HasProd f a L → HasProd (fun b => (f b)⁻¹) a⁻¹ L
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_one : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 1).HasBasis p U → (uniformity α).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.cons_head : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i)
  (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  (Monoid.PushoutI.NormalWord.cons g w hmw hgr).head = (MonoidHom.ofInjective ⋯).symm (⋯.equiv (g * (φ i) w.head)).1
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The continuous linear equivalences from `M` to itself form a group under composition.  -/
ContinuousLinearEquiv.automorphismGroup : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    (M₁ : Type u_4) →
      [inst_1 : TopologicalSpace M₁] → [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → Group (M₁ ≃L[R₁] M₁)
-- Mathlib.Topology.Constructions.SumProd
isEmbedding_prodMkLeft : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (y : Y),
  Topology.IsEmbedding fun x => (x, y)
-- Init.Data.UInt.Lemmas
UInt16.toNat_inj : ∀ {a b : UInt16}, a.toNat = b.toNat ↔ a = b
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_uSizeToBitVec : ∀ (n : USize), { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) →
    HasStrictDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Mathlib.Algebra.GroupWithZero.Basic
left_eq_mul₀ : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsLeftCancelMulZero M₀], a ≠ 0 → (a = a * b ↔ b = 1)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiable_sub_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x},
  MDiff (T% s) → MDiff (T% t) → MDiff fun x => ⟨x, (s - t) x⟩
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.mk : {X : Type u} →
  [inst : TopologicalSpace X] →
    {C : Set X} →
      {D : outParam (Set X)} →
        (cell : ℕ → Type u) →
          (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
            (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
              (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                  (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                    (∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D) →
                      (∀ (n : ℕ) (i : cell n),
                          ∃ I,
                            Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                              (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)) →
                        (∀ A ⊆ C,
                            (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧
                                IsClosed (A ∩ D) →
                              IsClosed A) →
                          IsClosed D → D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.RelCWComplex C D
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.inv`

---

`(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticAt.fun_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {x : E}, AnalyticAt 𝕜 f x → f x ≠ 0 → AnalyticAt 𝕜 (fun i => (f i)⁻¹) x
-- Init.Data.Nat.Basic
Nat.gt_of_not_le : ∀ {n m : ℕ}, ¬n ≤ m → n > m
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.generateHas_compl : ∀ {α : Type u_3} {C : Set (Set α)} {s : Set α},
  MeasurableSpace.DynkinSystem.GenerateHas C sᶜ ↔ MeasurableSpace.DynkinSystem.GenerateHas C s
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_dvd_iff_le_of_ne_one : ∀ {p : ℕ}, p ≠ 1 → ∀ {a n : ℕ}, a ≠ 0 → (p ^ n ∣ a ↔ n ≤ padicValNat p a)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The linear map `(LocalizedModule S M) → (LocalizedModule S M)` from `iso` is the identity.  -/
IsLocalizedModule.iso_localizedModule_eq_refl : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (M : Type u_2) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  IsLocalizedModule.iso S (LocalizedModule.mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)
-- Mathlib.Data.List.Rotate
List.instDecidableR_mathlib : {α : Type u} → [DecidableEq α] → {l l' : List α} → Decidable ((List.IsRotated.setoid α) l l')