mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.WP.SimpLemmas
Std.Do.WP.liftWith_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps]
  [inst_1 : Pure m] (f : ({β : Type u} → m β → m β) → m α),
  (Std.Do.wp (liftWith f)).apply Q = (Std.Do.wp (f fun {β} x => x)).apply Q
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ENat.LEInfty.out : ∀ {m : WithTop ℕ∞} [self : ENat.LEInfty m], m ≤ ↑⊤
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_sub : ∀ {ι : Type u_1} {M : Type u_3} [inst : Ring M] (f g : AddMonoidAlgebra M ι),
  (f - g).toDirectSum = f.toDirectSum - g.toDirectSum
-- Mathlib.Topology.Irreducible
/-- [Stacks Tag 004W](https://stacks.math.columbia.edu/tag/004W) ((2)) -/
isClosed_of_mem_irreducibleComponents : ∀ {X : Type u_1} [inst : TopologicalSpace X], ∀ s ∈ irreducibleComponents X, IsClosed s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k},
  (m.containsThenInsertIfNew k v).1 = m.contains k
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mk.congr_simp : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] (toContinuousMap toContinuousMap_1 : C(X, R))
  (e_toContinuousMap : toContinuousMap = toContinuousMap_1) (map_zero' : toContinuousMap 0 = 0),
  { toContinuousMap := toContinuousMap, map_zero' := map_zero' } =
    { toContinuousMap := toContinuousMap_1, map_zero' := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3) (id : ℕ) (c : β)
  (rupHints : Array ℕ) (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)),
  (match Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf with
    | [] => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
    | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
      h_4 id c pivot rupHints ratHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) =
    h_3 id c rupHints restPrf
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_of_forall_neg_add_le : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b : α},
  (∀ ε < 0, a + ε ≤ b) → a ≤ b
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_zero_add : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → Metric.closedBall 0 δ + s = Metric.cthickening δ s
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet s → IsLowerSet sᶜ
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The functor `CofibrantObject C ⥤ HoCat C`, considered as a localizer morphism.  -/
HomotopicalAlgebra.CofibrantObject.toHoCatLocalizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject.HoCat C))
-- Mathlib.RingTheory.Trace.Basic
/-- Given `pb : PowerBasis K S`, the trace of `pb.gen` is `-(minpoly K pb.gen).nextCoeff`.  -/
PowerBasis.trace_gen_eq_nextCoeff_minpoly : ∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra K S] [Nontrivial S]
  (pb : PowerBasis K S), (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
-- Lean.Level
Lean.Level.hash : Lean.Level → UInt64
-- Lean.Setup
Lean.Plugin.instFromJson : Lean.FromJson Lean.Plugin
-- Mathlib.Order.Lattice
inf_eq_and_sup_eq_iff : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_eq_zero_iff : ∀ {θ : Real.Angle}, 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.mapIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (i : X ≅ Y), (F.mapIso i).hom = F.map i.hom
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- The inner product on an inner product space of dimension 2 can be evaluated in terms
of a complex-number representation of the space.  -/
inner_map_complex : ∀ {G : Type u_4} [inst : SeminormedAddCommGroup G] [inst_1 : InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ) (x y : G),
  inner ℝ x y = (f y * (starRingEnd ℂ) (f x)).re
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitRightBracket.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
-- Mathlib.Geometry.Polygon.Basic
/-- Converting a triangle to a polygon and back yields the original triangle.  -/
Affine.Triangle.toPolygon_toTriangle : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (t : Affine.Triangle R P), Polygon.toTriangle R (Affine.Triangle.toPolygon t) ⋯ = t
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_comap_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M) (q : Submodule R M₂),
  Submodule.comap (LinearMap.inr R M M₂) (p.prod q) = q
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIsAddApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsAddApply (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Algebra.Notation.Support
Function.range_eq_image_or_of_mulSupport_subset : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {k : Set ι},
  Function.mulSupport f ⊆ k → Set.range f = f '' k ∨ Set.range f = insert 1 (f '' k)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.congr' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  MeasureTheory.Integrable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → MeasureTheory.Integrable g μ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the morphism from the second row to the third row  -/
CategoryTheory.ShortComplex.SnakeInput.v₂₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (self : CategoryTheory.ShortComplex.SnakeInput C) → self.L₂ ⟶ self.L₃
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.quotientEquivOrthogonal_mk : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x : E) (hx : x ∈ Kᗮ),
  K.quotientEquivOrthogonal (Submodule.Quotient.mk x) = ⟨x, hx⟩
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instFaithfulVAddForallOfNontrivial : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : VAdd M α] [FaithfulVAdd M α] [Nontrivial β],
  FaithfulVAdd Mᵈᵃᵃ (α → β)
