mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.comap_inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {J K : CategoryTheory.Precoverage D},
  CategoryTheory.Precoverage.comap F (J ⊓ K) =
    CategoryTheory.Precoverage.comap F J ⊓ CategoryTheory.Precoverage.comap F K
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)] {b : β a}, (t.insert a b).get! a = b
-- Mathlib.Tactic.DuplicateDecls
/-- Compute an array of duplicate declarations in the current environment.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.duplicateDeclarations : Mathlib.Tactic.DuplicateDecls.Target → Lean.CoreM (Array (Array Lean.Name))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtAllPlaces ⁻¹'
      ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis ''
        interior (NumberField.mixedEmbedding.fundamentalCone.paramSet K) ⊆
    interior (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_erase : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n i : ℕ),
  (Polynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.chainTopCoeff_eq_of_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] [inst_6 : IsDomain R] [inst_7 : P.IsCrystallographic] [inst_8 : Finite ι] {i j : ↥b.support},
  i ≠ j → ↑(RootPairing.chainTopCoeff ↑i ↑j) = -P.pairingIn ℤ ↑j ↑i
-- Mathlib.CategoryTheory.Localization.Construction
/-- A `MorphismProperty` in `W.Localization` is satisfied by all
morphisms in the localized category if it contains the image of the
morphisms in the original category, the inverses of the morphisms
in `W` and if it is stable under composition  -/
CategoryTheory.Localization.Construction.morphismProperty_eq_top : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}
  (P : CategoryTheory.MorphismProperty W.Localization) [P.IsStableUnderComposition],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) →
    (∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (CategoryTheory.Localization.Construction.wInv w hw)) → P = ⊤
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprLinarithConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.LinarithConfig
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AState.mk.inj : ∀ {generalizations : Array (Lean.Expr × Lean.Expr)} {propToProof : Lean.ExprMap Lean.Expr}
  {generalizations_1 : Array (Lean.Expr × Lean.Expr)} {propToProof_1 : Lean.ExprMap Lean.Expr},
  { generalizations := generalizations, propToProof := propToProof } =
      { generalizations := generalizations_1, propToProof := propToProof_1 } →
    generalizations = generalizations_1 ∧ propToProof = propToProof_1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.toProd_apply_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : N),
  AddMonoid.Coprod.toProd (AddMonoid.Coprod.inr x) = (0, x)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt.0.Int64.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int64)
-- Mathlib.Order.Filter.Pointwise
Filter.coe_pureAddMonoidHom : ∀ {α : Type u_2} [inst : AddZeroClass α], ⇑Filter.pureAddMonoidHom = pure
-- Mathlib.Order.Category.BddLat
BddLat.id_apply : ∀ (X : Lat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_inter_iUnion : ∀ {α : Type u_1} {ι : Sort u_9} {κ : Sort u_10} (f : ι → Set α) (g : κ → Set α),
  (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.instLieRing : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → LieRing (TensorProduct R A L)
-- Mathlib.Topology.Algebra.Monoid.Defs
SeparatelyContinuousAdd.continuous_const_add : ∀ {M : Type u_1} {inst : TopologicalSpace M} {inst_1 : Add M} [self : SeparatelyContinuousAdd M] {a : M},
  Continuous fun x => a + x
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Universe lift functor for commutative algebras.  -/
CommAlgCat.uliftFunctor : (R : Type u) → [inst : CommRing R] → CategoryTheory.Functor (CommAlgCat R) (CommAlgCat R)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanceL.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (r r_1 : Std.DTreeMap.Internal.Impl α β) (e_r : r = r_1)
      (hlb : l.Balanced) (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size),
      Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceL k v_1 l_1 r_1 ⋯ ⋯ ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spineToSimplex_arrow : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (i : Fin m) (f : X.Path m),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ h).op))
      (sx.spineToSimplex m h f) =
    f.arrow i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.keys_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.ExtDTreeMap.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.ExtDTreeMap.Const.get t x ⋯))
        t.keys.attach).unattach
-- Mathlib.Algebra.Order.Monoid.NatCast
one_le_two : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : LE α] [ZeroLEOneClass α] [AddLeftMono α], 1 ≤ 2
-- Init.Data.Array.Lemmas
Array.getElem?_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} {a : α},
  (xs.setIfInBounds i a)[j]? = if i = j then if i < xs.size then some a else none else xs[j]?
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_append_of_containsKey_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l l' : List ((_ : α) × β)} {a : α}
  {h' : Std.Internal.List.containsKey a (l ++ l') = true} (h : Std.Internal.List.containsKey a l' = false),
  Std.Internal.List.getValue a (l ++ l') h' = Std.Internal.List.getValue a l ⋯
-- Init.Data.BitVec.Basic
BitVec.instHShiftRightNat : {w : ℕ} → HShiftRight (BitVec w) ℕ (BitVec w)
-- Mathlib.Algebra.CharP.Invertible
/-- When two is invertible in a ring, every element is `Odd`.  -/
Odd.all : ∀ {R : Type u_1} [inst : Ring R] [Invertible 2] (a : R), Odd a
-- Batteries.Data.AssocList
Batteries.AssocList.instStreamProd : {α : Type u_1} → {β : Type u_2} → Std.Stream (Batteries.AssocList α β) (α × β)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.comp_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasLimit G], CategoryTheory.Limits.HasLimit (F.comp G)
-- Lean.Widget.UserWidget
Lean.Widget.WidgetSource.mk.inj : ∀ {sourcetext sourcetext_1 : String},
  { sourcetext := sourcetext } = { sourcetext := sourcetext_1 } → sourcetext = sourcetext_1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] {W : C} (k k_1 : W ⟶ X) (e_k : k = k_1)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.Limits.weakEqualizer.lift k h = CategoryTheory.Limits.weakEqualizer.lift k_1 ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.toCoheytingAlgebra : {α : Type u_1} → [self : Order.Coframe α] → CoheytingAlgebra α
-- Mathlib.Topology.Instances.Matrix
instContinuousMulMatrixOfContinuousAdd : ∀ {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Fintype n] [inst_2 : Mul R]
  [inst_3 : AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R], ContinuousMul (Matrix n n R)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_3 : ∀ (k : ℕ), (Lean.Grind.CommRing.Expr.natCast k).toPoly = Lean.Grind.CommRing.Poly.num ↑k
-- Lean.Data.Lsp.Internal
/-- Used in the `$/lean/queryModule` watchdog <- worker request, which is used by the worker to
extract information from the .ilean information in the watchdog.
 -/
Lean.Lsp.LeanQueryModuleParams : Type
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyoneda_map_app : ∀ {X Y : CommGrpCatᵒᵖ} (f : X ⟶ Y) (N : CommGrpCat),
  (CommGrpCat.coyoneda.map f).app N = CommGrpCat.ofHom (CommGrpCat.Hom.hom f.unop).compHom'
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_pow_eq_pow_inv : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (n : ℕ), ↑(a ^ n)⁻¹ = ↑a⁻¹ ^ n
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_add : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] (x : α) (v : Fin n → α) (w : Fin n.succ → α),
  Matrix.vecCons x v + w = Matrix.vecCons (x + Matrix.vecHead w) (v + Matrix.vecTail w)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.nullHomotopic.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ h₀_1 : S₁.X₁ ⟶ S₂.X₁) (e_h₀ : h₀ = h₀_1)
  (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ h₁_1 : S₁.X₂ ⟶ S₂.X₁),
  h₁ = h₁_1 →
    ∀ (h₂ h₂_1 : S₁.X₃ ⟶ S₂.X₂),
      h₂ = h₂_1 →
        ∀ (h₃ h₃_1 : S₁.X₃ ⟶ S₂.X₃) (e_h₃ : h₃ = h₃_1) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
          S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃ = S₁.nullHomotopic S₂ h₀_1 ⋯ h₁_1 h₂_1 h₃_1 ⋯
-- Mathlib.Data.ENNReal.Real
ENNReal.trichotomy : ∀ (p : ENNReal), p = 0 ∨ p = ⊤ ∨ 0 < p.toReal
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.mem_orthogonal_iff : ∀ {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} {N : Submodule R M} {m : M}, m ∈ B.orthogonal N ↔ ∀ n ∈ N, (B n) m = 0
-- Mathlib.Order.Hom.Lattice
/-- Composition of `SupHom`s as a `SupHom`.  -/
SupHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Max α] → [inst_1 : Max β] → [inst_2 : Max γ] → SupHom β γ → SupHom α β → SupHom α γ
-- Mathlib.Data.Option.Basic
Option.exists_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {p : β → Prop},
  (∃ y ∈ Option.map f o, p y) ↔ ∃ x ∈ o, p (f x)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- A reformulation of the Gamma recurrence relation which is true for `s = 0` as well.  -/
Complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_one : ∀ (s : ℂ), (Complex.Gamma s)⁻¹ = s * (Complex.Gamma (s + 1))⁻¹
-- Init.Data.SInt.Lemmas
Int8.mul_assoc : ∀ (a b c : Int8), a * b * c = a * (b * c)
-- Init.Data.String.Subslice
String.Slice.Subslice.endExclusive_toSlice : ∀ {s : String.Slice} {sl : s.Subslice}, sl.toSlice.endExclusive = sl.endExclusive.str
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- The left homotopy relation on morphisms of `Arrow V`.  -/
CategoryTheory.Arrow.leftHomotopic : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] → [CategoryTheory.Preadditive V] → HomRel (CategoryTheory.Arrow V)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The map `HoCat.iResolutionObj`, when applied to already fibrant objects, gives
a natural transformation `toHoCat ⟶ ι ⋙ HoCat.resolution`.  -/
HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.FibrantObject.toHoCat ⟶
        HomotopicalAlgebra.FibrantObject.ι.comp HomotopicalAlgebra.FibrantObject.HoCat.resolution
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.map_dpow : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {f : A →+* B},
  hI.IsDPMorphism hJ f → ∀ {n : ℕ} {a : A}, a ∈ I → f (hI.dpow n a) = hJ.dpow n (f a)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'_symm : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  Matrix.toBilin'.symm = LinearMap.BilinForm.toMatrix'
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.altNumParams : Lean.Meta.MatcherInfo → Array ℕ
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- If a group `G` acts on `X` by isometries, then `IsometryEquiv.constSMul` is the isometry of
`X` given by multiplication of a constant element of the group.  -/
IsometryEquiv.constSMul : {G : Type v} →
  {X : Type w} →
    [inst : PseudoEMetricSpace X] → [inst_1 : Group G] → [inst_2 : MulAction G X] → [IsIsometricSMul G X] → G → X ≃ᵢ X
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_quotient : ∀ {R : Type u_1} [inst : Semiring R] {A : Type u_5} {M : Type u_6} [inst_1 : Ring A] [inst_2 : AddCommGroup M]
  [inst_3 : SMul R A] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] (N : Submodule A M)
  [IsNoetherian R M], IsNoetherian R (M ⧸ N)
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_le_factorial : ∀ (n : ℕ), n.doubleFactorial ≤ n.factorial
-- Mathlib.Tactic.Linarith.Parsing
/-- `linearFormsAndMaxVar red pfs` is the main interface for computing the linear forms of a list
of expressions. Given a list `pfs` of proofs of comparisons, it produces a list `c` of `Comp`s of
the same length, such that `c[i]` represents the linear form of the type of `pfs[i]`.

It also returns the largest variable index that appears in comparisons in `c`.
 -/
Mathlib.Tactic.Linarith.linearFormsAndMaxVar : Lean.Meta.TransparencyMode → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Comp × ℕ)
-- Mathlib.Topology.Category.Profinite.Basic
/-- `FintypeCat.toLightProfinite` is fully faithful.  -/
FintypeCat.toProfiniteFullyFaithful : FintypeCat.toProfinite.FullyFaithful
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [Infinite M'] [Nontrivial R],
  Cardinal.mk (MonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_add_add_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
        CategoryTheory.AddMonObj.add) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
      CategoryTheory.AddMonObj.add
-- Mathlib.Data.Finset.Filter
Finset.filter_congr : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {s : Finset α},
  (∀ x ∈ s, p x ↔ q x) → Finset.filter p s = Finset.filter q s
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.invalidParams.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.invalidParams = 1
-- Mathlib.Topology.Order.LeftRightNhds
nhds_eq_iInf_abs_sub : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] (a : α), nhds a = ⨅ r, ⨅ (_ : r > 0), Filter.principal {b | |a - b| < r}
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_one : (-1).arg = Real.pi
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a group by a congruence relation is a group.  -/
Con.group : {M : Type u_1} → [inst : Group M] → (c : Con M) → Group c.Quotient
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_emod_self_right : ∀ (a b c : ℤ), (a * b - c) % b = -c % b
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
/-- Flat base change commutes with `H1Cotangent`.  -/
Algebra.tensorH1CotangentOfFlat : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [Module.Flat R T] →
                  TensorProduct R T (Algebra.H1Cotangent R S) ≃ₗ[T] Algebra.H1Cotangent T (TensorProduct R T S)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.deriv_rpow_const' : ∀ (p : ℝ), (deriv fun x => x ^ p) = fun x => p * x ^ (p - 1)
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.powQuotSuccInclusion_apply_coe : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  (i : ℕ) (x : ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ (i + 1)))),
  ↑((p.powQuotSuccInclusion P i) x) = ↑x
