mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- Up to homotopy, the category of `1`-hypercovers is cofiltered.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {E : J.OneHypercover S} {F : J.OneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F),
  ∃ W h,
    Nonempty
      (CategoryTheory.PreOneHypercover.Homotopy (CategoryTheory.PreOneHypercover.Hom.comp h f)
        (CategoryTheory.PreOneHypercover.Hom.comp h g))
-- Mathlib.Algebra.Group.Basic
vadd_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd β α] (p : Prop) [inst_1 : Decidable p] (a b : α) (c : β),
  (c +ᵥ if p then a else b) = if p then c +ᵥ a else c +ᵥ b
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_right_eball : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x + a) ⁻¹' Metric.eball b r = Metric.eball (b - a) r
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.constGetThenInsertIfNew?₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} {h : 0 < m.buckets.size} {a : α}
  {b : β} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Context : Type
-- Init.Data.Int.Gcd
Int.zero_gcd : ∀ {a : ℤ}, Int.gcd 0 a = a.natAbs
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.type : Lean.Compiler.LCNF.CtorInfo → Lean.Expr
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.ExceptT.run_bind.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok x with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_1 x
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
_private.Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange.0.tacticMap_simp : Lean.ParserDescr
-- Lean.Declaration
Lean.Declaration.inductDecl.sizeOf_spec : ∀ (lparams : List Lean.Name) (nparams : ℕ) (types : List Lean.InductiveType) (isUnsafe : Bool),
  sizeOf (Lean.Declaration.inductDecl lparams nparams types isUnsafe) =
    1 + sizeOf lparams + sizeOf nparams + sizeOf types + sizeOf isUnsafe
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_tdiv : ∀ {a b : ℤ}, a / b = a.tdiv b - if 0 ≤ a ∨ b ∣ a then 0 else b.sign
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_neg : ∀ {ι : Type u_1} {M : Type u_3} [inst : Ring M] (f : AddMonoidAlgebra M ι), (-f).toDirectSum = -f.toDirectSum
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the auxiliary object of a right fraction  -/
CategoryTheory.MorphismProperty.RightFraction.X' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.RightFraction X Y → C
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Two formal power series are equal if all their coefficients are equal.  -/
PowerSeries.ext : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R},
  (∀ (n : ℕ), (PowerSeries.coeff n) φ = (PowerSeries.coeff n) ψ) → φ = ψ
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The completion is complete.  -/
AbstractCompletion.complete : ∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion.{v, u} α), CompleteSpace self.space
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.vadd_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : VAdd K β] (k : K)
  (f : MeasureTheory.SimpleFunc α β) (a : α), (k +ᵥ f) a = k +ᵥ f a
-- Init.Prelude
instHMul : {α : Type u_1} → [Mul α] → HMul α α α
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.finsetClopens.congr_simp : ∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (d d_1 : DiscreteQuotient X),
  d = d_1 → DiscreteQuotient.finsetClopens X d = DiscreteQuotient.finsetClopens X d_1
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_strictMono : ∀ {M : Type u_1} [inst : AddMonoid M], StrictMono AddSubgroup.ofAddUnits
-- Aesop.Forward.SlotIndex
Aesop.instLESlotIndex : LE Aesop.SlotIndex
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_leadingCoeff_of_le : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α} {g : Γ} {a : α},
  ↑g = (s a).orderTop →
    (∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g') →
      (∀ (b : α), b ≠ a → (s b).coeff g = 0) → s.hsum.leadingCoeff = (s a).coeff g
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousAt_iff_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {x : α} [inst_1 : TopologicalSpace β],
  UpperHemicontinuousAt f x ↔ ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhds x
-- Mathlib.CategoryTheory.Action.Monoidal
Action.tensorObj_V : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V = CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.Bind.f.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Computation α ⊕ Computation β → Sort u_3) →
      (x : Computation α ⊕ Computation β) →
        ((ca : Computation α) → motive (Sum.inl ca)) → ((cb : Computation β) → motive (Sum.inr cb)) → motive x
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsClosedImmersion
  @AlgebraicGeometry.IsSeparated
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection on the base of a fiber bundle created from core is an open map  -/
FiberBundleCore.isOpenMap_proj : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F), IsOpenMap Z.proj
-- Lean.Level
Lean.Level.getOffset : Lean.Level → ℕ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKey!ₘ_eq_getKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  [inst_4 : Inhabited α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.getKey!ₘ k = Std.Internal.List.getKey! k t.toListModel
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.mkUnsafeCastTo : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.GaloisConnection.Basic
/-- `sSup` and `Iic` form a Galois insertion.  -/
giSSupIic : {α : Type u} → [inst : CompleteSemilatticeSup α] → GaloisInsertion sSup Set.Iic
-- Aesop.Frontend.Extension.Init
Aesop.DeclaredRuleSets.mk : Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name) →
  Std.HashSet Aesop.RuleSetName → Aesop.DeclaredRuleSets
