mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Pi
/-- The product of a family of ordered additive commutative monoids is
an ordered additive commutative monoid.  -/
Pi.isOrderedAddMonoid : ∀ {ι : Type u_6} {Z : ι → Type u_7} [inst : (i : ι) → AddCommMonoid (Z i)] [inst_1 : (i : ι) → Preorder (Z i)]
  [∀ (i : ι), IsOrderedAddMonoid (Z i)], IsOrderedAddMonoid ((i : ι) → Z i)
-- Mathlib.Topology.Order.T5
Set.ordConnectedComponent_mem_nhds : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {s : Set X},
  s.ordConnectedComponent a ∈ nhds a ↔ s ∈ nhds a
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.pullback_factors : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (y : CategoryTheory.Subobject Y) (h : W ⟶ X),
  y.Factors (CategoryTheory.CategoryStruct.comp h f) → ((CategoryTheory.Subobject.pullback f).obj y).Factors h
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instSemigroup : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] → (ρ : Representation A G V) → Semigroup (ρ.IntertwiningMap ρ)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.ofCommaMorphism_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {c c' :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)}
  (φ : c ⟶ c') (x : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.ofCommaMorphism φ).app x =
    match x with
    | CategoryTheory.WithTerminal.of x => φ.left.app x
    | CategoryTheory.WithTerminal.star => φ.right
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_of_length_le : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} {p : G.Walk u v} (h : p.length ≤ n),
  p.drop n = SimpleGraph.Walk.nil.copy ⋯ ⋯
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.zero'_eval : Turing.ToPartrec.Code.zero'.eval = fun v => pure (0 :: v)
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instAddCommSemigroup : AddCommSemigroup ℕ
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of a closed range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Rcc.HasRcoIntersection : Type w → Type w
-- Mathlib.Data.Ordmap.Invariants
/-- The `BalancedSz l r` asserts that a hypothetical tree with children of sizes `l` and `r` is
balanced: either `l ≤ δ * r` and `r ≤ δ * r`, or the tree is trivial with a singleton on one side
and nothing on the other.  -/
Ordnode.BalancedSz : ℕ → ℕ → Prop
-- Mathlib.Tactic.GRewrite.Core
/-- The outermost local context in which the rewrite makes sense. If the rewrite does not involve
bound variables, this is `none`. This is used for fixing the generated info tree, so that the
"Expected Type" is displayed correctly.  -/
Mathlib.Tactic.GRewrite.GRewriteResult.lctx? : Mathlib.Tactic.GRewrite.GRewriteResult → Option Lean.LocalContext
-- Mathlib.LinearAlgebra.Matrix.ZPow
IsUnit.det_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), IsUnit (A ^ n).det
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.nonUnitalStarAlgHom_apply : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S] [inst_6 : StarRing S]
  [inst_7 : TopologicalSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S] [inst_10 : NonUnitalRing A]
  [inst_11 : StarRing A] [inst_12 : Algebra R S] [inst_13 : Module R A] [inst_14 : Module S A]
  [inst_15 : IsScalarTower S A A] [inst_16 : SMulCommClass S A A] [inst_17 : IsScalarTower R S A]
  [inst_18 : StarModule R S] [inst_19 : ContinuousSMul R S] {a : A}
  (φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A) {f : C(S, R)} (h : QuasispectrumRestricts a ⇑f)
  (a_1 : ContinuousMapZero (↑(quasispectrum R a)) R),
  (QuasispectrumRestricts.nonUnitalStarAlgHom φ h) a_1 =
    φ
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (a_1.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
-- Mathlib.Data.Sym.Sym2
Sym2.disjoint_diagSet_fromRel : ∀ {α : Type u_1} {r : α → α → Prop} (hr : Std.Symm r), Disjoint Sym2.diagSet (Sym2.fromRel hr) ↔ Std.Irrefl r
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.iff_all_liftAt : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n),
  T.Iff φ (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt32HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Lean.Meta.ArgsPacker
/-- Given expression `e` of type `(x : a₁ ⊗' b₁ ⊕' a₂ ⊗' d₂ …) → e[x]`, uncurries the expression and
projects to the `i`th function of type,
```
((x : aᵢ) → (y : bᵢ) → e[.inr….inl (x,y)])
```
 -/
Lean.Meta.ArgsPacker.curryProj : Lean.Meta.ArgsPacker → Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Presieve.isSheafFor_singleton_iff_of_iso : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {S X Y : C}
  (f : X ⟶ S) (g : Y ⟶ S) (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp e.hom g = f →
    (CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f) ↔
      CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton g))
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.unsat_of_lift_unsat : ∀ (cnf : Std.Sat.CNF ℕ), (Std.Tactic.BVDecide.LRAT.Internal.CNF.lift cnf).Unsat → cnf.Unsat
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.forIn'.loop : {β : Type} →
  (Std.Http.Chunk → β → Std.Async.ContextAsync (ForInStep β)) → Std.Http.Body.Stream → β → Std.Async.ContextAsync β
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredOrEmptyForall : ∀ {α : Type w} {I : α → Type u₁} [inst : (i : α) → CategoryTheory.Category.{v₁, u₁} (I i)]
  [∀ (i : α), CategoryTheory.IsCofilteredOrEmpty (I i)], CategoryTheory.IsCofilteredOrEmpty ((i : α) → I i)
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.lift_apply : ∀ {X Y Z : TopCat} {f : X ⟶ Y} {g : X ⟶ Z} {x : ↑X},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CartesianMonoidalCategory.lift f g)) x =
    ((CategoryTheory.ConcreteCategory.hom f) x, (CategoryTheory.ConcreteCategory.hom g) x)
