mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Constructions
/-- Definition of `Pullback.TotalSpace.topologicalSpace`, which we make irreducible.  -/
pullbackTopology : {B : Type u_1} →
  (F : Type u_2) →
    (E : B → Type u_3) →
      {B' : Type u_4} →
        (f : B' → B) →
          [TopologicalSpace B'] →
            [TopologicalSpace (Bundle.TotalSpace F E)] → TopologicalSpace (Bundle.TotalSpace F (f *ᵖ E))
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_comp_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) (n : SimplexCategoryᵒᵖ),
  CategoryTheory.CategoryStruct.comp (ed.section_.app n) (X.hom.app n) = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_rotateL : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.rotateL x r).dual = r.dual.rotateR x l.dual
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Hom.ofLE.congr_simp : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂), SimpleGraph.Hom.ofLE h = SimpleGraph.Hom.ofLE h
-- Mathlib.CategoryTheory.Limits.Bicones
/-- Given a diagram `F : J ⥤ C` and two `Cone F`s, we can join them into a diagram `Bicone J ⥤ C`.
 -/
CategoryTheory.biconeMk : (J : Type v₁) →
  [inst : CategoryTheory.SmallCategory J] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        {F : CategoryTheory.Functor J C} →
          CategoryTheory.Limits.Cone F →
            CategoryTheory.Limits.Cone F → CategoryTheory.Functor (CategoryTheory.Bicone J) C
-- Mathlib.Analysis.Convex.Caratheodory
Caratheodory.minCardFinsetOfMemConvexHull_nonempty : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E} (hx : x ∈ (convexHull 𝕜) s),
  (Caratheodory.minCardFinsetOfMemConvexHull hx).Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Some image factorisation of `f` through a monomorphism (selected with choice).  -/
CategoryTheory.Limits.Image.imageFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasImage f] → CategoryTheory.Limits.ImageFactorisation f
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_isIdempotentElem_iff : ∀ {R : Type u_1} [inst : Semiring R] {e : R}, IsIdempotentElem (LinearMap.toSpanSingleton R R e) ↔ IsIdempotentElem e
-- Init.Data.List.Scan.Lemmas
List.scanr_eq_scanl_reverse : ∀ {α : Type u_1} {β : Type u_2} {init : β} {as : List α} {f : α → β → β},
  List.scanr f init as = (List.scanl (flip f) init as.reverse).reverse
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- **Alias** of the reverse direction of `WithZero.map'_surjective_iff`. -/
WithZero.map'_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α →* β},
  Function.Surjective ⇑f → Function.Surjective ⇑(WithZero.map' f)
-- Mathlib.Algebra.Group.ULift
ULift.rightCancelMonoid.eq_1 : ∀ {α : Type u} [inst : RightCancelMonoid α],
  ULift.rightCancelMonoid = Function.Injective.rightCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_univ_three : ∀ (a b c : ℕ),
  Nat.multinomial Finset.univ ![a, b, c] = (a + b + c).factorial / (a.factorial * b.factorial * c.factorial)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommAddMonObj.add_comm' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M],
  CategoryTheory.CategoryStruct.comp (β_ M M).inv CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add
-- Mathlib.Order.Sublattice
/-- A sublattice of a lattice inherits a lattice structure.  -/
Sublattice.instLatticeCoe : {α : Type u_2} → [inst : Lattice α] → (L : Sublattice α) → Lattice ↥L
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.homAddEquiv_apply : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (f : M.Hom N), SemimoduleCat.homAddEquiv f = f.hom
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.nsmul_zero : ∀ {M : Type u} [inst : Lean.Grind.NatModule M] (n : ℕ), n • 0 = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.DerivedLitsInvariant.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (fassignments_size : f.assignments.size = n)
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n)
  (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  f.DerivedLitsInvariant fassignments_size assignments assignments_size derivedLits =
    ∀ (i : Fin n),
      have i_lt_assignments_size := ⋯;
      have i_lt_f_assignments_size := ⋯;
      have assignments_i := assignments[↑i];
      have fassignments_i := f.assignments[↑i];
      (assignments_i = fassignments_i ∧ ∀ l ∈ derivedLits, ↑l.1 ≠ ↑i) ∨
        (∃ j,
            ↑(List.get derivedLits j).1 = ↑i ∧
              assignments_i =
                  Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment (List.get derivedLits j).2 fassignments_i ∧
                ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment (List.get derivedLits j).2 fassignments_i =
                      true ∧
                  ∀ (k : Fin (List.length derivedLits)), k ≠ j → ↑(List.get derivedLits k).1 ≠ ↑i) ∨
          ∃ j1 j2,
            ↑(List.get derivedLits j1).1 = ↑i ∧
              ↑(List.get derivedLits j2).1 = ↑i ∧
                (List.get derivedLits j1).2 = true ∧
                  (List.get derivedLits j2).2 = false ∧
                    assignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both ∧
                      fassignments_i = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned ∧
                        ∀ (k : Fin (List.length derivedLits)), k ≠ j1 → k ≠ j2 → ↑(List.get derivedLits k).1 ≠ ↑i
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y),
  (CategoryTheory.Limits.BinaryFan.map F s).snd = F.map s.snd
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.iSupLift_inclusion : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] {ι : Type u_1}
  [inst_7 : StarRing R] [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K}
  {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)}
  {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (h : K i ≤ T),
  (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalStarSubalgebra.inclusion h) x) = (f i) x
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.polarCoord_target : Complex.polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
-- Init.Data.String.PosRaw
/-- Returns either `p₁` or `p₂`, whichever has the least byte index.
 -/
String.Pos.Raw.min : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.instIsTopologicalAddGroupOfContinuousAdd : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α], IsTopologicalAddGroup (AddUnits α)
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.trailingTable : Lean.Parser.PrattParsingTables → Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceTextDocumentEdit : Lean.Lsp.FileSource Lean.Lsp.TextDocumentEdit
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBoundP?_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBTree.RBSet α cmp},
  t.lowerBoundP? cut = some x → x ∈ t
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.foldl.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {δ : Type w} (f : δ → (a : α) → β a → δ) (init : δ)
  (t : Std.DTreeMap.Raw α β cmp), Std.DTreeMap.Raw.foldl f init t = Std.DTreeMap.Internal.Impl.foldl f init t.inner
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.sup : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α},
  f.TotallyBounded → g.TotallyBounded → (f ⊔ g).TotallyBounded
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.homMk_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃),
  (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₂ = τ₂
-- Lean.Expr
_private.Lean.Expr.0.Lean.patternRefAnnotationKey : Lean.Name
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsSFiniteKernel.tsum_finite : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [self : ProbabilityTheory.IsSFiniteKernel κ],
  ∃ κs, (∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κs n)) ∧ κ = ProbabilityTheory.Kernel.sum κs
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.compl_neighborSet_disjoint : ∀ {V : Type u} (G : SimpleGraph V) (v : V), Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.atIdxSlow?_zero_repeat : ∀ {α : Type w} {f : α → α} {init : α}, Std.Iter.atIdxSlow? 0 (Std.Iter.repeat f init) = some init
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (p : PowerSeries R) (n d : ℕ),
  (PowerSeries.coeff (d + n)) (p * PowerSeries.X ^ n) = (PowerSeries.coeff d) p
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the top, bottom, suprema, and infima along a Galois coinsertion  -/
GaloisCoinsertion.liftBoundedOrder : {α : Type u} →
  {β : Type v} →
    {u : α → β} →
      {l : β → α} →
        [inst : PartialOrder β] → [inst_1 : Preorder α] → [BoundedOrder α] → GaloisCoinsertion l u → BoundedOrder β
-- Lean.Data.PersistentArray
_private.Lean.Data.PersistentArray.0.Lean.PersistentArray.foldrMAux : {α : Type u} → {m : Type v → Type w} → {β : Type v} → [Monad m] → (α → β → m β) → Lean.PersistentArrayNode α → β → m β
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (CommHopfAlgCat R) (Type v)
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.eq_iff_eq : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S}, v.IsEquiv w → ∀ {x y : R}, v x = v y ↔ w x = w y
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
by the sum of the elements.  -/
List.length_le_sum_of_one_le : ∀ (L : List ℕ), (∀ i ∈ L, 1 ≤ i) → L.length ≤ L.sum
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.M : Type → Type
-- Init.Control.StateCps
/-- An alternative implementation of a state monad transformer that internally uses continuation passing
style instead of tuples.
 -/
StateCpsT : Type u → (Type u → Type v) → Type u → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.CommRingObjCat C} {hom : R₁.X ⟶ R₂.X}
  {isRingHom : CategoryTheory.IsRingHom hom} {hom_1 : R₁.X ⟶ R₂.X} {isRingHom_1 : CategoryTheory.IsRingHom hom_1},
  { hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := isRingHom_1 } → hom = hom_1
-- Init.Data.UInt.BasicAux
/-- Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.toUInt8 : UInt64 → UInt8
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- A point `p` is equidistant to two lines `p₁ p₂` and `p₁ p₃` if the oriented angles at `p₁`
are equal modulo `π`.  -/
EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p₂ →
    p₁ ≠ p₃ →
      2 • EuclideanGeometry.oangle p₂ p₁ p = 2 • EuclideanGeometry.oangle p p₁ p₃ →
        dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) =
          dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₃]) p)
