mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.eLpNorm_condExpL2_le : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)),
  MeasureTheory.eLpNorm (↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) f)) 2 μ ≤ MeasureTheory.eLpNorm (↑↑f) 2 μ
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.extendRCLikeL_symm_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (a : WeakDual 𝕜 F),
  WeakDual.extendRCLikeL.symm a = StrongDual.toWeakDual (StrongDual.extendRCLikeₗ.symm (WeakDual.toStrongDual a))
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.exfalso'.sizeOf_spec : ∀ (p : Mathlib.Tactic.ITauto.Proof), sizeOf p.exfalso' = 1 + sizeOf p
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mk.inj : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  {prop prop_1 : (X : B) → CategoryTheory.ObjectProperty ↑(F.obj X)},
  { prop := prop } = { prop := prop_1 } → prop = prop_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_eq_getElem!_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.min! = t.toArray[0]!
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.cmdState : Lean.Server.Snapshots.Snapshot → Lean.Elab.Command.State
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R} [IsDomain R], g.Splits → g ≠ 0 → f ∣ g → f.Splits
-- Std.Time.Date.PlainDate
/-- Calculates the `Weekday` of a given `PlainDate` using Zeller's Congruence for the Gregorian calendar.
 -/
Std.Time.PlainDate.weekday : Std.Time.PlainDate → Std.Time.Weekday
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
_private.Mathlib.LinearAlgebra.Projectivization.PSL.PSL2.0.field_cond_of_four_le_card : ∀ {F : Type u_2} [inst : Field F], 4 ≤ Nat.card F → ∃ a, a ≠ 0 ∧ a ^ 2 ≠ 1
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_eq_zero : ∀ {x : ℝ}, Real.log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
-- Init.Data.List.Impl
List.replace.eq_2 : ∀ {α : Type u} [inst : BEq α] (x x_1 a : α) (as : List α),
  (a :: as).replace x x_1 =
    match x == a with
    | true => x_1 :: as
    | false => a :: as.replace x x_1
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of the
base point is a neighborhood of the preimage, within a set.  -/
extChartAt_preimage_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s t : Set M} [inst_5 : ChartedSpace H M] {x : M},
  t ∈ nhdsWithin x s →
    ↑(extChartAt I x).symm ⁻¹' t ∈ nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.mk'.inj : ∀ {α : Type u} {β : α → Type v} {inst : BEq α} {inst_1 : Hashable α}
  {inner inner_1 : Quotient (Std.DHashMap.isSetoid α β)}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Analysis.Analytic.Basic
/-- If a function `f` has a power series `p` on a ball within a set and `g` is linear,
then `g ∘ f` has the power series `g ∘ p` on the same ball.  -/
ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
  {x : E} {r : ENNReal} (g : F →L[𝕜] G),
  HasFPowerSeriesWithinOnBall f p s x r → HasFPowerSeriesWithinOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) s x r
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.mul_eq : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α}, a = 0 → 0 < b → b * a = 0
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.left_unit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C) {Z : C}
  (h : self.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.η.app (self.obj X)) (CategoryTheory.CategoryStruct.comp (self.μ.app X) h) = h
