mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.Bilinear
LinearMap.mkContinuous₂_norm_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ},
  0 ≤ C → ∀ (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖), ‖f.mkContinuous₂ C hC‖ ≤ C
-- Mathlib.GroupTheory.Rank
Group.rank_le_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [inst_2 : Group.FG G] [inst_3 : Group.FG H]
  (f : G →* H), Function.Surjective ⇑f → Group.rank H ≤ Group.rank G
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The seminorm controls the Schwartz estimate for any fixed `x`.  -/
SchwartzMap.le_seminorm : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap E F) (x : E),
  ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.measure_eq : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → ∀ {p : 𝓧 → Prop}, MeasurableSet {x | p x} → P {ω | p (X ω)} = μ {x | p x}
-- Init.Data.BitVec.Lemmas
/-- Show that `(x.toNat <<< n) ||| y.toNat` is within bounds of `BitVec (m + n)`.
 -/
BitVec.toNat_shiftLeft_or_toNat_lt_two_pow_add : ∀ {m n : ℕ} (x : BitVec m) (y : BitVec n), x.toNat <<< n ||| y.toNat < 2 ^ (m + n)
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_uInt8ToNat : ∀ (n : UInt8), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Lean.Server.Requests
Lean.Server.instInhabitedRequestError : Inhabited Lean.Server.RequestError
-- Mathlib.Order.Filter.SmallSets
Filter.tendsto_image_smallSets : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → β},
  Filter.Tendsto (fun x => f '' x) la.smallSets lb.smallSets ↔ Filter.Tendsto f la lb
-- Mathlib.Topology.Order.LiminfLimsup
BoundedGENhdsClass.isBounded_ge_nhds : ∀ {α : Type u_7} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : BoundedGENhdsClass α] (a : α),
  Filter.IsBounded (fun x1 x2 => x1 ≥ x2) (nhds a)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instDiv : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Div Y] → Div (LocallyConstant X Y)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.valid_singleton : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, {x}.Valid
-- Mathlib.Data.List.AList
AList.insertRec.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) (x : AList β),
  AList.insertRec H0 IH x =
    match x with
    | { entries := [], nodupKeys := nodupKeys } => H0
    | { entries := c :: l, nodupKeys := h } =>
      ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (AList.insertRec H0 IH { entries := l, nodupKeys := ⋯ }))
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform_snd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addDysonETransform e x).2 = x.2 ∩ (-e +ᵥ x.1)
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonMeasure_real_singleton_pos : ∀ {r : NNReal} (n : ℕ), 0 < r → 0 < (ProbabilityTheory.poissonMeasure r).real {n}
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.MulSubshift.mk.inj : ∀ {A : Type u_1} {inst : TopologicalSpace A} {G : Type u_2} {inst_1 : Monoid G} {carrier : Set (G → A)}
  {isClosed : IsClosed carrier} {mapsTo : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) carrier carrier}
  {carrier_1 : Set (G → A)} {isClosed_1 : IsClosed carrier_1}
  {mapsTo_1 : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) carrier_1 carrier_1},
  { carrier := carrier, isClosed := isClosed, mapsTo := mapsTo } =
      { carrier := carrier_1, isClosed := isClosed_1, mapsTo := mapsTo_1 } →
    carrier = carrier_1
-- Mathlib.Data.List.Cycle
/-- `chain R s` means that `R` holds between adjacent elements of `s`.

`chain R ([a, b, c] : Cycle α) ↔ R a b ∧ R b c ∧ R c a`  -/
Cycle.Chain : {α : Type u_1} → (α → α → Prop) → Cycle α → Prop
-- Lean.Parser.Term
Lean.Parser.Term.valueOf.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Integrable.integral_norm_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  ⦃f : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Elements of disjoint, normal subgroups commute.  -/
AddSubgroup.addCommute_of_normal_of_disjoint : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G),
  H₁.Normal → H₂.Normal → Disjoint H₁ H₂ → ∀ (x y : G), x ∈ H₁ → y ∈ H₂ → AddCommute x y
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.natEmbedding.congr_simp : ∀ {α : Type u} (s : Set α) (h : s.Infinite), Set.Infinite.natEmbedding s h = Set.Infinite.natEmbedding s h
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- The excenter of a triangle opposite a vertex bisects the angle at that vertex.  -/
Affine.Triangle.oangle_excenter_singleton_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t {i₁}) =
          EuclideanGeometry.oangle (Affine.Simplex.excenter t {i₁}) (t.points i₁) (t.points i₃)
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.below.transitive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → J.Saturate X a → Prop} (X : C) (S R : CategoryTheory.Sieve X)
  (a : J.Saturate X S) (a_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (CategoryTheory.Sieve.pullback f R)),
  CategoryTheory.Precoverage.Saturate.below a →
    motive X S a →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), CategoryTheory.Precoverage.Saturate.below ⋯) →
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), motive Y (CategoryTheory.Sieve.pullback f R) ⋯) →
          CategoryTheory.Precoverage.Saturate.below ⋯
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (s : AddSubgroup G), AddAction.stabilizer G ↑s = s
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- If `f` is a simple function taking values in `β → γ` and `g` is another simple function
with the same domain and codomain `β`, then `f.seq g = f a (g a)`.  -/
MeasureTheory.SimpleFunc.seq : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        MeasureTheory.SimpleFunc α (β → γ) → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α γ
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
strictConcaveOn_sqrt_mul_log_Ioi : StrictConcaveOn ℝ (Set.Ioi 1) fun x => √x * Real.log x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_extend_by_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M),
  (∑ i ∈ s, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConvexOn.map_condExp_le_trim : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} {mE : MeasurableSpace E}
  [BorelSpace E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConvexOn ℝ s φ →
    LowerSemicontinuousOn φ s →
      MeasureTheory.StronglyMeasurable φ →
        (∀ᵐ (a : α) ∂μ, f a ∈ s) →
          IsClosed s →
            MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m]
