mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.reflects_cone_isomorphism`.

---

If `F` reflects isomorphisms, then `functoriality F` reflects isomorphisms
as well.
 -/
CategoryTheory.Limits.Cones.reflects_cone_isomorphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms]
  (K : CategoryTheory.Functor J C), (CategoryTheory.Limits.Cone.functoriality K F).ReflectsIsomorphisms
-- Init.Data.Array.Basic
/-- Applies a function to the corresponding elements of two arrays, stopping at the end of the shorter
array.

Examples:
* `#[1, 2].zipWith (· + ·) #[5, 6] = #[6, 8]`
* `#[1, 2, 3].zipWith (· + ·) #[5, 6, 10] = #[6, 8, 13]`
* `#[].zipWith (· + ·) #[5, 6] = #[]`
* `#[x₁, x₂, x₃].zipWith f #[y₁, y₂, y₃, y₄] = #[f x₁ y₁, f x₂ y₂, f x₃ y₃]`
 -/
Array.zipWith : {α : Type u} → {β : Type u_1} → {γ : Type u_2} → (α → β → γ) → Array α → Array β → Array γ
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Pred.0.String.Slice.Pattern.Model.split.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (pos : s.Pos)
  (h_1 : (pos_1 : s.Pos) → some pos = some pos_1 → motive (some pos_1)) (h_2 : some pos = none → motive none),
  (match hd : some pos with
    | some pos_1 => h_1 pos_1 hd
    | none => h_2 hd) =
    h_1 pos ⋯
-- Mathlib.Topology.ContinuousOn
ContinuousOn.comp_inter : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {g : β → γ} {t : Set β},
  ContinuousOn g t → ContinuousOn f s → ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t)
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.monotone_dom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Monotone fun f => f.dom
-- Mathlib.Algebra.Group.Opposite
AddOpposite.unop_nsmul : ∀ {α : Type u_1} [inst : AddMonoid α] (x : αᵃᵒᵖ) (n : ℕ), AddOpposite.unop (n • x) = n • AddOpposite.unop x
-- Mathlib.Topology.Inseparable
specializes_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y},
  (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
-- Mathlib.Algebra.Group.Submonoid.Units
ofAddUnits_le_iff_le_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (H : AddSubgroup (AddUnits M)),
  H.ofAddUnits ≤ S ↔ H ≤ S.addUnits
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂_map_left_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  {X Y :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)}
  (φ : X ⟶ Y) (X_1 : D),
  ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).map φ).left.app X_1 = G.map (φ.left.app X_1)
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.AddSubmonoidClass.IsHomogeneous.ext : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] {ℳ : ι → σ} [inst_4 : DirectSum.Decomposition ℳ] {P : Type u_5}
  [inst_5 : SetLike P M] [AddSubmonoidClass P M] {p q : P},
  DirectSum.SetLike.IsHomogeneous ℳ p →
    DirectSum.SetLike.IsHomogeneous ℳ q → (∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q) → p = q
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `B` contains `A` if and only if `B` has a subgraph `B'` and `B'` is isomorphic to `A`.  -/
SimpleGraph.isContained_iff_exists_iso_subgraph : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β}, A.IsContained B ↔ ∃ B', Nonempty (A ≃g B'.coe)
-- Mathlib.Data.Set.Card.Arithmetic
Finset.set_encard_biUnion_le : ∀ {α : Type u_1} {ι : Type u_2} (t : Finset ι) (s : ι → Set α), (⋃ i ∈ t, s i).encard ≤ ∑ i ∈ t, (s i).encard
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.Contradiction.Config.mk : Bool → Bool → ℕ → Bool → Lean.Meta.Contradiction.Config
-- Init.Data.Dyadic.Basic
Dyadic.instIsLinearPreorder : Std.IsLinearPreorder Dyadic
-- Mathlib.CategoryTheory.Equivalence
/-- As a special case, given two equivalences `G` and `G'` between the same categories,
construct an isomorphism `G.inverse ≅ G.inverse` from an isomorphism `G.functor ≅ G.functor`.  -/
CategoryTheory.Iso.isoInverseOfIsoFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {G G' : C ≌ D} → (G.functor ≅ G'.functor) → (G.inverse ≅ G'.inverse)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.exists_of_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
-- Init.Data.SInt.Lemmas
ISize.le_toInt : ∀ (x : ISize), -2 ^ 63 ≤ x.toInt
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.modify.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : β → β),
  Std.DTreeMap.Internal.Impl.Const.modify k f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Algebra.Lie.Prod
