mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A right homology map data for a morphism of short complexes induces
a left homology map data in the opposite category.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} →
              CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- In a complex Banach algebra, the spectral radius is always attained by some element of the
spectrum.  -/
spectrum.exists_nnnorm_eq_spectralRadius : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A),
  ∃ z ∈ spectrum ℂ a, ↑‖z‖₊ = spectralRadius ℂ a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') {X Y : CategoryTheory.CostructuredArrow (S.prod S') (T, T')} (η : X ⟶ Y),
  (CategoryTheory.CostructuredArrow.prodFunctor S S' T T').map η =
    (CategoryTheory.CostructuredArrow.homMk η.left.1 ⋯, CategoryTheory.CostructuredArrow.homMk η.left.2 ⋯)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_succ : ∀ (o : Ordinal.{u_1}), Ordinal.veblen (Order.succ o) = Ordinal.deriv (Ordinal.veblen o)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_obj : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (j : J),
  (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).obj j =
    Opposite.op
      ((TopCat.Presheaf.pushforward C
            (CategoryTheory.Limits.colimit.ι (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) j)).obj
        (F.obj j).presheaf)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [inst_3 : X₁.HasTensor X₂]
  {A : C} {k : I}
  (f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) (i₁ i₂ : I)
  (hi : i₁ + i₂ = k) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) h) =
    CategoryTheory.CategoryStruct.comp (f i₁ i₂ hi) h
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₂ = f.right.left
-- Mathlib.Algebra.Star.LinearMap
/-- A linear map is self-adjoint (with respect to the intrinsic star) iff it is star-preserving.  -/
LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  (f : WithConv (E →ₗ[R] F)), IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_dvd_ordProj_of_dvd : ∀ {a b : ℕ}, b ≠ 0 → a ∣ b → ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
-- Mathlib.Analysis.SpecificLimits.Normed
/-- A normed ring has summable geometric series if, for all `ξ` of norm `< 1`, the geometric series
`∑ ξ ^ n` converges. This holds both in complete normed rings and in normed fields, providing a
convenient abstraction of these two classes to avoid repeating the same proofs.  -/
HasSummableGeomSeries : (K : Type u_4) → [NormedRing K] → Prop
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_div : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f : α → G}
  [MeasurableDiv G], Measurable f → ∀ (c : G), Measurable fun x => c / f x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_9 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (n : ℕ) (rhs : Std.Tactic.BVDecide.BVExpr n)
  (lhs : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftRight rhs) =
    Std.Tactic.BVDecide.BVExpr.eval assign lhs >>> Std.Tactic.BVDecide.BVExpr.eval assign rhs
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_nonempty : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), (Topology.RelCWComplex.openCell n j).Nonempty
-- Mathlib.RingTheory.PicardGroup
Submodule.unitsQuotEquivRelPic_apply_coe : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] (a : (Submodule R A)ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).range),
  ↑((Submodule.unitsQuotEquivRelPic R A) a) =
    ↑((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R A))
        ((QuotientGroup.congr (Units.map ↑(Submodule.spanSingleton R)).range (Submodule.unitsToPic R A).ker
            (MulEquiv.refl (Submodule R A)ˣ) ⋯)
          a))
