mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.flip_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g), t.flip.pt = t.pt
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The semiring topology on `MvPowerSeries` of a topological semiring  -/
MvPowerSeries.WithPiTopology.instIsTopologicalSemiring : ∀ (σ : Type u_1) (R : Type u_2) [inst : TopologicalSpace R] [inst_1 : Semiring R] [IsTopologicalSemiring R],
  IsTopologicalSemiring (MvPowerSeries σ R)
-- Mathlib.Data.Finsupp.SMul
Finsupp.distribMulAction : (α : Type u_1) →
  (M : Type u_3) →
    {R : Type u_6} → [inst : Monoid R] → [inst_1 : AddMonoid M] → [DistribMulAction R M] → DistribMulAction R (α →₀ M)
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.assoc'_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (W X Y Z : C)
  [inst_2 :
    CategoryTheory.MonoidalCoherence W
      (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).symm
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toMeasure_map_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α) (s : Set β) {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  Measurable f → MeasurableSet s → (PMF.map f p).toMeasure s = p.toMeasure (f ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk''.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : D} [inst_5 : CategoryTheory.ModObj A M]
  [inst_6 : CategoryTheory.ModObj A N] (f : M ⟶ N)
  (smul_hom :
    CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
        CategoryTheory.ModObj.smul),
  CategoryTheory.Mod.Hom.mk'' f smul_hom = { hom := f, isModHom := ⋯ }
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase0.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.erase0 c = Lean.Meta.Grind.AC.DiseqCnstrProof.erase0 c_1) = (c = c_1)
-- Init.Data.List.TakeDrop
List.tail_drop : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (List.drop i l).tail = List.drop (i + 1) l
-- Mathlib.Data.Part
Part.mod_get_eq : ∀ {α : Type u_1} [inst : Mod α] (a b : Part α) (hab : (a % b).Dom), (a % b).get hab = a.get ⋯ % b.get ⋯
-- Mathlib.Algebra.Order.Positive.Field
Positive.Subtype.inv : {K : Type u_1} → [inst : Field K] → [inst_1 : LinearOrder K] → [IsStrictOrderedRing K] → Inv { x // 0 < x }
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isRevMatch_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch p pos ↔
    ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯) = true
-- Init.Data.String.Subslice
/-- The entire slice, as a subslice of itself.  -/
String.Slice.toSubslice : (s : String.Slice) → s.Subslice
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `c.c₃?` must be `some`  -/
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂ : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.forgetToFinPartOrdFaithful : (CategoryTheory.forget₂ FinBoolAlg FinPartOrd).Faithful
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {X : T → Ω → E} {P : MeasureTheory.Measure Ω} {p q : ℝ} {M : NNReal},
  ProbabilityTheory.IsKolmogorovProcess X P p q M →
    ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_union_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε ∪ Metric.sphere x ε = Metric.closedBall x ε
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mulAction.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : MulAction α β],
  Set.mulAction = { toSMul := Set.smul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- `a` semiconjugates `x` to `a * x * a⁻¹`.  -/
SemiconjBy.conj_mk : ∀ {G : Type u_3} [inst : Group G] (a x : G), SemiconjBy a x (a * x * a⁻¹)
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_le_self : ∀ {a : ℤ} (b : ℤ), 0 ≤ a → a.fdiv b ≤ a
-- Lean.Elab.Tactic.RCases
/-- A hyphen `-`, which clears the active hypothesis and any dependents.  -/
Lean.Elab.Tactic.RCases.RCasesPatt.clear : Lean.Syntax → Lean.Elab.Tactic.RCases.RCasesPatt
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.matches : Aesop.RuleFilter → Aesop.RuleName → Bool
-- Mathlib.Combinatorics.SimpleGraph.Maps
Equiv.simpleGraph_refl : ∀ {V : Type u_1}, (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)
-- Mathlib.NumberTheory.Primorial
le_primorial_self : ∀ {n : ℕ}, n ≤ primorial n
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.homogeneousLocalizationToStalk.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↑(ProjectiveSpectrum.top 𝒜))
  (y : HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal),
  AlgebraicGeometry.homogeneousLocalizationToStalk 𝒜 x y =
    Quotient.liftOn' y
      (fun f =>
        (CategoryTheory.ConcreteCategory.hom
            ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ
              (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
          (AlgebraicGeometry.sectionInBasicOpen 𝒜 x f))
      ⋯
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
_private.Mathlib.CategoryTheory.Abelian.FreydMitchell.0.CategoryTheory.Abelian.FreydMitchell.F : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.AsSmall C)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_neg : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f : E →SL[σ] F}, ContinuousLinearMapWOT.ofCLM (-f) = -ContinuousLinearMapWOT.ofCLM f
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- The morphism from `V` to `U i` for some `i`.
 -/