-- Mathlib.Algebra.Group.Conj
addConj_neg : ∀ {α : Type u} [inst : AddGroup α] {a b : α}, -(b + a + -b) = b + -a + -b
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.mk.inj : ∀ {p : Lean.Grind.Linarith.Poly} {h : Lean.Meta.Grind.Arith.Linear.EqCnstrProof} {p_1 : Lean.Grind.Linarith.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof}, { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.concat.eq_def : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.concat p₂ =
    match p₁ with
    | Lean.Grind.CommRing.Poly.num k₁ => p₂.addConst k₁
    | Lean.Grind.CommRing.Poly.add k m p₁ => Lean.Grind.CommRing.Poly.add k m (p₁.concat p₂)
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0) →
      ∀ {t : Set α}, MeasurableSet t → μ t ≠ ⊤ → f =ᵐ[μ.restrict t] 0
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurrySum_currySum : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] (f : MultilinearMap R N M₂), f.currySum.uncurrySum = f
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_3} {J : Type u_4} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} B] [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Comma L R)]
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderLimitsOfShape J],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsAddMonHomComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N O : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] [inst_4 : CategoryTheory.AddMonObj O]
  (f : M ⟶ N) (g : N ⟶ O) [CategoryTheory.IsAddMonHom f] [CategoryTheory.IsAddMonHom g],
  CategoryTheory.IsAddMonHom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.equivOp.eq_1 : ∀ {M : Type u_2} [inst : Add M] (H : AddSubsemigroup M), H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_rcc : ∀ {a b : ℤ}, (a...=b).size = (b + 1 - a).toNat
-- Lean.Parser.Basic
Lean.Parser.andthenFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCycles_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.d i j) = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_neg' : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalRing R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (f : R → R),
  cfc (-f) = -cfc f
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj.hasMap : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃],
  ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
        X₃).HasMap
    r
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- [Stacks Tag 00EC](https://stacks.math.columbia.edu/tag/00EC) -/
PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem : ∀ {R : Type u} [inst : CommRing R] (e : R),
  IsIdempotentElem e → PrimeSpectrum.zeroLocus {e} = ↑(PrimeSpectrum.basicOpen (1 - e))
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
/-- A natural isomorphism between `F G : Paths V ⥤ C` is defined by its components and
its unary naturality squares.  -/
CategoryTheory.Paths.liftNatIso : {V : Type u₁} →
  [inst : Quiver V] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} →
          (α_app : (v : V) → F.obj v ≅ G.obj v) →
            (∀ {X Y : V} (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y).hom =
                  CategoryTheory.CategoryStruct.comp (α_app X).hom (G.map f.toPath)) →
              (F ≅ G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eq_head_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
    ∀ {he : l.isEmpty = false}, Std.Internal.List.minKey l he = (Std.Internal.List.keys l).head ⋯
-- Init.PropLemmas
Decidable.not_imp_iff_and_not : ∀ {a b : Prop} [Decidable a], ¬(a → b) ↔ a ∧ ¬b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      (m₁.diff m₂ ⋯).getKey! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then default else m₁.getKey! k
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.and : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p q : α → Prop},
  Measurable p → Measurable q → Measurable fun a => p a ∧ q a
-- Mathlib.Data.Finset.Sigma
Finset.sigma_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)},
  (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
-- Mathlib.Topology.CompactOpen
/-- A variant of `ContinuousMap.continuous_of_continuous_uncurry` in terms of
`ContinuousMap.mkD`.
Of course, in this particular setting, `fun x ↦ mkD (f x) g` is just `f`,
but the `mkD` spelling appears naturally in the context of `C(α, β)`-valued integration.  -/
ContinuousMap.continuous_mkD_of_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {T : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace T] (f : T → X → Y) (g : C(X, Y)),
  Continuous (Function.uncurry f) → Continuous fun x => ContinuousMap.mkD (f x) g
-- Init.Data.List.Lemmas
List.leftpad_suffix : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, l <:+ List.leftpad n a l
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instLineDerivLeftSMulRealTopENat : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F],
  LineDerivLeftSMul ℝ E (TestFunction Ω F ⊤) (TestFunction Ω F ⊤)
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.eq_of_mem_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {a b : (a : α) × β a} {l : List ((a : α) × β a)},
  a ∈ l → b ∈ l → (a.fst == b.fst) = true → Std.Internal.List.DistinctKeys l → a = b
-- Init.Data.List.Range
List.range'_succ_left : ∀ {s n step : ℕ}, List.range' (s + 1) n step = List.map (fun x => x + 1) (List.range' s n step)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.edist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x y : α),
  edist (h x) (h y) = edist x y
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flip_flip : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D]
  (F : CategoryTheory.Functor B (CategoryTheory.Functor C D)), F.flip.flip = F
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} [inst_1 : SizeOf α] (c : Fin N.succ → α) (r : Fin N.succ → ℝ)
  (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)),
  sizeOf { c := c, r := r, rpos := rpos, h := h, hlast := hlast, inter := inter } = 1