mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
/-- The counit isomorphism of the
equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ` .  -/
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).comp
          (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C) ≅
        CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)
-- Mathlib.Data.Rat.Lemmas
Rat.isSquare_natCast_iff : ∀ {n : ℕ}, IsSquare ↑n ↔ IsSquare n
-- Mathlib.Data.NNReal.Defs
/-- A version of `nnreal_induction_on` which splits into three cases (zero, positive and negative)
instead of two.  -/
Real.nnreal_induction_on' : ∀ {motive : ℝ → Prop},
  motive 0 →
    (∀ (x : NNReal), 0 < x → motive ↑x) → (∀ (x : NNReal), 0 < x → motive ↑x → motive (-↑x)) → ∀ (r : ℝ), motive r
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autGaloisSystem_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B),
  (CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f =
    GrpCat.ofHom (CategoryTheory.PreGaloisCategory.autMapHom f.val)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.epi_iff_surjective : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B),
  CategoryTheory.Epi f ↔ Function.Surjective ⇑(Rep.Hom.hom f)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.HasPushout.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.Limits.HasPushout f g = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMulOneClass : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : MulOneClass R] → [BoundedMul R] → [ContinuousMul R] → MulOneClass (BoundedContinuousFunction α R)
-- Lean.ResolveName
Lean.AliasState : Type
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_def : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F) (x : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.descFunLift F s x =
    match x with
    | RingCat.Colimits.Prequotient.of j x => (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
    | RingCat.Colimits.Prequotient.zero => 0
    | RingCat.Colimits.Prequotient.one => 1
    | x.neg => -RingCat.Colimits.descFunLift F s x
    | x.add y => RingCat.Colimits.descFunLift F s x + RingCat.Colimits.descFunLift F s y
    | x.mul y => RingCat.Colimits.descFunLift F s x * RingCat.Colimits.descFunLift F s y
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.lift₀_apply : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  {P : Type u_3} [inst_2 : CommMonoidWithZero P] (f : S.LocalizationMap N) (g : M →*₀ P)
  (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : N),
  (f.lift₀ g hg) x = g (f.sec x).1 * ↑((IsUnit.liftRight ((↑g).domRestrict S) hg) (f.sec x).2)⁻¹
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr →
  Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.Probability.Moments.Variance
/-- **Alias** of `ProbabilityTheory.ofReal_variance`. -/
MeasureTheory.MemLp.ofReal_variance_eq : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ
-- Mathlib.Order.Category.BddDistLat
/-- Constructs an equivalence between bounded distributive lattices from an order isomorphism
between them.  -/
BddDistLat.Iso.mk : {α β : BddDistLat} → ↑α.toDistLat ≃o ↑β.toDistLat → (α ≅ β)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} {l : List α} {k : α},
  Std.DTreeMap.Raw.Const.insertManyIfNewUnit t (k :: l) =
    Std.DTreeMap.Raw.Const.insertManyIfNewUnit (t.insertIfNew k ()) l
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence holds if and only if all extended distances are the same.  -/
congruent_iff_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Congruent v₁ v₂ ↔ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
-- Mathlib.Analysis.Normed.Group.AddTorsor
IsometryEquiv.vaddConst_symm_apply : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x p' : P), (IsometryEquiv.vaddConst x).symm p' = p' -ᵥ x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termY₂ : Lean.ParserDescr
-- Batteries.Data.List.Lemmas
List.countPBefore_nil : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ}, List.countPBefore p [] n = 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier (X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (f.hom.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U))))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U)) x) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- `S.map (cochainsFunctor k G)` is short exact in each degree.  -/
groupCohomology.map_cochainsFunctor_eval_shortExact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact →
    ∀ (n : ℕ),
      (X.map
          ((groupCohomology.cochainsFunctor k G).comp
            (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) n))).ShortExact
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_apply_one : ArithmeticFunction.moebius 1 = 1
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (h.iso m).inv.hom) m =
    ((CategoryTheory.Subobject.pullback (h.χ m)).obj h.Ω₀).arrow
-- Mathlib.Order.BoundedOrder.Lattice
top_inf_eq : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (a : α), ⊤ ⊓ a = a
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The cocone over the proposed colimit commutative group.  -/
CommGrpCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J CommGrpCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.basis_zero : ∀ (L : PeriodPair), L.basis 0 = L.ω₁
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.ext_iff : ∀ {x y : Std.Http.Header.Name}, x = y ↔ x.value = y.value
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instMax : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → Max (MeasureTheory.Filtration ι m)
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- If the derivative of x is 0, then it's in the range of `algebraMap A B`.  -/
Differential.ContainConstants.mem_range_of_deriv_eq_zero : ∀ {A : Type u_1} {B : Type u_2} {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B}
  {inst_3 : Differential B} [self : Differential.ContainConstants A B] {x : B}, x′ = 0 → x ∈ (algebraMap A B).range
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.snd = Monoid.Coprod.lift 1 (MonoidHom.id N)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωSup_le_ωSup_of_le : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {c₀ c₁ : OmegaCompletePartialOrder.Chain α},
  c₀ ≤ c₁ → OmegaCompletePartialOrder.ωSup c₀ ≤ OmegaCompletePartialOrder.ωSup c₁
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opEquivalence_functor : CategoryTheory.Cat.opEquivalence.functor = CategoryTheory.Cat.opFunctor
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedRing R] [HasSummableGeomSeries R]
  [inst_5 : NormedAlgebra 𝕜 R] {h : E → R},
  Differentiable 𝕜 h → (∀ (x : E), IsUnit (h x)) → Differentiable 𝕜 fun x => Ring.inverse (h x)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.diff : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  e.IsImage s t → e.IsImage s' t' → e.IsImage (s \ s') (t \ t')
-- Mathlib.Data.Sigma.Basic
Sigma.fst_injective_iff : ∀ {α : Type u_1} {β : α → Type u_4}, Function.Injective Sigma.fst ↔ ∀ (a : α), Subsingleton (β a)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Homotopy equivalent topological spaces have equivalent fundamental groupoids.  -/
FundamentalGroupoidFunctor.equivOfHomotopyEquiv : {X : Type u_3} →
  {Y : Type u_4} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        ContinuousMap.HomotopyEquiv X Y →
          (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of X)) ≌
            ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of Y)))
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {Y : C}
  {X : CategoryTheory.SimplicialObject C} {n b q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    ∀ (hnbq : n + 1 = b + q),
      AlgebraicTopology.DoldKan.HigherFacesVanish q (CategoryTheory.CategoryStruct.comp φ (X.σ ⟨b, ⋯⟩))
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.isCompact_setOfPred_clusterPt : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α},
  f.TotallyBounded → IsCompact {x | ClusterPt x f}
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hypType.injEq : ∀ (a : Lean.FVarId) (a_1 : Lean.SubExpr.Pos) (a_2 : Lean.FVarId) (a_3 : Lean.SubExpr.Pos),
  (Lean.SubExpr.GoalLocation.hypType a a_1 = Lean.SubExpr.GoalLocation.hypType a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.String.PosRaw
/-- Offsets `p` by `offset` on the left. This is not an `HAdd` instance because it should be a
relatively rare operation, so we use a name to make accidental use less likely. To offset a position
by the size of a character character `c` or string `s`, you can use `c + p` resp. `s + p`.

This should be seen as an operation that converts relative positions into absolute positions.

See also `Pos.Raw.increaseBy`, which is an "advancing" operation.
 -/
String.Pos.Raw.offsetBy : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- Given a vector `v` of length `n`, make a vector of length `n + 1` whose product is `1`,
by appending the inverse of the product of `v`.  -/
Equiv.Perm.VectorsProdEqOne.vectorEquiv : (G : Type u_2) → [inst : Group G] → (n : ℕ) → List.Vector G n ≃ ↑(Equiv.Perm.vectorsProdEqOne G (n + 1))
-- Std.Http.Protocol.H1
/-- Resolves an `Expect: 100-continue` decision.

When `status` is `100 Continue`, sends the interim response and advances to body
reading. For any other status, sends the rejection response (typically 417), disables
keep-alive, and closes the reader — the body will not be received.
 -/
Std.Http.Protocol.H1.Machine.canContinue : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Status → Std.Http.Protocol.H1.Machine dir
-- Init.Data.Int.Gcd
Int.gcd_sub_left_left_of_dvd : ∀ {m k : ℤ} (n : ℤ), m ∣ k → (k - n).gcd m = n.gcd m
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpToOn_zero_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.mk.inj : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} {inst : Finite ι} {inst_1 : CommRing R} {inst_2 : LieRing L}
  {inst_3 : LieAlgebra R L} {H : LieSubalgebra R L} {A : Matrix ι ι ℤ} {h e f : ι → L}
  {cartan_eq_lieSpan : H = LieSubalgebra.lieSpan R L (Set.range h)}
  {span_ef : LieSubalgebra.lieSpan R L (Set.range e ∪ Set.range f) = ⊤} {linInd : LinearIndependent R h}
  {nondegen : A.Nondegenerate} {sl2 : ∀ (i : ι), IsSl2Triple (h i) (e i) (f i)} {lie_h_h : ∀ (i j : ι), ⁅h i, h j⁆ = 0}
  {lie_h_e : ∀ (i j : ι), ⁅h j, e i⁆ = A i j • e i} {lie_h_f : ∀ (i j : ι), ⁅h j, f i⁆ = -A i j • f i}
  {lie_e_f_ne : ∀ (i j : ι), i ≠ j → ⁅e i, f j⁆ = 0} {A_1 : Matrix ι ι ℤ} {h_1 e_1 f_1 : ι → L}
  {cartan_eq_lieSpan_1 : H = LieSubalgebra.lieSpan R L (Set.range h_1)}
  {span_ef_1 : LieSubalgebra.lieSpan R L (Set.range e_1 ∪ Set.range f_1) = ⊤} {linInd_1 : LinearIndependent R h_1}
  {nondegen_1 : A_1.Nondegenerate} {sl2_1 : ∀ (i : ι), IsSl2Triple (h_1 i) (e_1 i) (f_1 i)}
  {lie_h_h_1 : ∀ (i j : ι), ⁅h_1 i, h_1 j⁆ = 0} {lie_h_e_1 : ∀ (i j : ι), ⁅h_1 j, e_1 i⁆ = A_1 i j • e_1 i}
  {lie_h_f_1 : ∀ (i j : ι), ⁅h_1 j, f_1 i⁆ = -A_1 i j • f_1 i} {lie_e_f_ne_1 : ∀ (i j : ι), i ≠ j → ⁅e_1 i, f_1 j⁆ = 0},
  { A := A, h := h, e := e, f := f, cartan_eq_lieSpan := cartan_eq_lieSpan, span_ef := span_ef, linInd := linInd,
        nondegen := nondegen, sl2 := sl2, lie_h_h := lie_h_h, lie_h_e := lie_h_e, lie_h_f := lie_h_f,
        lie_e_f_ne := lie_e_f_ne } =
      { A := A_1, h := h_1, e := e_1, f := f_1, cartan_eq_lieSpan := cartan_eq_lieSpan_1, span_ef := span_ef_1,
        linInd := linInd_1, nondegen := nondegen_1, sl2 := sl2_1, lie_h_h := lie_h_h_1, lie_h_e := lie_h_e_1,
        lie_h_f := lie_h_f_1, lie_e_f_ne := lie_e_f_ne_1 } →
    A = A_1 ∧ h = h_1 ∧ e = e_1 ∧ f = f_1
-- Init.Data.UInt.Lemmas
UInt16.sub_eq_iff_eq_add : ∀ {a b c : UInt16}, a - b = c ↔ a = c + b
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doLetArrow; doElems`
`doLetArrow` is of the form
```
"let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
```
where
```
def doIdDecl   := leading_parser ident >> optType >> leftArrow >> doElemParser
def doPatDecl  := leading_parser termParser >> optType >> leftArrow >> doElemParser >> optional ((" | " >> doSeq) >> optional doSeq)
```
 -/
