mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter m₂ ⋯).getD k fallback = fallback
-- Mathlib.Order.Hom.Set
Set.sumEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {s : Set α × Set β}, Set.sumEquiv.symm s = Sum.inl '' s.1 ∪ Sum.inr '' s.2
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A commutative square involving the morphisms `mor₂` of two distinguished triangles
can be extended as morphism of triangles  -/
CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
  T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (b : T₁.obj₂ ⟶ T₂.obj₂) (c : T₁.obj₃ ⟶ T₂.obj₃),
        CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ →
          ∃ a,
            CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ ∧
              CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
                CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Mathlib.Dynamics.Flow
Flow.IsSemiconjugacy.semiconj : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  {β : Type u_3} [inst_3 : TopologicalSpace β] {π : α → β} {ϕ : Flow τ α} {ψ : Flow τ β},
  Flow.IsSemiconjugacy π ϕ ψ → ∀ (t : τ), Function.Semiconj π (ϕ.toFun t) (ψ.toFun t)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.eq_2 : ∀ (motive : PosNum → PosNum → Sort u_1) (b : PosNum) (h_1 : (a : PosNum) → motive a PosNum.one)
  (h_2 : (b : PosNum) → motive PosNum.one b) (h_3 : (a b : PosNum) → motive a.bit0 b.bit0)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit1) (h_5 : (a b : PosNum) → motive a.bit1 b.bit0)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit1),
  (b = PosNum.one → False) →
    (match PosNum.one, b with
      | a, PosNum.one => h_1 a
      | PosNum.one, b => h_2 b
      | a.bit0, b.bit0 => h_3 a b
      | a.bit0, b.bit1 => h_4 a b
      | a.bit1, b.bit0 => h_5 a b
      | a.bit1, b.bit1 => h_6 a b) =
      h_2 b
-- Mathlib.Computability.Reduce
ManyOneDegree.liftOn_eq : ∀ {φ : Sort u_1} (p : Set ℕ) (f : Set ℕ → φ) (h : ∀ (p q : ℕ → Prop), ManyOneEquiv p q → f p = f q),
  (ManyOneDegree.of p).liftOn f h = f p
-- Mathlib.Algebra.Order.Star.Basic
/-- The combination `(IsSelfAdjoint.star_eq <| .of_nonneg ·)` for use with dot notation.  -/
LE.le.star_eq : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 ≤ x → star x = x
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_one : Real.toNNReal 1 = 1
-- Mathlib.Algebra.BigOperators.Associated
Associates.prod_mk : ∀ {M : Type u_2} [inst : CommMonoid M] {p : Multiset M}, (Multiset.map Associates.mk p).prod = Associates.mk p.prod
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.toSheaf R).Additive
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.leftUnitor_inv_apply : ∀ {X : TopCat} {x : ↑X},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) x = (PUnit.unit, x)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_fin_Icc_eq_prod_nat_Icc : ∀ {α : Type u_1} [inst : CommMonoid α] {n : ℕ} (a b : Fin n) (f : Fin n → α),
  ∏ i ∈ Finset.Icc a b, f i = ∏ i ∈ Finset.Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_induced : ∀ {α : Type u_5} {β : Type u_6} [inst : Bornology β] {f : α → β} {s : Set α},
  Bornology.IsBounded s ↔ Bornology.IsBounded (f '' s)
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toAddCommGroup : {E : Type u_8} → [self : NormedAddCommGroup E] → AddCommGroup E
-- Mathlib.Order.SupIndep
Finset.supIndep_univ_bool : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Bool → α),
  Finset.univ.SupIndep f ↔ Disjoint (f false) (f true)
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Allowed (by the linter) whitespace characters  -/
_private.Mathlib.Tactic.Linter.TextBased.UnicodeLinter.0.Mathlib.Linter.TextBased.UnicodeLinter.ASCII.allowedWhitespace : Char → Bool
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonAssocCommSemiring.mul_comm : ∀ {α : Type u} [self : NonAssocCommSemiring α] (a b : α), a * b = b * a
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_atBot : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [IsStrictOrderedRing α],
  Filter.Tendsto Int.ceil Filter.atBot Filter.atBot
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_of_not_sigmaFinite : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ENNReal} (hm : mΩ ≤ mΩ₀),
  ¬MeasureTheory.SigmaFinite (P.trim hm) → P⁻[X | mΩ] = 0
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_comp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D₁ D₂ D₃ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ} (h₁₂ : D₁ ≤ D₂)
  (h₂₃ : D₂ ≤ D₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h₁₂)
      (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h₂₃) =
    CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap ⋯
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
/-- A measure `μ` is zero or a probability measure if `μ univ = 0` or `μ univ = 1`. This class
of measures appears naturally when conditioning on events, and many results which are true for
probability measures hold more generally over this class.  -/
MeasureTheory.IsZeroOrProbabilityMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Init.Data.Ord.Basic
Ordering.instAssociativeThen : Std.Associative Ordering.then
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_toOrderIso_symm : ∀ (f : CircleDeg1Liftˣ), ⇑(CircleDeg1Lift.toOrderIso f).symm = ⇑↑f⁻¹
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addMonoidHomOfForallMemZMultiples.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G}
  (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g),
  addMonoidHomOfForallMemZMultiples hg hg' =
    { toFun := fun x => Classical.choose ⋯ • g', map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) (X : B), (F.comp G).obj X = G.obj (F.obj X)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Balanced.below.black : ∀ {α : Type u_1} {motive : (a : RBTree.RBNode α) → (a_1 : RBTree.RBColor) → (a_2 : ℕ) → a.Balanced a_1 a_2 → Prop}
  {x : RBTree.RBNode α} {c₁ : RBTree.RBColor} {n : ℕ} {y : RBTree.RBNode α} {c₂ : RBTree.RBColor} {v : α}
  (a : x.Balanced c₁ n) (a_1 : y.Balanced c₂ n),
  RBTree.RBNode.Balanced.below a →
    motive x c₁ n a → RBTree.RBNode.Balanced.below a_1 → motive y c₂ n a_1 → RBTree.RBNode.Balanced.below ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.leftInvOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.LeftInvOn (↑e.symm) (↑e) e.source
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {a : α} [inst_1 : Inhabited (β a)] {b : β a},
  (Std.DTreeMap.Internal.Impl.insert a b t ⋯).impl.get! a = b
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A cofork on `f g : X ⟶ Y` is determined by the morphism `π : Y ⟶ P` satisfying
`f ≫ π = g ≫ π`.  -/
CategoryTheory.Limits.Cofork.ofπ : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {P : C} →
          (π : Y ⟶ P) →
            CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π →
              CategoryTheory.Limits.Cofork f g
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂)
  (hj : j₁ ≤ j₂),
  CategoryTheory.Arrow.mk (iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj) =
    CategoryTheory.SmallObject.SuccStruct.arrowMap iter₂.F k₁ k₂ h₁₂ h₂
