mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLT.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3)
  (size : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightDualIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y₁ Y₂ : C}
  (p₁ : CategoryTheory.ExactPairing X Y₁) (p₂ : CategoryTheory.ExactPairing X Y₂),
  CategoryTheory.rightDualIso p₁ p₂ =
    { hom := CategoryTheory.CategoryStruct.id Xᘁ, inv := CategoryTheory.CategoryStruct.id Xᘁ, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.ModelTheory.Bundled
/-- When `φ` is injective, `defaultExpansion` expands a model of `T` to a model of `φ.onTheory T`
arbitrarily.  -/
FirstOrder.Language.Theory.ModelType.defaultExpansion : {L : FirstOrder.Language} →
  {T : L.Theory} →
    {L' : FirstOrder.Language} →
      {φ : L →ᴸ L'} →
        φ.Injective →
          [(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)] →
            [(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)] →
              (M : T.ModelType) → [Inhabited ↑M] → (φ.onTheory T).ModelType
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq.sizeOf_spec : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits, then `F : C ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfOp : {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.CreatesColimits F.op] → CategoryTheory.CreatesLimits F
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.summable_linear_right_add_one_mul_linear_right : ∀ (z : ℂ) (c₁ c₂ : ℤ), Summable fun n => ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.inl_of_binaryCoproductDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y], CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₁₃ = h.l.f
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a...=b` by
varying the lower bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b < a`, the statement holds for the empty range `a...=b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, the
statement holds for nonempty ranges `a...b` if it holds for the smaller range
`(a + 1)...=b`.

The following is an example reproving `length_toList_rcc`.

```
example (a b : Nat) : (a...=b).toList.length = b + 1 - a := by
  induction a, b using Nat.induct_rcc_left
  case base =>
    simp only [Nat.toList_rcc_eq_nil, List.length_nil, *]; omega
  case step =>
    simp only [Nat.toList_rcc_eq_cons, List.length_cons, *]; omega
``` -/
Nat.induct_rcc_left : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b < a → motive a b) → (∀ (a b : ℕ), a ≤ b → motive (a + 1) b → motive a b) → ∀ (a b : ℕ), motive a b
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_C : ∀ {K : Type u} [inst : Field K] (k : K), (RatFunc.C k).intDegree = 0
-- Mathlib.Topology.Compactness.Lindelof
mem_coLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.coLindelof X ↔ ∃ t, IsLindelof t ∧ tᶜ ⊆ s
-- Std.Time.Time.HourMarker
/-- Post meridiem.
 -/
Std.Time.HourMarker.pm : Std.Time.HourMarker
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.LpAddConst.eq_1 : ∀ (p : ENNReal), p.LpAddConst = if p ∈ Set.Ioo 0 1 then 2 ^ (1 / p.toReal - 1) else 1
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that members of `FrameHomClass` commute with arbitrary suprema/joins.  -/
FrameHomClass.map_sSup : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {inst : CompleteLattice α} {inst_1 : CompleteLattice β}
  {inst_2 : FunLike F α β} [self : FrameHomClass F α β] (f : F) (s : Set α), f (sSup s) = sSup (⇑f '' s)
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.image : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [inst : TopologicalSpace β] {s : Set α},
  TopologicalSpace.IsSeparable s → ∀ {f : α → β}, Continuous f → TopologicalSpace.IsSeparable (f '' s)
-- Mathlib.Algebra.MvPolynomial.Division
_private.Mathlib.Algebra.MvPolynomial.Division.0.MvPolynomial.«term_/ᵐᵒⁿᵒᵐⁱᵃˡ_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_subtype_comap : ∀ {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {α : Type u_6} [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (f : α → G), ∫ (x : ↑s), f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫ (x : α) in s, f x ∂μ
-- Mathlib.GroupTheory.Perm.Sign
/-- Given a list `l : List α` and a permutation `f : Perm α` such that the nonfixed points of `f`
are in `l`, recursively factors `f` as a product of transpositions.  -/
Equiv.Perm.swapFactorsAux : {α : Type u} →
  [inst : DecidableEq α] →
    (l : List α) → (f : Equiv.Perm α) → (∀ {x : α}, f x ≠ x → x ∈ l) → { l // l.prod = f ∧ ∀ g ∈ l, g.IsSwap }
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.source = e.target
-- Mathlib.Algebra.Module.SnakeLemma
SnakeLemma.δ_aux : ∀ {R : Type u_1} [inst : CommRing R] {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {N₃ : Type u_7}
  [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₃]
  [inst_5 : AddCommGroup N₁] [inst_6 : Module R N₁] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  [inst_9 : AddCommGroup N₃] [inst_10 : Module R N₃] (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₂ : M₂ →ₗ[R] M₃)
  (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃),
  Function.Exact ⇑g₁ ⇑g₂ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      ∀ (σ : M₃ → M₂),
        ⇑f₂ ∘ σ = id →
          ∀ (ρ : N₂ → N₁),
            ρ ∘ ⇑g₁ = id →
              ∀ {K₃ : Type u_9} [inst_11 : AddCommGroup K₃] [inst_12 : Module R K₃] (ι₃ : K₃ →ₗ[R] M₃),
                Function.Exact ⇑ι₃ ⇑i₃ → ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.shrink.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S),
  E.shrink = E.presieve₀.preZeroHypercover
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.hasStrictFDerivAt_leftFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (self : ImplicitFunctionData 𝕜 E F G),
  HasStrictFDerivAt self.leftFun self.leftDeriv self.pt
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesRxcSize.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : Std.Rxc.HasSize α] [inst_3 : Std.Rxc.HasSize β] {f : Std.PRange.UpwardEnumerable.Map α β},
  (∀ {a b : α}, Std.Rxc.HasSize.size a b = Std.Rxc.HasSize.size (f.toFun a) (f.toFun b)) → f.PreservesRxcSize
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.left_unique : ∀ {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β}, G.IsLink e x z → G.IsLink e y z → x = y
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.natIsoLift_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D}
  (τ : (CategoryTheory.Quotient.functor r).comp F ≅ (CategoryTheory.Quotient.functor r).comp G),
  (CategoryTheory.Quotient.natIsoLift r τ).hom = CategoryTheory.Quotient.natTransLift r τ.hom
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_ssubset_left_iff`. -/
Set.diff_ssubset_left_iff : ∀ {α : Type u_1} {s t : Set α}, s \ t ⊂ s ↔ (s ∩ t).Nonempty
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a : Lean.Grind.CommRing.Expr) (k : ℕ),
  x = a.pow k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_9 a k
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_add_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ),
  ⌈a + ↑n⌉ = ⌈a⌉ + ↑n
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.of_addHom_image : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {A B : Finset G} {a0 b0 : G} [inst_2 : DecidableEq H]
  (f : G →ₙ+ H),
  (∀ ⦃a b c d : G⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d) →
    UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0) → UniqueAdd A B a0 b0
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add : ∀ {a b c d : ENNReal}, a < c → b < d → a + b < c + d
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<*>`, general version.  -/
SatisfiesM.seq : ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
  {q : α_1 → Prop} [inst : Applicative m] [LawfulApplicative m] {x : m α},
  SatisfiesM p₁ f → SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (f a)) → SatisfiesM q (f <*> x)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.uset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.uset fvarId i y h) = 1 + sizeOf fvarId + sizeOf i + sizeOf y + sizeOf h
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termF₁_1 : Lean.ParserDescr
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.even_or_odd : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) [NoZeroDivisors S], ψ.Even ∨ ψ.Odd
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.differentiableAt_sinh : ∀ {x : ℝ}, DifferentiableAt ℝ Real.sinh x
-- Init.Core
Sum.inl.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (val : α), sizeOf (Sum.inl val) = 1 + sizeOf val
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.image_ball : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ),
  Subtype.val '' Metric.ball a r = Metric.ball (↑a) r ∩ {a | p a}