Lean.Elab.Term.Do.ToCodeBlock.doLetArrowToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eVariationOn_rightLim_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α}, IsOpen s → eVariationOn (Function.rightLim f) s ≤ eVariationOn f s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).maxKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Order.SuccPred.Basic
Order.Iio_succ_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → Set.Iio (Order.succ a) = Set.Iic a
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsDownNat : (ComplexShape.down ℕ).EulerCharSigns
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The homotopy extension theorem: if `p : A ⟶ X` is a cofibration,
`l₀ : X ⟶ B` is a morphism, if there is a right homotopy `h` between
the composition `f₀ := i ≫ l₀` and a morphism `f₁ : A ⟶ B`,
then there exists a morphism `l₁ : X ⟶ B` and a right homotopy `h'` from
`l₀` to `l₁` which is compatible with `h` (in particular, `i ≫ l₁ = f₁`).  -/
HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A B X : C}
  {P : HomotopicalAlgebra.PathObject B} {f₀ f₁ : A ⟶ B} [HomotopicalAlgebra.IsFibrant B] [P.IsGood]
  (h : P.RightHomotopy f₀ f₁) (i : A ⟶ X) [HomotopicalAlgebra.Cofibration i] (l₀ : X ⟶ B),
  autoParam (CategoryTheory.CategoryStruct.comp i l₀ = f₀)
      HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension._auto_1 →
    ∃ l₁ h', CategoryTheory.CategoryStruct.comp i h'.h = h.h