-- Mathlib.Data.Finset.NAry
Finset.image₂_empty_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α},
  Finset.image₂ f s ∅ = ∅
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.TreeSet.Raw.ofList l cmp ↔ l.contains k = true
-- Mathlib.Probability.Independence.Basic
/-- Given random variables `X i : Ω i → 𝓧 i`, they are independent when viewed as random
variables defined on the product space `Π i, Ω i`.  -/
ProbabilityTheory.iIndepFun_pi : ∀ {ι : Type u_11} [inst : Fintype ι] {Ω : ι → Type u_12} {mΩ : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {𝓧 : ι → Type u_13}
  [inst_2 : (i : ι) → MeasurableSpace (𝓧 i)] {X : (i : ι) → Ω i → 𝓧 i},
  (∀ (i : ι), AEMeasurable (X i) (μ i)) →
    ProbabilityTheory.iIndepFun (fun i ω => X i (ω i)) (MeasureTheory.Measure.pi μ)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_mem_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {a : α} {n : ℕ}, a ∈ s → a ^ n ∈ s ^ n
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_apply₂₁ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α) (i : o) (j : l), Matrix.fromBlocks A B C D (Sum.inr i) (Sum.inl j) = C i j
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (X : C),
  (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ici_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ici a)), Subtype.val '' Set.Ioi b = Set.Ioi ↑b
-- Mathlib.Algebra.Torsor.Defs
/-- Dividing two points produces 1 if and only if they are equal.  -/
sdiv_eq_one_iff_eq : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p₁ p₂ : P}, p₁ /ₛ p₂ = 1 ↔ p₁ = p₂
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.toTermSuggestion : LeanSearchClient.SearchResult → Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_ne_zero_tfae : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V),
  [f.normDet ≠ 0, f.ker = ⊥, Module.finrank 𝕜 ↥f.range = Module.finrank 𝕜 U,
      Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range), Function.Injective ⇑f].TFAE
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (x : V),
  NormedSpace.normalize (-x) = -NormedSpace.normalize x
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instZero.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Zero G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G],
  ContMDiffMap.instZero = { zero := ContMDiffMap.const 0 }
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.radical_inf : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, (I ⊓ J).radical = I.radical ⊓ J.radical
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.integralBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.integralBasis K =
    Module.Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K (NumberField.RingOfIntegers.basis K)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_extChartAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {y : E},
  y ∈ (extChartAt I x).target → writtenInExtChartAt I (modelWithCornersSelf 𝕜 E) x (↑(extChartAt I x)) y = y
-- Mathlib.Analysis.Convex.Strict
StrictConvex.preimage_smul : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : CommSemiring 𝕜] [IsDomain 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜 E] [Module.IsTorsionFree 𝕜 E]
  [ContinuousConstSMul 𝕜 E] {s : Set E}, StrictConvex 𝕜 s → ∀ (c : 𝕜), StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s)