-- Mathlib.Topology.Instances.AddCircle.Real
/-- The `AddMonoidHom` from `ZMod N` to `ℝ / ℤ` sending `j mod N` to `j / N mod 1`.  -/
ZMod.toAddCircle : {N : ℕ} → [NeZero N] → ZMod N →+ UnitAddCircle
-- Mathlib.CategoryTheory.Limits.Final
/-- The functor `CostructuredArrow.pre X T S` is initial if `T` is initial.  -/
CategoryTheory.CostructuredArrow.initial_pre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (T : CategoryTheory.Functor C D) [T.Initial]
  (S : CategoryTheory.Functor D E) (X : E), (CategoryTheory.CostructuredArrow.pre T S X).Initial
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {s : Set E} {x : E}, MDiffAt[s] ⇑f x
-- Mathlib.Data.Sigma.Basic
/-- Interpret a function on `Σ x : α, β x` as a dependent function with two arguments.

This also exists as an `Equiv` as `Equiv.piCurry γ`.  -/
Sigma.curry : {α : Type u_1} →
  {β : α → Type u_4} → {γ : (a : α) → β a → Type u_7} → ((x : Sigma β) → γ x.fst x.snd) → (x : α) → (y : β x) → γ x y
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst.eq_2 : ∀ (n : ℕ), Nat.stirlingFirst 0 n.succ = 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.compare_right_aux : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    (∀ (g : ℝ → ℝ), List.head? basis = some g → (Real.log ∘ g) =o[Filter.atTop] (Real.log ∘ f)) →
      ∀ g ∈ basis, (Real.log ∘ g) =o[Filter.atTop] (Real.log ∘ f)
