mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Lattice.Nat
Set.biUnion_lt_succ : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋃ k, ⋃ (_ : k < n + 1), u k = (⋃ k, ⋃ (_ : k < n), u k) ∪ u n
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- **Alias** of `CircleIntegrable.continuousOn_smul`.

---

If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g • f` is
circle integrable.
 -/
CircleIntegrable.smul_of_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (g • f) c R
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_comp : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n')
  (e₁' : m' ≃ m'') (e₂' : n' ≃ n''),
  ⇑(Matrix.reindexLinearEquiv R A e₁' e₂') ∘ ⇑(Matrix.reindexLinearEquiv R A e₁ e₂) =
    ⇑(Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductive.go.eq_def : ∀ (ctx : Lean.Meta.IndPredBelow.Context✝) (minorArgs : Array Lean.Expr) (body : Lean.Expr) (i : ℕ)
  (vars : Array Lean.Expr),
  Lean.Meta.IndPredBelow.mkBelowInductive.go✝ ctx minorArgs body i vars =
    if h : i < minorArgs.size then do
      let type ← Lean.Meta.inferType minorArgs[i]
      match Lean.Meta.IndPredBelow.isIH✝ type ctx with
        | some val => do
          let __do_lift ← liftM (Lean.mkFreshUserName `ih)
          Lean.Meta.withLocalDeclD __do_lift (Lean.Meta.IndPredBelow.ihTypeToBelowType✝ type ctx) fun below =>
              Lean.Meta.IndPredBelow.mkBelowInductive.go✝ ctx minorArgs body (i + 1)
                ((vars.push below).push minorArgs[i])
        | x => Lean.Meta.IndPredBelow.mkBelowInductive.go✝ ctx minorArgs body (i + 1) (vars.push minorArgs[i])
    else Lean.Meta.mkForallFVars vars (Lean.Meta.IndPredBelow.ihTypeToBelowType✝ body ctx)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.finite_of_isBasis : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsRkFinite X → M.IsBasis I X → I.Finite
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] (c : ENNReal),
  c ≠ 0 → MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive (c • μ) T
-- Mathlib.Topology.Baire.BaireMeasurable
IsMeagre.baireMeasurableSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsMeagre s → BaireMeasurableSet s
-- Aesop.Tree.Data
Aesop.RappData.isIrrelevant : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Bool
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.eq_mul : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I → g = ↑f * h
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is closed under multiplication.  -/
IntermediateField.mul_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x y : L}, x ∈ S → y ∈ S → x * y ∈ S
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsAffineCoprodScheme : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.IsAffine (X ⨿ Y)
-- Mathlib.Algebra.Lie.TransferInstance
/-- Transfer `LieRing` across an `AddEquiv`  -/
AddEquiv.lieRing : {M : Type u_2} → {L : Type u_3} → [inst : AddCommGroup M] → [inst_1 : LieRing L] → M ≃+ L → LieRing M
-- Init.Data.List.Erase
List.eraseP_append_left : ∀ {α : Type u_1} {p : α → Bool} {a : α},
  p a = true → ∀ {l₁ : List α} (l₂ : List α), a ∈ l₁ → List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq.eq_3 : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  (x = Lean.Grind.CommRing.Mon.unit → x_1 = Lean.Grind.CommRing.Mon.unit → False) →
    (∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
        (b_1 : Lean.Grind.CommRing.Mon),
        x = Lean.Grind.CommRing.Mon.mult a a_1 → x_1 = Lean.Grind.CommRing.Mon.mult b b_1 → False) →
      Lean.Grind.CommRing.instBEqMon.beq x x_1 = false
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_and : ∀ (a b : USize) (h : System.Platform.numBits = 64), (a &&& b).toBitVec64 h = a.toBitVec64 h &&& b.toBitVec64 h
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instStarModuleReal : StarModule ℝ ℂ
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : α →Co β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for the `max` operator. The `max` of two numbers is nonnegative if at least one
is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero.  -/
Mathlib.Meta.Positivity.evalMax : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α},
  (m₁ ∩ m₂).getKey! k = if k ∈ m₂ then m₁.getKey! k else default
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoDiv hp a (b + ↑m * p) = toIcoDiv hp a b + ↑m
-- Mathlib.Analysis.Quaternion
/-- Coercion `ℂ →ₐ[ℝ] ℍ` as an algebra homomorphism.  -/
Quaternion.ofComplex : ℂ →ₐ[ℝ] Quaternion ℝ
-- Std.Tactic.Do.Syntax
/-- `vcgen` step for `sym => …` blocks. No `with` clause: compose with subsequent grind
steps using `<;>` instead.  -/
Lean.Parser.Tactic.Grind.vcgen : Lean.ParserDescr
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_self_lt_prod_self : ∀ {α : Type u_1} [inst : Preorder α] {s₁ s₂ : LowerSet α}, s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.instMonadTraverserParenthesizerM : Lean.Syntax.MonadTraverser Lean.PrettyPrinter.ParenthesizerM
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom_comp : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} {O : Type u_10} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : AddMonoid O] (f : N →+ O) (g : M →+ N),
  AddMonoidAlgebra.mapDomainBialgHom R (f.comp g) =
    (AddMonoidAlgebra.mapDomainBialgHom R f).comp (AddMonoidAlgebra.mapDomainBialgHom R g)