-- Mathlib.Tactic.Translate.Reorder
/-- Determine for each `i : Fin n` to what `j : Fin n` it should get translated.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.guessReorder.visit : Lean.Expr →
  Lean.Expr →
    {n : ℕ} →
      Vector (Option (Fin n)) n →
        ReaderT (Std.HashMap Lean.FVarId ℕ × Std.HashMap Lean.FVarId ℕ)
          (StateRefT' IO.RealWorld (Std.HashSet (Lean.Expr × Lean.Expr)) (OptionT BaseIO)) (Vector (Option (Fin n)) n)
-- Std.Time.Format.Modifier
Std.Time.Modifier.Z.inj : ∀ {presentation presentation_1 : Std.Time.OffsetZ},
  Std.Time.Modifier.Z presentation = Std.Time.Modifier.Z presentation_1 → presentation = presentation_1
-- Mathlib.Data.Set.Image
Set.instNonemptyElemImage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) [Nonempty ↑s], Nonempty ↑(f '' s)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableMul₂.toMeasurableMul : ∀ {M : Type u_2} [inst : MeasurableSpace M] [inst_1 : Mul M] [MeasurableMul₂ M], MeasurableMul M
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.contractFst_dirac : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (x : X) (y : Y) (f : C(X × Y, R)),
  ((AbstractMeasure.contractFst (AbstractMeasure.dirac R x)) f) y = f (x, y)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor.injEq : ∀ (e : Lean.Expr) (f : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr) (f_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e f =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e_1 f_1) =
    (e = e_1 ∧ f = f_1)
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.tacticEmpty : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (ra rb : Lean.Grind.CommRing.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core a b ra rb) =
    1 + sizeOf a + sizeOf b + sizeOf ra + sizeOf rb
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial.congr_simp : ∀ (p p_1 : NNReal) (e_p : p = p_1) (h : p ≤ 1) (n : ℕ), PMF.binomial p h n = PMF.binomial p_1 ⋯ n
-- Init.Data.List.Pairwise
List.nodup_iff_pairwise_ne : ∀ {α : Type u_1} {l : List α}, l.Nodup ↔ List.Pairwise (fun x1 x2 => x1 ≠ x2) l
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- If a vertex `v` occurs in the list of vertices of a path `p : Path a b`, then `p` can be
decomposed as a concatenation of a subpath from `a` to `v` and a subpath from `v` to `b`.  -/
Quiver.Path.exists_eq_comp_of_mem_vertices : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {v : V}, v ∈ p.vertices → ∃ p₁ p₂, p = p₁.comp p₂
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.pullbackMap.isCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] [inst_3 : p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (f : R ⟶ S)
  (ha : p.obj a = S), p.IsCartesian f (HasFibers.pullbackMap f ha)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIco_coe_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ico a (a + p)),
  (AddCircle.equivIco p a) ↑x = ⟨x, hx⟩
-- Lean.Structure
/-- Information about structure parents. These are in the order they appear in the `extends` clause.  -/
Lean.StructureInfo.parentInfo : Lean.StructureInfo → Array Lean.StructureParentInfo
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.mapIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ≅ Y) (g : X ≅ Z), (CategoryTheory.Limits.coprod.mapIso f g).hom = CategoryTheory.Limits.coprod.map f.hom g.hom
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_lt_sqrt : ∀ {x y : ℝ}, 0 ≤ x → x < y → √x < √y
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr) (k : ℕ)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.pow k with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_5 a k
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.checkNotBool : Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.addX P Q = -(Q 1 ^ 2 * P 2) * P 0
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_inj : ∀ {α : Type u_1} {a b : α}, toBoolRing a = toBoolRing b ↔ a = b
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree_le_maxDegree : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.minDegree ≤ G.maxDegree
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_closure_coe_preimage : ∀ {G : Type u_1} [inst : Group G] {k : Set G}, Subgroup.closure (Subtype.val ⁻¹' k) = ⊤
-- Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
/-- In a linearly ordered group with the order topology, the powers of a single element form a
discrete subgroup.  -/
Subgroup.instDiscreteTopologyZMultiples : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] (g : G), DiscreteTopology ↥(Subgroup.zpowers g)
-- Mathlib.Order.RelIso.Basic
RelIso.symm_bijective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Bijective RelIso.symm
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_add : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p + q).divX = p.divX + q.divX
-- Mathlib.CategoryTheory.Sites.Canonical
/-- If `J` is subcanonical, we obtain a "Yoneda" functor from the defining site
into the sheaf category.
 -/
CategoryTheory.GrothendieckTopology.yoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [J.Subcanonical] → CategoryTheory.Functor C (CategoryTheory.Sheaf J (Type v))
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A coequalizer diagram gives rise to a regular epimorphism.  -/
CategoryTheory.Cofork.IsColimit.regularEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : C} →
      {p₁ p₂ : A ⟶ B} →
        {c : CategoryTheory.Limits.Cofork p₁ p₂} → CategoryTheory.Limits.IsColimit c → CategoryTheory.RegularEpi c.π
-- Lean.Parser.Command
Lean.Parser.Command.register_tactic_tag.formatter : Lean.PrettyPrinter.Formatter
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Equality.
 -/