-- Mathlib.Order.Hom.Lattice
InfHom.instPartialOrder : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → PartialOrder (InfHom α β)
-- Init.Data.UInt.Bitwise
UInt16.toFin_and : ∀ (a b : UInt16), (a &&& b).toFin = a.toFin &&& b.toFin
-- Mathlib.Topology.Homotopy.Lifting
/-- A map `f` from a path-connected, locally path-connected space `A` to another space `X` lifts
uniquely through a local homeomorphism `p : E → X` if for every path `γ` in `A`, the composed
path `f ∘ γ` in `X` lifts to `E` with endpoint only dependent on the endpoint of `γ` and
independent of the path chosen. In this theorem, we require that a specific point `a₀ : A` is
lifted to a specific point `e₀ : E` over `a₀`.  -/
IsLocalHomeomorph.existsUnique_continuousMap_lifts : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X},
  IsLocalHomeomorph p →
    ∀ [PathConnectedSpace A] [LocallyPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E),
      p e₀ = f a₀ →
        (∀ (γ : C(↑unitInterval, A)), γ 0 = a₀ → ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)) →
          (∀ (γ γ' : C(↑unitInterval, A)) (Γ Γ' : C(↑unitInterval, E)),
              γ 0 = a₀ →
                γ' 0 = a₀ →
                  Γ 0 = e₀ → Γ' 0 = e₀ → p ∘ ⇑Γ = ⇑(f.comp γ) → p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1) →
            ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.p_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.Hom Q), CategoryTheory.CategoryStruct.comp P.p f.f = CategoryTheory.CategoryStruct.comp f.f Q.p
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorem.mk.sizeOf_spec : ∀ (funPropName : Lean.Name) (thmOrigin funOrigin : Mathlib.Meta.FunProp.Origin) (mainArgs : Array ℕ)
  (appliedArgs priority : ℕ) (form : Mathlib.Meta.FunProp.TheoremForm),
  sizeOf
      { funPropName := funPropName, thmOrigin := thmOrigin, funOrigin := funOrigin, mainArgs := mainArgs,
        appliedArgs := appliedArgs, priority := priority, form := form } =
    1 + sizeOf funPropName + sizeOf thmOrigin + sizeOf funOrigin + sizeOf mainArgs + sizeOf appliedArgs +
        sizeOf priority +
      sizeOf form
-- Mathlib.FieldTheory.Normal.Closure
/-- `normalClosure` as a `ClosureOperator`.  -/
IntermediateField.normalClosureOperator : (F : Type u_1) →
  (L : Type u_3) →
    [inst : Field F] →
      [inst_1 : Field L] → [inst_2 : Algebra F L] → [Normal F L] → ClosureOperator (IntermediateField F L)
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.PseudoMetrizableSpace.regularSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X], RegularSpace X
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.Simps.apply.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (h : α ≃*o β), OrderMonoidIso.Simps.apply h = ⇑h
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.Localization.η.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₂.IsLocalization W₂] (G' : CategoryTheory.Functor D₁ D₂)
  (F' : CategoryTheory.Functor D₂ D₁) [inst_5 : CategoryTheory.CatCommSq G L₁ L₂ G']
  [inst_6 : CategoryTheory.CatCommSq F L₂ L₁ F'],
  CategoryTheory.Adjunction.Localization.η adj L₁ L₂ W₂ G' F' =
    CategoryTheory.Localization.liftNatTrans L₂ W₂ ((F.comp G).comp L₂) L₂ (F'.comp G') (CategoryTheory.Functor.id D₂)
      (CategoryTheory.Functor.whiskerRight adj.counit L₂)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddSemigroup` by an additive congruence relation is
an `AddSemigroup`.  -/
AddCon.addSemigroup : {M : Type u_4} → [inst : AddSemigroup M] → (c : AddCon M) → AddSemigroup c.Quotient
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.symm_mapAlgEquiv`. -/
MonoidAlgebra.symm_mapRangeAlgEquiv : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (e : A ≃ₐ[R] B),
  (MonoidAlgebra.mapAlgEquiv R M e).symm = MonoidAlgebra.mapAlgEquiv R M e.symm
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_comp : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add' W f₁ f₂) g =
    CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f₁ g)
      (CategoryTheory.CategoryStruct.comp f₂ g)
-- Mathlib.Data.Sym.Sym2.Order
Sym2.inf_mk : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a b : α), s(a, b).inf = a ⊓ b
-- Std.Time.Date.PlainDate
Std.Time.instReprPlainDate.repr : Std.Time.PlainDate → ℕ → Std.Format
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- Notation for the pushout-product of morphisms.  -/
CategoryTheory.MonoidalCategory.Arrow.«term_□_» : Lean.TrailingParserDescr
-- Init.Data.Nat.Basic
Nat.pred_lt_pred : ∀ {n m : ℕ}, n ≠ 0 → n < m → n.pred < m.pred
-- Init.GetElem
getElem_congr : ∀ {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [inst : GetElem coll idx elem valid]
  {c d : coll} (h : c = d) {i j : idx} (h' : i = j) (w : valid c i), c[i] = d[j]
-- Init.Data.UInt.Bitwise
UInt64.ofFin_shiftRight_mod : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a >>> (b % 64)) = UInt64.ofFin a >>> UInt64.ofFin b
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `Equiv.addLeft` as an `OrderIso`. See also `OrderEmbedding.addLeft`.  -/
OrderIso.addLeft : {α : Type u} → [inst : AddGroup α] → [inst_1 : LE α] → [AddLeftMono α] → α → α ≃o α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.contDiffOn : ∀ {𝕜 : 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} {x : E} {m n : WithTop ℕ∞},
  m ≤ n →
    (m = ↑⊤ → n = ⊤) → ContDiffWithinAt 𝕜 n f s x → ∃ u ∈ nhdsWithin x (insert x s), u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.mk_lt_mk : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s},
  AddLocalization.mk a₁ a₂ < AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁
-- Init.Data.Int.DivMod.Bootstrap
Int.add_mul_emod_self_left : ∀ (a b c : ℤ), (a + b * c) % b = a % b
-- Mathlib.Algebra.Ring.Defs
/-- Zero is a left absorbing element for multiplication  -/
NonUnitalNonAssocRing.zero_mul : ∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a : α), 0 * a = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The target of a 1-simplex in a path is identified with the target vertex.  -/
SSet.Path.arrow_tgt : ∀ {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin n),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) (f.arrow i) = f.vertex i.succ
-- Mathlib.Data.Fin.SuccPred
Fin.succ_castPred_le_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n), (a.castPred ha).succ ≤ b ↔ a < b
-- Init.Data.List.Erase
List.head_erase_mem : ∀ {α : Type u_1} [inst : BEq α] (xs : List α) (a : α) (h : xs.erase a ≠ []), (xs.erase a).head h ∈ xs
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrLeft_apply : ∀ {ι : Type u_7} {ι' : Type u_8} (S : ι' → Type u_9) (e : ι ≃ ι') [inst : (i : ι') → NonUnitalNonAssocSemiring (S i)]
  (a : (i : ι) → S (e.symm.symm i)) (i : ι'), (RingEquiv.piCongrLeft S e) a i = ⋯ ▸ a (e.symm i)
-- Mathlib.Algebra.Algebra.Operations
Submodule.setSemiring_smul_def : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (s : SetSemiring A)
  (P : Submodule R A), s • P = Submodule.span R (SetSemiring.down s) * P
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSubOfContinuousSub : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Sub β] → [ContinuousSub β] → Sub C(α, β)
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistrib_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι] (f : (i : ι) → Module.Dual R (M i)) (m : (i : ι) → M i),
  (PiTensorProduct.dualDistrib ((PiTensorProduct.tprod R) fun i => f i)) (⨂ₜ[R] (i : ι), m i) = ∏ i, (f i) (m i)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.anyM_filterM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Std.Iter β}
  {f p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.Iter.filterM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then p x else pure { down := false })
      (Std.Iter.mapM pure it)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : One G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G], ⇑1 = 1
-- Init.Data.UInt.Lemmas
UInt16.add_left_neg : ∀ (a : UInt16), -a + a = 0
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.mk : Lean.Expr → Lean.Expr → Lean.LocalContext → Lean.LocalInstances → Lean.Meta.DefEqContext
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.regularCoverage.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C],
  CategoryTheory.regularCoverage C = CategoryTheory.regularCoverage C
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_zpow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℤ), (x ^ n).valuation = n * x.valuation
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_of_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (f : β → α) {b : β},
  b ∈ s → ∃ a, s.sup (WithBot.some ∘ f) = ↑a
-- Init.Data.SInt.Bitwise
ISize.toInt64_or : ∀ (a b : ISize), (a ||| b).toInt64 = a.toInt64 ||| b.toInt64
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.instPseudoMetricSpace : {ι : Type u_2} →
  {X : Type u_3} →
    {Y : ι → Type u_4} →
      {f : (i : ι) → X → Y i} →
        [Encodable ι] → [(i : ι) → PseudoMetricSpace (Y i)] → PseudoMetricSpace (Metric.PiNatEmbed X Y f)
