mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Sylow
/-- **Frattini's Argument**: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
of `N`, then `N_G(P) ⊔ N = G`.  -/
Sylow.normalizer_sup_eq_top : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p ↥N)]
  (P : Sylow p ↥N), Subgroup.normalizer ↑(Subgroup.map N.subtype ↑P) ⊔ N = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The addition of two Jacobian point classes on a Weierstrass curve `W`.

If `P` and `Q` are two Jacobian point representatives on `W`, then `W.addMap ⟦P⟧ ⟦Q⟧` is
definitionally equivalent to `W.add P Q`.  -/
WeierstrassCurve.Jacobian.addMap : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Jacobian R →
      WeierstrassCurve.Jacobian.PointClass R →
        WeierstrassCurve.Jacobian.PointClass R → WeierstrassCurve.Jacobian.PointClass R
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `α →ₙ+* β` denotes the type of non-unital ring homomorphisms from `α` to `β`.  -/
«term_→ₙ+*_» : Lean.TrailingParserDescr
-- Mathlib.Data.ENat.Basic
ENat.map_natCast_eq_zero : ∀ {n : ℕ∞} {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α]
  [CharZero α], ENat.map Nat.cast n = 0 ↔ n = 0
-- Mathlib.Analysis.Analytic.Uniqueness
Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {p : E [×n]→L[𝕜] F}, ((fun y => p fun x => y) =O[nhds 0] fun y => ‖y‖ ^ (n + 1)) → ∀ (y : E), (p fun x => y) = 0
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.pow_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x : A}, x ∈ S → ∀ (n : ℕ), x ^ n ∈ S
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.pi.mem_val : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t')
  {p : Finset (Fin n)} (hp : p ∈ K.parts) (w : ↥(SimpleGraph.ErdosStone.filter✝ K t)),
  ∀ v ∈ ↑(SimpleGraph.ErdosStone.filter.pi✝ K w) p hp, G.Adj (↑w) v
-- Std.Time.Date.Unit.Week
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Week.OfYear.Ordinal.ofInt : (data : ℤ) → 1 ≤ data ∧ data ≤ 53 → Std.Time.Week.OfYear.Ordinal
-- Mathlib.Order.InitialSeg
PrincipalSeg.lt_iff_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a a' : α} [inst_1 : PartialOrder α] (f : α <i β),
  f.toRelEmbedding a < f.toRelEmbedding a' ↔ a < a'
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_le_iff_le_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve Y)
  (T : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.pushforward f R ≤ T ↔ R ≤ CategoryTheory.Presieve.pullback f T
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_col : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α), (Matrix.of f).transpose.col = f
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.card_primitiveRoots : ∀ (k : ℕ), (primitiveRoots k ℂ).card = k.totient
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instRespectsLeftOppositeOpOfRespectsRight : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P Q : CategoryTheory.MorphismProperty C)
  [P.RespectsRight Q], P.op.RespectsLeft Q.op
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.coe_inv_map_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] {A : Type v} [inst_2 : CommRing A]
  (f : R →+* A), ↑(W.map f).Δ'⁻¹ = f ↑W.Δ'⁻¹
