mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Result
/-- Represent an integer as a "raw" typed expression.

This `.lit (.natVal n)` internally to represent a natural number,
rather than the preferred `OfNat.ofNat` form.
We use this internally to avoid unnecessary typeclass searches.
 -/
Mathlib.Meta.NormNum.mkRawRatLit : ℚ → Q(ℚ)
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.ProjectiveResolution X} {X' : C} {R' : CategoryTheory.ProjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f),
  CategoryTheory.CategoryStruct.comp φ.hom' R'.π' =
    CategoryTheory.CategoryStruct.comp R.π' ((CochainComplex.singleFunctor C 0).map f)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.liftOrderHom_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : { a // a ≠ 1 } → α)
  (h : ∀ (a b : { a // a ≠ 1 }), FiniteMulArchimedeanClass.mk ↑a ⋯ ≤ FiniteMulArchimedeanClass.mk ↑b ⋯ → f a ≤ f b)
  {a : M} (ha : a ≠ 1), (FiniteMulArchimedeanClass.liftOrderHom f h) (FiniteMulArchimedeanClass.mk a ha) = f ⟨a, ha⟩
-- Mathlib.Topology.Constructions
ContinuousAt.restrictPreimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y}
  {x : ↑(f ⁻¹' s)}, ContinuousAt f ↑x → ContinuousAt (s.restrictPreimage f) x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeComp : ∀ {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] (J : Type w)
  [inst_3 : LinearOrder J] (G₁ : CategoryTheory.Functor C D) (G₂ : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G₁]
  [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G₂],
  CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J (G₁.comp G₂)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Reinterpret an ordered additive monoid homomorphism as an order homomorphism.  -/
OrderAddMonoidHom.toOrderHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : AddZeroClass α] → [inst_3 : AddZeroClass β] → (α →+o β) → α →o β
-- Init.Data.UInt.Lemmas
USize.sub_left_inj : ∀ {a b : USize} (c : USize), a - c = b - c ↔ a = b
-- Batteries.Data.List.Lemmas
List.nodup_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, (List.findIdxs p xs s).Nodup
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving_id : ∀ {E : Type u_4} {p : ENNReal} [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β]
  {μb : MeasureTheory.Measure β},
  MeasureTheory.Lp.compMeasurePreserving id ⋯ = AddMonoidHom.id ↥(MeasureTheory.Lp E p μb)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rcc_eq_some : ∀ {m n i : ℕ}, i < n + 1 - m → (m...=n).toList[i]? = some (m + i)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        Z)
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_add : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : Add β],
  MeasureTheory.stoppedValue (u + v) τ = MeasureTheory.stoppedValue u τ + MeasureTheory.stoppedValue v τ
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi'_eq_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [inst_2 : Encodable ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.Measure.pi' μ = MeasureTheory.Measure.pi μ
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `N` is a normal subgroup of `G` and `IsGaloisGroup N B C`, then the quotient group `G ⧸ N`
acts on `B` by `(g : G ⧸ N) • x = g • x`.  -/
IsGaloisGroup.mulSemiringActionQuotient : (G : Type u_1) →
  [inst : Group G] →
    (B : Type u_3) →
      (C : Type u_4) →
        [inst_1 : Semiring C] →
          [inst_2 : MulSemiringAction G C] →
            (N : Subgroup G) →
              [inst_3 : CommSemiring B] →
                [inst_4 : Algebra B C] →
                  [FaithfulSMul B C] → [IsGaloisGroup (↥N) B C] → [inst_7 : N.Normal] → MulSemiringAction (G ⧸ N) B
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (toPrecoverage : CategoryTheory.Precoverage C)
  (pullback :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ toPrecoverage.coverings X, ∃ T ∈ toPrecoverage.coverings Y, T.FactorsThruAlong S f)
  (toPrecoverage_1 : CategoryTheory.Precoverage C)
  (pullback_1 :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage_1.coverings X, ∃ T ∈ toPrecoverage_1.coverings Y, T.FactorsThruAlong S f),
  ({ toPrecoverage := toPrecoverage, pullback := pullback } =
      { toPrecoverage := toPrecoverage_1, pullback := pullback_1 }) =
    (toPrecoverage = toPrecoverage_1)
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.below.compl : ∀ {α : Type u_3} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop}
  {a : Set α} (a_1 : MeasurableSpace.DynkinSystem.GenerateHas s a),
  MeasurableSpace.DynkinSystem.GenerateHas.below a_1 → motive a a_1 → MeasurableSpace.DynkinSystem.GenerateHas.below ⋯