-- Mathlib.Data.Nat.Choose.Factorization
/-- If a prime `p` has positive multiplicity in the `n`th central binomial coefficient,
`p` is no more than `2 * n`  -/
Nat.factorization_centralBinom_eq_zero_of_two_mul_lt : ∀ {p n : ℕ}, 2 * n < p → n.centralBinom.factorization p = 0
-- Mathlib.Tactic.NormNum.Irrational
/-- Finds `NotPowerCertificate` showing that `m` is not `n`-power.  -/
Mathlib.Meta.NormNum.findNotPowerCertificate : (m n : Q(ℕ)) → Lean.MetaM (Mathlib.Meta.NormNum.NotPowerCertificate m n)
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Symm.flip_eq`. -/
Symmetric.flip_eq : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], flip r = r
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- Information which arguments are fixed  -/
Lean.Elab.Structural.RecArgInfo.fixedParamPerm : Lean.Elab.Structural.RecArgInfo → Lean.Elab.FixedParamPerm
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Sum of elements in an `IntermediateField` indexed by a `Finset` is in the `IntermediateField`.
 -/
IntermediateField.sum_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {ι : Type u_4} {t : Finset ι} {f : ι → L}, (∀ c ∈ t, f c ∈ S) → ∑ i ∈ t, f i ∈ S
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_eq_sum_mapIdx : ∀ (b : ℕ) (L : List ℕ), Nat.ofDigits b L = (List.mapIdx (fun i a => a * b ^ i) L).sum
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- Through the equivalence `(AugmentedSimplexCategoryᵒᵖ ⥤ C) ≌ SimplicialObject.Augmented C`,
dropping the augmentation corresponds to precomposition with
`inclusionᵒᵖ : SimplexCategoryᵒᵖ ⥤ AugmentedSimplexCategoryᵒᵖ`.  -/
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.comp
        CategoryTheory.SimplicialObject.Augmented.drop ≅
      (CategoryTheory.Functor.whiskeringLeft SimplexCategoryᵒᵖ AugmentedSimplexCategoryᵒᵖ C).obj
        AugmentedSimplexCategory.inclusion.op
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend_d_to_eq_zero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι')
  (j : ι), e.f j = j' → ¬c.Rel (c.prev j) j → (K.extend e).d i' j' = 0
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G'] [inst_6 : NormedSpace ℝ G'] [IsOrderedAddMonoid G']
  {T : Set α → G' →L[ℝ] G''},
  MeasureTheory.FinMeasAdditive μ T →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
      ∀ {f g : MeasureTheory.SimpleFunc α G'},
        MeasureTheory.Integrable (⇑f) μ →
          MeasureTheory.Integrable (⇑g) μ →
            f ≤ g → MeasureTheory.SimpleFunc.setToSimpleFunc T f ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T g
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.instPowNat : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Pow (Matrix.SpecialLinearGroup n R) ℕ
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNNReal_add_natCast : ∀ (r : NNReal) (n : ℕ), ↑(r + ↑n) = ↑r + ↑n
-- Mathlib.GroupTheory.Index
AddSubgroup.index_eq_zero_iff_infinite : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 0 ↔ Infinite (G ⧸ H)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.not_lt_zero : ∀ {α : Type u_1} [inst : LT α] (a : WithZero α), ¬a < 0
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_toCloseds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (s : TopologicalSpace.Compacts α), ↑s.toCloseds = ↑s
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.Const.get! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited β] → Std.ExtDTreeMap α (fun x => β) cmp → α → β
-- Mathlib.Algebra.Group.ULift
ULift.addLeftCancelSemigroup.eq_1 : ∀ {α : Type u} [inst : AddLeftCancelSemigroup α],
  ULift.addLeftCancelSemigroup = Function.Injective.addLeftCancelSemigroup ⇑Equiv.ulift ⋯ ⋯
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchAt?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos : s.Pos},
  String.Slice.Pattern.Model.matchAt? pat startPos = none ↔ ¬String.Slice.Pattern.Model.MatchesAt pat startPos
-- Mathlib.Topology.Algebra.Monoid.Defs
SeparatelyContinuousMul.continuous_mul_const : ∀ {M : Type u_1} {inst : TopologicalSpace M} {inst_1 : Mul M} [self : SeparatelyContinuousMul M] {a : M},
  Continuous fun x => x * a
-- Init.Data.List.Lemmas
List.reverse_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (List.replicate n a).reverse = List.replicate n a
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`.  -/
ConditionallyCompleteLinearOrder.compare_eq_compareOfLessAndEq : ∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (a b : α), compare a b = compareOfLessAndEq a b
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- If all closed balls of large enough radius are compact, then the space is proper. Especially
useful when the lower bound for the radius is 0.  -/
ProperSpace.of_isCompact_closedBall_of_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] (R : ℝ),
  (∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)) → ProperSpace α
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for the cofinite filter  -/
Filter.Realizer.cofinite : {α : Type u_1} → [DecidableEq α] → Filter.cofinite.Realizer
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.isVanKampen_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  (H : CategoryTheory.IsPushout f g h i),
  H.IsVanKampen ↔ CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯)
