mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.mk.congr_simp : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (toEquiv toEquiv_1 : P₁ ≃ P₂) (e_toEquiv : toEquiv = toEquiv_1)
  (linear linear_1 : V₁ ≃ₗ[k] V₂) (e_linear : linear = linear_1)
  (map_vadd' : ∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p),
  { toEquiv := toEquiv, linear := linear, map_vadd' := map_vadd' } =
    { toEquiv := toEquiv_1, linear := linear_1, map_vadd' := ⋯ }
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_join_eq_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.join Q P = Q
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.has_iUnion : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {β : Type u_4} [Countable β] {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) → (∀ (i : β), d.Has (f i)) → d.Has (⋃ i, f i)
-- Mathlib.NumberTheory.LSeries.ZetaZeros
/-- The complement of the zero set of `riemannZeta` is codiscrete within `{1}ᶜ`.  -/
_private.Mathlib.NumberTheory.LSeries.ZetaZeros.0.riemannZetaZeros_codiscreteWithin_compl_one : riemannZetaZerosᶜ ∈ Filter.codiscreteWithin {1}ᶜ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.eq.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (a : List ((a : α) × β a)) (a_1 : Std.DTreeMap.Internal.Cell α β k) (a_2 : List ((a : α) × β a)),
  sizeOf (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Algebra.Order.UpperLower
upperClosure_vadd : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s : Set α) (a : α),
  upperClosure (a +ᵥ s) = a +ᵥ upperClosure s
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBMap.alter.adapt.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (v : β) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Analysis.Normed.Field.UnitBall
Submonoid.coe_unitSphere : ∀ (𝕜 : Type u_2) [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜],
  ↑(Submonoid.unitSphere 𝕜) = Metric.sphere 0 1
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] {X Y : C} {n : ℕ} (f f_1 : CategoryTheory.Abelian.Ext X Y n),
  f = f_1 → CategoryTheory.Abelian.Ext.mapExactFunctor F f = CategoryTheory.Abelian.Ext.mapExactFunctor F f_1
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the reverse direction of `hasDerivAt_iff_isLittleO`. -/
HasDerivAt.of_isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  ((fun x' => f x' - f x - (x' - x) • f') =o[nhds x] fun x' => x' - x) → HasDerivAt f f' x
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure_univ : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.closure Set.univ = ⊤
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.range_map : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A),
  relations.map.range = Submodule.span A (Set.range relations.relation)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkFirstStx : Array (Lean.TSyntax `tactic) → Lean.CoreM (Lean.TSyntax `tactic)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.fst.injEq : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} (a : Std.IterM m β) (a_1 : Std.IterM m β) (a_2 : Std.IterM m β)
  (a_3 : Std.IterM m β),
  (Std.Iterators.Types.Append.fst a a_1 = Std.Iterators.Types.Append.fst a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- Maps elements of `α` to their `n`-th successor. This should semantically behave like repeatedly
applying `succ`, but it might be more efficient.

This function uses an `UpwardEnumerable α` instance.
`LawfulUpwardEnumerable α` ensures the compatibility with `succ` and `succ?`.

If no other implementation is provided in UpwardEnumerable instance, succMany? repeatedly applies succ?.
 -/
Std.PRange.UpwardEnumerable.succMany : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → [Std.PRange.InfinitelyUpwardEnumerable α] → ℕ → α → α
-- Init.Data.String.Lemmas.FindPos
String.lt_posGE_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos}, q < s.posGE p h ↔ q.offset < p
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.fixingAddSubgroup_map_addConj_eq : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M},
  g +ᵥ t = s →
    AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.addConj g)) (fixingAddSubgroup M t) = fixingAddSubgroup M s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          W.addX P Q =
            ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 +
                        W.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) -
                      W.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                    P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                  Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) *
                (P 0 * Q 2 - Q 0 * P 2) /
              (P 2 * Q 2) ^ 2
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.Hom.add_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.Preadditive A] {P Q : CategoryTheory.Sheaf J A}
  (f g : P ⟶ Q) (U : Cᵒᵖ), (f + g).hom.app U = f.hom.app U + g.hom.app U