-- Mathlib.Topology.Order.OrderClosed
le_on_closure : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α} {s : Set β},
  (∀ x ∈ s, f x ≤ g x) → ContinuousOn f (closure s) → ContinuousOn g (closure s) → ∀ ⦃x : β⦄, x ∈ closure s → f x ≤ g x
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getEntryLE?.go : {α : Type u} →
  {β : α → Type v} → [Ord α] → α → Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {p : P},
  p ∈ affineSpan ℝ (Set.range s.points) →
    ∀ {signs : Finset (Fin (n + 1))},
      (∃ r, ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = (if i ∈ signs then -1 else 1) * r) ↔
        s.ExcenterExists signs ∧ p = s.excenter signs
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitDesc.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F),
  MonCat.FilteredColimits.colimitDesc F t =
    MonCat.ofHom
      {
        toFun :=
          (F.comp (CategoryTheory.forget MonCat)).descColimitType
            ((F.comp (CategoryTheory.forget MonCat)).coconeTypesEquiv.symm
              ((CategoryTheory.forget MonCat).mapCocone t)),
        map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Convex.Function
/-- Right translation preserves strict concavity.  -/
StrictConcaveOn.translate_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCancelCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E]
  [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f → ∀ (c : E), StrictConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- A Hilbert space admits a Hilbert basis.  -/
exists_hilbertBasis : ∀ (𝕜 : Type u_2) [inst : RCLike 𝕜] (E : Type u_3) [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E], ∃ w b, ⇑b = Subtype.val
-- Mathlib.Algebra.Lie.Basic
/-- Lie module equivalences are symmetric.  -/
LieModuleEquiv.symm : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → (M ≃ₗ⁅R,L⁆ N) → N ≃ₗ⁅R,L⁆ M
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.coeff_mem_coeffSubmodule : ∀ {R₀ : Type u_1} {R : Type u_2} [inst : CommRing R₀] [inst_1 : CommRing R] [inst_2 : Algebra R₀ R] {n : ℕ}
  {e : ChevalleyThm.PolynomialC.InductionObj✝ R n} {i : Fin n} {d : ℕ},
  (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).coeff d ∈ ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule✝ R₀ e
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instSMulCommClass : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9}
  [inst_4 : Monoid R'] [inst_5 : Monoid R''] [inst_6 : Semiring A] [inst_7 : Module A M] [inst_8 : Module A N]
  [inst_9 : DistribMulAction R' N] [inst_10 : ContinuousConstSMul R' N] [inst_11 : SMulCommClass A R' N]
  [inst_12 : DistribMulAction R'' N] [inst_13 : ContinuousConstSMul R'' N] [inst_14 : SMulCommClass A R'' N]
  [SMulCommClass R' R'' N], SMulCommClass R' R'' (M [⋀^ι]→L[A] N)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum_map_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D)
  {c c' : C} (f : c ⟶ c'),
  (F.sum G).map ((CategoryTheory.Sum.inr_ A C).map f) = (CategoryTheory.Sum.inr_ B D).map (G.map f)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.app_shift_assoc : ∀ {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₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ (X : C) {Z : D} (h : F₂.obj ((CategoryTheory.shiftFunctor C a).obj X) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) h =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X))
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₂ a).inv.app X) h))
-- Lean.Elab.Do.Basic
/-- Adds the new reaching definitions of the given `tunneledVars` in `childCtx` relative to `rootCtx` as
non-dependent decls.
 -/
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.addReachingDefsAsNonDep : {α : Type} → Lean.LocalContext → Lean.LocalContext → Std.HashMap Lean.Name α → Lean.MetaM Lean.LocalContext
-- Mathlib.MeasureTheory.Group.Arithmetic
List.aemeasurable_sum : ∀ {M : Type u_2} {α : Type u_3} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : List (α → M)),
  (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.sum μ
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_eq_sinh_div_cosh : ∀ (x : ℂ), Complex.tanh x = Complex.sinh x / Complex.cosh x
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.Pattern.Model.split.induct_unfolding : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice}
  (motive : (firstRejected curr : s.Pos) → firstRejected ≤ curr → List s.Subslice → Prop),
  (∀ (firstRejected : s.Pos) (hle : firstRejected ≤ s.endPos),
      motive firstRejected s.endPos hle [s.subslice firstRejected s.endPos hle]) →
    (∀ (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr),
        ¬curr = s.endPos →
          ∀ (pos : s.Pos),
            String.Slice.Pattern.Model.matchAt? pat curr = some pos →
              curr < pos →
                motive pos pos ⋯ (String.Slice.Pattern.Model.split pat pos pos ⋯) →
                  motive firstRejected curr hle
                    (s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯)) →
      (∀ (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr) (h : ¬curr = s.endPos),
          String.Slice.Pattern.Model.matchAt? pat curr = none →
            motive firstRejected (curr.next h) ⋯ (String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯) →
              motive firstRejected curr hle (String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯)) →
        ∀ (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr),
          motive firstRejected curr hle (String.Slice.Pattern.Model.split pat firstRejected curr hle)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- See Note [custom simps projection]  -/
ContinuousAddEquiv.Simps.symm_apply : (G : Type u) →
  [inst : TopologicalSpace G] →
    (H : Type v) → [inst_1 : TopologicalSpace H] → [inst_2 : Add G] → [inst_3 : Add H] → G ≃ₜ+ H → H → G
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_pos : ∀ {K : Type u_1} [inst : RCLike K] {x : ℝ}, 0 < ↑x ↔ 0 < x
-- Mathlib.Topology.Connected.PathConnected
pathComponentIn_congr : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X},
  x ∈ pathComponentIn F y → pathComponentIn F x = pathComponentIn F y
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ_comp_equiv : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {ι' : Type w₃} {σ : Type w₂} {σ' : Type w₄} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (Q' : Algebra.Generators S T ι') (P' : Algebra.Generators R S σ'),
  Algebra.Generators.H1Cotangent.δ Q P ∘ₗ ↑(Algebra.Generators.H1Cotangent.equiv Q' Q) =
    Algebra.Generators.H1Cotangent.δ Q' P'
-- Mathlib.Order.ModularLattice
Disjoint.isCompl_sup_left_of_isCompl_sup_right : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α],
  Disjoint b c → IsCompl a (b ⊔ c) → IsCompl (a ⊔ b) c