TopCat.Presheaf.SheafCondition.OpensLeCover.homToIndex : {X : TopCat} →
  {ι : Type u_2} →
    {U : ι → TopologicalSpace.Opens ↑X} → (V : TopCat.Presheaf.SheafCondition.OpensLeCover U) → V.obj ⟶ U V.index
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Result.step.inj : ∀ {e' proof : Lean.Expr} {done contextDependent : Bool} {e'_1 proof_1 : Lean.Expr} {done_1 contextDependent_1 : Bool},
  Lean.Meta.Sym.Simp.Result.step e' proof done contextDependent =
      Lean.Meta.Sym.Simp.Result.step e'_1 proof_1 done_1 contextDependent_1 →
    e' = e'_1 ∧ proof = proof_1 ∧ done = done_1 ∧ contextDependent = contextDependent_1
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.apply_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f g : α →𝒄 β} {x y : α}, f ≤ g → x ≤ y → f x ≤ g y
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.coe_evalEvalRingHom : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R), ⇑(Polynomial.evalEvalRingHom x y) = Polynomial.evalEval x y
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.gcd.eq_1 : ∀ (a b : ℤ), Int.Internal.Linear.gcd✝ a b = Int.ofNat (a.gcd b)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- **Alias** of `Complex.UnitDisc.im_star`. -/
Complex.UnitDisc.im_conj : ∀ (z : Complex.UnitDisc), (star z).im = -z.im
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.unitsEquivIsUnitSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M),
  S.unitsEquivIsUnitSubmonoid = S.unitsEquivUnitsType.trans Submonoid.unitsTypeEquivIsUnitSubmonoid
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprCPUTimes : Repr Std.Internal.UV.System.CPUTimes
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.beq : {α : Type u} →
  {β : Type v} →
    [BEq α] →
      [Hashable α] →
        [BEq β] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → (Std.DHashMap.Internal.Raw₀ α fun x => β) → Bool
-- Init.Data.Int.Gcd
Int.gcd_eq_right_iff_dvd : ∀ {b a : ℤ}, 0 ≤ b → (↑(a.gcd b) = b ↔ b ∣ a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.numCases : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → ℕ
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- The neighbourhood filter of an invertible element consists of all sets containing that
element.  -/
WithZeroTopology.nhds_coe_units : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), nhds ↑γ = pure ↑γ
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanHom_one_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanHom 1 A B f ↔ Set.MapsTo f A B
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_C_mul_of_isUnit : ∀ {R : Type u} {a : R} [inst : Semiring R],
  IsUnit a → ∀ (p : Polynomial R), (Polynomial.C a * p).natDegree = p.natDegree