-- Mathlib.Data.Nat.Init
Or.by_cases.eq_1 : ∀ {p q : Prop} [inst : Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α),
  h.by_cases h₁ h₂ = if hp : p then h₁ hp else h₂ ⋯
-- Mathlib.Analysis.Normed.Algebra.Spectrum
Real.spectralRadius_mem_spectrum_or : ∀ {A : Type u_4} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {a : A},
  (spectrum ℝ a).Nonempty → (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : G ⟶ F)
  {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).map f).f = f.f
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
intervals `Ioo (-N) N`· Note that for `G = ℤ` this coincides with
`symmetricIcc` so one should use that. See `symmetricIcc_eq_symmetricIoo_int`.  -/
SummationFilter.symmetricIoo : (G : Type u_1) → [Neg G] → [inst : Preorder G] → [LocallyFiniteOrder G] → SummationFilter G
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_iterate_succ_le : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} (n : ℕ), toZ i0 (Order.succ^[n] i0) ≤ ↑n
-- Mathlib.Tactic.SetNotationForOrder
/-- A temporary linter to help adapt to `@[set_notation_for_order]`.
It gives a warning when a lemma is in the wrong namespace for dot-notation.  -/
Mathlib.Meta.SetNotationForOrder.subsetDotNotationLinter : Batteries.Tactic.Lint.Linter
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_adjoin : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  (Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {fallback : α},
  ∅.minKeyD fallback = fallback
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [W.HasLeftCalculusOfFractions] →
        CategoryTheory.Category.{max u_1 v_1, u_1} (CategoryTheory.MorphismProperty.LeftFraction.Localization W)
-- Mathlib.Data.List.Forall2
List.right_unique_forall₂' : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop},
  Relator.RightUnique R → ∀ {a : List α} {b c : List β}, List.Forall₂ R a b → List.Forall₂ R a c → b = c
-- Aesop.Rule.Name
Aesop.instHashableBuilderName : Hashable Aesop.BuilderName
-- Mathlib.Geometry.RingedSpace.SheafedSpace
TopCat.Presheaf.stalkCongr.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y : ↑X} (e : Inseparable x y), F.stalkCongr e = F.stalkCongr e
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instNonUnitalSubsemiringClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A],
  NonUnitalSubsemiringClass (NonUnitalSubalgebra R A) A
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.vadd_subset : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α} {x : α},
  IsUpperSet s → 0 ≤ x → x +ᵥ s ⊆ s
-- Mathlib.Topology.Maps.Basic
IsOpenMap.accPt_comap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {x : X} {l : Filter Y}, AccPt (f x) l → AccPt x (Filter.comap f l)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.coe_le_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupNorm E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.equiv'.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (g : Polynomial R)
  (pb pb_1 : PowerBasis R S) (e_pb : pb = pb_1) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0)
  (h₂ : (Polynomial.aeval pb.gen) g = 0), AdjoinRoot.equiv' g pb h₁ h₂ = AdjoinRoot.equiv' g pb_1 ⋯ ⋯
-- Mathlib.Data.Finset.Sort
Finset.listMap_orderEmbOfFin_finRange : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k),
  List.map (⇑(s.orderEmbOfFin h)) (List.finRange k) = s.sort fun a b => a ≤ b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff! m₂).getKeyD k fallback = fallback
-- Mathlib.Geometry.Euclidean.Incenter
/-- Whether an excenter exists with a given choice of signs.  -/
Affine.Simplex.ExcenterExists : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → Prop
-- Mathlib.Algebra.Order.Field.Basic
le_div_iff_of_neg' : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (a ≤ b / c ↔ b ≤ c * a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k fallback : α},
  (Std.DHashMap.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback