mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.subsingleton_isRoot_of_natDegree_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [IsLeftCancelMulZero R],
  p.natDegree = 1 → {x | p.IsRoot x}.Subsingleton
-- Std.Http.Data.URI.Basic
Std.Http.URI.Port.empty.sizeOf_spec : sizeOf Std.Http.URI.Port.empty = 1
-- Mathlib.Algebra.Group.Shrink
Shrink.instSub : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Sub α] → Sub (Shrink.{v, u_2} α)
-- Mathlib.Logic.Function.Defs
/-- Compose a unary function `f` with a binary function `g`.  -/
Function.bicompr : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → (γ → δ) → (α → β → γ) → α → β → δ
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- If `A` is totally unimodular and each row of `B` is all zeros except for at most a single `1`,
then `fromRows A B` is totally unimodular.  -/
Matrix.fromRows_isTotallyUnimodular_iff_rows : ∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq n]
  {A : Matrix m n R} {B : Matrix m' n R},
  (Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s) → ((A.fromRows B).IsTotallyUnimodular ↔ A.IsTotallyUnimodular)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.attachWith.congr_simp : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] (it it_1 : Std.IterM m β)
  (e_it : it = it_1) (P : β → Prop) (h : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out),
  it.attachWith P h = it_1.attachWith P ⋯
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.aestronglyMeasurable_exp_mul_sum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ}
  {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X i ω)) μ) →
    MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * (∑ i ∈ s, X i) ω)) μ
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.mk.injEq : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Monoid G] (V : Type w)
  [hV1 : AddCommGroup V] [hV2 : Module k V] [hV3 : TopologicalSpace V] [hV4 : IsTopologicalAddGroup V]
  [hV5 : ContinuousSMul k V] (ρ : ContRepresentation k G V) (V_1 : Type w) (hV1_1 : AddCommGroup V_1)
  (hV2_1 : Module k V_1) (hV3_1 : TopologicalSpace V_1) (hV4_1 : IsTopologicalAddGroup V_1)
  (hV5_1 : ContinuousSMul k V_1) (ρ_1 : ContRepresentation k G V_1),
  ({ V := V, hV1 := hV1, hV2 := hV2, hV3 := hV3, hV4 := hV4, hV5 := hV5, ρ := ρ } =
      { V := V_1, hV1 := hV1_1, hV2 := hV2_1, hV3 := hV3_1, hV4 := hV4_1, hV5 := hV5_1, ρ := ρ_1 }) =
    (V = V_1 ∧ hV1 ≍ hV1_1 ∧ hV2 ≍ hV2_1 ∧ hV3 ≍ hV3_1 ∧ ρ ≍ ρ_1)
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Asymptotically, the logarithmic counting function for the poles of a sum `∑ a ∈ s, f a` is less than
or equal to the sum of the logarithmic counting functions for the poles of the `f ·`.
 -/
ValueDistribution.logCounting_sum_top_eventuallyLE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {α : Type u_3} (s : Finset α) (f : α → 𝕜 → E),
  (∀ a ∈ s, Meromorphic (f a)) →
    ValueDistribution.logCounting (∑ a ∈ s, f a) ⊤ ≤ᶠ[Filter.atTop] ∑ a ∈ s, ValueDistribution.logCounting (f a) ⊤
-- Mathlib.Order.CompleteLattice.Basic
iInf_congr : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨅ i, f i = ⨅ i, g i
-- Mathlib.Topology.PreorderRestrict
Preorder.continuous_restrictLe₂ : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (i : α) → TopologicalSpace (X i)] {a b : α}
  (hab : a ≤ b), Continuous (Preorder.restrictLe₂ hab)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_min : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π),
  ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace
-- Mathlib.RingTheory.Artinian.Module
isArtinian_pi : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [inst_2 : (i : ι) → AddCommGroup (M i)]
  [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), IsArtinian R (M i)], IsArtinian R ((i : ι) → M i)
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.instVAddInvariantMeasureSubtypeMemAddSubmonoidOfIsAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddMonoid G] (s : AddSubmonoid G)
  [μ.IsAddLeftInvariant], MeasureTheory.VAddInvariantMeasure (↥s) G μ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.Tactic.ClickSuggestions.Util
/-- `rw` cannot rewrite here, because the subexpression contains bound variables.
So, we suggest `simp_rw`.  -/
Mathlib.Tactic.ClickSuggestions.RwKind.hasBVars : Mathlib.Tactic.ClickSuggestions.RwKind
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ioi : ∀ {α : Type v} [inst : Preorder α] [NoMinOrder α], ⋃ a, Set.Ioi a = Set.univ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 2nd differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
`k`-linear map `Fun(G × G, A) → Fun(G × G × G, A)`. It sends
`(f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).`  -/
groupCohomology.d₂₃ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u_1, u, u} k G) → ModuleCat.of k (G × G → ↑A) ⟶ ModuleCat.of k (G × G × G → ↑A)
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $(-∞, b]$ of elements `x` such that `x ≤ b`. Basically `Set.Iic b` as a finset.  -/
Finset.Iic : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → α → Finset α
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder : ∀ (X : HeytAlg), (CategoryTheory.HasForget₂.forget₂.obj X).isBoundedOrder = HeytingAlgebra.toBoundedOrder
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α}
  (lhs rhs cin lhs_1 rhs_1 cin_1 : aig.Ref),
  ({ lhs := lhs, rhs := rhs, cin := cin } = { lhs := lhs_1, rhs := rhs_1, cin := cin_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ cin = cin_1)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃),
  (e.trans e').homotopyInvHomId =
    (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans
      (((e.homotopyInvHomId.compRight e'.hom).compLeft e'.inv).trans
        ((CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans e'.homotopyInvHomId))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeArrowRightFuncOfHasIterationOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : LinearOrder J]
  [CategoryTheory.Limits.HasIterationOfShape J C],
  CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J CategoryTheory.Arrow.rightFunc
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.contains_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.contains k = t₂.contains k
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- The empty function is a fundamental sequence for 0.  -/
Ordinal.IsFundamentalSeq.zero : ∀ (f : ↑(Set.Iio 0) → ↑(Set.Iio 0)), Ordinal.IsFundamentalSeq f
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.ext : ∀ {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} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} {x y : D₁.Hom D₂}, x.hom = y.hom → x = y
-- Aesop.Util.Basic
Aesop.isEmptyTrie : {α : Type} → Lean.Meta.DiscrTree.Trie α → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.getValueD k (Std.Internal.List.insertList l toInsert) fallback =
        Std.Internal.List.getValueD k toInsert (Std.Internal.List.getValueD k l fallback)
-- Init.Data.Repr
Char.repr : Char → String
-- Mathlib.GroupTheory.Exponent
/-- If `H` is a normal additive subgroup of `G`, then the exponent of `G ⧸ H` divides the
exponent of `G`.  -/
AddGroup.exponent_quotient_dvd : ∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal],
  AddMonoid.exponent (G ⧸ H) ∣ AddMonoid.exponent G
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_mul_cycle' : ∀ {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Fintype p] [inst_3 : NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R),
  (A * (B * C)).trace = (C * (A * B)).trace
-- Mathlib.Data.Set.Function
Function.Semiconj.bijOn_image : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s t : Set α},
  Function.Semiconj f fa fb → Set.BijOn fa s t → Set.InjOn f t → Set.BijOn fb (f '' s) (f '' t)
-- Init.Prelude
One.mk : {α : Type u} → α → One α
-- Mathlib.Algebra.Category.Semigrp.Basic
CategoryTheory.Iso.addSemigrpIsoToAddEquiv.eq_1 : ∀ {X Y : AddSemigrp} (i : X ≅ Y),
  i.addSemigrpIsoToAddEquiv = (AddSemigrp.Hom.hom i.hom).toAddEquiv (AddSemigrp.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuousOn.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  UpperSemicontinuousOn f s → UpperSemicontinuousOn g s → UpperSemicontinuousOn (fun x => max (f x) (g x)) s
-- Init.Data.SInt.Lemmas
Int64.le_iff_lt_or_eq : ∀ {a b : Int64}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.exists_maximal_isMatchingFree : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  G.IsMatchingFree → ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapRange.congr_simp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_4} [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] (v v_1 : MeasureTheory.VectorMeasure α M),
  v = v_1 → ∀ (f f_1 : M →+ N) (e_f : f = f_1) (hf : Continuous ⇑f), v.mapRange f hf = v_1.mapRange f_1 ⋯
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.iSupLift.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] {ι : Type u_1}
  [inst_7 : StarRing R] [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : Nonempty ι] (K : ι → NonUnitalStarSubalgebra R A) (dir : Directed (fun x1 x2 => x1 ≤ x2) K)
  (f f_1 : (i : ι) → ↥(K i) →⋆ₙₐ[R] B) (e_f : f = f_1)
  (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h))
  (T : NonUnitalStarSubalgebra R A) (hT : T = iSup K),
  NonUnitalStarSubalgebra.iSupLift K dir f hf T hT = NonUnitalStarSubalgebra.iSupLift K dir f_1 ⋯ T hT
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.inner_toLp_toLp : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype ι] (x y : ι → 𝕜),
  inner 𝕜 (WithLp.toLp 2 x) (WithLp.toLp 2 y) = y ⬝ᵥ star x
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
SSet.Subcomplex.evaluation_obj : ∀ (X : SSet) (j : SimplexCategoryᵒᵖ) (A : X.Subcomplex), (SSet.Subcomplex.evaluation X j).obj A = A.obj j
-- Lean.Parser.Term
Lean.Parser.Term.letOpts.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.Lemmas
instLawfulCommIdentityInt8HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.continuous_of_dominated : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {X : Type u_6} [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → α → G}
  {bound : α → ℝ},
  (∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) μ) →
    (∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, Continuous fun x => F x a) → Continuous fun x => ∫ (a : α), F x a ∂μ
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.Balanced.reverse : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {t : RBTree.RBNode α}, t.Balanced c n → t.reverse.Balanced c n
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.eventually_nnnorm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {l : Filter A},
  l.IsIncreasingApproximateUnit → ∀ᶠ (x : A) in l, ‖x‖₊ ≤ 1
-- Batteries.Data.List.Perm
List.subperm_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Subperm (l ++ l₂) ↔ l₁.Subperm l₂
-- Init.Data.Dyadic.Round
Dyadic.precision_roundDown : ∀ {x : Dyadic} {prec : ℤ}, (x.roundDown prec).precision ≤ some prec
-- Init.Data.String.FindPos
String.Slice.findNextPos : (offset : String.Pos.Raw) → (s : String.Slice) → offset < s.rawEndPos → s.Pos
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
ContinuousLinearMap.fpowerSeries_apply_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E),
  f.fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 E (f x)
-- Mathlib.Topology.Order.SuccPred
PredOrder.isPredLimit_of_mem_frontier : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α} {s : Set α}, a ∈ frontier s → Order.IsPredLimit a
-- Mathlib.Algebra.Polynomial.Splits
/-- A polynomial splits if and only if it has as many roots as its degree.  -/
Polynomial.splits_iff_card_roots : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R], f.Splits ↔ f.roots.card = f.natDegree
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFun_ne_north_pole : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(ℝ ∙ v)ᗮ),
  stereoInvFun hv w ≠ ⟨v, ⋯⟩
-- Mathlib.Algebra.Lie.TraceForm
/-- This lemma justifies the terminology "invariant" for trace forms.  -/
LieModule.lie_traceForm_eq_zero : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x : L),
  ⁅x, LieModule.traceForm R L M⁆ = 0
-- Std.Internal.Do.Order.Basic
Lean.Order.instPartialOrderProp_std : Lean.Order.PartialOrder Prop
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.not_and_eq : ∀ (p q : Prop), (¬(p ∧ q)) = (p → ¬q)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.sub_ratCast : ∀ (q : ℚ) {x : ℝ}, Irrational x → Irrational (x - ↑q)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.apply_eq_zero_iff : ∀ {α : Type u_1} (p : PMF α) (a : α), p a = 0 ↔ a ∉ p.support
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.of_comp_right : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn (g ∘ f) s → IsLocalHomeomorphOn f s → IsLocalHomeomorphOn g (f '' s)
-- Aesop.Rule.Name
Aesop.instInhabitedRuleName : Inhabited Aesop.RuleName
-- Mathlib.Analysis.BoundedVariation
/-- A bounded variation function into `ℝ` is differentiable almost everywhere. Superseded by
`ae_differentiableWithinAt_of_mem`.  -/
LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real : ∀ {f : ℝ → ℝ} {s : Set ℝ}, LocallyBoundedVariationOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
-- Init.Data.String.Basic
String.getUTF8Byte.congr_simp : ∀ (s s_1 : String) (e_s : s = s_1) (p p_1 : String.Pos.Raw) (e_p : p = p_1) (h : p < s.rawEndPos),
  s.getUTF8Byte p h = s_1.getUTF8Byte p_1 ⋯
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_range : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [Finite ι], b.toDual.range = ⊤
-- Init.Data.UInt.Lemmas
commandDeclare_uint_theorems__ : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- The graph with a single `s-t` edge. It is empty iff `s = t`.  -/
SimpleGraph.edge : {V : Type u_1} → V → V → SimpleGraph V
-- Lean.Declaration
Lean.QuotKind.type.sizeOf_spec : sizeOf Lean.QuotKind.type = 1
-- Init.Data.Vector.Range
Vector.snd_lt_of_mem_zipIdx : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {k : ℕ} {xs : Vector α n}, x ∈ xs.zipIdx k → x.2 < n + k
-- Init.Data.SInt.Basic
instLTInt16 : LT Int16
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_ne_zero_iff' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, ‖a‖₊ ≠ 0 ↔ a ≠ 1
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- We have `[W, 0] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable. Version within a set.  -/
VectorField.mlieBracketWithin_zero_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I W 0 s = 0
-- Init.Data.Order.PackageFactories
/-- This structure contains all the data needed to create a `LinearPreorderPackage α` instance. Its fields
are automatically provided if possible. For the detailed rules how the fields are inferred, see
`LinearPreorderPackage.ofLE`.
 -/
Std.Packages.LinearPreorderOfLEArgs : Type u → Type u
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_div : ∀ {x y : ℝ}, x ≠ 0 → y ≠ 0 → Real.log (x / y) = Real.log x - Real.log y
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜] [Finite ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜 F]
  {G : Type u_5} [inst_8 : AddCommGroup G] [inst_9 : TopologicalSpace G] [inst_10 : Module 𝕜 G]
  [inst_11 : ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s : Set (G × ((i : ι) → E i))}
  {x : G × ((i : ι) → E i)}, ContinuousWithinAt (fun p => (f p.1) p.2) s x
-- Init.Data.List.Lemmas
List.getElem?_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ i, l[i]? = some a
-- Init.Data.Iterators.Basic
Std.IterM.isPlausibleSuccessorOf_of_yield : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it' it : Std.IterM m β} {out : β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) → it'.IsPlausibleSuccessorOf it
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r' : Std.DTreeMap.Internal.Impl α β) (szr : ℕ) (k'' : α) (v'' : β k'')
  (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
      Sort u_3)
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
  (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_le_size_insertMany : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, m.size ≤ (m.insertMany l).size
-- Init.Data.List.MinMaxIdx
List.minIdxOn_eq_of_minIdxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {i : ℕ}
  (h : List.minIdxOn? f xs = some i), List.minIdxOn f xs ⋯ = i
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- A variant of `inv_mul_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable.  -/
eq_mul_of_inv_mul_eq₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → b⁻¹ * a = c → a = b * c
-- Init.Data.Dyadic.Basic
Dyadic.precision_ofIntWithPrec_le : ∀ {i : ℤ}, i ≠ 0 → ∀ (prec : ℤ), (Dyadic.ofIntWithPrec i prec).precision ≤ some prec
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsDominantOfSurjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f], AlgebraicGeometry.IsDominant f
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.trans : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y z : M}, x ≡ y [SMOD U] → y ≡ z [SMOD U] → x ≡ z [SMOD U]
-- Mathlib.Analysis.Real.Sqrt
/-- The square root of a real number. This returns 0 for negative inputs.

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`.  -/
Real.sqrt : ℝ → ℝ
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_eq_ringKrullDim_iff : ∀ {R : Type u_1} [inst : CommRing R] [FiniteRingKrullDim R] [inst_2 : IsLocalRing R] {I : Ideal R} [inst_3 : I.IsPrime],
  ↑(Ideal.primeHeight✝ I) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
-- Mathlib.Probability.StrongLaw
/-- The truncation of `Xᵢ` up to `i` satisfies the strong law of large numbers
(with respect to the truncated expectation) along the sequence
`c^n`, for any `c > 1`. This follows from `strong_law_aux1` by varying `ε`.  -/
ProbabilityTheory.strong_law_aux2 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    Pairwise (Function.onFun (fun f g => ProbabilityTheory.IndepFun f g MeasureTheory.volume) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
        (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
          ∀ {c : ℝ},
            1 < c →
              ∀ᵐ (ω : Ω),
                (fun n =>
                    ∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω -
                      ∫ (a : Ω),
                        (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a) =o[Filter.atTop]
                  fun n => ↑⌊c ^ n⌋₊