-- Mathlib.Order.SymmDiff
bihimp_left_involutive : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), Function.Involutive fun x => bihimp x a
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of the forward direction of `antisymmRel_iff_eq`. -/
AntisymmRel.eq : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop} [Std.Refl r] [Std.Antisymm r], AntisymmRel r a b → a = b
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero_inv_app : ∀ {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) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (X : C),
  (CategoryTheory.Functor.CommShift.isoZero F A).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X))
      (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CochainComplex.mappingConeCompHomotopyEquiv f g =
    { hom := CochainComplex.MappingConeCompHomotopyEquiv.hom f g,
      inv := CochainComplex.MappingConeCompHomotopyEquiv.inv f g, homotopyHomInvId := Homotopy.ofEq ⋯,
      homotopyInvHomId := CochainComplex.MappingConeCompHomotopyEquiv.homotopyInvHomId f g }
-- Mathlib.Data.Nat.Cast.WithTop
Nat.cast_withBot : ∀ (n : ℕ), ↑n = ↑n
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_mul_mk'_of_map_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7}
  [inst_1 : NonUnitalNonAssocSemiring M] [inst_2 : Semiring M'] [inst_3 : Module R M] [inst_4 : Algebra R M']
  (f : M →ₗ[R] M'),
  (∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂) →
    ∀ [inst_5 : IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : ↥S),
      IsLocalizedModule.mk' f m₁ s₁ * IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (m₁ * m₂) (s₁ * s₂)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- `a ^ 0 = 1`  -/
LinearOrderedCommGroupWithZero.zpow_zero' : ∀ {α : Type u_3} [self : LinearOrderedCommGroupWithZero α] (a : α), a ^ 0 = 1
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.mk.inj : ∀ {toInlayHintInfo : Lean.Elab.InlayHintInfo} {lctx : Lean.LocalContext}
  {deferredResolution : Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo}
  {toInlayHintInfo_1 : Lean.Elab.InlayHintInfo} {lctx_1 : Lean.LocalContext}
  {deferredResolution_1 : Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo},
  { toInlayHintInfo := toInlayHintInfo, lctx := lctx, deferredResolution := deferredResolution } =
      { toInlayHintInfo := toInlayHintInfo_1, lctx := lctx_1, deferredResolution := deferredResolution_1 } →
    toInlayHintInfo = toInlayHintInfo_1 ∧ lctx = lctx_1 ∧ deferredResolution = deferredResolution_1
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
/-- The explicit cocone with tensor products as the fibered coproduct in `CommAlgCat`.  -/
CommAlgCat.binaryCofan : {R : Type u} → [inst : CommRing R] → (A B : CommAlgCat R) → CategoryTheory.Limits.BinaryCofan A B
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃Functor_obj_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₁) (k : C₃) (j : C₂),
  (((CategoryTheory.Functor.flip₂₃Functor.obj F).obj G).obj k).obj j = ((F.obj G).obj j).obj k
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_iff_le_and_ne` -/
ssubset_iff_subset_and_ne : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊂ b ↔ a ⊆ b ∧ a ≠ b
-- Mathlib.Data.Finset.Sups
Finset.compl_mem_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α} {a : α}, a ∈ s → aᶜ ∈ s.compls
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.curryLinearEquiv_symm_apply : ∀ {α : Type u_9} {β : Type u_10} (R : Type u_11) {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (a : α →₀ β →₀ M), (Finsupp.curryLinearEquiv R).symm a = a.uncurry
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- `ιInvApp` is the left inverse of `D.ι i` on `U`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)),
  ∃ (eq :
    Opposite.op U =
      Opposite.op
        ((TopologicalSpace.Opens.map
              (CategoryTheory.Limits.colimit.ι D.diagram.multispan
                  (Opposite.unop (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)))).base).obj
          (⋯.functor.obj U))),
    CategoryTheory.CategoryStruct.comp (D.ιInvApp U) (D.diagramOverOpenπ U i) =
      (D.U i).presheaf.map (CategoryTheory.eqToHom eq)
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderIso.image_setOfPred_maximal`. -/
OrderIso.image_setOf_maximal : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (P : α → Prop),
  ⇑f '' {x | Maximal P x} = {x | Maximal (fun x => P (f.symm x)) x}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A pushout cocone is just a cocone on the span formed by two morphisms `f : X ⟶ Y` and
`g : X ⟶ Z`.  -/
CategoryTheory.Limits.PushoutCocone : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : C} → (X ⟶ Y) → (X ⟶ Z) → Type (max (max 0 u) v)
-- Mathlib.Algebra.GradedMulAction
/-- A graded version of `SMul`. Scalar multiplication combines grades additively, i.e.
if `a ∈ A i` and `m ∈ M j`, then `a • b` must be in `M (i + j)`.  -/
GradedMonoid.GSMul : {ιA : Type u_1} →
  {ιM : Type u_3} → (ιA → Type u_4) → (ιM → Type u_5) → [VAdd ιA ιM] → Type (max (max (max u_1 u_3) u_4) u_5)