-- Mathlib.Data.Finset.DenselyOrdered
Finset.exists_between' : ∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α] (s t : Finset α) [NoMaxOrder α] [NoMinOrder α] [Nonempty α],
  (∀ x ∈ s, ∀ y ∈ t, x < y) → ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
-- Mathlib.Topology.ClusterPt
notMem_closure_iff_nhdsWithin_eq_bot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∉ closure s ↔ nhdsWithin x s = ⊥
-- Mathlib.Algebra.Star.Basic
star_intCast : ∀ {R : Type u} [inst : NonAssocRing R] [inst_1 : StarRing R] (z : ℤ), star ↑z = ↑z
-- Init.Data.String.ToSlice
String.ToSlice.mk : {α : Type u} → (α → String.Slice) → String.ToSlice α
-- Lean.DocString.Types
/-- Embedded TeX math, to be rendered by an engine such as TeX or KaTeX. The `mode` determines whether
it is rendered in inline mode or display mode; even display-mode math is an inline element for
purposes of document structure.
 -/
Lean.Doc.Inline.math : {i : Type u} → Lean.Doc.MathMode → String → Lean.Doc.Inline i
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_eq_add_sum : ∀ {R : Type u_1} {a b u₀ : R} [inst : CommSemiring R] (n : ℕ),
  arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.comap_isNonloop_iff : ∀ {α : Type u_1} {β : Type u_2} {e : α} {M : Matroid β} {f : α → β}, (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flip_flip : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N), P.flip.flip = P
-- Mathlib.RepresentationTheory.Induced
Rep.indMap.eq_1 : ∀ {k : Type u} {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B),
  Rep.indMap φ f =
    Rep.ofHom
      {
        toLinearMap :=
          Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
            (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
            { toLinearMap := LinearMap.lTensor (MonoidAlgebra k H) (Rep.Hom.hom f).toLinearMap, isIntertwining' := ⋯ },
        isIntertwining' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.instFintypeWalkingParallelPairHom : (j j' : CategoryTheory.Limits.WalkingParallelPair) → Fintype (CategoryTheory.Limits.WalkingParallelPairHom j j')
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β),
  ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).hom.app X).f i =
    CategoryTheory.CategoryStruct.id (X.X i)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the first vector passed to `oangle` by a negative real produces the same angle
