mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_rng_of_top : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {X : Type u_3}
  [inst_1 : TopologicalSpace X] {f : X → RestrictedProduct (fun i => R i) (fun i => A i) ⊤},
  Continuous f ↔ Continuous (DFunLike.coe ∘ f)
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The proposition that `invFun` is a right-inverse of `toFun` on `target`.  -/
PartialEquiv.right_inv' : ∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : β⦄, x ∈ self.target → ↑self (self.invFun x) = x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.keys_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.DTreeMap.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DTreeMap.Const.get t x ⋯))
        t.keys.attach).unattach
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_succ : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (n : ℕ), S.lowerCentralSeries (n + 1) = ⁅S.lowerCentralSeries n, S⁆
-- Mathlib.RingTheory.Ideal.Defs
Ideal.mul_sub_mul_mem : ∀ {α : Type u} [inst : Ring α] (I : Ideal α) {a b c d : α} [I.IsTwoSided], a - b ∈ I → c - d ∈ I → a * c - b * d ∈ I
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] ≤ [L : E]` are finite,
then `F = E`.  -/
IntermediateField.eq_of_le_of_finrank_le' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional (↥F) L], F ≤ E → Module.finrank (↥F) L ≤ Module.finrank (↥E) L → F = E
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addHaarContent.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.haar.addHaarContent K₀ =
    { toFun := fun K => ⟨MeasureTheory.Measure.haar.addCHaar K₀ K, ⋯⟩, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }
-- Mathlib.Data.Multiset.Lattice
/-- Supremum of a multiset: `sup {a, b, c} = a ⊔ b ⊔ c`  -/
Multiset.sup : {α : Type u_1} → [inst : SemilatticeSup α] → [OrderBot α] → Multiset α → α
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? : {α : Type u} →
  {β : Type v} →
    [BEq α] →
      [Hashable α] →
        (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → β → Option β × Std.DHashMap.Internal.Raw₀ α fun x => β
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_dirac : ∀ {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure α}, m.bind MeasureTheory.Measure.dirac = m
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
_private.Mathlib.Data.Fin.Tuple.NatAntidiagonal.0.List.Nat.antidiagonalTuple.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (k n : ℕ) → motive k.succ n),
  (match 0, 0 with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | k.succ, n => h_3 k n) =
    h_1 ()
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_eq_zero_iff_lt : ∀ {n k : ℕ}, n.descFactorial k = 0 ↔ n < k
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_mono_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E] {a b b' : E}
  {r : k}, b ≤ b' → 0 ≤ r → (AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b') r
-- Init.Data.Vector.Basic
Vector.take.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ), xs.take i = Vector.mk (xs.toArray.take i) ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.beqModel_eq_true_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  [∀ (k : α), ReflBEq (β k)] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ → l₁.Perm l₂ → Std.Internal.List.beqModel l₁ l₂ = true
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.congr : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_2, u, u} k H}
  {B : Rep.{u_2, u, u} k G} {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : Rep.res f₁ A ⟶ B} {T : Type u_1}
  (F : (f : G →* H) → (Rep.res f A ⟶ B) → T), F f₁ φ = F f₂ (h ▸ φ)
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftFunctorZero'_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero' C (φ 0) ⋯).inv.app X)
      ((CategoryTheory.pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.continuous_integral_comp_L1 : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  {𝕜' : Type u_7} [inst_1 : RCLike 𝕜] [inst_2 : RCLike 𝕜'] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F] [inst_7 : NormedSpace ℝ F] {σ : 𝕜 →+* 𝕜'}
  [RingHomIsometric σ] (L : E →SL[σ] F), Continuous fun φ => ∫ (x : X), L (↑↑φ x) ∂μ
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.add : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMaxOn f s a → IsLocalMaxOn g s a → IsLocalMaxOn (fun x => f x + g x) s a
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_pow : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (n : ℕ) (f : ι → M),
  ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.norm_snd_le : ∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.snd‖ ≤ ‖x‖
-- Init.Data.SInt.Lemmas
Int64.neg_ofNat : ∀ {n : ℕ}, -Int64.ofNat n = Int64.ofInt (-↑n)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_sdiff_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] {s : Finset ι},
  s.Nonempty → ∀ (f : ι → α) (a : α), (s.inf fun b => a \ f b) = a \ s.sup f
-- Mathlib.Algebra.Order.Floor.Div
smul_floorDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : MulActionWithZero α β] [inst_5 : FloorDiv α β] {a : α} [PosSMulMono α β]
  [PosSMulReflectLE α β], 0 < a → ∀ (b : β), a • b ⌊/⌋ a = b
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.steps : Lean.Meta.Grind.Arith.CommRing.State → ℕ
-- Init.Data.String.Lemmas.Search
String.back?_eq : ∀ {s : String}, s.back? = s.toList.getLast?
-- Init.Data.List.Scan.Basic
/-- Folds a monadic function over a list from the left, accumulating partial results starting with
`init`. The accumulated values are combined with the each element of the list in order, using `f`.
 -/
List.scanlM : {m : Type u_1 → Type u_2} → {β : Type u_1} → {α : Type u_3} → [Monad m] → (β → α → m β) → β → List α → m (List β)
-- Std.Sync.CancellationToken
/-- Creates a new cancellation token.
 -/
Std.CancellationToken.new : BaseIO Std.CancellationToken
-- Mathlib.Tactic.Linarith.Preprocessing
/-- Definition overridden in `Mathlib.Tactic.Linarith.NNRealPreprocessor`.  -/
Mathlib.Tactic.Linarith.nnrealToRealTransform : IO.Ref (List Lean.Expr → Lean.MetaM (List Lean.Expr))
-- Mathlib.Geometry.Manifold.Immersion
/-- A choice of chart on the domain `M` of an immersion `f` at `x`:
w.r.t. this chart and the data `h.codChart` and `h.equiv`,
`f` will look like an inclusion `u ↦ (u, 0)` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.codChart` and `h.codChart`.  -/
Manifold.IsImmersionAt.domChart : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} → Manifold.IsImmersionAt I J n f x → OpenPartialHomeomorph M H
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The `weightedTotalDegree'` of the zero polynomial is `⊥`.  -/
MvPolynomial.weightedTotalDegree'_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] (w : σ → M), MvPolynomial.weightedTotalDegree' w 0 = ⊥
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.of_isEmpty : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (s : Set X)
  [IsEmpty E], IsCoveringMapOn f s
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.norm_le_mul : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {K : NNReal},
  LipschitzWith K f → f 0 = 0 → ∀ (x : E), ‖f x‖ ≤ ↑K * ‖x‖