-- Lean.Elab.ConfigEval.DeriveEvalExpr
_private.Lean.Elab.ConfigEval.DeriveEvalExpr.0.Lean.Elab.ConfigEval.ensureEvalExpr.getIndType : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.InductiveVal
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.newLetDecls : Lean.Elab.Term.MutualClosure.ClosureState → Array Lean.LocalDecl
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.span_basisSet : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  Submodule.span ℚ (⇑toRatVec✝ '' IsProperLinearSet.basisSet✝ hs) = ⊤
-- Mathlib.Condensed.Light.Module
LightCondensed.forget_map_hom_app_hom_apply : ∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) (S : LightProfiniteᵒᵖ)
  (a :
    ↑(((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).obj X).obj S)),
  (CategoryTheory.ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app S)) a =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app S)) a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.star_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing 𝕜]
  [inst_6 : StarRing A] [inst_7 : StarModule 𝕜 A] [inst_8 : NormedStarGroup A] (a : DoubleCentralizer 𝕜 A) (b : A),
  (star a).toProd.1 b = star (a.toProd.2 (star b))
-- Mathlib.Control.Basic
CommApplicative.toLawfulApplicative : ∀ {m : Type u → Type v} {inst : Applicative m} [self : CommApplicative m], LawfulApplicative m
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- When `R` is a field `F`, then a nontrivial additive character is primitive  -/
AddChar.IsPrimitive.of_ne_one : ∀ {R' : Type v} [inst : CommMonoid R'] {F : Type u} [inst_1 : Field F] {ψ : AddChar F R'}, ψ ≠ 1 → ψ.IsPrimitive
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getKey` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getKeyₘ : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → (l : Std.DTreeMap.Internal.Impl α β) → (k : α) → (l.getKey?ₘ k).isSome = true → α
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.not_spanning_iff_closure_ssubset : ∀ {α : Type u_2} {M : Matroid α} {S : Set α},
  autoParam (S ⊆ M.E) Matroid.not_spanning_iff_closure_ssubset._auto_1 → (¬M.Spanning S ↔ M.closure S ⊂ M.E)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.iIndepFun_indicator : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_6} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Zero β]
  [inst_1 : One β] {m : MeasurableSpace β} {s : ι → Set Ω},
  ProbabilityTheory.iIndepSet s μ → ProbabilityTheory.iIndepFun (fun n => (s n).indicator fun _ω => 1) μ
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- Boundaryless `ModelWithCorners` implies boundaryless manifold.  -/
ModelWithCorners.instBoundarylessManifold : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [I.Boundaryless], BoundarylessManifold I M
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Finset.hasSum : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α)
  (L : optParam (SummationFilter ↑↑s) (SummationFilter.unconditional ↑↑s)) [L.LeAtTop],
  HasSum (f ∘ Subtype.val) (∑ b ∈ s, f b) L
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxBraidedMonMapMon : {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 D] →
            {F : CategoryTheory.Functor C D} →
              [inst_4 : CategoryTheory.SymmetricCategory C] →
                [inst_5 : CategoryTheory.SymmetricCategory D] → [inst_6 : F.LaxBraided] → F.mapMon.LaxBraided
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_mono_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁.addEnergy t ≤ s₂.addEnergy t
-- Mathlib.Algebra.Tropical.Basic
Tropical.instNoZeroDivisorsWithTop : ∀ {R : Type u_1} [inst : AddCommMonoid R], NoZeroDivisors (Tropical (WithTop R))
-- Mathlib.Order.Monotone.Basic
Monotone.strictMono_iff_injective : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → (StrictMono f ↔ Function.Injective f)
-- Mathlib.Analysis.Convex.Combination
/-- This is a version of `Finset.mem_convexHull` stated without `Finset.centerMass`.  -/
Finset.mem_convexHull' : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s : Finset E} {x : E},
  x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.opEquivalence_functor : CategoryTheory.RelCat.opEquivalence.functor = CategoryTheory.RelCat.opFunctor
-- Mathlib.Order.Filter.Defs
Filter.mem_bot : ∀ {α : Type u_1} {s : Set α}, s ∈ ⊥
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜), iteratedDeriv n (fun x => -f x) a = -iteratedDeriv n f a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.lintegral_mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ENNReal)
  (hf : MeasureTheory.AEStronglyMeasurable f μ), (MeasureTheory.AEEqFun.mk f hf).lintegral = ∫⁻ (a : α), f a ∂μ
-- Mathlib.Order.Filter.Pointwise
Filter.add_eq_zero_iff : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {f g : Filter α}, f + g = 0 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a + b = 0
-- Mathlib.RingTheory.LocalProperties.Projective
Module.finrank_of_isLocalizedModule_of_free : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Rₛ : Type u_4)
  {Mₛ : Type u_5} [inst_3 : AddCommGroup Mₛ] [inst_4 : Module R Mₛ] [inst_5 : CommRing Rₛ] [inst_6 : Algebra R Rₛ]
  [inst_7 : Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ]
  [IsLocalizedModule S f] [Module.Free R M] [Nontrivial Rₛ], Module.finrank Rₛ Mₛ = Module.finrank R M
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instNonUnitalSemiring : {α : Type u_1} →
  [DecidableEq α] →
    [inst : NonUnitalSemiring α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → [NoZeroDivisors α] → NonUnitalSemiring (WithTop α)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.unsat_iff : ∀ {aig : Std.Sat.AIG ℕ} {state : Std.Sat.AIG.toCNF.State✝ aig},
  Std.Sat.AIG.toCNF.State.Unsat✝ state ↔ (Std.Sat.AIG.toCNF.State.cnf✝ state).Unsat
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddLeftCancelMonoidOfAddOpposite : {M : Type u_1} → [AddLeftCancelMonoid Mᵃᵒᵖ] → AddLeftCancelMonoid Mᵈᵃᵃ
-- Mathlib.Data.Fin.Tuple.Curry
Function.OfArity.curryEquiv_apply : ∀ {α β : Type u} (n : ℕ) (a : (Fin n → α) → β), (Function.OfArity.curryEquiv n) a = Function.FromTypes.curry a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instFullAddGrpFunctorOppositeAddGrpCatYonedaAddGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddGrp.Full
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_min' : ∀ {G : Type u} [inst : AddMonoid G] (n : ℕ), 0 < n → (∀ (g : G), n • g = 0) → AddMonoid.exponent G ≤ n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Raw.Const.get! (m₁ ∩ m₂) k =
          if m₂.contains k = true then Std.DTreeMap.Raw.Const.get! m₁ k else default
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_nat_inv_pow : ∀ (x : ℂ) {n : ℕ}, n ≠ 0 → (x ^ (↑n)⁻¹) ^ n = x
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.le_comap_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (L M : BooleanSubalgebra β)
  (f : BoundedLatticeHom α β),
  BooleanSubalgebra.comap f L ⊔ BooleanSubalgebra.comap f M ≤ BooleanSubalgebra.comap f (L ⊔ M)
-- Mathlib.RingTheory.Localization.Defs
Localization.toLocalizationMap_eq_monoidOf : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R},
  IsLocalization.toLocalizationMap M (Localization M) = Localization.monoidOf M
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrLeft'_symm : ∀ {α : Type u_2} {β : Type u_3} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] (e : α ≃ β),
  (RingEquiv.piCongrLeft' (fun x => R) e).symm = RingEquiv.piCongrLeft' (fun i => R) e.symm
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset_2 : HSub Std.Time.DateTime Std.Time.Hour.Offset Std.Time.DateTime
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is a complex, this is the morphism from the opcycles of `S` in
degree `k + 1` to the cycles of `S` in degree `k + 2`.  -/
CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S : CategoryTheory.ComposableArrows C (n + 3)} →
          (hS : S.IsComplex) →
            (k : ℕ) →
              (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles._auto_1) →
                [inst_2 : (S.sc hS k ⋯).HasRightHomology] →
                  [inst_3 : (S.sc hS (k + 1) ⋯).HasLeftHomology] → (S.sc hS k ⋯).opcycles ⟶ (S.sc hS (k + 1) ⋯).cycles
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.ofHom_id : ∀ (P : TopCat → Prop) {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : CompHausLike.HasProp P X],
  CompHausLike.ofHom P (ContinuousMap.id X) = CategoryTheory.CategoryStruct.id (CompHausLike.of P X)
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.map_jacobson_of_bijective : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {I : Ideal R} {f : R →+* S},
  Function.Bijective ⇑f → Ideal.map f I.jacobson = (Ideal.map f I).jacobson
-- Std.Http.Data.Headers.Basic
Std.Http.instEncodeV11OfHeader : {α : Type} → [h : Std.Http.Header α] → Std.Http.Internal.Encode Std.Http.Version.v11 α
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.eq_rpow_inv : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → z ≠ 0 → (x = y ^ z⁻¹ ↔ x ^ z = y)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_3.splitter : (motive : ONote → Sort u_1) →
  (o : ONote) →
    (Unit → motive ONote.zero) → ((e' : ONote) → (n' : ℕ+) → (a' : ONote) → motive (e'.oadd n' a')) → motive o
-- Mathlib.RingTheory.Regular.RegularSequence
Ideal.ofList_singleton : ∀ {R : Type u_1} [inst : Semiring R] (r : R), Ideal.ofList [r] = Ideal.span {r}
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.congr_eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) (h_1 : Unit → motive none)
  (h_2 :
    (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
        (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup }))
  (h_3 : (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some val)),
  x = none →
    (match x with
      | none => h_1 ()
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } => h_2 l nodupkey nodup
      | some val => h_3 val) ≍
      h_1 ()
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `f` is monic, the powers of `h.root` form a basis.  -/
IsAdjoinRootMonic.powerBasis : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRootMonic S f → PowerBasis R S
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_cells : ∀ {μ : YoungDiagram} (c : ℕ × ℕ), c ∈ μ.cells ↔ c ∈ μ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `inv_lt'`. -/
inv_lt_of_inv_lt' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
  a⁻¹ < b → b⁻¹ < a
-- Mathlib.Order.InitialSeg
/-- An initial segment can be extended to an isomorphism by joining a second well order to the
domain.  -/
InitialSeg.exists_sum_relIso : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s),
  ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