LieHom.coe_prod : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
/-- The functor mapping an object `X : Over I` to the object of sections of `X` over `I`, defined
by the following pullback diagram. The functor's mapping of morphisms is induced by `pullbackMap`,
that is by the universal property of chosen pullbacks.

```
 sections X -->  I ⟹ X
   |               |
   |               |
   v               v
  𝟙_ C   ----->  I ⟹ I
```
 -/
CategoryTheory.Over.sections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (I : C) →
        [inst_2 : CategoryTheory.Closed I] →
          [CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)] →
            CategoryTheory.Functor (CategoryTheory.Over I) C
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_symm_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ),
  (CategoryTheory.yonedaEquiv.symm x).app Y =
    TypeCat.ofHom fun f => (CategoryTheory.ConcreteCategory.hom (F.map (Quiver.Hom.op f))) x
-- Mathlib.Logic.Equiv.Fintype
Equiv.extendSubtype_mem : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : Finite ↑{x | p x}]
  (e : { x // p x } ≃ { x // q x }) (x : α), p x → q (e.extendSubtype x)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_compl' : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] (s : Set α) (f : α → G), sᶜ.indicator f = f + -s.indicator f
-- Mathlib.RingTheory.Localization.Away.AdjoinRoot
Algebra.FinitePresentation.of_isLocalizationAway : ∀ {R : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing S']
  [inst_3 : Algebra R S] [inst_4 : Algebra R S'] [inst_5 : Algebra S S'] [IsScalarTower R S S'] (f : S)
  [IsLocalization.Away f S'] [Algebra.FinitePresentation R S], Algebra.FinitePresentation R S'
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `IsometryEquiv.image_closedEBall`. -/
IsometryEquiv.image_emetric_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α)
  (r : ENNReal), ⇑h '' Metric.closedEBall x r = Metric.closedEBall (h x) r
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.bind_assoc : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x}
  {x : Std.Iterators.HetT m α} {f : α → Std.Iterators.HetT m β} {g : β → Std.Iterators.HetT m γ},
  (x.bind f).bind g = x.bind fun a => (f a).bind g
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.get?_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α fun x => β} {a : α},
  Std.DHashMap.Internal.AssocList.get? a l = Std.Internal.List.getValue? a l.toList
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.algebraMap_apply : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (r : R), (algebraMap R (MvPolynomial σ S₁)) r = MvPolynomial.C ((algebraMap R S₁) r)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instSMul : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → [SMul R T] → SMul (WithAbs v) T
-- Mathlib.Algebra.Group.Even
instDecidablePredMulOppositeIsSquare : {α : Type u_2} → [inst : Mul α] → [DecidablePred IsSquare] → DecidablePred IsSquare
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- The bifunctor which sends an abelian sheaf `F` and an object `U` to the
`n`th Ext-group from the free abelian sheaf generated by the
presheaf of sets `yoneda.obj U` to `F`.  -/
CategoryTheory.Sheaf.cohomologyPresheafFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          ℕ → CategoryTheory.Functor (CategoryTheory.Sheaf J AddCommGrpCat) (CategoryTheory.Functor Cᵒᵖ AddCommGrpCat)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMap_tprod_eq_map : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i),
  PiTensorProduct.piTensorHomMap ((PiTensorProduct.tprod R) f) = PiTensorProduct.map f
-- Mathlib.Data.Set.Operations
Set.mem_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ s
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_insertRupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (f.insertRupUnits units).1.clauses = f.clauses
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.comp_continuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {γ : Type u_3}
  [inst_2 : TopologicalSpace γ], Isometry f → ∀ {g : γ → α}, Continuous (f ∘ g) ↔ Continuous g
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_ne_one : ∀ (z : Complex.UnitDisc), ↑z ≠ 1
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.apply_symm_apply : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (y : β),
  h (h.symm y) = y
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.Hom.ext : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} {f g : A ⟶ B}, f.right = g.right → f = g
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceGT : Lean.Meta.Simp.Simproc
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatMarkerNarrow : Std.Time.DateFormatSymbols → Std.Time.HourMarker → String
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.tendsto_nhds_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_3} {f : OnePoint X → α} {l : Filter α},
  Filter.Tendsto f (nhds OnePoint.infty) l ↔
    ∀ s ∈ l, f OnePoint.infty ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ Action V G` preserves limits of some shape `J`
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`.  -/
Action.preservesLimitsOfShape_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp (Action.forget V G)) →
    CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- The target object  -/