-- Mathlib.RingTheory.Frobenius
IsArithFrobAt.conj : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {G : Type u_3}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] {Q : Ideal S} {σ : G},
  IsArithFrobAt R σ Q → ∀ (τ : G), IsArithFrobAt R (τ * σ * τ⁻¹) (τ • Q)
-- Lean.Parser.Basic
Lean.Parser.leadingParser : Lean.Name →
  Lean.Parser.PrattParsingTables → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.insertMany_list_singleton : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {k : α} {v : β k},
  t.insertMany [⟨k, v⟩] = t.insert k v
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y Z : AlgebraicGeometry.Scheme}
  (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [inst : AlgebraicGeometry.IsAffine Z],
  P (CategoryTheory.CategoryStruct.comp f g) ↔ P g
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.neg.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (q : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.neg q =
    Quot.liftOn q
      (fun x =>
        match x with
        | (a, b) => Lean.Grind.Ring.OfSemiring.Q.mk (b, a))
      ⋯
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `Quot.locallyPathConnectedSpace`.

---

Quotients of locally path-connected spaces are locally path-connected.  -/
Quot.locPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {r : X → X → Prop},
  LocallyPathConnectedSpace (Quot r)
-- Mathlib.GroupTheory.Complement
/-- A left transversal is finite iff the subgroup has finite index.  -/
AddSubgroup.IsComplement.finite_left_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G},
  AddSubgroup.IsComplement S ↑H → (Finite ↑S ↔ H.FiniteIndex)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_right_le_size_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₂.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Data.Nat.Factorization.Defs
/-- We can write both `n.factorization p` and `n.factors.count p` to represent the power
of `p` in the factorization of `n`: we declare the former to be the simp-normal form.  -/
Nat.primeFactorsList_count_eq : ∀ {n p : ℕ}, List.count p n.primeFactorsList = n.factorization p
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.NormalizedHom → Sort u} (t : Mathlib.Tactic.BicategoryLike.NormalizedHom)
  (F_1 :
    (t : Mathlib.Tactic.BicategoryLike.NormalizedHom) → Mathlib.Tactic.BicategoryLike.NormalizedHom.below t → motive t),
  Mathlib.Tactic.BicategoryLike.NormalizedHom.brecOn t F_1 =
    F_1 t (Mathlib.Tactic.BicategoryLike.NormalizedHom.brecOn.go t F_1).2
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm_coe : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (hl : l.Nodup), (↑l).formPerm hl = l.formPerm
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.equivalenceLeftToRight_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C)
  (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F),
  (CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).right = CategoryTheory.Arrow.Hom.right G
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.eq_of_mul_eq_mul_of_coprime_aux : ∀ {a b x y : ℕ}, a.Coprime b → a * x = b * y → a ∣ y
-- Mathlib.Data.List.Zip
List.revzip_swap : ∀ {α : Type u} (l : List α), List.map Prod.swap l.revzip = l.reverse.revzip
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFin_add : ∀ {𝕜 : 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] {n : ℕ}
  (f g : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F),
  ContinuousAlternatingMap.alternatizeUncurryFin (f + g) =
    ContinuousAlternatingMap.alternatizeUncurryFin f + ContinuousAlternatingMap.alternatizeUncurryFin g
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.eval₂_reflect_mul_pow : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : CommSemiring S] (i : R →+* S) (x : S)
  [inst_2 : Invertible x] (N : ℕ) (f : Polynomial R),
  f.natDegree ≤ N → Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) * x ^ N = Polynomial.eval₂ i x f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.real_exp_eq_normedSpace_exp : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A},
  autoParam (IsSelfAdjoint a) CFC.real_exp_eq_normedSpace_exp._auto_1 → cfc Real.exp a = NormedSpace.exp a
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- The rank of the radical of a quadratic map is invariant under equivalences.  -/
QuadraticMap.Equivalent.rank_radical_eq : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup M']
  [inst_2 : AddCommGroup P] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R M'] [inst_6 : Module R P]
  {Q : QuadraticMap R M P} {Q' : QuadraticMap R M' P},
  Q.Equivalent Q' → Module.finrank R ↥Q.radical = Module.finrank R ↥Q'.radical
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.inl_eq_inr_of_epi_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f],
  CategoryTheory.Limits.pushout.inl f f = CategoryTheory.Limits.pushout.inr f f