-- Lean.Message
Lean.instFromJsonSerialMessage : Lean.FromJson Lean.SerialMessage
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctor_obj_map : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C)
  {X_1 Y : J₁ × J₂} (f : X_1 ⟶ Y),
  ((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₂ C).obj X).map f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.1.map f.1) (X.2.obj X_1.2))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.1.obj Y.1) (X.2.map f.2))
-- Init.Data.Vector.Lemmas
Vector.findRev?_toArray : ∀ {α : Type} {n : ℕ} {p : α → Bool} {xs : Vector α n}, Array.findRev? p xs.toArray = Vector.findRev? p xs
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.ext_iff : ∀ {V : Type u_1} {x y : Digraph V}, x = y ↔ x.Adj = y.Adj
-- Mathlib.Analysis.Convex.Hull
convexHull_nonempty_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, ((convexHull 𝕜) s).Nonempty ↔ s.Nonempty
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forget_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.ReflQuiv.forget.map F = F.toFunctor.toReflPrefunctor
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.norm_mem_spanNorm : ∀ (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] [Module.Free R S] {I : Ideal S}, ∀ x ∈ I, (Algebra.norm R) x ∈ Ideal.spanNorm R I
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ext_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : AddMonoidAlgebra R M}, x = y ↔ x.coeff = y.coeff
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellation : Type
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulRight_one` for matrix multiplication.  -/
mulRightLinearMap_one : ∀ {l : Type u_1} {m : Type u_2} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : Semiring R] [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A],
  mulRightLinearMap l R 1 = LinearMap.id
-- Lean.Compiler.LCNF.Basic
/-- Return `true` if the arrow type contains an instance implicit argument.
 -/
Lean.Compiler.LCNF.hasLocalInst : Lean.Expr → Lean.CoreM Bool
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.union_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} {Y : C} (f : Y ⟶ X),
  (R ⊔ S).arrows f ↔ R.arrows f ∨ S.arrows f
-- Mathlib.Order.WithBot
WithBot.forall_ne_bot : ∀ {α : Type u_1} {p : WithBot α → Prop}, (∀ (x : WithBot α), x ≠ ⊥ → p x) ↔ ∀ (x : α), p ↑x
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyHomInvId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.HomotopyEquiv.refl S).homotopyHomInvId = CategoryTheory.ShortComplex.Homotopy.ofEq ⋯
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.PromiseCheckedResult.checkedEnvPromise : Lean.Environment.PromiseCheckedResult → IO.Promise Lean.Kernel.Environment
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.negMap_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.negMap ⟦P⟧ = ⟦W'.neg P⟧
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} [inst_7 : One F], fderivWithin 𝕜 1 s = 0
-- Std.Data.ExtHashMap.Lemmas
/-- Variant of `getElem?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtHashMap.getElem?_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α},
  (Std.ExtHashMap.map f m)[k]? = Option.pmap (fun v h' => f (m.getKey k h') v) m[k]? ⋯
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- The absolute norm of the ideal `I : Ideal R` is the cardinality of the quotient `R ⧸ I`.  -/
Ideal.absNorm : {S : Type u_1} → [inst : CommRing S] → [IsDedekindDomain S] → [Module.Free ℤ S] → Ideal S →*₀ ℕ
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsupp.disjoint_nhdsWithin_cofinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : Zero Y] (f : Function.locallyFinsupp X Y) (p : X),
  Disjoint (nhdsWithin p (Function.locallyFinsuppWithin.support f)) Filter.cofinite
-- Init.Data.List.Nat.Basic
List.append_eq_append_iff_of_size_eq_right : ∀ {α : Type u_1} {ws xs ys zs : List α}, ys.length = zs.length → (ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs)
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_true_of_and_eq_true_right : ∀ {a b : Bool}, (a && b) = true → b = true
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Returns true if the given predicate is true for all items in the RBSet.  -/
RBTree.RBSet.all : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Bool) → Bool
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toCompleteLattice : {α : Type u} → [self : CompletelyDistribLattice α] → CompleteLattice α
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.zero_mul : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [ContinuousMul M] {f : ℕ → M},
  HasProd (fun n => f (n + 1)) m → HasProd f (f 0 * m)
-- Init.Data.Nat.Coprime
Nat.coprime_one_right : ∀ (n : ℕ), n.Coprime 1
-- Mathlib.RingTheory.Int.Basic
/-- If `gcd a (m * n) ≠ 1`, then `gcd a m ≠ 1` or `gcd a n ≠ 1`.  -/
Int.gcd_ne_one_iff_gcd_mul_right_ne_one : ∀ {a : ℤ} {m n : ℕ}, a.gcd (↑m * ↑n) ≠ 1 ↔ a.gcd ↑m ≠ 1 ∨ a.gcd ↑n ≠ 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : SizeOf C] (carrier : TopCat)
  (presheaf : TopCat.Presheaf C carrier),
  sizeOf { carrier := carrier, presheaf := presheaf } = 1 + sizeOf carrier + sizeOf presheaf
-- Mathlib.Order.GaloisConnection.Basic
isLUB_image2_of_isGLB_isLUB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) → IsGLB s a₀ → IsLUB t b₀ → IsLUB (Set.image2 l s t) (l a₀ b₀)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.nextCoeff_multiset_prod : ∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R),
  (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of the range of a surjective homomorphism from a
nilpotent group is less or equal the nilpotency class of the domain.  -/
Group.nilpotencyClass_le_of_surjective : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] (f : G →* G'),
  Function.Surjective ⇑f → ∀ [h : Group.IsNilpotent G], Group.nilpotencyClass G' ≤ Group.nilpotencyClass G
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
SchwartzMap.coeFn_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.smul_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ), c • Metric.ball x r = Metric.ball (c • x) r
-- Mathlib.Analysis.RCLike.Basic
RCLike.ext : ∀ {K : Type u_1} [inst : RCLike K] {z w : K}, RCLike.re z = RCLike.re w → RCLike.im z = RCLike.im w → z = w
-- Mathlib.Algebra.Star.Pi
Pi.instStarAddMonoidForall : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → AddMonoid (f i)] → [(i : I) → StarAddMonoid (f i)] → StarAddMonoid ((i : I) → f i)
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- A set of points `s` satisfying both `ρ a ≤ c * μ a` and `ρ a ≥ d * μ a` at arbitrarily small
sets in a Vitali family has measure `0` if `c < d`. Indeed, the first inequality should imply
that `ρ s ≤ c * μ s`, and the second one that `ρ s ≥ d * μ s`, a contradiction if `0 < μ s`.  -/
VitaliFamily.null_of_frequently_le_of_frequently_ge : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ →
    ∀ {c d : NNReal},
      c < d →
        ∀ (s : Set α),
          (∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a) →
            (∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a) → μ s = 0
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRank_restrict : ∀ {α : Type u} (M : Matroid α) (X : Set α), (M.restrict X).cRank = M.cRk X
-- Init.Core
EStateM.Result.ok.injEq : ∀ {ε σ α : Type u} (a : α) (a_1 : σ) (a_2 : α) (a_3 : σ),
  (EStateM.Result.ok a a_1 = EStateM.Result.ok a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.Nat.Lemmas
Nat.pos_of_lt_mul_left : ∀ {a b c : ℕ}, a < b * c → 0 < c
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsLocalExtr.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {f : E → ℝ} {a : E}, IsLocalExtr f a → lineDeriv ℝ f a = 0
-- Mathlib.Algebra.Order.Ring.Defs
/-- Turn an ordered domain into a strict ordered ring.  -/
IsOrderedRing.toIsStrictOrderedRing : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Nontrivial R],
  IsStrictOrderedRing R
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.inv.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Group (G i)] (x : ι) (x_4 : G x) (h : x_4 ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x_4 h).inv = Monoid.CoprodI.NeWord.singleton x_4⁻¹ ⋯
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_congr : ∀ {𝕜 : 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 : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  Set.EqOn ω₁ ω₂ s → ω₁ x = ω₂ x → extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_projected_entry' : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {entry : Std.Sat.AIG.Entrypoint α},
  ⟦assign, { aig := entry.aig, ref := { gate := entry.ref.gate, invert := entry.ref.invert, hgate := ⋯ } }⟧ =
    ⟦assign, entry⟧
-- Mathlib.Data.Set.Prod
Set.diagonal.eq_1 : ∀ (α : Type u_1), Set.diagonal α = {p | p.1 = p.2}
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.mvar : Lean.Meta.SynthInstance.ConsumerNode → Lean.Expr
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.instDiscreteTopologyCarrierObjDiscrete : ∀ {X : Type u}, DiscreteTopology ↑(TopCat.discrete.obj X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (P : W'.Point), (-P).xRep = P.xRep
-- Init.Data.SInt.Lemmas
ISize.maxValue.eq_1 : ISize.maxValue = ISize.ofInt (2 ^ (System.Platform.numBits - 1) - 1)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_zero_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (f : α → ENNReal), MeasureTheory.Measure.withDensity 0 f = 0
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.homOfLe.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  {G G' : CategoryTheory.Subfunctor F} (h : G ≤ G'),
  CategoryTheory.Subfunctor.homOfLe h = CategoryTheory.Subfunctor.homOfLe h
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.ofBijectiveAlgebraMap_dimension : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (h : Function.Bijective ⇑(algebraMap R S)), (Algebra.Presentation.ofBijectiveAlgebraMap h).dimension = 0
-- Mathlib.Data.Set.Card
/-- A version of the pigeonhole principle for `Set`s rather than `Finset`s.

See also `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` and
`Set.exists_ne_map_eq_of_encard_lt_of_maps_to`.  -/
Set.exists_ne_map_eq_of_ncard_lt_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β},
  t.ncard < s.ncard →
    ∀ {f : α → β},
      (∀ a ∈ s, f a ∈ t) →
        autoParam t.Finite Set.exists_ne_map_eq_of_ncard_lt_of_maps_to._auto_1 → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_sub_same : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → AddGroup (α j)] (i : Fin (n + 1)) (x y : α i)
  (p : (j : Fin n) → α (i.succAbove j)), i.insertNth x p - i.insertNth y p = Pi.single i (x - y)
-- Lean.Elab.Do.Legacy
/-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`.  -/
Lean.Elab.Term.Do.Code.ite : Lean.Syntax →
  Option Lean.Elab.Term.Do.Var →
    Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.forget_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.forget F).obj t = t.pt
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g)
  (M : CategoryTheory.Sheaf (J.over Y) A) (X_1 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackCongr A h).inv.app M).hom.app X_1 =
    M.obj.map ((CategoryTheory.Over.mapCongr f g h).hom.app (Opposite.unop X_1)).op
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_addX : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x₁ x₂ ℓ : R), (W'.map f).addX (f x₁) (f x₂) (f ℓ) = f (W'.addX x₁ x₂ ℓ)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsCardinalLocallyPresentable.toHasCardinalFilteredGenerator : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {κ : Cardinal.{w}} {inst_1 : Fact κ.IsRegular}
  [self : CategoryTheory.IsCardinalLocallyPresentable C κ], CategoryTheory.HasCardinalFilteredGenerator C κ
-- Mathlib.Analysis.Calculus.FDeriv.Pow
HasFDerivAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E}, HasFDerivAt f f' x → ∀ (n : ℕ), HasFDerivAt (fun x => f x ^ n) ((n • f x ^ (n - 1)) • f') x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIsLeftCancelAdd : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Add M] [IsLeftCancelAdd M], IsLeftCancelAdd (l.Germ M)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toBoundedContinuousFunctionCLM_apply : ∀ (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E),
  ((SchwartzMap.toBoundedContinuousFunctionCLM 𝕜 E F) f) x = f x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffOn.mul : ∀ {𝕜 : 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 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H 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]
  [ContMDiffMul I n G] {f g : M → G} {s : Set M},
  ContMDiffOn I' I n f s → ContMDiffOn I' I n g s → ContMDiffOn I' I n (f * g) s
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- The class of fibrations in a category with fibrations.  -/
HomotopicalAlgebra.fibrations : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] → CategoryTheory.MorphismProperty C