-- Init.Data.Nat.Basic
Nat.lt_succ : ∀ {m n : ℕ}, m < n.succ ↔ m ≤ n
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (Set.Ico a b)⁻¹ = Set.Ioc b⁻¹ a⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.ext_iff : ∀ {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart), d₁ = d₂ ↔ d₁.toProd = d₂.toProd
-- Mathlib.Order.Cover
CovBy.unique_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ⋖ c → b ⋖ c → a = b
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- A σ-compact measure zero subset is meagre.
(More generally, every Fσ set of measure zero is meagre.)  -/
IsMeagre.of_isSigmaCompact_null : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X}
  [μ.IsOpenPosMeasure] [T2Space X], IsSigmaCompact s → μ s = 0 → IsMeagre s
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℝ E] (a : α),
  MeasureTheory.AEStronglyMeasurable f (κ a) →
    MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instPreadditiveQuotientHomologicalComplexHomotopic : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) → CategoryTheory.Preadditive (CategoryTheory.Quotient (homotopic V c))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (f : NumberField.mixedEmbedding.mixedSpace K → ENNReal),
  ∫⁻ (x : NumberField.mixedEmbedding.realMixedSpace K) in (NumberField.mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(NumberField.mixedEmbedding.polarCoord K).symm x) =
    ∫⁻ (x : NumberField.mixedEmbedding.mixedSpace K), f x
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.isTopologicalBasis_insert_univ_subbasis : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  TopologicalSpace.IsTopologicalBasis (insert Set.univ {s | ∃ a, (Set.Ici a)ᶜ = s})
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.instAddMonoidHomClassAddHom : ∀ {M : Type u_10} {N : Type u_11} [inst : AddMonoid M] [inst_1 : AddLeftCancelMonoid N], AddMonoidHomClass (M →ₙ+ N) M N
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `liftNC` as a `RingHom`, for when `f x` and `g y` commute  -/
SkewMonoidAlgebra.liftNCRingHom : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        [inst_2 : MulSemiringAction G k] →
          {R : Type u_3} →
            [inst_3 : Semiring R] →
              (f : k →+* R) →
                (g : G →* R) → (∀ {x : k} {y : G}, f (y • x) * g y = g y * f x) → SkewMonoidAlgebra k G →+* R