-- Mathlib.Data.Complex.Basic
Complex.ofReal_im : ∀ (r : ℝ), (↑r).im = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.ofNat_ctorIdx : ∀ (x : Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Γ'.ofNat x.ctorIdx = x
-- Std.Time.Format.DateFormat
Std.Time.DateFormat.mk.inj : ∀ {firstDayOfWeek : Std.Time.Weekday} {minimalDaysInFirstWeek : Std.Time.Internal.Bounded.LE 0 6}
  {symbols : Std.Time.DateFormatSymbols} {firstDayOfWeek_1 : Std.Time.Weekday}
  {minimalDaysInFirstWeek_1 : Std.Time.Internal.Bounded.LE 0 6} {symbols_1 : Std.Time.DateFormatSymbols},
  { firstDayOfWeek := firstDayOfWeek, minimalDaysInFirstWeek := minimalDaysInFirstWeek, symbols := symbols } =
      { firstDayOfWeek := firstDayOfWeek_1, minimalDaysInFirstWeek := minimalDaysInFirstWeek_1, symbols := symbols_1 } →
    firstDayOfWeek = firstDayOfWeek_1 ∧ minimalDaysInFirstWeek = minimalDaysInFirstWeek_1 ∧ symbols = symbols_1
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_congr_ring : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (S : Type u_4) [inst_3 : DivisionSemiring S] [inst_4 : Module S M] (f : α → α) (g : α → M)
  (n : ℕ) (x : α), birkhoffAverage R f g n x = birkhoffAverage S f g n x
-- Mathlib.SetTheory.ZFC.PSet
PSet.instSingleton : Singleton PSet.{u_1} PSet.{u_1}
-- Std.Sync.Channel
/-- Whether the channel is closed already.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.closed : {α : Type} → Std.CloseableChannel.Zero.State✝ α → Bool
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.toList_toArray : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α], m.WF → m.toArray.toList = m.toList
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.Functor.LeftExtension.nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} {F : CategoryTheory.Functor C₂ D} (E : R.LeftExtension F)
  (w : CategoryTheory.TwoSquare T L R B) (X₃ : C₃) [(w.costructuredArrowRightwards X₃).Final],
  Nonempty ((E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃) ↔
    Nonempty (E.IsPointwiseLeftKanExtensionAt (B.obj X₃))
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.splitter : {α : Type u_1} →
  (motive : List α → (α → α → Bool) → Sort u_2) →
    (x : List α) →
      (x_1 : α → α → Bool) →
        ((x : α → α → Bool) → motive [] x) →
          ((a : α) → (x : α → α → Bool) → motive [a] x) →
            ((a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) → motive x x_1
-- Init.Data.Iterators.Basic
/-- Converts elements of `Shrink α` into elements of `α`.  -/
Std.Shrink.inflate : {α : Type u_1} → Std.Shrink α → α
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_4.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b with
    | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
    | l => h_2 l) =
    h_1 a x b
-- Mathlib.Algebra.Quandle
Rack.invAct_apply : ∀ {R : Type u_1} [inst : Rack R] (x y : R), (Rack.act' x)⁻¹ y = Rack.invAct x y
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.swap α β)
-- Init.Data.Int.DivMod.Lemmas
Int.ofNat_tmod : ∀ (m n : ℕ), ↑(m % n) = (↑m).tmod ↑n
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.fderivLM 𝕜 n k) = ⇑(ContDiffMapSupportedIn.fderivLM 𝕜' n k)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
  [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {s : Set E}, AnalyticOnNhd 𝕜' f s → AnalyticOnNhd 𝕜 f s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (Std.ExtTreeMap.ofList l cmp).contains k = (List.map Prod.fst l).contains k
-- Mathlib.Order.SupClosed
latticeClosure_prod : ∀ {α : Type u_3} {β : Type u_4} [inst : DistribLattice α] [inst_1 : DistribLattice β] (s : Set α) (t : Set β),
  latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.le_opENorm_of_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) {c : ENNReal} {x : E}, ‖x‖ₑ ≤ c → ‖f x‖ₑ ≤ ‖f‖ₑ * c
-- Mathlib.Algebra.Algebra.Prod
AlgEquiv.prodCongr_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_5} {T : Type u_6} {A : Type u_7} {B : Type u_8}
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring S] [inst_4 : Semiring T] [inst_5 : Algebra R S]
  [inst_6 : Algebra R T] [inst_7 : Algebra R A] [inst_8 : Algebra R B] (l : S ≃ₐ[R] A) (r : T ≃ₐ[R] B) (x : S × T),
  (l.prodCongr r) x = ((↑l).prodCongr ↑r) x
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.toSubsemiring_lt_toSubsemiring : ∀ {R : Type u_1} [inst : CommRing R] {P₁ P₂ : RingPreordering R}, ↑P₁ < ↑P₂ ↔ P₁ < P₂
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerRight_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {x x_1 x_2 : CategoryTheory.Bicategory.InducedBicategory C F} {x_3 x_4 : x ⟶ x_1} (η : x_3 ⟶ x_4) (h : x_1 ⟶ x_2),
  (CategoryTheory.Bicategory.whiskerRight η h).hom = CategoryTheory.Bicategory.whiskerRight η.hom h.hom