-- Mathlib.Data.Fintype.Sigma
Finset.univ_sigma_univ : ∀ {ι : Type u_1} {κ : ι → Type u_3} [inst : (i : ι) → Fintype (κ i)] [inst_1 : Fintype ι],
  (Finset.univ.sigma fun x => Finset.univ) = Finset.univ
-- Init.Data.UInt.Lemmas
UInt32.toFin_toUSize : ∀ (n : UInt32), n.toUSize.toFin = Fin.castLE UInt32.size_le_usizeSize n.toFin
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The comparison morphism from the initial object in the target category to the image of the initial
object.
 -/
CategoryTheory.Limits.initialComparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasInitial C] →
            [inst_3 : CategoryTheory.Limits.HasInitial D] → ⊥_ D ⟶ G.obj (⊥_ C)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → β → γ},
  m.WF → (Std.HashMap.Raw.map f m).toList.Perm (List.map (fun p => (p.1, f p.1 p.2)) m.toList)
-- Mathlib.FieldTheory.Perfect
/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
a bijection from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowEquivRoots_apply`.  -/
Polynomial.rootsExpandPowEquivRoots : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      (p : ℕ) →
        [ExpChar R p] →
          (f : Polynomial R) →
            [inst_3 : DecidableEq R] →
              [PerfectRing R p] → (n : ℕ) → ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset ≃ ↥f.roots.toFinset
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMap_apply : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₂ e₂]
  (p : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x),
  ↑(Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂) p =
    (p.proj,
      Bundle.Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj ∘SL p.snd ∘SL Bundle.Trivialization.symmL 𝕜₁ e₁ p.proj)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.generated_le_generatedNormal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)),
  CategoryTheory.Subgroupoid.generated X ≤ CategoryTheory.Subgroupoid.generatedNormal X
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Assumes right covariance.  -/
Right.mul_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [MulPosMono α], 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Mathlib.Order.Monotone.Basic
Antitone.strictAnti_iff_injective : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Antitone f → (StrictAnti f ↔ Function.Injective f)
-- Mathlib.Algebra.Quaternion
Quaternion.coe_zero : ∀ {R : Type u_3} [inst : CommRing R], ↑0 = 0
-- Init.System.IO
/-- Discards the passed owned reference. This leads to `a` and any object reachable from it never being
freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
would be similarly costly to deallocation). It is still considered a safe operation as it cannot
lead to undefined behavior.
 -/
Runtime.forget : {α : Sort u_1} → α → BaseIO Unit
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.inducedMeasure_regular : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B], (H.inducedMeasure μA μC).Regular
-- Init.Prelude
Lean.Macro.instNonemptyMethodsRef : Nonempty Lean.Macro.MethodsRef
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The `X` in the standard etale algebra `R[X][Y]/⟨f, Yg-1⟩`.  -/
StandardEtalePair.X : {R : Type u_1} → [inst : CommRing R] → (P : StandardEtalePair R) → P.Ring
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toSDiff : {α : Type u} → [self : BooleanAlgebra α] → SDiff α
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.mk.congr_simp : ∀ {α : Type u_1} (E E_1 : Set α) (e_E : E = E_1) (IsBase IsBase_1 : Set α → Prop) (e_IsBase : IsBase = IsBase_1)
  (Indep Indep_1 : Set α → Prop) (e_Indep : Indep = Indep_1)
  (indep_iff' : ∀ ⦃I : Set α⦄, Indep I ↔ ∃ B, IsBase B ∧ I ⊆ B) (exists_isBase : ∃ B, IsBase B)
  (isBase_exchange : Matroid.ExchangeProperty IsBase)
  (maximality : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  { E := E, IsBase := IsBase, Indep := Indep, indep_iff' := indep_iff', exists_isBase := exists_isBase,
      isBase_exchange := isBase_exchange, maximality := maximality, subset_ground := subset_ground } =
    { E := E_1, IsBase := IsBase_1, Indep := Indep_1, indep_iff' := ⋯, exists_isBase := ⋯, isBase_exchange := ⋯,
      maximality := ⋯, subset_ground := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_transpose : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.transpose.charmatrix = M.charmatrix.transpose
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.egirth.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α), G.egirth = ⨅ a, ⨅ w, ⨅ (_ : w.IsCycle), ↑w.length
-- Lean.Server.CodeActions.Attr
/-- An entry in the command code actions extension, containing the attribute arguments.  -/
Lean.CodeAction.CommandCodeActionEntry : Type
-- Lean.Elab.Tactic.Conv.Pattern
_private.Lean.Elab.Tactic.Conv.Pattern.0.Lean.Elab.Tactic.Conv.getContext : Lean.MetaM Lean.Meta.Simp.Context