-- Lean.Meta.Tactic.Grind.ForallProp
/-- Given a proof of an `EMatchTheorem`, returns `true`, if there are no
anchor references restricting the search, or there is an anchor
references `ref` s.t. `ref` matches `proof`.
 -/
Lean.Meta.Grind.checkAnchorRefsEMatchTheoremProof : Lean.Expr → Lean.Meta.Grind.GrindM Bool
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_inj : ∀ {R : Type u_2} [inst : NonAssocRing R] {S T : Subring R}, S.op = T.op ↔ S = T
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Ideal.dvdNotUnit_iff_lt : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {I J : Ideal A}, DvdNotUnit I J ↔ J < I
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_toSlice : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat pos₁ pos₂ ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat.toSlice pos₁ pos₂
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- Left `wrap` cancellation theorem of the form
```
toInt a = i.wrap a' → toInt b = b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
```
 -/
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.c_wl? : Lean.Meta.Grind.Arith.Cutsat.ToIntThms → Option Lean.Expr
-- Mathlib.Topology.MetricSpace.Thickening
IsCompact.exists_thickening_subset_open : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  IsCompact s → IsOpen t → s ⊆ t → ∃ δ, 0 < δ ∧ Metric.thickening δ s ⊆ t
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_castPred : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n), (i.castPred h).castSucc = i
-- Mathlib.GroupTheory.Torsion
IsMulTorsion.eq_1 : ∀ (G : Type u_1) [inst : Monoid G], IsMulTorsion G = ∀ (g : G), IsOfFinOrder g
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.iff_not_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Iff φ φ.not.not
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.bot_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ⊥ = 0
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.image_op_smul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, MulOpposite.op '' s • t = t * s
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.convexCombPair_iConvexComb_iConvexComb.match_1_1.splitter : (motive : Fin 0 → Sort u_1) → (a : Fin 0) → motive a
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_le_minKey_erase : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α}
  {he : (Std.Internal.List.eraseKey k l).isEmpty = false},
  (compare (Std.Internal.List.minKey l ⋯) (Std.Internal.List.minKey (Std.Internal.List.eraseKey k l) he)).isLE = true
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.reduceBinPred : Lean.Name → ℕ → (ℕ → ℕ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- `Precoherent` is preserved by equivalence of categories.  -/
CategoryTheory.Equivalence.precoherent : ∀ {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] [CategoryTheory.Precoherent C] (e : C ≌ D),
  CategoryTheory.Precoherent D
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l)[k']? = some v
-- Mathlib.Data.Set.FiniteExhaustion
/-- A `FiniteExhaustion` of a set `s` is a monotonically increasing sequence
of finite sets such that their union is `s`.  -/
Set.FiniteExhaustion : {α : Type u_1} → Set α → Type u_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.Ψ₂Sq_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 4 ≠ 0 → W.Ψ₂Sq ≠ 0
-- Mathlib.Topology.Connected.LocallyPathConnected
IsOpen.pathComponentIn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X} [LocallyPathConnectedSpace X],
  IsOpen F → ∀ (x : X), IsOpen (pathComponentIn F x)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field contains the ring's 1.  -/