Std.Tactic.BVDecide.BVBinPred.eq : Std.Tactic.BVDecide.BVBinPred
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.star_iff : ∀ {R : Type u_1} [inst : InvolutiveStar R] {x : R}, IsSelfAdjoint (star x) ↔ IsSelfAdjoint x
-- Aesop.Stats.Basic
Aesop.Stats.mk.injEq : ∀ (total configParsing ruleSetConstruction search ruleSelection script forwardState : Aesop.Nanos)
  (scriptGenerated : Option Aesop.ScriptGenerated) (ruleStats : Array Aesop.RuleStats)
  (goalStats : Array Aesop.GoalStats)
  (total_1 configParsing_1 ruleSetConstruction_1 search_1 ruleSelection_1 script_1 forwardState_1 : Aesop.Nanos)
  (scriptGenerated_1 : Option Aesop.ScriptGenerated) (ruleStats_1 : Array Aesop.RuleStats)
  (goalStats_1 : Array Aesop.GoalStats),
  ({ total := total, configParsing := configParsing, ruleSetConstruction := ruleSetConstruction, search := search,
        ruleSelection := ruleSelection, script := script, forwardState := forwardState,
        scriptGenerated := scriptGenerated, ruleStats := ruleStats, goalStats := goalStats } =
      { total := total_1, configParsing := configParsing_1, ruleSetConstruction := ruleSetConstruction_1,
        search := search_1, ruleSelection := ruleSelection_1, script := script_1, forwardState := forwardState_1,
        scriptGenerated := scriptGenerated_1, ruleStats := ruleStats_1, goalStats := goalStats_1 }) =
    (total = total_1 ∧
      configParsing = configParsing_1 ∧
        ruleSetConstruction = ruleSetConstruction_1 ∧
          search = search_1 ∧
            ruleSelection = ruleSelection_1 ∧
              script = script_1 ∧
                forwardState = forwardState_1 ∧
                  scriptGenerated = scriptGenerated_1 ∧ ruleStats = ruleStats_1 ∧ goalStats = goalStats_1)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.mk_vadd_toLp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : M) {f : α → E} (hf : MeasureTheory.MemLp f p μ),
  DomAddAct.mk c +ᵥ MeasureTheory.MemLp.toLp f hf = MeasureTheory.MemLp.toLp (fun x => f (c +ᵥ x)) ⋯