CategoryTheory.Dial.tgt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] → CategoryTheory.Dial C → C
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal`.

---

The norm of a maximal ideal as an element of `ℝ≥0` is `> 1`  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], 1 < ↑(Ideal.absNorm v.asIdeal)
-- Mathlib.CategoryTheory.Action
CategoryTheory.actionAsFunctor_obj : ∀ (M : Type u_1) [inst : Monoid M] (X : Type u) [inst_1 : MulAction M X] (x : CategoryTheory.SingleObj M),
  (CategoryTheory.actionAsFunctor M X).obj x = X
-- Mathlib.FieldTheory.Fixed
FixedBy.subfield.eq_1 : ∀ {M : Type u} [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F] (m : M),
  FixedBy.subfield F m =
    { carrier := MulAction.fixedBy F m, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯,
      inv_mem' := ⋯ }
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_comp_const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜),
  (iteratedDeriv n fun z => f (s - z)) = fun t => (-1) ^ n • iteratedDeriv n f (s - t)
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_of_univ_subsingleton : ∀ {α : Type u}, Set.univ.Subsingleton → Subsingleton α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The ideal sheaf induced by an ideal of the global sections.  -/
AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop : {X : AlgebraicGeometry.Scheme} → Ideal ↑(X.presheaf.obj (Opposite.op ⊤)) → X.IdealSheafData
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.compLeft_compRight : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (l r : M →ₗ[R] M), (B.compLeft l).compRight r = B.comp l r
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_two_pi : Complex.cos (2 * ↑Real.pi) = 1
-- Mathlib.Order.Filter.Lift
Filter.lift_map_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Filter γ} {m : α → β},
  (Filter.map m f).lift g ≤ f.lift (g ∘ Set.image m)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_rightUnitor : ∀ {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.NatIso.unop F.rightUnitor =
    F.unop.rightUnitor.symm ≪≫
      F.unop.isoWhiskerLeft (CategoryTheory.Functor.unopId D).symm ≪≫ (F.unopComp (CategoryTheory.Functor.id Dᵒᵖ)).symm
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult.mk : Lean.Expr → Lean.Expr → Lean.Elab.Term.MkInstResult✝
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Positive part of a simple function in L1 space.  -/
MeasureTheory.L1.SimpleFunc.posPart : {α : Type u_1} → {m : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → ↥(α →₁ₛ[μ] ℝ) → ↥(α →₁ₛ[μ] ℝ)
-- Mathlib.RingTheory.NoetherNormalization
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.sum_r_mul_ne : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v w : Fin (n + 1) →₀ ℕ),
  (∀ (i : Fin (n + 1)), v i < 2 + f.totalDegree) →
    (∀ (i : Fin (n + 1)), w i < 2 + f.totalDegree) →
      v ≠ w → ∑ x, (fun i => (2 + f.totalDegree) ^ ↑i) x * v x ≠ ∑ x, (fun i => (2 + f.totalDegree) ^ ↑i) x * w x
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_eq_liminf : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
  Filter.bliminf u f p = Filter.liminf u (f ⊓ Filter.principal {x | p x})
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoShortComplexH2_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.isoShortComplexH2 A).hom =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 1 2 3 groupCohomology.isoShortComplexH2._proof_1
              groupCohomology.isoShortComplexH2._proof_2).hom.app
        (groupCohomology.inhomogeneousCochains A))
      (CategoryTheory.ShortComplex.isoMk (groupCohomology.cochainsIso₁ A) (groupCohomology.cochainsIso₂ A)
          (groupCohomology.cochainsIso₃ A) ⋯ ⋯).hom
-- Mathlib.Algebra.Group.ULift
ULift.addRightCancelSemigroup : {α : Type u} → [AddRightCancelSemigroup α] → AddRightCancelSemigroup (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.ofIdComp_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)),
  t.ofIdComp.left = t.lift
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α}
  {h : k ∈ Std.ExtTreeSet.filter f t}, (Std.ExtTreeSet.filter f t).get k h = t.get k ⋯
-- Mathlib.Data.Set.Function
Set.SurjOn.rightInvOn_invFunOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.SurjOn f s t → Set.RightInvOn (Function.invFunOn f s) f t
-- Mathlib.Topology.VectorBundle.Riemannian
IsContinuousRiemannianBundle.mk : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F : Type u_2} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_3} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E],
  (∃ g, (Continuous fun x => ⟨x, g x⟩) ∧ ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w) →
    IsContinuousRiemannianBundle F E
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associator_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.f =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.contDiffOn_inv_linear : ∀ (k : ℕ) (d : ℤ), ContDiffOn ℂ (↑k) (fun z => 1 / (z + ↑d)) Complex.integerComplement
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.sqLe_add_mixed : ∀ {c d x y z w : ℕ}, Zsqrtd.SqLe x c y d → Zsqrtd.SqLe z c w d → c * (x * z) ≤ d * (y * w)
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.coe_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Type u_3}
  [inst_2 : FunLike F X Y] [inst_3 : ContinuousMapClass F X Y] (f : F) (x : X), ↑f x = f x
-- Mathlib.ModelTheory.Topology.Types
CompleteType.isTopologicalBasis_range_typesWith : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1}, TopologicalSpace.IsTopologicalBasis (Set.range T.typesWith)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Set.Countable.exists_cycleOn : ∀ {α : Type u_2} {s : Set α}, s.Countable → ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s
-- Mathlib.Order.Hom.Lattice
/-- Composition of `InfHom`s as an `InfHom`.  -/
InfHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Min α] → [inst_1 : Min β] → [inst_2 : Min γ] → InfHom β γ → InfHom α β → InfHom α γ
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpackMantissa_def : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpackMantissa b = BitVec.extractLsb' 0 spec.mantissaBitsWithoutImplicit b
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- **Alias** of `HahnSeries.order_mul_of_ne_zero`. -/
HahnSeries.order_mul_of_nonzero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.leadingCoeff * y.leadingCoeff ≠ 0 → (x * y).order = x.order + y.order
-- Init.Data.Int.Order
Int.toNat_natCast : ∀ (n : ℕ), (↑n).toNat = n
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G'),
  adj1.rightAdjointUniq adj2 = (CategoryTheory.conjugateIsoEquiv adj1 adj2) (CategoryTheory.Iso.refl F)
-- Mathlib.Tactic.Translate.ToAdditive
/-- An attribute that tells that certain arguments of this definition are not
involved when translating.
This helps the translation heuristic by also transforming definitions if `ℕ` or another
fixed type occurs as one of these arguments.  -/
Mathlib.Tactic.ToAdditive.to_additive_ignore_args : Lean.ParserDescr
-- Mathlib.Data.PNat.Basic
PNat.ofNat_inj : ∀ {m n : ℕ} [inst : NeZero m] [inst_1 : NeZero n], OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
_private.Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart.0.LindemannWeierstrass.P.eq_1 : ∀ (f : Polynomial ℂ) (s : ℂ),
  LindemannWeierstrass.P✝ f s =
    Complex.exp s * Polynomial.eval 0 (Polynomial.sumIDeriv f) - Polynomial.eval s (Polynomial.sumIDeriv f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.equiv_iff_toList_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ t₁.toList = t₂.toList
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.maximalOfPrime : ∀ {R : Type u_1} {inst : CommRing R} [self : Ring.DimensionLEOne R] {p : Ideal R}, p ≠ ⊥ → p.IsPrime → p.IsMaximal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?_eq_getEntryGT?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGT? k t = Std.DTreeMap.Internal.Impl.getEntryGT?ₘ k t
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.coe_finsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  ↑(ρ.finsupport x₀) = Function.support fun i => (ρ i) x₀