mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (F.map f₀₂) (F.map f₂₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom h =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) h)))
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_empty_right : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (s : Finset α), s.mulEnergy ∅ = 0
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.probReal_univ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ],
  μ.real Set.univ = 1
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : CategoryTheory.Category.{t, w} J}
  {X : C} {diag : CategoryTheory.Functor J C} {π : (CategoryTheory.Functor.const J).obj X ⟶ diag}
  {isLimit : CategoryTheory.Limits.IsLimit { pt := X, π := π }} {diag_1 : CategoryTheory.Functor J C}
  {π_1 : (CategoryTheory.Functor.const J).obj X ⟶ diag_1}
  {isLimit_1 : CategoryTheory.Limits.IsLimit { pt := X, π := π_1 }},
  { diag := diag, π := π, isLimit := isLimit } = { diag := diag_1, π := π_1, isLimit := isLimit_1 } →
    diag = diag_1 ∧ π ≍ π_1 ∧ isLimit ≍ isLimit_1
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.isDenseInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → IsDenseInducing e
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_pair : ∀ {α : Type u} {x y : α}, x ≠ y → {x, y}.Nontrivial
-- Aesop.Rule
Aesop.UnsafeRuleInfo : Type
-- Mathlib.Algebra.Group.Hom.Defs
/-- If the codomain of an injective additive monoid homomorphism is torsion free,
then so is the domain.  -/
Function.Injective.isAddTorsionFree : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] [IsAddTorsionFree N] (f : M →+ N),
  Function.Injective ⇑f → IsAddTorsionFree M
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The orbit corresponding to an element of the quotient by `AddAction.orbitRel`  -/
AddAction.orbitRel.Quotient.orbit : {G : Type u_1} →
  {α : Type u_2} → [inst : AddGroup G] → [inst_1 : AddAction G α] → AddAction.orbitRel.Quotient G α → Set α
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
product. Both factors are truncated at the same level `n`.  -/
MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (f g : MvPowerSeries σ R)
  {m : σ →₀ ℕ},
  m ≤ n →
    MvPolynomial.coeff m ((MvPowerSeries.trunc' R n) f * (MvPowerSeries.trunc' R n) g) = (MvPowerSeries.coeff m) (f * g)
-- Mathlib.Analysis.InnerProductSpace.OfNorm
/-- **Fréchet–von Neumann–Jordan Theorem**. A normed space `E` whose norm satisfies the
parallelogram identity can be given a compatible inner product.  -/
InnerProductSpace.ofNorm : (𝕜 : Type u_1) →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          (∀ (x y : E), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) → InnerProductSpace 𝕜 E
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Γevaluation_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (Y.Γevaluation (f x)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop f) (X.Γevaluation x)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects finite limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite colimits.  -/
CategoryTheory.Limits.reflectsFiniteColimits_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteLimits F.unop],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.refl_symm : ∀ {M : Type u_4} [inst : Mul M], (MulEquiv.refl M).symm = MulEquiv.refl M
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Evaluation of continuous maps at a point, bundled as an algebra homomorphism.  -/
ContinuousMap.evalAlgHom : {X : Type u_1} →
  (S : Type u_2) →
    (R : Type u_3) →
      [inst : TopologicalSpace X] →
        [inst_1 : CommSemiring S] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Algebra S R] →
              [inst_4 : TopologicalSpace R] → [inst_5 : IsTopologicalSemiring R] → X → C(X, R) →ₐ[S] R
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ext : {γ : Type} → Lean.KeyedDeclsAttribute γ → Lean.KeyedDeclsAttribute.Extension γ
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unopMap_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.unopMap φ).τ₂ = φ.τ₂.unop
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_adjoin_of_mem : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E} {s : E},
  s ∈ S → s ∈ IntermediateField.adjoin F S
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.ofSubtype.match_1.splitter : (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) → (p : α.Arrow (TypeVec.repeat n Prop)) → (x : Fin2 n) → TypeVec.Subtype_ p x → Sort u_2) →
  (n : ℕ) →
    (α : TypeVec.{u_1} n) →
      (p : α.Arrow (TypeVec.repeat n Prop)) →
        (x : Fin2 n) →
          (x_1 : TypeVec.Subtype_ p x) →
            ((n : ℕ) →
                (α : TypeVec.{u_1} (n + 1)) →
                  (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) →
                    (i : Fin2 n) → (x : TypeVec.Subtype_ p i.fs) → motive (n + 1) α p i.fs x) →
              ((n : ℕ) →
                  (α : TypeVec.{u_1} (n + 1)) →
                    (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) →
                      (x : TypeVec.Subtype_ p Fin2.fz) → motive (n + 1) α p Fin2.fz x) →
                motive n α p x x_1
-- Mathlib.Algebra.BigOperators.WithTop
WithTop.prod_eq_top_ex_top : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀}, ∏ j ∈ s, f j = ⊤ → ∃ i ∈ s, f i = ⊤
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_symm_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ),
  (CategoryTheory.uliftYonedaEquiv.symm x).app Y =
    TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map y.down.op)) x
-- Std.Http.Data.URI.Basic
Std.Http.URI.Query.instSingletonProdString : Singleton (String × String) Std.Http.URI.Query
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.State.mk.sizeOf_spec : ∀ (status : Std.HashMap String ℕ) (progress : Bool) (solvedSuggestions : Array ProofWidgets.Html),
  sizeOf { status := status, progress := progress, solvedSuggestions := solvedSuggestions } =
    1 + sizeOf status + sizeOf progress + sizeOf solvedSuggestions
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.gate.injEq : ∀ {α : Type} (a : Std.Tactic.BVDecide.Gate) (a_1 a_2 : Std.Tactic.BVDecide.BoolExpr α) (a_3 : Std.Tactic.BVDecide.Gate)
  (a_4 a_5 : Std.Tactic.BVDecide.BoolExpr α),
  (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2 = Std.Tactic.BVDecide.BoolExpr.gate a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Order.BooleanAlgebra.Set
/-- See also `Set.sdiff_inter_right_comm`.  -/
Set.inter_sdiff_assoc : ∀ {α : Type u_1} (a b c : Set α), (a ∩ b) \ c = a ∩ (b \ c)
-- Std.Data.HashMap.Lemmas
Std.HashMap.unitOfList_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α},
  (Std.HashMap.unitOfList l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instFinite : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α], Std.Iterators.Finite (Std.Rxo.Iterator α) Id
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderivWithin_eq_of_mem : ∀ {𝕜 : 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] {f f₁ : E → F} {x : E} {s : Set E},
  f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_union : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] (s t : Set M),
  ProperCone.dual p (s ∪ t) = ProperCone.dual p s ⊓ ProperCone.dual p t
-- Mathlib.Data.Int.Bitwise
Int.lnot.eq_1 : ∀ (n : ℕ), (Int.ofNat n).lnot = Int.negSucc n
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_1.splitter : {σ : Type u_1} →
  (motive : σ × Bool → Sort u_2) →
    (x : σ × Bool) → ((fst : σ) → (checkSuccess : Bool) → motive (fst, checkSuccess)) → motive x
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.support_eq_symm_image : ∀ {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] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E],
  Function.support ↑f = ↑(extChartAt I c).symm '' (Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?_some : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {x : α} {v : β} [Std.TransCmp cmp] {t : RBTree.RBMap α β cmp},
  t.find? x = some v ↔ ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq
-- Mathlib.Data.Set.Defs
/-- We introduce `≤` before `⊆` to help the unifier when applying lattice theorems
to subset hypotheses.  -/
Set.instLE : {α : Type u} → LE (Set α)
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.coe_toComplL : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformContinuousConstSMul 𝕜 E], ⇑UniformSpace.Completion.toComplL = UniformSpace.Completion.coe'
-- Init.Data.String.Basic
List.isUTF8FirstByte_getElem_utf8Encode_singleton : ∀ {c : Char} {i : ℕ} {hi : i < [c].utf8Encode.size}, [c].utf8Encode[i].IsUTF8FirstByte ↔ i = 0
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- When `Φ : LocalizerMorphism W₁ W₂`, if the composition `Φ.functor ⋙ L₂` is a
localization functor for `W₁`, then `Φ` is a localized equivalence.  -/
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  [(Φ.functor.comp L₂).IsLocalization W₁], Φ.IsLocalizedEquivalence
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∏ᶜ I.left ⟶ ∏ᶜ I.right` via `I.fst`.  -/
CategoryTheory.Limits.MulticospanIndex.fstPiMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasProduct I.left] →
          [inst_2 : CategoryTheory.Limits.HasProduct I.right] → ∏ᶜ I.left ⟶ ∏ᶜ I.right
-- Mathlib.Algebra.Group.Defs
zpow_neg_coe_of_pos : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G) {n : ℕ}, 0 < n → a ^ (-↑n) = (a ^ n)⁻¹
-- Mathlib.Order.Filter.Basic
Filter.eventuallyLE_antisymm_iff : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.le_iff : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G₁ G₂ : StructureGroupoid H}, G₁ ≤ G₂ ↔ ∀ e ∈ G₁, e ∈ G₂
-- Mathlib.RepresentationTheory.Invariants
/-- Given a normal subgroup S ≤ G, this is the functor sending a `G`-representation `A` to the
`G ⧸ S`-representation it induces on `A^S`.  -/
Rep.quotientToInvariantsFunctor : (k : Type u) →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) → [inst_2 : S.Normal] → CategoryTheory.Functor (Rep.{w, u, v} k G) (Rep.{w, u, v} k (G ⧸ S))
-- Init.GetElem
Fin.instLawfulGetElemValOfNat : ∀ {cont : Type u_1} {elem : Type u_2} {dom : cont → ℕ → Prop} {n : ℕ} [inst : GetElem? cont ℕ elem dom]
  [h : LawfulGetElem cont ℕ elem dom], LawfulGetElem cont (Fin n) elem fun xs i => dom xs ↑i
-- Lean.Parser.Syntax
/-- Declares a binder predicate.  For example:
```
binder_predicate x " > " y:term => `($x > $y)
```
 -/
Lean.Parser.Command.binderPredicate : Lean.Parser.Parser
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
dreduceDIte : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.Rayleigh
beattySeq.eq_1 : ∀ (r : ℝ) (k : ℤ), beattySeq r k = ⌊↑k * r⌋
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ},
  t.WF → ((Std.TreeMap.Raw.filterMap f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), (f (t.getKey k h) t[k]).isSome = true)
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.objectField : Lean.Json.CompressWorkItemKind✝
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.inf_le : ∀ {R : Type u} [inst : CommSemiring R] {I J P : Ideal R}, P.IsPrime → (I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet_iff_iCondIndepSets_singleton : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s : ι → Set Ω),
  (∀ (i : ι), MeasurableSet (s i)) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepSet m' hm' s μ ↔ ProbabilityTheory.iCondIndepSets m' hm' (fun i => {s i}) μ
-- Mathlib.Order.Filter.Extr
Filter.EventuallyEq.isMaxFilter_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  f =ᶠ[l] g → f a = g a → (IsMaxFilter f l a ↔ IsMaxFilter g l a)
-- Mathlib.Algebra.Group.Defs
/-- Zero is a left neutral element for addition  -/
AddZeroClass.zero_add : ∀ {M : Type u} [self : AddZeroClass M] (a : M), 0 + a = a
-- Mathlib.Data.Set.Operations
/-- `g` is an inverse to `f` viewed as a map from `s` to `t`  -/
Set.InvOn : {α : Type u} → {β : Type v} → (β → α) → (α → β) → Set α → Set β → Prop
-- Mathlib.Data.List.Perm.Basic
List.map_perm_map_iff : ∀ {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → β},
  Function.Injective f → ((List.map f l).Perm (List.map f l') ↔ l.Perm l')
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- The product of cycle factors is equal to the original `f : perm α`.  -/
Equiv.Perm.cycleFactorsFinset_noncommProd : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α)
  (comm : optParam ((↑f.cycleFactorsFinset).Pairwise Commute) ⋯), f.cycleFactorsFinset.noncommProd id comm = f
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.of_isIso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ]
  [CategoryTheory.IsIso φ], p.IsStronglyCartesian f φ
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIcc_eq_map_Icc_nat : (SummationFilter.symmetricIcc ℤ).filter = Filter.map (fun N => Finset.Icc (-↑N) ↑N) Filter.atTop
-- Mathlib.Data.Int.Fib.Basic
Int.fib_two_mul_add_one_eq_natFib_natAbs : ∀ {n : ℤ}, Int.fib (2 * n + 1) = ↑(Nat.fib (2 * n + 1).natAbs)
-- Std.Http.Data.Method
Std.Http.Method.delete.sizeOf_spec : sizeOf Std.Http.Method.delete = 1
-- Mathlib.RingTheory.KrullDimension.Regular
/-- If `M` is a finite module over a Noetherian local ring `R`, `r₁, …, rₙ` is an
`M`-sequence, then `dim M/(r₁, …, rₙ)M + n = dim M`.  -/
Module.supportDim_add_length_eq_supportDim_of_isRegular : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] [IsLocalRing R] (rs : List R),
  RingTheory.Sequence.IsRegular M rs →
    Module.supportDim R (M ⧸ Ideal.ofList rs • ⊤) + ↑rs.length = Module.supportDim R M
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.mul_param : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
  Asymptotics.SuperpolynomialDecay l k f → Asymptotics.SuperpolynomialDecay l k (f * k)
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toListRev`.
 -/
Std.Iter.Total.toListRev : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.Iterators.Finite α Id] → Std.Iter.Total β → List β
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.mk : Array Lean.Elab.Command.InductiveView →
  Array Lean.Elab.Command.InductiveElabStep2 →
    Array Lean.Expr →
      Array Lean.Expr →
        List Lean.Name →
          ℕ →
            ℕ →
              List Lean.InductiveType →
                Bool →
                  Array Lean.Elab.Command.ElabHeaderResult →
                    Array Lean.Expr → Bool → Lean.Elab.Command.AddAndFinalizeContext✝
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.continuous : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  Continuous ⇑f
-- Init.Data.UInt.Bitwise
UInt16.and_not_self : ∀ {a : UInt16}, a &&& ~~~a = 0
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.lineDifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s : Set E} {x v : E}, LineDifferentiableWithinAt 𝕜 f s x v → s ∈ nhds x → LineDifferentiableAt 𝕜 f x v
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.bucket.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (self self_1 : Array (Std.DHashMap.Internal.AssocList α β))
  (e_self : self = self_1) (h : 0 < self.size) (k k_1 : α),
  k = k_1 → Std.DHashMap.Internal.bucket self h k = Std.DHashMap.Internal.bucket self_1 ⋯ k_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_insert_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → insert a (Set.Ioo a b) = Set.Ico a b
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.associated_sec_fst : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [inst_3 : IsLocalization.Away x S] (s : S), Associated ((algebraMap R S) (IsLocalization.Away.sec x s).1) s
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `g` does not vanish in the interior of the ball.  -/
Complex.CanonicalDecomp.ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.CanonicalDecomp f g R → ∀ u ∈ Metric.ball 0 R, g u ≠ 0
-- Lean.SubExpr
/-- One of the hypotheses.  -/
Lean.SubExpr.GoalLocation.hyp : Lean.FVarId → Lean.SubExpr.GoalLocation
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instPreservesZeroMorphismsOpcyclesFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomologicalComplex.opcyclesFunctor C c i).PreservesZeroMorphisms
-- Init.Data.String.PosRaw
String.Pos.Raw.addString_eq : ∀ (p : String.Pos.Raw) (s : String), p + s = { byteIdx := p.byteIdx + s.utf8ByteSize }
-- Mathlib.RepresentationTheory.Equiv
Representation.Equiv.mk.congr_simp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (e e_1 : V ≃ₗ[A] W) (e_e : e = e_1)
  (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e), Representation.Equiv.mk e he = Representation.Equiv.mk e_1 ⋯
-- Lean.Meta.Tactic.Grind.EMatch
/-- Assigns `bidx` with the marker for a delayed equality proof for generalized patterns.
The proof is assigned after we have the complete assignment.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignDelayedEqProof? : Lean.Meta.Grind.EMatch.Choice → ℕ → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mono' : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] {m : MeasurableSpace Ω} (self : MeasureTheory.Filtration ι m),
  Monotone ↑self
-- Mathlib.Logic.Function.Basic
Function.update_apply_of_injective : ∀ {α : Sort u} {β : α → Sort v} {α' : Sort w} [inst : DecidableEq α] [inst_1 : DecidableEq α'] (g : (a : α) → β a)
  {f : α' → α},
  Function.Injective f →
    ∀ (i : α') (a : β (f i)) (j : α'), Function.update g (f i) a (f j) = Function.update (fun i => g (f i)) i a j
-- Mathlib.Analysis.Complex.Order
Complex.real_lt_real : ∀ {x y : ℝ}, ↑x < ↑y ↔ x < y