-- Mathlib.RingTheory.PrincipalIdealDomain
Irreducible.isCoprime_or_dvd : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] {p : R}, Irreducible p → ∀ (i : R), IsCoprime p i ∨ p ∣ i
-- Lean.Meta.Tactic.Grind.Types
/-- Marks current goal as inconsistent without assigning `mvarId`.  -/
Lean.Meta.Grind.markAsInconsistent : Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.mk.sizeOf_spec : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : SizeOf H]
  (toClosedSubmodule : ClosedSubmodule ℝ H) (IsSeparating : toClosedSubmodule ⊓ toClosedSubmodule.mulI = ⊥)
  (IsCyclic : toClosedSubmodule ⊔ toClosedSubmodule.mulI = ⊤),
  sizeOf { toClosedSubmodule := toClosedSubmodule, IsSeparating := IsSeparating, IsCyclic := IsCyclic } =
    1 + sizeOf toClosedSubmodule + sizeOf IsSeparating + sizeOf IsCyclic
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₁.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))),
  Homotopy.mkInductiveAux₁ e zero one comm_one succ 0 = ⟨zero, ⟨one, comm_one⟩⟩
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.transparency.injEq : ∀ (md : Lean.Meta.TransparencyMode) (alsoForIndex : Bool) (md_1 : Lean.Meta.TransparencyMode) (alsoForIndex_1 : Bool),
  (Aesop.Frontend.BuilderOption.transparency md alsoForIndex =
      Aesop.Frontend.BuilderOption.transparency md_1 alsoForIndex_1) =
    (md = md_1 ∧ alsoForIndex = alsoForIndex_1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_eq_getD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  t.get! a = t.getD a default
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.contractSnd_dirac : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (x : X) (y : Y) (f : C(X × Y, R)),
  ((AbstractMeasure.contractSnd (AbstractMeasure.dirac R y)) f) x = f (x, y)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G},
  fderiv 𝕜 (⇑iso ∘ f) x = ↑iso ∘SL fderiv 𝕜 f x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.penultimate_concat : ∀ {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj v t), (p.concat h).penultimate = v
-- Lean.Elab.MutualInductive
Lean.Elab.Command.CtorView.mk.injEq : ∀ (ref : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) (declName : Lean.Name) (declId binders : Lean.Syntax)
  (type? : Option Lean.Syntax) (ref_1 : Lean.Syntax) (modifiers_1 : Lean.Elab.Modifiers) (declName_1 : Lean.Name)
  (declId_1 binders_1 : Lean.Syntax) (type?_1 : Option Lean.Syntax),
  ({ ref := ref, modifiers := modifiers, declName := declName, declId := declId, binders := binders, type? := type? } =
      { ref := ref_1, modifiers := modifiers_1, declName := declName_1, declId := declId_1, binders := binders_1,
        type? := type?_1 }) =
    (ref = ref_1 ∧
      modifiers = modifiers_1 ∧ declName = declName_1 ∧ declId = declId_1 ∧ binders = binders_1 ∧ type? = type?_1)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_monomial : ∀ {R : Type u_1} [inst : CommSemiring R] {m n : ℕ},
  m ≤ n → ∀ (r : R), ((Polynomial.monomial m) r).homogenize n = (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r
-- Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
/-- All nondegenerate quadratic forms on an algebraically closed field of characteristic not equal
to 2 are equivalent.  -/
QuadraticForm.equivalent_of_isAlgClosed : ∀ {K : Type u_2} [inst : Field K] [IsAlgClosed K] [inst_2 : Invertible 2] {M : Type u_3} [inst_3 : AddCommGroup M]
  [inst_4 : Module K M] [FiniteDimensional K M] (Q₁ Q₂ : QuadraticForm K M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q₁) →
    LinearMap.SeparatingLeft (QuadraticMap.associated Q₂) → QuadraticMap.Equivalent Q₁ Q₂
-- Mathlib.LinearAlgebra.Dimension.Constructions
Submodule.lt_top_of_finrank_lt_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Submodule R M},
  Module.finrank R ↥s < Module.finrank R M → s < ⊤