-- Mathlib.Data.Finset.Basic
Finset.sdiff_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint (t \ s) s
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_nonneg : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), 0 ≤ dist x y
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.projectiveFamily.eq_1 : ∀ (I : Finset NNReal),
  ProbabilityTheory.BrownianReal.projectiveFamily I =
    MeasureTheory.Measure.map (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm)
      (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.polarizationEquiv_toLinearMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic] [inst_7 : P.IsRootSystem], ↑P.PolarizationEquiv = P.Polarization
-- Lean.Parser.Command
Lean.Parser.Command.structImplicitBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- LeanSearchClient.Syntax
LeanSearchClient.leanSearchTermImpl : Lean.Elab.Term.TermElab
-- Mathlib.Data.Finset.Image
Equiv.finsetCongr_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.finsetCongr.symm = e.symm.finsetCongr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f x` has
finite limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then `fderiv`
derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)` equals `(u, v) ↦ v • cb - u • ca`.  -/
intervalIntegral.fderiv_integral_of_tendsto_ae : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
        Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca) →
          Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb) →
            fderiv ℝ (fun p => ∫ (x : ℝ) in p.1..p.2, f x) (a, b) =
              (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- the underlying presheaf of modules of a sheaf of modules  -/
SheafOfModules.val : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → SheafOfModules R → PresheafOfModules R.obj
-- Mathlib.Data.Finsupp.PointwiseSMul
/-- **Alias** of `AddMonoidAlgebra.smul_eq`. -/
Finsupp.smul_eq : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : VAdd G P] [inst_1 : IsLeftCancelVAdd G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V)
  (p : P) (hp : optParam ((↑f.coeff.support).vaddAntidiagonal (Function.support x) p).Finite ⋯),
  (f • x) p = ∑ gh ∈ Finset.VAddAntidiagonal p hp, f.coeff gh.1 • x gh.2
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.stateful.inj : ∀ {h h_1 : Lean.TSyntax `Lean.binderIdent},
  Lean.Parser.Tactic.MRefinePat.stateful h = Lean.Parser.Tactic.MRefinePat.stateful h_1 → h = h_1
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- The **Banach-Steinhaus** theorem, or **Uniform Boundedness Principle**, for maps from a
barrelled space to any polynormable space.  -/
PolynormableSpace.banach_steinhaus : ∀ {ι : Type u_2} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {E : Type u_6} {F : Type u_7} [inst : NontriviallyNormedField 𝕜₁]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} [RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E]
  [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₁ E] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace E]
  [inst_8 : UniformSpace F] [IsUniformAddGroup E] [IsUniformAddGroup F] [ContinuousSMul 𝕜₁ E] [BarrelledSpace 𝕜₁ E]
  {𝓕 : ι → E →SL[σ₁₂] F} [PolynormableSpace 𝕜₂ F],
  (∀ (x : E), Bornology.IsVonNBounded 𝕜₂ (Set.range fun i => (𝓕 i) x)) → UniformEquicontinuous (DFunLike.coe ∘ 𝓕)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- A category has chosen pullbacks if every morphism has a chosen pullback.  -/
CategoryTheory.ChosenPullbacks : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type (max u₁ v₁)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V),
  LinearMap.IsAdjointPair B B ⇑(B.leftAdjointOfNondegenerate b φ) ⇑φ
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rii.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rii α},
  r.iter.toList = r.toList
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_pointReflection : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (x : P₁),
  ⇑(ContinuousAffineEquiv.pointReflection k x) = ⇑(Equiv.pointReflection x)
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
/-- The discriminant of the power basis given by a primitive root of unity `ζ` is the same as the
discriminant of the power basis given by `ζ - 1`.  -/
IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one : ∀ {n : ℕ} [inst : NeZero n] {K : Type u} [inst_1 : Field K] [inst_2 : CharZero K] {ζ : K}
  [ce : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n),
  Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
this.  -/
Ideal.mem_span_pow_iff_exists_isHomogeneous : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (x : ι → R) (y : R),
  y ∈ Ideal.span (Set.range x) ^ n ↔ ∃ p, p.IsHomogeneous n ∧ (MvPolynomial.eval x) p = y
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instCanLiftSetCoeForallForallForallMemForallHAdd : ∀ {M : Type u_1} [inst : Add M],
  CanLift (Set M) (AddSubsemigroup M) SetLike.coe fun s => ∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s
-- Lean.Compiler.MetaAttr
/-- Environment extension collecting `meta` annotations.  -/
_private.Lean.Compiler.MetaAttr.0.Lean.metaExt : Lean.TagDeclarationExtension
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTrunc.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff], K.stupidTrunc e = (K.restriction e).extend e
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sSup_of_not_bddAbove : ∀ {s : Set ℝ}, ¬BddAbove s → sSup s = 0
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsFiniteMeasureOnCompacts.inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [ContinuousInv G] [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  MeasureTheory.IsFiniteMeasureOnCompacts μ.inv
-- Lean.MonadEnv
Lean.isRec : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.Topology.Closure
isOpen_iff_forall_mem_open : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product map of two `C^n` functions on a set is `C^n` on the product set.  -/
ContDiffOn.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {F' : Type u_6}
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g t → ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t)
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.image_eq_target_inter_inv_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {s : Set X}, s ⊆ e.source → ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmoduleToDual_apply_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) [inst_7 : IsDomain R] [inst_8 : Module.IsTorsionFree R S] (N : Submodule R M)
  (x : ↥(B.dualSubmodule N)) (y : ↥N), ((B.dualSubmoduleToDual N) x) y = B.dualSubmoduleParing x y
-- Mathlib.RingTheory.MvPolynomial.FreeCommRing
FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [inst : DecidableEq κ] [inst_1 : CommRing R] [inst_2 : DecidableEq R]
  (p : ι → MvPolynomial κ R),
  ((FirstOrder.Ring.mvPolynomialSupportLEEquiv fun i => (p i).support).symm fun i =>
      MvPolynomial.coeff (↑i.snd) (p i.fst)) =
    ⟨p, ⋯⟩
-- Mathlib.Data.Part
Part.eq_of_get_eq_get : ∀ {α : Type u_1} {a b : Part α} (ha : a.Dom) (hb : b.Dom), a.get ha = b.get hb → a = b
-- Mathlib.Algebra.Group.Subgroup.Order
Subgroup.isCoatom_comap : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G ≃* H) {K : Subgroup H},
  IsCoatom (Subgroup.comap (↑f) K) ↔ IsCoatom K
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_insert_of_notMem_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α} (X : Set α), e ∉ M.E → M.eRk (insert e X) = M.eRk X
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_mapComp_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b_1 c : C} (f : a ⟶ b_1) (g : b_1 ⟶ c),
  ((CategoryTheory.Bicategory.Prod.sectR b C).mapComp f g).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id b)).hom
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_one : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A]
  [inst_3 : Star A], ⇑1 = id
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_const_le : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] (a : E), ‖fun x => a‖₊ ≤ ‖a‖₊
-- Init.Data.Array.Lemmas
Array.getElem_mem_toList : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs[i] ∈ xs.toList
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.productEquiv_apply : ∀ {ι : Type u_1} [inst : Finite ι] (X : ι → FintypeCat) (x : (∏ᶜ X).obj) (i : ι),
  (CategoryTheory.Limits.FintypeCat.productEquiv X) x i =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π X i)) x
-- Mathlib.SetTheory.Ordinal.Notation
ONote.ofNat_zero : ↑0 = 0
-- Mathlib.ModelTheory.DirectLimit
/-- The isomorphism between a direct limit of a system of substructures and their union.  -/
FirstOrder.Language.DirectLimit.Equiv_iSup : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      [inst_1 : Nonempty ι] →
        [inst_2 : IsDirectedOrder ι] →
          {M : Type u_1} →
            [inst_3 : L.Structure M] →
              (S : ι →o L.Substructure M) →
                L.Equiv
                  (FirstOrder.Language.DirectLimit (fun i => ↥(S i)) fun x x_1 h =>
                    FirstOrder.Language.Substructure.inclusion ⋯)
                  ↥(iSup ⇑S)