IntermediateField.one_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),
  1 ∈ S
-- Mathlib.SetTheory.Lists
Lists'.brecOn.go : {α : Type u} →
  {motive : (a : Bool) → Lists' α a → Sort u_1} →
    {a : Bool} →
      (t : Lists' α a) → ((a : Bool) → (t : Lists' α a) → Lists'.below t → motive a t) → motive a t ×' Lists'.below t
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instSupSet : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → SupSet (MeasureTheory.Filtration ι m)
-- Batteries.Lean.AttributeExtra
/-- The underlying `ParametricAttribute`.  -/
Lean.ParametricAttributeExtra.attr : {α : Type} → Lean.ParametricAttributeExtra α → Lean.ParametricAttribute α
-- Mathlib.Combinatorics.Enumerative.Composition
instDecidableEqComposition : {n : ℕ} → DecidableEq (Composition n)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  {ι : Type u_3} [inst_6 : Fintype ι] {X : ι → Ω → E},
  (∀ (i : ι), ProbabilityTheory.HasGaussianLaw (X i) P) →
    ProbabilityTheory.iIndepFun X P → ProbabilityTheory.HasGaussianLaw (fun ω => ∑ i, X i ω) P
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `zero_apply`. -/
NonarchAddGroupSeminorm.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).isEmpty = false ↔
      ∃ k, ∃ (h : m.contains k = true), f k (m.get k h) = true)
-- Mathlib.Combinatorics.Additive.Dissociation
AddDissociated.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] (s : Set α), AddDissociated s = Set.InjOn (fun x => ∑ x ∈ x, x) {t | ↑t ⊆ s}
-- Mathlib.Analysis.CStarAlgebra.Basic
Pi.cstarRing : ∀ {ι : Type u_4} {R : ι → Type u_7} [inst : (i : ι) → NonUnitalNormedRing (R i)] [inst_1 : (i : ι) → StarRing (R i)]
  [inst_2 : Fintype ι] [∀ (i : ι), CStarRing (R i)], CStarRing ((i : ι) → R i)
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.continuous_toPiNat : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [inst : Encodable ι]
  [inst_1 : (i : ι) → PseudoMetricSpace (Y i)] [inst_2 : TopologicalSpace X],
  (∀ (i : ι), Continuous (f i)) → Continuous Metric.PiNatEmbed.toPiNat
-- Mathlib.Analysis.Complex.Harmonic.Analytic
/-- **Alias** of `InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq`. -/
harmonic_is_realOfHolomorphic : ∀ {f : ℂ → ℝ} {z : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.ball z R) →
    ∃ F, AnalyticOnNhd ℂ F (Metric.ball z R) ∧ Set.EqOn (fun z => (F z).re) f (Metric.ball z R)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_rpow_of_log_lt : ∀ {x y z : ℝ}, 0 < y → Real.log x < z * Real.log y → x < y ^ z
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocInfo.injEq : ∀ (i i_1 : Lean.Elab.DocInfo), (Lean.Elab.Info.ofDocInfo i = Lean.Elab.Info.ofDocInfo i_1) = (i = i_1)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
/-- See the public version `PowerSeries.WithPiTopology.tprod_one_sub_X_pow` that removes
`IsTopologicalRing`.  -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries.0.PowerSeries.WithPiTopology.tprod_one_sub_X_pow' : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R],
  ∏' (n : ℕ), (1 - PowerSeries.X ^ (n + 1)) = PowerSeries.pentagonalSeries R
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ι_app : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeSup α] [inst_3 : OrderBot α] (F : CategoryTheory.Functor J α) (x : J),
  (CategoryTheory.Limits.CompleteLattice.finiteColimitCocone F).cocone.ι.app x = CategoryTheory.homOfLE ⋯
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_closure_of_mem : ∀ {α : Type u_2} {X : Set α} {e : α} (M : Matroid α),
  e ∈ X → autoParam (X ⊆ M.E) Matroid.mem_closure_of_mem._auto_1 → e ∈ M.closure X
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrLeft_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D),
  e.congrLeft.inverse = (CategoryTheory.Functor.whiskeringLeft C D E).obj e.functor