-- Mathlib.Data.EReal.Inv
EReal.mul_div : ∀ (a b c : EReal), a * (b / c) = a * b / c
-- Init.Data.List.Find
List.findFinIdx?_subtype : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) →
    List.findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g l.unattach)
-- Mathlib.Order.Filter.AtTopBot.Field
Filter.tendsto_neg_const_mul_pow_atTop : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ},
  n ≠ 0 → c < 0 → Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atBot
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_5),
  (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).X₁ = X.E f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instZero : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Zero (PerfectClosure K p)
-- Mathlib.Algebra.Group.Shrink
Shrink.instZero : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Zero α] → Zero (Shrink.{v, u_2} α)
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBySet.quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  {s : Set R}, Module.IsTorsionBySet R M s → Module.IsTorsionBySet R (M ⧸ N) s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMonoOn.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulLeftStrictMono α], StrictMonoOn f s → ∀ (c : α), StrictMonoOn (fun x => c * f x) s
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.  -/
LinearMap.BilinForm.sum_repr_mul_repr_mul : ∀ {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} {ι : Type u_9} (b : Module.Basis ι R M) (x y : M),
  ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) = (B x) y
-- Mathlib.Topology.Instances.Irrational
dense_irrational : Dense {x | Irrational x}
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.Hom.hom.eq_1 : ∀ {X Y : CommGrpCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_discr_isUnit : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R),
  IsUnit 2 → (IsUnit W.twoTorsionPolynomial.discr ↔ IsUnit W.Δ)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.algebraMap_apply : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (k : K),
  (algebraMap K v.Completion) k = { toCompletion := ↑(WithAbs.toAbs (↑v) k) }
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endMulEquivAutGalois.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F = CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F
-- Lean.Meta.Basic
/-- Similar to `isDefEq`, but ensures default transparency is used.  -/
Lean.Meta.isDefEqD : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Std.Time.Zoned.TimeZone
/-- The name of the time zone.
 -/
Std.Time.TimeZone.name : Std.Time.TimeZone → String
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
/-- If `T` is flat over `R`, there is a `T`-linear isomorphism
`T ⊗[R] P.H1Cotangent ≃ₗ[T] (P.baseChange).H1Cotangent`.  -/
Algebra.Extension.tensorH1CotangentOfFlat : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) →
            (T : Type u_3) →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [Module.Flat R T] → TensorProduct R T P.H1Cotangent ≃ₗ[T] P.baseChange.H1Cotangent
-- Mathlib.Topology.Order.Compact
IsCompact.exists_sSup_image_eq_and_ge : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIciTopology α] {s : Set β},
  IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x
-- Mathlib.Algebra.CharP.Two
CharTwo.intCast_eq_ite : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] (n : ℤ), ↑n = if Even n then 0 else 1
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_bot' : ∀ {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NeZero μ] (X : Ω → ℝ),
  ProbabilityTheory.condVar ⊥ X μ = fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mk.inj : ∀ {A : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {left : A} {right : B} {hom : L.obj left ⟶ R.obj right} {left_1 : A} {right_1 : B}
  {hom_1 : L.obj left_1 ⟶ R.obj right_1},
  { left := left, right := right, hom := hom } = { left := left_1, right := right_1, hom := hom_1 } →
    left = left_1 ∧ right = right_1 ∧ hom ≍ hom_1