-- Mathlib.Order.Filter.Extr
sup_eq_of_isMaxOn : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] [inst_1 : OrderBot β] {D : α → β} {s : Finset α} {a : α},
  a ∈ s → IsMaxOn D (↑s) a → s.sup D = D a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)],
  (CategoryTheory.MonoidalCategory.externalProduct U F).IsLeftKanExtension
    (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft U
      (CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ U) F)
-- Std.Sync.Broadcast
/-- Receive a value from the channel, blocking until the transmission could be completed.
 -/
Std.Broadcast.Sync.Receiver.recv : {α : Type} → [Inhabited α] → Std.Broadcast.Sync.Receiver α → BaseIO (Option α)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- Formula for orthogonal projection onto a single vector.  -/
Submodule.starProjection_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : E} (w : E), (𝕜 ∙ v).starProjection w = (inner 𝕜 v w / ↑(‖v‖ ^ 2)) • v
-- Mathlib.MeasureTheory.Order.Lattice
Finset.measurable_range_sup' : ∀ {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [inst : MeasurableSpace δ] [inst_1 : SemilatticeSup α]
  [MeasurableSup₂ α] {f : ℕ → δ → α} {n : ℕ}, (∀ k ≤ n, Measurable (f k)) → Measurable ((Finset.range (n + 1)).sup' ⋯ f)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
when `H` is a subgroup of the normalizer of `N` in `G`.  -/
AddSubgroup.coe_add_of_left_le_normalizer_right : ∀ {G : Type u_2} [inst : AddGroup G] (H N : AddSubgroup G), H ≤ AddSubgroup.normalizer ↑N → ↑(H ⊔ N) = ↑H + ↑N
-- Mathlib.CategoryTheory.Shift.ShiftedHom
/-- The bijection `(X ⟶ Y) ≃ ShiftedHom X Y m₀` when `m₀ = 0`.  -/
CategoryTheory.ShiftedHom.homEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {M : Type u_4} →
      [inst_1 : AddMonoid M] →
        [inst_2 : CategoryTheory.HasShift C M] →
          {X Y : C} → (m₀ : M) → m₀ = 0 → (X ⟶ Y) ≃ CategoryTheory.ShiftedHom X Y m₀
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.integral_norm_condDistrib_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F},
  AEMeasurable Y μ →
    MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
      MeasureTheory.Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) x)
        (MeasureTheory.Measure.map X μ)
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- The isomorphism `obj F X ⟨Order.succ j, _⟩ ≅ X`.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            ¬IsMax j →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                (X : C) → CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨Order.succ j, ⋯⟩ ≅ X
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM.eq_1 : ∀ {𝕜 : 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 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] (g : E → 𝕜),
  SchwartzMap.smulLeftCLM F g =
    if hg : Function.HasTemperateGrowth g then SchwartzMap.bilinLeftCLM (ContinuousLinearMap.lsmul 𝕜 𝕜).flip hg else 0
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instIsTriangulated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], CategoryTheory.IsTriangulated (DerivedCategory C)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A single point is concyclic.  -/
EuclideanGeometry.concyclic_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p : P), EuclideanGeometry.Concyclic {p}
-- Mathlib.RingTheory.Perfection
Perfection.instCommRing : (R : Type u_1) → [inst : CommRing R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → CommRing (Perfection R p)
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.primrec_pappAck : Primrec Nat.Partrec.Code.pappAck
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.y` be any element such that `S.a + η * S.b = λ * S.y`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.y : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution✝ hζ → NumberField.RingOfIntegers K
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricPMFRealSum : ∀ {p : ℝ}, 0 < p → p ≤ 1 → HasSum (fun n => ProbabilityTheory.geometricPMFReal p n) 1
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_add : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M] (s t : Set M),
  sInf (s + t) = sInf s + sInf t
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
/-- Morphisms relatively to the `⊥` subcomplexes of `X` and `Y`
identify to morphisms `X ⟶ Y`.  -/
SSet.RelativeMorphism.botEquiv : {X Y : SSet} → SSet.RelativeMorphism ⊥ ⊥ (SSet.Subcomplex.isInitialBot.to ⊥.toSSet) ≃ (X ⟶ Y)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- Given two `C^n` functions `f` and `g` from `ℝ` to a real manifold which coincide locally
around a point `s`, then the piecewise function using `f` before `t` and `g` after is `C^n`.  -/
ContMDiff.piecewise_Iic : ∀ {n : WithTop ℕ∞} {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_12}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_13} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {f g : ℝ → M} {s : ℝ},
  ContMDiff (modelWithCornersSelf ℝ ℝ) I n f →
    ContMDiff (modelWithCornersSelf ℝ ℝ) I n g →
      f =ᶠ[nhds s] g → ContMDiff (modelWithCornersSelf ℝ ℝ) I n ((Set.Iic s).piecewise f g)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_comap_subtype : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M), Submodule.map p.subtype (Submodule.comap p.subtype p') = p ⊓ p'
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Representatives of 2-morphisms in the free bicategory.  -/
CategoryTheory.FreeBicategory.Hom₂ : {B : Type u} → [inst : Quiver B] → {a b : CategoryTheory.FreeBicategory B} → (a ⟶ b) → (a ⟶ b) → Type (max u v)
-- Mathlib.AlgebraicTopology.SingularSet
instIsLeftAdjointSSetTopCatToTop : SSet.toTop.IsLeftAdjoint
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.snd : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : α → β × γ},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).2) μ
-- Mathlib.Data.Fintype.EquivFin
not_injective_infinite_finite : ∀ {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] (f : α → β), ¬Function.Injective f
-- Lean.Parser.Command
/-- `#import_path Foo` prints the transitive import chain that brings the declaration `Foo`
into the current file's scope.
 -/
Lean.Parser.Command.importPath : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J),
  AlgebraicGeometry.Scheme.IdealSheafData.inclusion h = AlgebraicGeometry.Scheme.IdealSheafData.inclusion h