-- Mathlib.RingTheory.Congruence.Basic
/-- The supremum of a set of congruence relations `S` equals the smallest congruence relation
containing the binary relation 'there exists `c ∈ S` such that `x` is related to `y` by `c`'.  -/
RingCon.sSup_eq_ringConGen : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)), sSup S = ringConGen fun x y => ∃ c ∈ S, c x y
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.of_mem_closure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x y z : A},
  IsIntegral R x → IsIntegral R y → z ∈ Subring.closure {x, y} → IsIntegral R z
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `simp` can prove this as `Basis.coe_reindex` + `EquivLike.range_comp`  -/
Module.Basis.range_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (e : ι ≃ ι'), Set.range ⇑(b.reindex e) = Set.range ⇑b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' fallback : α}, cmp k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addLeft.eq_1 : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M),
  u.addLeft = { toFun := fun x => ↑u + x, invFun := fun x => ↑(-u) + x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.isOne_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r : R},
  Mathlib.Meta.NormNum.IsNat r 1 → Mathlib.Meta.NormNum.IsNat ((algebraMap R A) (r + 0)) 1
-- Init.Internal.Order.While
repeatM.congr_simp : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} [inst_1 : Nonempty β] (f f_1 : α → m (α ⊕ β)),
  f = f_1 → ∀ (a a_1 : α), a = a_1 → repeatM f a = repeatM f_1 a_1
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of a finite extension `E / F` is smaller than the degree of `E / F`.  -/
Field.finSepDegree_le_finrank : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  Field.finSepDegree F E ≤ Module.finrank F E
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_2 : (x : List α) → (x_2 : List β) → motive x x_2),
  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
    (match x, x_1 with
      | a :: as, b :: bs => h_1 a as b bs
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
eval_minpolyDiv_self : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  Polynomial.eval x (minpolyDiv R x) = (Polynomial.aeval x) (Polynomial.derivative (minpoly R x))
-- Mathlib.Order.Filter.Pointwise
Filter.pureOneHom_apply : ∀ {α : Type u_2} [inst : One α] (a : α), Filter.pureOneHom a = pure a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_link : ∀ {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced},
  (Std.DTreeMap.Internal.Impl.link k v l r hl hr).impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Algebra.Group.Defs
IsDedekindFiniteAddMonoid.add_eq_zero_symm : ∀ {M : Type u_2} {inst : AddZero M} [self : IsDedekindFiniteAddMonoid M] {a b : M}, a + b = 0 → b + a = 0
-- Mathlib.RingTheory.Length
Module.length_compositionSeries : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (s : CompositionSeries (Submodule R M)), RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ↑s.length = Module.length R M
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.mk.sizeOf_spec : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : SizeOf E] (f g : ℝ → E) (k : ℝ)
  (ε : ℂ) (f₀ g₀ : E) (hf_int : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
  (hg_int : MeasureTheory.LocallyIntegrableOn g (Set.Ioi 0) MeasureTheory.volume) (hk : 0 < k) (hε : ε ≠ 0)
  (h_feq : ∀ x ∈ Set.Ioi 0, f (1 / x) = (ε * ↑(x ^ k)) • g x)
  (hf_top : ∀ (r : ℝ), (fun x => f x - f₀) =O[Filter.atTop] fun x => x ^ r)
  (hg_top : ∀ (r : ℝ), (fun x => g x - g₀) =O[Filter.atTop] fun x => x ^ r),
  sizeOf
      { f := f, g := g, k := k, ε := ε, f₀ := f₀, g₀ := g₀, hf_int := hf_int, hg_int := hg_int, hk := hk, hε := hε,
        h_feq := h_feq, hf_top := hf_top, hg_top := hg_top } =
    1 + sizeOf k + sizeOf ε + sizeOf f₀ + sizeOf g₀ + sizeOf hk
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.ext : ∀ {R : Type u} {inst : Semiring R} {M N : SemimoduleCat R} {x y : M.Hom N}, x.hom' = y.hom' → x = y
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.trajContent.eq_1 : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
  ProbabilityTheory.Kernel.trajContent κ x₀ = MeasureTheory.projectiveFamilyContent ⋯
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_uInt16ToNat : ∀ (n : UInt16), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Mathlib.Tactic.Polynomial.Basic
Mathlib.Tactic.Polynomial.monomial_eq_smul : ∀ {R : Type u_2} [inst : CommSemiring R] (a : R) (n : ℕ), (Polynomial.monomial n) a = a • Polynomial.X ^ n
-- Mathlib.Data.Opposite
Opposite.unop_eq_iff_eq_op : ∀ {α : Sort u} {x : αᵒᵖ} {y : α}, Opposite.unop x = y ↔ x = Opposite.op y
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` expressed with the real-valued measure of a set defined with
an extended norm.

The `IsFiniteMeasure` hypothesis is necessary, otherwise `μ.real {...}` could be zero because
the measure of the set is infinite.  -/
MeasureTheory.tendstoInMeasure_iff_measureReal_enorm : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {l : Filter ι} {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ENNReal), 0 < ε → ε ≠ ⊤ → Filter.Tendsto (fun i => μ.real {x | ε ≤ ‖f i x - g x‖ₑ}) l (nhds 0)
-- Mathlib.Topology.Sheaves.MayerVietoris
/-- A square consisting of opens `X₂ ⊓ X₃`, `X₂`, `X₃` and `X₂ ⊔ X₃` is
a Mayer-Vietoris square.  -/
Opens.mayerVietorisSquare' : {T : Type u} →
  [inst : TopologicalSpace T] →
    (sq : CategoryTheory.Square (TopologicalSpace.Opens T)) →
      sq.X₄ = sq.X₂ ⊔ sq.X₃ → sq.X₁ = sq.X₂ ⊓ sq.X₃ → (Opens.grothendieckTopology T).MayerVietorisSquare
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.bijective_fromSigma_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F},
  CategoryTheory.Functor.CoconeTypes.IsColimit c → Function.Bijective (CategoryTheory.Limits.CofanTypes.fromSigma F c)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqLambdaTheorem.beq : Mathlib.Meta.FunProp.LambdaTheorem → Mathlib.Meta.FunProp.LambdaTheorem → Bool
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.instRespectsIsoLocalEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.localEpi.RespectsIso
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.elabUsingElabFns : Lean.Syntax → Option Lean.Expr → Bool → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Order.Hom.Order
OrderHom.instInfSet : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : CompleteLattice β] → InfSet (α →o β)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodCongr_symm : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_5} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] {M₃ : Type u_6}
  [inst_5 : TopologicalSpace M₃] [inst_6 : AddCommMonoid M₃] {M₄ : Type u_7} [inst_7 : TopologicalSpace M₄]
  [inst_8 : AddCommMonoid M₄] [inst_9 : Module R₁ M₁] [inst_10 : Module R₁ M₂] [inst_11 : Module R₁ M₃]
  [inst_12 : Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄), (e.prodCongr e').symm = e.symm.prodCongr e'.symm
-- Std.Time.Duration
/-- Adds a `Nanosecond.Offset` to a `Duration`
 -/
Std.Time.Duration.subNanoseconds : Std.Time.Duration → Std.Time.Nanosecond.Offset → Std.Time.Duration
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_self_lt_top_iff : ∀ {a : ENNReal}, a * a < ⊤ ↔ a < ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.ExtDTreeMap.filterMap f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.ExtDTreeMap.Const.get t x ⋯)).isSome).get!
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = true → motive true) → (x = false → motive false) → motive x
-- Mathlib.Topology.MetricSpace.Closeds
/-- `NonemptyCompacts.toCloseds` is an isometry  -/
TopologicalSpace.NonemptyCompacts.isometry_toCloseds : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry TopologicalSpace.NonemptyCompacts.toCloseds
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.hasPushout_over_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.Limits.HasPushout 0 0
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_le_left_iff_nonpos : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → ((AffineMap.lineMap a b) r ≤ a ↔ r ≤ 0)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.isThreeCycle_sq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α}, g.IsThreeCycle → (g * g).IsThreeCycle
-- Mathlib.Analysis.Normed.Group.Constructions
norm_snd_le : ∀ {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : Norm F] (x : E × F), ‖x.2‖ ≤ ‖x‖
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instInhabitedLoogleMatch.default : LeanSearchClient.LoogleMatch
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualCopairing_nondegenerate : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁] (W : Subspace K V₁),
  (Submodule.dualCopairing W).Nondegenerate
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Lean.Meta.InferType
/-- The resulting type is a de-Bruijn variable with index `idx`.
The index is used to check the type of the corresponding binder.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.bvar : ℕ → Lean.Meta.ArrowPropResult✝
-- Lean.Parser.Do
Lean.Parser.Term.doMatchAlts.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.one_le : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : FractionalIdeal S P}, 1 ≤ I ↔ 1 ∈ I
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.brecOn.eq : ∀ {α : Type} {motive : Std.Tactic.BVDecide.BoolExpr α → Sort u} (t : Std.Tactic.BVDecide.BoolExpr α)
  (F_1 : (t : Std.Tactic.BVDecide.BoolExpr α) → Std.Tactic.BVDecide.BoolExpr.below t → motive t),
  Std.Tactic.BVDecide.BoolExpr.brecOn t F_1 = F_1 t (Std.Tactic.BVDecide.BoolExpr.brecOn.go t F_1).2
-- Mathlib.NumberTheory.Divisors
Nat.sum_divisors_eq_sum_properDivisors_add_self : ∀ {n : ℕ}, ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
-- Mathlib.Probability.Independence.Process.Basic
/-- A stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$.  -/
ProbabilityTheory.Kernel.IndepFun.process_indepFun : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  (∀ (i : S), Measurable (X i)) →
    Measurable Y →
      (∀ (I : Finset S), ProbabilityTheory.Kernel.IndepFun (fun ω i => X (↑i) ω) Y κ P) →
        ∀ [ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) Y κ P
-- Mathlib.Data.Seq.Computation
Computation.head_think : ∀ {α : Type u} (s : Computation α), s.think.head = none
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.compYonedaIso_inv_app_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : D) (X_1 : Cᵒᵖ)
  (x : F.obj (Opposite.unop X_1) ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((adj.compYonedaIso.inv.app X).app X_1)) x =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X_1)) (G.map x)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- The group homomorphism from `RingAut R` to `RingAut k` where `k`
is the residue field of `R`.  -/
IsLocalRing.ResidueField.mapAut : {R : Type u_1} → [inst : CommRing R] → [inst_1 : IsLocalRing R] → RingAut R →* RingAut (IsLocalRing.ResidueField R)
-- Lean.Elab.Arg
/-- Auxiliary inductive datatype for combining unelaborated syntax
and already elaborated expressions. It is used to elaborate applications.
 -/
Lean.Elab.Term.Arg : Type
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_symm_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : D),
  (adj.homEquiv (G.obj X) X).symm (CategoryTheory.CategoryStruct.id (G.obj X)) = adj.counit.app X
-- Mathlib.Control.Monad.Basic
/-- reduce the equivalence between two reader monads to the equivalence between
their respective function spaces  -/
ReaderT.equiv : {ρ₁ α₁ : Type u₀} →
  {ρ₂ α₂ : Type u₁} →
    {m₁ : Type u₀ → Type v₀} →
      {m₂ : Type u₁ → Type v₁} → (ρ₁ → m₁ α₁) ≃ (ρ₂ → m₂ α₂) → ReaderT ρ₁ m₁ α₁ ≃ ReaderT ρ₂ m₂ α₂
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.zero : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] (g : α → F) (l : Filter α), 0 =o[𝕜; l] g
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.iSup_map_single : ∀ {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [inst : (i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)}
  [inst_1 : DecidableEq ι], ⨆ i, AddSubmonoid.map (AddMonoidHom.single M i) (P i) = AddSubmonoid.pi Set.univ P
-- Mathlib.Tactic.DeriveTraversable
/-- similar to `traverseField` but for `Functor`  -/
Mathlib.Deriving.Traversable.mapField : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Logic.Basic
Subsingleton.forall₂_iff : ∀ {ι : Sort u_3} [Subsingleton ι] (P : ι → ι → Prop), (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- If `K : CochainComplex C ℤ`, this is the canonical truncation `≤ n` of `K`.  -/
CochainComplex.truncLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : CochainComplex C ℤ) →
        [CategoryTheory.Limits.HasZeroObject C] →
          [∀ (i : ℤ), HomologicalComplex.HasHomology K i] → ℤ → CochainComplex C ℤ
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control : Type
-- Mathlib.Data.Finset.Sups
Finset.disjSups.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t : Finset α),
  s.disjSups t = Finset.image (fun ab => ab.1 ⊔ ab.2) ({ab ∈ s ×ˢ t | Disjoint ab.1 ab.2})
-- Lean.Parser.Term
Lean.Parser.Term.scoped : Lean.Parser.Parser