-- Lean.Elab.Command
Lean.Elab.Command.State.mk : Lean.Environment →
  Lean.MessageLog →
    List Lean.Elab.Command.Scope →
      Lean.NameSet →
        ℕ →
          ℕ →
            Lean.NameGenerator →
              Lean.DeclNameGenerator →
                Lean.Elab.InfoState →
                  Lean.TraceState →
                    Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Elab.Command.State
-- Mathlib.FieldTheory.AbelRuffini
isAlgebraic_solvableByRad : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  (solvableByRad F E).IsAlgebraic
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.sub_supermartingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Supermartingale g ℱ μ → MeasureTheory.Submartingale (f - g) ℱ μ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.presheafIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K A} (i i_1 : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  i = i_1 → CategoryTheory.Functor.IsCoverDense.presheafIso i = CategoryTheory.Functor.IsCoverDense.presheafIso i_1
-- Aesop.Script.TacticState
_private.Aesop.Script.TacticState.0.Aesop.Script.TacticState.throwUnknownGoalError : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → {α : Type} → Lean.MVarId → Lean.MessageData → m α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_eraseKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)}
  {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue! a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then default else Std.Internal.List.getValue! a l
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.instToMessageDataNewDecl : Lean.ToMessageData Lean.Meta.IndPredBelow.NewDecl✝
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_none_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.maxKey? = none ↔ t.isEmpty = true)
-- Mathlib.Algebra.Group.Action.Defs
add_vadd_zero : ∀ {M : Type u_9} {N : Type u_10} [inst : AddZeroClass N] [inst_1 : VAdd M N] [VAddCommClass M N N] (x : M) (y : N),
  y + (x +ᵥ 0) = x +ᵥ y
-- Std.Http.Internal.String
/-- Quotes `s` as an HTTP `quoted-string`, panicking if `s` contains characters that cannot be
represented by `qdtext`/`quoted-pair`.
 -/
Std.Http.Internal.quoteHttpString! : String → String
-- Mathlib.Order.Filter.Map
Filter.map_sup : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {m : α → β},
  Filter.map m (f₁ ⊔ f₂) = Filter.map m f₁ ⊔ Filter.map m f₂
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_mul_left_right : ∀ (m n k : ℕ), m.Coprime (n + m * k) ↔ m.Coprime n
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.isFragment_smul_finset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G} {a : G},
  Finset.IsFragment✝ K S (a • A) ↔ Finset.IsFragment✝ K S A
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- `Scheme.Γ : Schemeᵒᵖ ⥤ CommRingCat` preserves colimits of diagrams consisting of
affine schemes.  -/
AlgebraicGeometry.preservesColimit_Γ : ∀ {I : Type w} [inst : CategoryTheory.Category.{v, w} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Schemeᵒᵖ)
  [∀ (i : I), AlgebraicGeometry.IsAffine (Opposite.unop (D.obj i))],
  CategoryTheory.Limits.PreservesColimit D AlgebraicGeometry.Scheme.Γ
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.MeasurePreserving.zpow : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [CompactSpace G] [RootableBy G ℤ] {n : ℤ},
  n ≠ 0 →
    ∀ {X : Type u_2} [inst_8 : MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G},
      MeasureTheory.MeasurePreserving f μ' μ → MeasureTheory.MeasurePreserving (fun x => f x ^ n) μ' μ
-- Mathlib.Topology.Order.LiminfLimsup
isCobounded_ge_nhds : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] (a : α),
  Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) (nhds a)
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.shiftedGenWeightSpace.shift_symm_apply : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) (a : ↥(LieModule.genWeightSpace M χ)),
  (LieModule.shiftedGenWeightSpace.shift R L M χ).symm a = a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forM_eq_forM_keys : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'], m.WF → ∀ {f : α → m' PUnit.{w + 1}}, (forM m fun a => f a.1) = m.keys.forM f
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.denseRange_pureCauchy : ∀ {α : Type u} [inst : UniformSpace α], DenseRange CauchyFilter.pureCauchy
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteGrp.Hom.mk.injEq : ∀ {A B : ProfiniteGrp.{u}} (hom' hom'_1 : ↑A.toProfinite.toTop →ₜ* ↑B.toProfinite.toTop),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.mk.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (a : α), ↑a = Quotient.mk'' a