as negating that vector.  -/
Orientation.oangle_smul_left_of_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ}, r < 0 → o.oangle (r • x) y = o.oangle (-x) y
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.comm_sq₂ : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7}
  {W₃ : Type u_8} [inst_3 : SeminormedAddCommGroup W₁] [inst_4 : SeminormedAddCommGroup W₂]
  [inst_5 : SeminormedAddCommGroup W₃] {f₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂}
  {f₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂}
  {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃},
  ψ.comp f₁ = f₂.comp φ → ψ'.comp f₂ = f₃.comp φ' → (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_mul_eq_inter : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω},
  MeasurableSet s →
    ∀ (t : Set Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ], μ[t | s] * μ s = μ (s ∩ t)
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.ker_coeAddHom : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F), AddCon.ker ↑f = AddCon.ker f
-- Std.Internal.Parsec.ByteArray
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.skipWs : ByteArray.Iterator → ByteArray.Iterator
-- Mathlib.Data.Nat.Squarefree
_private.Mathlib.Data.Nat.Squarefree.0.Nat.minSqFacAux.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (n k : ℕ) (h_1 : (n k : ℕ) → motive n k),
  (match n, k with
    | n, k => h_1 n k) =
    h_1 n k
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- a morphism `S₁.X₃ ⟶ S₂.X₂`  -/
CategoryTheory.ShortComplex.Homotopy.h₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} → CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → (S₁.X₃ ⟶ S₂.X₂)
-- Std.Internal.Do.Order.Basic
Lean.Order.le_iInf : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {ι : Type v} (f : ι → α) (x : α),
  (∀ (i : ι), Lean.Order.PartialOrder.rel x (f i)) → Lean.Order.PartialOrder.rel x (Lean.Order.iInf f)
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_last : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M), b.flag (Fin.last n) = ⊤
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
/-- A localizer morphism `Φ : LocalizerMorphism W₁ W₂` is a right derivability
structure if it has right resolutions and the 2-square where the left and right functors
are localization functors for `W₁` and `W₂` are Guitart exact.  -/
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mem_toSubmonoid : ∀ {R : Type u} [inst : NonAssocRing R] {s : Subring R} {x : R}, x ∈ s.toSubmonoid ↔ x ∈ s
-- Init.System.IO
IO.FileRight.mk.sizeOf_spec : ∀ (user group other : IO.AccessRight),
  sizeOf { user := user, group := group, other := other } = 1 + sizeOf user + sizeOf group + sizeOf other
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk.sizeOf_spec : ∀ {ι : Type u_2} [inst : SizeOf ι] (lower upper : ι → ℝ) (lower_lt_upper : ∀ (i : ι), lower i < upper i),
  sizeOf { lower := lower, upper := upper, lower_lt_upper := lower_lt_upper } = 1
-- Init.Data.UInt.Bitwise
USize.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : USize}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.underObj_ind_eq_ind_underObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (X : C),
  P.ind.underObj = P.underObj.ind