-- Lean.DocString.Add
Lean.VersoDocResult.mk : Lean.VersoDocString → Array Lean.Doc.DeferredCheck → Lean.VersoDocResult
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_dvd_totient : ∀ (n : ℕ), ArithmeticFunction.carmichael n ∣ n.totient
-- Mathlib.Order.ULift
ULift.down_sup : ∀ {α : Type u} [inst : Max α] (a b : ULift.{u_1, u} α), (a ⊔ b).down = a.down ⊔ b.down
-- Init.Data.String.Lemmas.FindPos
String.Pos.ofSliceFrom_prev : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).startPos},
  String.Pos.ofSliceFrom (p.prev h) = (String.Pos.ofSliceFrom p).prev ⋯
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_sup_right : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} {x : M}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- The fundamental property of the operator norm of a continuous alternating map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`, `nnnorm` version.  -/
ContinuousAlternatingMap.le_opNNNorm : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m : ι → E), ‖f m‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects finite coproducts, then `F.leftOp : Cᵒᵖ ⥤ D` reflects finite
products.  -/
CategoryTheory.Limits.reflectsFiniteProducts_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteCoproducts F],
  CategoryTheory.Limits.ReflectsFiniteProducts F.leftOp
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Up to a (unique) isomorphism, the functor
`pullFunctor : F.DescentData f ⥤ F.DescentData f'` does not depend
on the auxiliary data.  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {p : S' ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S'} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (w :
                                ∀ (j : ι'),
                                  CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                    CategoryTheory.CategoryStruct.comp (f' j) p) →
                              {β : ι' → ι} →
                                {p'' : (j : ι') → X' j ⟶ X (β j)} →
                                  (w' :
                                      ∀ (j : ι'),
                                        CategoryTheory.CategoryStruct.comp (p'' j) (f (β j)) =
                                          CategoryTheory.CategoryStruct.comp (f' j) p) →
                                    CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w ≅
                                      CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w'
-- Mathlib.Algebra.Lie.Basic
neg_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M),
  ⁅-x, m⁆ = -⁅x, m⁆