mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : SizeOf α] (Has : Set α → Prop) (has_empty : Has ∅) (has_compl : ∀ {a : Set α}, Has a → Has aᶜ)
  (has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)),
  sizeOf { Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat } =
    1 + sizeOf has_empty
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.A_c_eq_zero : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m}, ↑A 1 0 = 0 → ↑A 0 0 * ↑A 1 1 = m
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheckSite.decl.inj : ∀ {name name_1 : Lean.Name},
  Lean.Doc.DeferredCheckSite.decl name = Lean.Doc.DeferredCheckSite.decl name_1 → name = name_1
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift_self : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (h : D.IsTerminal e),
  h.lift ⋯ = CategoryTheory.CategoryStruct.id e
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_to_real : RCLike.I = 0
-- Lean.Elab.ConfigEval.Extra
/-- Uses global option declarations with the prefix `optionPrefix` when setting `Options`.
Assumes that `item` is shifted, with the rest of the item being the option name suffix to use.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.evalSetOptions : Lean.Name → Lean.Options → Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM Lean.Options
-- Mathlib.Algebra.Group.Defs
/-- If all additions cancel then every element is add-regular.  -/
IsAddRegular.all : ∀ {R : Type u_2} [inst : Add R] [IsCancelAdd R] (g : R), IsAddRegular g
-- Init.Data.SInt.Lemmas
Int64.toISize_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toISize = ISize.ofNat n
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.mk.inj : ∀ {pre post : Lean.Meta.Simp.Simproc} {dpre dpost : Lean.Meta.Simp.DSimproc}
  {discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)} {wellBehavedDischarge : Bool}
  {pre_1 post_1 : Lean.Meta.Simp.Simproc} {dpre_1 dpost_1 : Lean.Meta.Simp.DSimproc}
  {discharge?_1 : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)} {wellBehavedDischarge_1 : Bool},
  { pre := pre, post := post, dpre := dpre, dpost := dpost, discharge? := discharge?,
        wellBehavedDischarge := wellBehavedDischarge } =
      { pre := pre_1, post := post_1, dpre := dpre_1, dpost := dpost_1, discharge? := discharge?_1,
        wellBehavedDischarge := wellBehavedDischarge_1 } →
    pre = pre_1 ∧
      post = post_1 ∧
        dpre = dpre_1 ∧ dpost = dpost_1 ∧ discharge? = discharge?_1 ∧ wellBehavedDischarge = wellBehavedDischarge_1
-- Lean.Declaration
Lean.ReducibilityHints.opaque.sizeOf_spec : sizeOf Lean.ReducibilityHints.opaque = 1
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instMonoid : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Monoid γ] → [ContinuousMul γ] → Monoid (α →ₘ[μ] γ)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAt_le : ∀ {N i : ℕ}, i ≤ N → (Polynomial.revAt N) i = N - i
-- Mathlib.Data.ENat.Lattice
ENat.iInf_toNat : ∀ {ι : Sort u_1} {f : ι → ℕ}, (⨅ i, ↑(f i)).toNat = ⨅ i, f i
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul_left : ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD n]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termY₂_1 : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Order
AddEquiv.strictMono_subsemigroupCongr : ∀ {G : Type u_1} [inst : AddCommMonoid G] [inst_1 : Preorder G] {S T : AddSubsemigroup G} (h : S = T),
  StrictMono ⇑(AddEquiv.subsemigroupCongr h)
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Constructor for `TwoSquare`.  -/
CategoryTheory.TwoSquare.mk : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                (T : CategoryTheory.Functor C₁ C₂) →
                  (L : CategoryTheory.Functor C₁ C₃) →
                    (R : CategoryTheory.Functor C₂ C₄) →
                      (B : CategoryTheory.Functor C₃ C₄) → (T.comp R ⟶ L.comp B) → CategoryTheory.TwoSquare T L R B
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.WithGeneratedByTopology.isClosed_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {U : Set (Topology.WithGeneratedByTopology X Y)},
  IsClosed U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed (⇑f ⁻¹' ⇑Topology.WithGeneratedByTopology.equiv.symm ⁻¹' U)
-- Mathlib.Topology.DerivedSet
/-- The derived set of a set is the set of all accumulation points of it.
 -/