-- Mathlib.Lean.Meta.Simp
/-- Construct a `SimpTheorems` from a list of names.  -/
Lean.Meta.simpTheoremsOfNames : optParam (List Lean.Name) [] → optParam Bool false → Lean.MetaM Lean.Meta.SimpTheorems
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.toFormula.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂).toFormula = t₁.equal t₂
-- Init.Data.Int.Lemmas
Int.neg_ofNat_succ : ∀ (n : ℕ), -↑n.succ = Int.negSucc n
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- The conjugate transpose of a matrix defined in term of `star`.  -/
Matrix.«term_ᴴ» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- A morphism factors through the image sheaf.  -/
CategoryTheory.Sheaf.toImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F F' : CategoryTheory.Sheaf J (Type w)} → (f : F ⟶ F') → F ⟶ CategoryTheory.Sheaf.image f
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- The natural isomorphism `RF ≅ RF'` on right derived functors that is
induced by a natural isomorphism `F ≅ F'`.  -/
CategoryTheory.Functor.rightDerivedNatIso : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (RF RF' : CategoryTheory.Functor D H) →
              {F F' : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : F ⟶ L.comp RF) →
                    (α' : F' ⟶ L.comp RF') →
                      (W : CategoryTheory.MorphismProperty C) →
                        [inst_3 : L.IsLocalization W] →
                          [RF.IsRightDerivedFunctor α W] → [RF'.IsRightDerivedFunctor α' W] → (F ≅ F') → (RF ≅ RF')
-- Lean.Elab.Do.Legacy
/-- Given `stx` which is a `letPatDecl`, `letEqnsDecl`, or `letIdDecl`, return true if it has binders.  -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.letDeclArgHasBinders : Lean.Syntax → Bool
-- Mathlib.Order.Filter.Pi
Filter.pi_inf_principal_pi_eq_bot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (i : ι), (f i).NeBot]
  {I : Set ι}, Filter.pi f ⊓ Filter.principal (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ Filter.principal (s i) = ⊥
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.sl2SubalgebraOfRoot.congr_simp : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  {α α_1 : LieModule.Weight K (↥H) L} (e_α : α = α_1) (hα : α.IsNonZero),
  LieAlgebra.IsKilling.sl2SubalgebraOfRoot hα = LieAlgebra.IsKilling.sl2SubalgebraOfRoot ⋯
-- Mathlib.GroupTheory.Torsion
/-- A nontrivial torsion-free additive abelian group is not torsion.  -/
not_isAddTorsion_of_isAddTorsionFree : ∀ {G : Type u_1} [inst : AddCommGroup G] [Nontrivial G] [IsAddTorsionFree G], ¬IsAddTorsion G
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_3.eq_1 : ∀ (motive : List String → List String → Sort u_1) (h_1 : Unit → motive [] [])
  (h_2 : (x : String) → (s : List String) → motive [] (x :: s))
  (h_3 : (pre : String) → (l s' : List String) → motive (pre :: l) s'),
  (match [], [] with
    | [], [] => h_1 ()
    | [], x :: s => h_2 x s
    | pre :: l, s' => h_3 pre l s') =
    h_1 ()
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The functor `Cᵒᵖ ⥤ C ⥤ AddCommGrpCat` which sends `X : C` and `Y : C`
to `Ext X Y n`.  -/
CategoryTheory.Abelian.extFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.HasExt C] → ℕ → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C AddCommGrpCat)
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.of_comp_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m)
  [inst_5 : IsAdicComplete I N],
  AdicCompletion.of I N ∘ₗ IsAdicComplete.StrictMono.lift I ha f ⋯ =
    AdicCompletion.lift I (IsAdicComplete.StrictMono.extend ha f) ⋯
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.posRootForm_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [inst_7 : IsStrictOrderedRing S] [inst_8 : Algebra S R]
  [inst_9 : FaithfulSMul S R] [inst_10 : Module S M] [inst_11 : IsScalarTower S R M] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι], (P.posRootForm S).posForm = P.RootFormIn S
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftEq_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l')
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftEq R l l' h hl).hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Products.max_eq_eval : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
  [inst_2 : Inhabited I] (l : Profinite.NobelingProof.Products I),
  ↑l ≠ [] →
    (↑l).head! = Profinite.NobelingProof.term I ho →
      (Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C l) =
        Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) l.Tail
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_nonneg : ∀ (p : Polynomial ℂ), 0 ≤ p.mahlerMeasure
-- Mathlib.NumberTheory.WellApproximable
/-- In a seminormed group `A`, given a sequence of distances `δ₁, δ₂, ...`, `wellApproximable A δ`
is the limsup as `n → ∞` of the sets `approxOrderOf A n δₙ`. Thus, it is the set of points that
lie in infinitely many of the sets `approxOrderOf A n δₙ`.  -/
wellApproximable : (A : Type u_1) → [SeminormedGroup A] → (ℕ → ℝ) → Set A
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R), x.divMonomial 0 = x
-- Mathlib.Analysis.RCLike.BoundedContinuous
BoundedContinuousFunction.AlgHom.compLeftContinuousBounded.congr_simp : ∀ {α : Type u} {β : Type v} {γ : Type w} (𝕜 : Type u_1) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedRing γ] [inst_3 : NormedAlgebra 𝕜 γ] [inst_4 : NormedRing β] [inst_5 : NormedAlgebra 𝕜 β]
  (g g_1 : β →ₐ[𝕜] γ) (e_g : g = g_1) {C C_1 : NNReal} (e_C : C = C_1) (hg : LipschitzWith C ⇑g),
  BoundedContinuousFunction.AlgHom.compLeftContinuousBounded 𝕜 g hg =
    BoundedContinuousFunction.AlgHom.compLeftContinuousBounded 𝕜 g_1 ⋯
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.connectionClosed.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.connectionClosed = 1
-- Mathlib.Logic.Function.Basic
Function.Surjective.of_comp_left : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Surjective (f ∘ g) → Function.Injective f → Function.Surjective g
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instContinuousLinearMapClassWeakDual : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.tendsto_integral_Ico_integral_Ici : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E} (b : ℝ),
  MeasureTheory.IntegrableOn f (Set.Ici b) μ →
    Filter.Tendsto a l Filter.atTop →
      Filter.Tendsto (fun i => ∫ (x : ℝ) in Set.Ico b (a i), f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Ici b, f x ∂μ))
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_insert_of_mem : ∀ {y z : PSet.{u_1}} (x : PSet.{u_1}), z ∈ y → z ∈ insert x y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_none_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey? = none ↔ t = ∅