-- Mathlib.Order.Filter.Map
Filter.comap_const_of_mem : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {x : β}, (∀ t ∈ g, x ∈ t) → Filter.comap (fun x_1 => x) g = ⊤
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.inl_comp_pushoutSymmetry_hom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushoutSymmetry f g).hom Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr g f) Q
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.instBEq : BEq Aesop.IndexMatchLocation
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {X : ι → Type u_4} [inst_1 : (i : ι) → TopologicalSpace (X i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (X i)] [∀ (i : ι), MeasureTheory.volume.IsOpenPosMeasure]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume], MeasureTheory.volume.IsOpenPosMeasure
-- Mathlib.LinearAlgebra.FreeModule.Norm
instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs : ∀ {S : Type u_2} {ι : Type u_3} [inst : CommRing S] [inst_1 : IsDomain S] {F : Type u_4} [inst_2 : Field F]
  [inst_3 : Algebra (Polynomial F) S] [inst_4 : Finite ι] (b : Module.Basis ι (Polynomial F) S) {I : Ideal S}
  (hI : I ≠ ⊥) (i : ι), FiniteDimensional F (Polynomial F ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The pmf of the Poisson distribution depending on its rate, as a function to ℝ  -/
ProbabilityTheory.poissonPMFReal : NNReal → ℕ → ℝ
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.lt_neg_of_pos_of_infinitesimal : ∀ {x : ℝ*}, x.Infinitesimal → ∀ (r : ℝ), 0 < r → -↑r < x
-- Mathlib.NumberTheory.Bernoulli
bernoulli_one : bernoulli 1 = -1 / 2
-- Mathlib.Data.Vector.Basic
List.Vector.replicate_succ : ∀ {α : Type u_1} {n : ℕ} (val : α), List.Vector.replicate (n + 1) val = val ::ᵥ List.Vector.replicate n val
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_top : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M], ↑⊤ = Set.univ
-- Lean.Elab.Util
Lean.Elab.MacroStack : Type
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀)
      (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q) =
    ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.ι
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v : V} (x : V) (x_1 : x ∈ SimpleGraph.Walk.nil.support),
  SimpleGraph.Walk.nil.dropUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesEpimorphisms.of_natTrans`. -/
CategoryTheory.Functor.preservesEpimorphisms.of_natTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesEpimorphisms] (f : F ⟶ G) [∀ (X : C), CategoryTheory.Epi (f.app X)],
  G.PreservesEpimorphisms
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.card_infinitePlace : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : NumberField k]
  [inst_4 : NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K],
  Fintype.card (NumberField.InfinitePlace K) = Fintype.card (NumberField.InfinitePlace k) * Module.finrank k K
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.deleteMin.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool),
  Batteries.BinomialHeap.Imp.Heap.deleteMin le Batteries.BinomialHeap.Imp.Heap.nil = none
-- Mathlib.Order.KrullDimension
Order.coheight_lt_top : ∀ {α : Type u_1} [inst : Preorder α] [FiniteDimensionalOrder α] (x : α), Order.coheight x < ⊤
-- Mathlib.Data.Set.Card
Set.fintypeCard_eq_ncard : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], Fintype.card ↑s = s.ncard
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.kernel_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x y : X),
  RKHS.kernel H x y = ContinuousLinearMap.adjoint (RKHS.kerFun H x) ∘SL RKHS.kerFun H y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_filter!_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k : α}, t.WF → (Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.Logic.Equiv.List
/-- A noncomputable way to arbitrarily choose an ordering on a finite type.
It is not made into a global instance, since it involves an arbitrary choice.
This can be locally made into an instance with `attribute [local instance] Fintype.toEncodable`.  -/
Fintype.toEncodable : (α : Type u_2) → [Fintype α] → Encodable α
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdUnique_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique β] (a : WithLp p (α × β)),
  (IsometryEquiv.withLpProdUnique p α β) a = a.fst
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forIn'.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (range : Std.Legacy.Range)
  (f : (i : ℕ) → i ∈ range → β → m (ForInStep β)) (b : β) (i : ℕ) (hs : (i - range.start) % range.step = 0)
  (hl : range.start ≤ i),
  Std.Legacy.Range.forIn'.loop✝ range f b i hs hl =
    if h : i < range.stop then do
      let __do_lift ← f i ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          have this := ⋯;
          Std.Legacy.Range.forIn'.loop✝ range f b (i + range.step) ⋯ ⋯
    else pure b
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_union₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t μ → MeasureTheory.AEDisjoint μ s t → μ (s ∪ t) = μ s + μ t
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.cases : Aesop.CasesTarget → Lean.Meta.TransparencyMode → Bool → Array Aesop.CtorNames → Aesop.RuleTacDescr
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.of_subsingleton : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Monoid A] [inst_2 : Zero A] [Subsingleton A] {a : A},
  IsStrictlyPositive a
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.Pattern.isRefutable : Lean.Meta.Match.Pattern → Bool
-- Batteries.Data.Fin.Lemmas
Fin.bind_findRev?_isSome : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findRev? fun i => (f i).isSome).bind f = Fin.findSomeRev? f
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.biprodComparison_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.biprod.snd) h
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.ofMVarId : Lean.MVarId → Lean.MetaM Aesop.GoalWithMVars
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.instMonadMCtxM : Lean.MonadMCtx Lean.MetavarContext.MkBinding.M