-- Mathlib.Analysis.Complex.Hadamard
/-- When the function `f` is bounded above on a vertical strip, then so is `F`.  -/
Complex.HadamardThreeLines.F_BddAbove : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E),
  ∀ ε > 0,
    BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
      BddAbove (norm ∘ Complex.HadamardThreeLines.F f ε '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)
-- Mathlib.RingTheory.Ideal.Oka
/-- If a ring `R` verify:
1. All prime ideals of `R` satisfy an Oka predicate `P`.
2. One ideal not satisfying `P` implies that there is an ideal maximal for not satisfying `P`.

Then all the ideals of `R` satisfy `P`.  -/
Ideal.IsOka.forall_of_forall_prime : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Ideal R → Prop},
  Ideal.IsOka P →
    (∀ (I : Ideal R), ¬P I → ∃ I, Maximal (fun x => ¬P x) I) → (∀ (I : Ideal R), I.IsPrime → P I) → ∀ (I : Ideal R), P I
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {G : Type u_2} [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {u : 𝕜 → F},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 u s x →
      derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The approximation at the index of the successor of the domain's cardinality is a fixed point  -/
OrdinalApprox.gfpApprox_ord_mem_fixedPoint : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  f x ≤ x → OrdinalApprox.gfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instInjectiveObjIsInjective : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.InjectiveObject C),
  CategoryTheory.Injective X.obj
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.filterMap_push.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C}
  (h_1 : t.truncGE b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncGTπ a)
      (CategoryTheory.CategoryStruct.comp (t.truncGTIsoTruncGE a b h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncGEπ b) h_1
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.main : Lean.Expr → List Lean.Meta.Grind.EMatch.Cnstr → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.Algebra.Lie.Ideal
LieHom.ker_le_comap : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L'), f.ker ≤ LieIdeal.comap f J
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β k → β k}, (t.modify k f).maxKey! = t.maxKey!
-- Mathlib.Analysis.InnerProductSpace.NormPow
Differentiable.fderiv_norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : F → E},
  Differentiable ℝ f →
    ∀ {x : F} {p : ℝ},
      1 < p → fderiv ℝ (fun x => ‖f x‖ ^ p) x = (p * ‖f x‖ ^ (p - 2)) • (innerSL ℝ) (f x) ∘SL fderiv ℝ f x
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Init.Control.State
StateT.instMonadExceptOf : {σ : Type u} → {m : Type u → Type v} → [Monad m] → (ε : Type u_1) → [MonadExceptOf ε m] → MonadExceptOf ε (StateT σ m)
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.natCast_natAbs_valMinAbs : ∀ {n : ℕ} [NeZero n] (a : ZMod n), ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.zsmul_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → SubNegMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubgroupClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (n : ℤ) (i : ι), (n • x) i = n • x i
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_inv_apply_1_1 : ∀ {X Y Z : TopCat}
  {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).1.1 = x.1
-- Mathlib.Topology.Connected.TotallyDisconnected
IsPreconnected.subsingleton : ∀ {α : Type u} [inst : TopologicalSpace α] [TotallyDisconnectedSpace α] {s : Set α}, IsPreconnected s → s.Subsingleton
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfSucc_eq_id : SimplexCategory.mkOfSucc 0 = CategoryTheory.CategoryStruct.id { len := 1 }
-- Mathlib.Order.InitialSeg
PrincipalSeg.monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] (f : α <i β),
  Monotone ⇑f.toRelEmbedding
-- Mathlib.Combinatorics.SimpleGraph.Paths
_private.Mathlib.Combinatorics.SimpleGraph.Paths.0.SimpleGraph.Walk.bypass.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2)
  (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_1 : V) → (ha : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons ha p)),
  (match u, SimpleGraph.Walk.nil with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons ha p => h_2 v v_1 ha p) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.desc_self : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (t : CategoryTheory.Limits.IsColimit c),
  t.desc c = CategoryTheory.CategoryStruct.id c.pt