-- Mathlib.Data.Vector.Basic
List.Vector.mapAccumr_cons : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} {n : ℕ} {x : α} {s : σ} (xs : List.Vector α n) {f : α → σ → σ × β},
  List.Vector.mapAccumr f (x ::ᵥ xs) s =
    have r := List.Vector.mapAccumr f xs s;
    have q := f x r.1;
    (q.1, q.2 ::ᵥ r.2)
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.toOrderEmbedding.eq_1 : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : α → β) (hf : LeftOrdContinuous f)
  (h : Function.Injective f), LeftOrdContinuous.toOrderEmbedding f hf h = { toFun := f, inj' := h, map_rel_iff' := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingularLift_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P
-- Mathlib.CategoryTheory.Action.Basic
/-- Auxiliary definition for `functorCategoryEquivalence`.  -/
Action.FunctorCategoryEquivalence.counitIso : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        Action.FunctorCategoryEquivalence.inverse.comp Action.FunctorCategoryEquivalence.functor ≅
          CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis'.isBase_restrict : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → (M.restrict X).IsBase I
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.replicateCol_empty : ∀ {α : Type u} {ι : Type u_1} (v : Fin 0 → α), Matrix.replicateCol ι v = Matrix.of ![]
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `infIrred_toDual`. -/
SupIrred.dual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupIrred a → InfIrred (OrderDual.toDual a)
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_le_of_shell' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {ε C : ℝ}, 0 < ε → 0 ≤ C → ∀ {c : 𝕜}, ‖c‖ < 1 → (∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) → ‖f‖ ≤ C
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then given `x y : R` with
`f x = 0`, we have `f (x * y) = 0`.  -/
map_mul_zero_of_map_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → ∀ {x : R}, f x = 0 → ∀ (y : R), f (x * y) = 0
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ_eq : ∀ {κ₁ κ₂ : Cardinal.{w}} {X : Type w}
  (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B))
  (m :
    (B : Set X) →
      (hB : HasCardinalLT (↑B) κ₂) → (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X)
  (B : Set X) (hB : HasCardinalLT (↑B) κ₂),
  Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ✝ Y m B =
    Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ₀✝ Y m B hB
-- Init.Prelude
/-- [Monads](https://en.wikipedia.org/wiki/Monad_(functional_programming)) are an abstraction of
sequential control flow and side effects used in functional programming. Monads allow both
sequencing of effects and data-dependent effects: the values that result from an early step may
influence the effects carried out in a later step.

The `Monad` API may be used directly. However, it is most commonly accessed through
[`do`-notation](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation).

Most `Monad` instances provide implementations of `pure` and `bind`, and use default implementations
for the other methods inherited from `Applicative`. Monads should satisfy certain laws, but
instances are not required to prove this. An instance of `LawfulMonad` expresses that a given
monad's operations are lawful.
 -/
Monad : (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.Order.Filter.Finite
Filter.eventually_subset_of_finite : ∀ {α : Type u} {ι : Type u_2} {f : Filter ι} {s : ι → Set α} {t : Set α},
  t.Finite → (∀ a ∈ t, ∀ᶠ (i : ι) in f, a ∈ s i) → ∀ᶠ (i : ι) in f, t ⊆ s i
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.copy_eq : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = ↑p), p.copy s hs = p
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.equivImage.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β} (s : Set α)
  (hf : MeasurableEmbedding f),
  MeasurableEmbedding.equivImage s hf =
    { toEquiv := Equiv.Set.image f s ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Init.Core
_private.Init.Core.0.Quotient.rel : {α : Sort u} → {s : Setoid α} → Quotient s → Quotient s → Prop
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : ι.Full]
  [inst_3 : ι.Faithful] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A]
  {Z_1 : ChainComplex C ℕ} (h : Λ.chainComplex Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Λ.chainComplexMap (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (Λ.chainComplexMap f)
      (CategoryTheory.CategoryStruct.comp (Λ.chainComplexMap g) h)
-- Mathlib.Topology.Algebra.Field
IsTopologicalDivisionRing.toContinuousInv₀ : ∀ {K : Type u_1} {inst : DivisionRing K} {inst_1 : TopologicalSpace K} [self : IsTopologicalDivisionRing K],
  ContinuousInv₀ K
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Pos.Raw.set.match_1.eq_1 : ∀ (motive : String → String.Pos.Raw → Char → Sort u_1) (s : String) (i : String.Pos.Raw) (c : Char)
  (h_1 : (s : String) → (i : String.Pos.Raw) → (c : Char) → motive s i c),
  (match s, i, c with
    | s, i, c => h_1 s i c) =
    h_1 s i c
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Duration` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subDuration : Std.Time.Timestamp → Std.Time.Duration → Std.Time.Timestamp
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The underlying `2`-simplex in a structure `SSet.Edge.CompStruct`.  -/
SSet.Edge.CompStruct.simplex : {X : SSet} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {e₁₂ : SSet.Edge x₁ x₂} → {e₀₂ : SSet.Edge x₀ x₂} → e₀₁.CompStruct e₁₂ e₀₂ → X.obj (Opposite.op { len := 2 })
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than the given key.
 -/
Std.DTreeMap.Const.getEntryGT : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α × β
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, the angle between the first and the second plus the angle
between the second and the third equals the angle between the first and the third.  -/
Orientation.oangle_add : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V}, x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x y + o.oangle y z = o.oangle x z
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk.congr_simp : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (toPartialEquiv toPartialEquiv_1 : PartialEquiv Z (B × F)) (e_toPartialEquiv : toPartialEquiv = toPartialEquiv_1)
  (open_target : IsOpen toPartialEquiv.target) (baseSet baseSet_1 : Set B) (e_baseSet : baseSet = baseSet_1)
  (open_baseSet : IsOpen baseSet) (source_eq : toPartialEquiv.source = proj ⁻¹' baseSet)
  (target_eq : toPartialEquiv.target = baseSet ×ˢ Set.univ)
  (proj_toFun : ∀ p ∈ toPartialEquiv.source, (↑toPartialEquiv p).1 = proj p),
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
    { toPartialEquiv := toPartialEquiv_1, open_target := ⋯, baseSet := baseSet_1, open_baseSet := ⋯, source_eq := ⋯,
      target_eq := ⋯, proj_toFun := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_uInt8ToBitVec : ∀ (n : UInt8), { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.MutualMeasure.args.injEq : ∀ (a a_1 : Array ℕ),
  (Lean.Elab.WF.GuessLex.MutualMeasure.args a = Lean.Elab.WF.GuessLex.MutualMeasure.args a_1) = (a = a_1)