derivedSet : {X : Type u_1} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerAnodyneExtensions.whiskerRight : ∀ {X Y : SSet} {f : X ⟶ Y},
  SSet.innerAnodyneExtensions f →
    ∀ (Z : SSet), SSet.innerAnodyneExtensions (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
/-- When the coefficients are a field, the coroot conditions for irreducibility follow from those
for the roots.  -/
RootPairing.IsIrreducible.mk' : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [inst_3 : Module K M] [inst_4 : Module K N] [Nontrivial M] (P : RootPairing ι K M N),
  (∀ (q : Submodule K M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤) → P.IsIrreducible
-- Init.Data.BitVec.Lemmas
BitVec.mk_zero : ∀ {w : ℕ} {h : 0 < 2 ^ w}, { toFin := ⟨0, h⟩ } = 0#w
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.subtype_comp_inclusion : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M),
  M.subtype.comp (BooleanSubalgebra.inclusion h) = L.subtype
-- Mathlib.Analysis.Convex.Gauge
/-- If `s` is a neighborhood of the origin, then `gauge s` is continuous at the origin.
See also `continuousAt_gauge`.  -/
continuousAt_gauge_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], s ∈ nhds 0 → ContinuousAt (gauge s) 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : CategoryTheory.SimplicialObject C} {n : ℕ}
  [self : X.IsCoskeletal n],
  CategoryTheory.Functor.IsRightKanExtension X
    (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X))
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment : Bool → Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.M : Type → Type
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.add_iff_right` -/
Differentiable.fun_add_iff_right : ∀ {𝕜 : 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] {f g : E → F},
  Differentiable 𝕜 f → ((Differentiable 𝕜 fun i => f i + g i) ↔ Differentiable 𝕜 g)
-- Mathlib.Algebra.Tropical.BigOperators
List.untrop_prod : ∀ {R : Type u_1} [inst : AddMonoid R] (l : List (Tropical R)), Tropical.untrop l.prod = (List.map Tropical.untrop l).sum
-- Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
SSet.instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType : ∀ [CategoryTheory.Limits.HasCoproducts (Type u)],
  CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{v', u, u + 1}
    (CategoryTheory.MorphismProperty.monomorphisms SSet)
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (x : α),
  MeasureTheory.llr μ ν x = Real.log (μ.rnDeriv ν x).toReal
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the left respects higher differentiability at a
point in a domain.  -/
ContinuousLinearEquiv.comp_contDiffWithinAt_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞}
  (e : F ≃L[𝕜] G), ContDiffWithinAt 𝕜 n (⇑e ∘ f) s x ↔ ContDiffWithinAt 𝕜 n f s x
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- The forgetful functor the pro-étale site of `S` to schemes over `S`.  -/
AlgebraicGeometry.Scheme.ProEt.forget : (S : AlgebraicGeometry.Scheme) → CategoryTheory.Functor S.ProEt (CategoryTheory.Over S)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isThin_of_isSeparating_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], ⊥.IsSeparating → Quiver.IsThin C
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- The entries in each column are strictly increasing (top to bottom).  -/
SemistandardYoungTableau.col_strict' : ∀ {μ : YoungDiagram} (self : SemistandardYoungTableau μ) {i1 i2 j : ℕ},
  i1 < i2 → (i2, j) ∈ μ → self.entry i1 j < self.entry i2 j
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.instUniqueStructureEmpty : {M : Type w} → Unique (FirstOrder.Language.empty.Structure M)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    C → (succ : C → C) → ((X : C) → X ⟶ succ X) → CategoryTheory.SmallObject.SuccStruct C
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Composition of two continuous homomorphisms.  -/
ContinuousMonoidHom.comp : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      [inst : Monoid A] →
        [inst_1 : Monoid B] →
          [inst_2 : Monoid C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] → [inst_5 : TopologicalSpace C] → (B →ₜ* C) → (A →ₜ* B) → A →ₜ* C
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.empty : Aesop.RuleStatsTotals
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.usize : Lean.IR.IRType
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (l : Std.DTreeMap.Internal.Impl α β) →
            l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3) →
        (l : Std.DTreeMap.Internal.Impl α β) →
          (hl : l.Balanced) →
            (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size) →
              ((hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf hl hlr) →
                ((size : ℕ) →
                    (k' : α) →
                      (v' : β k') →
                        (l' r' : Std.DTreeMap.Internal.Impl α β) →
                          (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalancedAtRoot
                                  (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr) →
                  motive l hl hlr
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.restrictSupportIdeal.congr_simp : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (s s_1 : Set (σ →₀ ℕ)) (e_s : s = s_1) (hs : IsUpperSet s),
  MvPolynomial.restrictSupportIdeal R s hs = MvPolynomial.restrictSupportIdeal R s_1 ⋯
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingEquiv_symm_apply : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α ≃+* β) (hf : Continuous ⇑f) (hf' : Continuous ⇑f.symm) (a : UniformSpace.Completion β),
  (UniformSpace.Completion.mapRingEquiv f hf hf').symm a = UniformSpace.Completion.map (⇑f.symm) a
-- Init.Grind.Lemmas
Lean.Grind.Bool.or_eq_of_eq_true_left : ∀ {a b : Bool}, a = true → (a || b) = true
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] {f g : sInfHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.csSup_mem : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s t : Set α},
  IsClub s → t ⊆ s → t.Nonempty → BddAbove t → sSup t ∈ s
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.hasSum_repr_symm : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (f : ↥(lp (fun x => 𝕜) 2)),
  HasSum (fun i => ↑f i • b i) (b.repr.symm f)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modifyGetThe_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ α : Type u}
  {post : α → σ → Pred} {epost : EPred} (f : σ → α × σ),
  Std.Internal.Do.wp (modifyGetThe σ f) post epost = Std.Internal.Do.wp (MonadStateOf.modifyGet f) post epost
-- Init.Data.Format.Basic
Std.Format.MonadPrettyFormat.mk : {m : Type → Type} →
  (String → m Unit) → (ℕ → m Unit) → m ℕ → (ℕ → m Unit) → (ℕ → m Unit) → Std.Format.MonadPrettyFormat m
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.pos' : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < r
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.mk_val : ∀ {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (y : α) (h₁ : ↑u + y = 0) (h₂ : y + ↑u = 0),
  { val := ↑u, neg := y, val_neg := h₁, neg_val := h₂ } = u
-- Mathlib.Algebra.Order.Round
round.eq_1 : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (x : α),
  round x = if 2 * Int.fract x < 1 then ⌊x⌋ else ⌈x⌉
-- Init.Data.Int.OfNat
Nat.ToInt.of_eq : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → a = b → a' = b'
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- A variant of `hasBasis_nhds_zero` where `· ≠ 0` is unbundled.  -/
IsValuativeTopology.hasBasis_nhds_zero' : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R],
  (nhds 0).HasBasis (fun x => x ≠ 0) fun x => {x_1 | (ValuativeRel.valuation R) x_1 < x}
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.ne : Mathlib.Meta.Positivity.OrderRel✝
-- Init.Data.Fin.Lemmas
Fin.val_mk : ∀ {m n : ℕ} (h : m < n), ↑⟨m, h⟩ = m
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddCommSemigroup : {α : Type u_1} → [AddCommSemigroup α] → AddCommSemigroup αᵐᵒᵖ
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_multisetSum : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] (s : Multiset (WithLp p V)),
  s.sum.ofLp = (Multiset.map WithLp.ofLp s).sum
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃FunctorObj_obj : ∀ {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₂₃)),
  (CategoryTheory.bifunctorComp₂₃FunctorObj F).obj G₂₃ = CategoryTheory.bifunctorComp₂₃ F G₂₃
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.toNontrivial : ∀ {R : Type u} [self : EuclideanDomain R], Nontrivial R
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k ≠ ∅ → ∀ {fallback : α}, (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
-- Mathlib.Order.OmegaCompletePartialOrder
_private.Mathlib.Order.OmegaCompletePartialOrder.0.OmegaCompletePartialOrder.Chain.pair.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (x : ℕ) → motive x),
  (x = 0 → False) →
    (match x with
      | 0 => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instCompactSpaceElemCoeCompacts : ∀ {X : Type u_4} [inst : TopologicalSpace X] (K : TopologicalSpace.Compacts X), CompactSpace ↑↑K
-- Lean.Elab.DeprecatedArg
/-- Format the deprecation warning message for a deprecated argument.  -/
Lean.Elab.formatDeprecatedArgMsg : Lean.Elab.DeprecatedArgEntry → Lean.MessageData
-- Init.Data.FloatArray.Basic
FloatArray.instEmptyCollection : EmptyCollection FloatArray
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearEquiv_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.symm.toLinearEquiv = e.symm
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- A function with the property `IsMeasurableRatCDF`.
Used in a piecewise construction to convert a function which only satisfies the properties
defining `IsMeasurableRatCDF` on some set into a true `IsMeasurableRatCDF`.  -/
ProbabilityTheory.defaultRatCDF : ℚ → ℝ
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_eqOn_pow_div : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → Set.EqOn (fun x_1 => p.rpowIntegrand₀₁ x_1 x) (fun t => t ^ (p - 1) * x / (t + x)) (Set.Ioi 0)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_cons : ∀ {n : ℕ}, (*...=n).toArray = #[0] ++ (1...=n).toArray
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- If the universal vertices of a graph `G` decompose `G` into cliques such that the Tutte isn't
violated, then `G` has a perfect matching.  -/
SimpleGraph.Subgraph.IsPerfectMatching.exists_of_isClique_supp : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  Even (Nat.card V) →
    ¬G.IsTutteViolator G.universalVerts →
      (∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) →
        ∃ M, M.IsPerfectMatching
-- Init.Data.List.Attach
List.attach_filterMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β},
  (List.filterMap f l).attach =
    List.filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      l.attach
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuousConstVAdd.uniformContinuous_const_vadd : ∀ {M : Type v} {X : Type x} {inst : UniformSpace X} {inst_1 : VAdd M X} [self : UniformContinuousConstVAdd M X] (c : M),
  UniformContinuous fun x => c +ᵥ x
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ u v, b < G.edist u v
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α}, Std.DHashMap.Const.get? ∅ a = none
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_eq_top_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a b : WithTop α},
  a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.minView.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (l : Std.DTreeMap.Internal.Impl α β) →
            l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3) →
        (l : Std.DTreeMap.Internal.Impl α β) →
          (hl : l.Balanced) →
            (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size) →
              ((hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf hl hlr) →
                ((size : ℕ) →
                    (k' : α) →
                      (v' : β k') →
                        (l' r' : Std.DTreeMap.Internal.Impl α β) →
                          (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalancedAtRoot
                                  (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr) →
                  motive l hl hlr
-- Lean.Elab.ConfigEval.DeriveEvalTerm
/-- Resolves `id` as if it were a dotted identifier for namespace `c`,
and returns `s` if the resolved name is of the form `Name.str c s`.
 -/
_private.Lean.Elab.ConfigEval.DeriveEvalTerm.0.Lean.Elab.ConfigEval.EvalTerm.resolveDottedAtomicNameForConstNamespace : Lean.Name → Lean.Ident → Lean.Elab.TermElabM String
-- Init.Data.List.Nat.Modify
List.modify_eq_nil_iff : ∀ {α : Type u_1} {f : α → α} {i : ℕ} {l : List α}, l.modify i f = [] ↔ l = []
-- Mathlib.Order.Types.Defs
/-- `Quotient.inductionOn₂` specialized to `OrderType`.  -/
OrderType.inductionOn₂ : ∀ {C : OrderType.{u_1} → OrderType.{u_2} → Prop} (o₁ : OrderType.{u_1}) (o₂ : OrderType.{u_2}),
  (∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β],
      C (OrderType.type α) (OrderType.type β)) →
    C o₁ o₂
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a `CommMonoid` homomorphism `g : M →* P` where for Submonoids `S ⊆ M, T ⊆ P` we have
`g(S) ⊆ T`, the induced Monoid homomorphism from the Localization of `M` at `S` to the
Localization of `P` at `T`: if `f : M →* N` and `k : P →* Q` are Localization maps for `S` and
`T` respectively, we send `z : N` to `k (g x) * (k (g y))⁻¹`, where `(x, y) : M × S` are such
that `z = f x * (f y)⁻¹`.  -/
Submonoid.LocalizationMap.map : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} →
            [inst_2 : CommMonoid P] →
              S.LocalizationMap N →
                {g : M →* P} →
                  {T : Submonoid P} →
                    (∀ (y : ↥S), g ↑y ∈ T) → {Q : Type u_4} → [inst : CommMonoid Q] → T.LocalizationMap Q → N →* Q
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Rank-nullity theorem using `finrank` and subtraction.  -/
Submodule.finrank_quotient : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_2} R] [StrongRankCondition R] [Module.Finite R M] {S : Type u_1} [inst_6 : Ring S]
  [inst_7 : SMul R S] [inst_8 : Module S M] [inst_9 : IsScalarTower R S M] (N : Submodule S M),
  Module.finrank R (M ⧸ N) = Module.finrank R M - Module.finrank R ↥N
-- Init.Data.BitVec.Lemmas
BitVec.toNat_mul_toNat_lt : ∀ {w : ℕ} {x y : BitVec w}, x.toNat * y.toNat < 2 ^ (w * 2)