-- Mathlib.Topology.MetricSpace.Contracting
/-- The unique fixed point of a contracting map in a nonempty complete metric space.  -/
ContractingWith.fixedPoint : {α : Type u_1} →
  [inst : MetricSpace α] → {K : NNReal} → (f : α → α) → ContractingWith K f → [Nonempty α] → [CompleteSpace α] → α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyComplex.mk : ∀ {K : Type u_1} [inst : Field K], (∀ (v : NumberField.InfinitePlace K), v.IsComplex) → NumberField.IsTotallyComplex K
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp.injEq : ∀ (e : Lean.Expr) (f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁) (η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (e_1 : Lean.Expr) (f₁_1 g₁_1 f₂_1 g₂_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e_1 f₁_1 g₁_1 f₂_1 g₂_1 η_1 θ_1) =
    (e = e_1 ∧ f₁ = f₁_1 ∧ g₁ = g₁_1 ∧ f₂ = f₂_1 ∧ g₂ = g₂_1 ∧ η = η_1 ∧ θ = θ_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_alter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).size ≤ m.size + 1
-- Lean.Environment
/-- "Forward declaration" needed for updating the attribute table with user-defined attributes.
User-defined attributes are declared using the `initialize` command. The `initialize` command is just syntax sugar for the `init` attribute.
The `init` attribute is initialized after the `attributeExtension` is initialized. We cannot change the order since the `init` attribute is an attribute,
and requires this extension.
The `attributeExtension` initializer uses `attributeMapRef` to initialize the attribute mapping.
When we a new user-defined attribute declaration is imported, `attributeMapRef` is updated.
Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`.
 -/
Lean.updateEnvAttributes : Lean.Environment → IO Lean.Environment
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `getLast_edges_eq_mk_penultimate_end` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.mk_penultimate_end_eq_getLast_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil), s(p.penultimate, w) = p.edges.getLast ⋯
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.integralBasis_repr_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.RingOfIntegers K)
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  ((NumberField.integralBasis K).repr ((algebraMap (NumberField.RingOfIntegers K) K) x)) i =
    (algebraMap ℤ ℚ) (((NumberField.RingOfIntegers.basis K).repr x) i)
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.eq : ∀ {α : Type u_1} {f : Filter α} (self : f.Realizer), self.F.toFilter = f
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddCon.instPartialOrder =
    { toLE := AddCon.instLE, lt := fun a b => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯ }
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.exists_eq_inl_add : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G), ∃ n, σ g = S.inl n + σ' g
-- Mathlib.GroupTheory.Sylow
IsPGroup.sylow_mem_fixedPoints_iff : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P : Subgroup G},
  IsPGroup p ↥P → ∀ {Q : Sylow p G}, Q ∈ MulAction.fixedPoints (↥P) (Sylow p G) ↔ P ≤ ↑Q
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.spine_arrow : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := hₘ })) (i : Fin m),
  (X.spine m hₘ Δ).arrow i =
    (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ hₘ).op))
      Δ
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.of_f : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {i j : ι} {hij : i ≤ j}
  {x : G i}, (DirectLimit.Module.of R ι G f j) ((f i j hij) x) = (DirectLimit.Module.of R ι G f i) x
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- If `C` has finite coproducts, a functor `Discrete α ⥤ C` lifts to a functor
`Finset (Discrete α) ⥤ C` by taking coproducts.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [CategoryTheory.Limits.HasFiniteProducts C] →
        CategoryTheory.Functor (CategoryTheory.Discrete α) C →
          CategoryTheory.Functor (Finset (CategoryTheory.Discrete α))ᵒᵖ C
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket `[V, W] (x)` of two vector fields at a point, defined as
`DW(x) (V x) - DV(x) (W x)`.  -/
VectorField.lieBracket : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (E → E) → (E → E) → E → E
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_preconnected_bot : ∀ {V : Type u} [Nontrivial V], ¬⊥.Preconnected
-- Init.Data.SInt.Lemmas
Int64.mul_neg : ∀ (a b : Int64), a * -b = -(a * b)
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_ideal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R],
  (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0) fun I => ↑I
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasureClass.measure_empty : ∀ {F : Type u_2} {α : outParam (Type u_3)} {inst : FunLike F (Set α) ENNReal}
  [self : MeasureTheory.OuterMeasureClass F α] (f : F), f ∅ = 0
-- Mathlib.CategoryTheory.Shift.CommShift
/-- If a functor `F : C ⥤ D` is equipped with "commutation isomorphisms" with the
shifts by `a` and `b`, then there is a commutation isomorphism with the shift by `a + b`.  -/
CategoryTheory.Functor.CommShift.isoAdd : {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} →
          {A : Type u_4} →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  {a b : A} →
                    ((CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) →
                      ((CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) →
                        ((CategoryTheory.shiftFunctor C (a + b)).comp F ≅
                          F.comp (CategoryTheory.shiftFunctor D (a + b)))
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfShape J F],
  CategoryTheory.Limits.ReflectsLimit K F