-- Batteries.Data.Vector.Lemmas
Vector.scanlM_map : ∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {n : ℕ} {init : β} [inst : Monad m]
  [LawfulMonad m] {f : α₁ → α₂} {g : β → α₂ → m β} {as : Vector α₁ n},
  Vector.scanlM g init (Vector.map f as) = Vector.scanlM (fun x1 x2 => g x1 (f x2)) init as
-- Mathlib.Topology.ContinuousMap.Basic
Homeomorph.continuousMapCongr_apply : ∀ {X₁ : Type u_5} {X₂ : Type u_6} {Y₁ : Type u_7} {Y₂ : Type u_8} [inst : TopologicalSpace X₁]
  [inst_1 : TopologicalSpace X₂] [inst_2 : TopologicalSpace Y₁] [inst_3 : TopologicalSpace Y₂] (e : X₁ ≃ₜ X₂)
  (e' : Y₁ ≃ₜ Y₂) (f : C(X₁, Y₁)),
  (e.continuousMapCongr e') f =
    { toFun := ⇑e', continuous_toFun := ⋯ }.comp (f.comp { toFun := ⇑e.symm, continuous_toFun := ⋯ })
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.instInvOneClassNonZeroDivisors : {K : Type u_3} →
  [inst : Field K] →
    {R₁ : Type u_4} →
      [inst_1 : CommRing R₁] →
        [IsDomain R₁] →
          [inst_3 : Algebra R₁ K] → [IsFractionRing R₁ K] → InvOneClass (FractionalIdeal (nonZeroDivisors R₁) K)
-- Init.Control.Basic
/-- A way to lift a computation from one monad to another while providing the lifted computation with a
means of interpreting computations from the outer monad. This provides a means of lifting
higher-order operations automatically.

Clients should typically use `control` or `controlAt`, which request an instance of `MonadControlT`:
the reflexive, transitive closure of `MonadControl`. New instances should be defined for
`MonadControl` itself.
 -/
MonadControl : semiOutParam (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Batteries.Data.Vector.Lemmas
Vector.scanrM_map : ∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {n : ℕ} {init : β} [inst : Monad m]
  [LawfulMonad m] {f : α₁ → α₂} {g : α₂ → β → m β} {as : Vector α₁ n},
  Vector.scanrM g init (Vector.map f as) = Vector.scanrM (fun a b => g (f a) b) init as
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCone` is the right inverse to `mapConeInv`.  -/
CategoryTheory.Functor.mapConeInvMapCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J D} →
              (H : CategoryTheory.Functor D C) →
                [inst_3 : H.IsEquivalence] → (c : CategoryTheory.Limits.Cone F) → H.mapConeInv (H.mapCone c) ≅ c
-- Mathlib.Algebra.Group.Prod
MulHom.snd_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), (MulHom.snd N P).comp (f.prod g) = g
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The polynomial `X ^ n` has spectral value `0`.  -/
spectralValue_X_pow : ∀ {R : Type u_1} [inst : SeminormedRing R] [Nontrivial R] (n : ℕ), spectralValue (Polynomial.X ^ n) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology of a short complex `S` identifies to the kernel of the induced morphism
`cokernel S.f ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.homologyIsoKernelDesc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasHomology] →
          [inst_3 : CategoryTheory.Limits.HasCokernel S.f] →
            [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)] →
              S.homology ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι),
  (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.hom.app P).f.f n = P.p.f n
-- Lean.Expr
Lean.Expr.Data.hasLevelMVar : Lean.Expr.Data → Bool
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it₁ : Std.IterM m β} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β) →
                (b : β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩) →
              ((it₁' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Init.Data.Int.Pow
Int.pow_nonneg_of_even : ∀ {m : ℤ} {n : ℕ}, n % 2 = 0 → 0 ≤ m ^ n
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioo_disjoint_Ioo : ∀ {α : Type v} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α} [DenselyOrdered α],
  Disjoint (Set.Ioo a₁ a₂) (Set.Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.mem_pow_idealOfVars_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : ℕ) (p : MvPolynomial σ R),
  p ∈ MvPolynomial.idealOfVars σ R ^ n ↔ ∀ x ∈ p.support, n ≤ Finsupp.degree x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {a : α} [inst : Inhabited α], ∅.getKey! a = default
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k : α}, (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).contains k = (m.contains k || l.contains k)