mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
uniqueMDiffWithinAt_iff_inter_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M},
  UniqueMDiffAt[s] x ↔ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.card_topEdgeLabeling : ∀ {V : Type u_1} {K : Type u_3} [inst : DecidableEq V] [inst_1 : Fintype V] [inst_2 : Fintype K],
  Fintype.card (SimpleGraph.TopEdgeLabeling V K) = Fintype.card K ^ (Fintype.card V).choose 2
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.copy : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  P = P' →
    (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f) →
      AlgebraicGeometry.HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q'
-- Mathlib.NumberTheory.Dioph
/-- The set of places where two Diophantine functions are equal is Diophantine.  -/
Dioph.«term_D=_» : Lean.TrailingParserDescr
-- Mathlib.Order.BoundedOrder.Basic
subsingleton_of_top_le_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊤ ≤ ⊥ → Subsingleton α
-- Init.Data.Array.Lemmas
Array.forall_mem_flatten : ∀ {α : Type u_1} {p : α → Prop} {xss : Array (Array α)}, (∀ x ∈ xss.flatten, p x) ↔ ∀ xs ∈ xss, ∀ x ∈ xs, p x
-- Mathlib.Order.Interval.Set.Basic
Set.self_notMem_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∉ Set.Iio a
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_zero : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })), SSet.yonedaEquiv.symm x = SSet.const x
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.imp_right : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) {C D : Stream'.WSeq α → Stream'.WSeq β → Prop},
  (∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s t → D s t) →
    ∀ {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)},
      Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO R D o p
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_of_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → m.get! a = default
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_union_closure_empty_eq : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure X ∪ M.closure ∅ = M.closure X
-- Mathlib.Algebra.Group.Defs
npowRec'.eq_def : ∀ {M : Type u_2} [inst : One M] [inst_1 : Mul M] (x : ℕ) (x_1 : M),
  npowRec' x x_1 =
    match x, x_1 with
    | 0, x => 1
    | 1, m => m
    | k.succ.succ, m => npowRec' (k + 1) m * m
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_algebraMap : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (r : R),
  QuadraticAlgebra.trace ((algebraMap R (QuadraticAlgebra R a b)) r) = 2 * r
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, a ∈ t → t[a]? = some t[a]!
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.idealOfLE_top : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.idealOfLE ⊤ ⋯ = ⊥
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  (H : CategoryTheory.Functor E E'), (F.comp G).comp H = F.comp (G.comp H)
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Eta-expanded form of `Function.HasTemperateGrowth.add` -/
Function.HasTemperateGrowth.fun_add : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f g : E → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth fun i => f i + g i
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.finite_universalFactorizationMap : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  (MvPolynomial.universalFactorizationMap R n m k hn).Finite
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₃.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.u₃✝ S = FermatLastTheoremForThreeGen.Solution.u₃✝ S_1
-- Mathlib.Data.Set.Prod
Set.graphOn_inj : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β}, Set.graphOn f s = Set.graphOn g s ↔ Set.EqOn f g s
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.comp_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x y z : FundamentalGroupoid X) (p : x ⟶ y) (q : y ⟶ z),
  CategoryTheory.CategoryStruct.comp p q = Path.Homotopic.Quotient.trans p q
-- Mathlib.Algebra.Prime.Lemmas
prime_pow_succ_dvd_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p x y : M},
  Prime p → ∀ {i : ℕ}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x ∨ p ∣ y
-- Mathlib.Condensed.Light.Module
/-- The category of light condensed abelian groups, defined as sheaves of `ℤ`-modules over
`LightProfinite.{0}` with respect to the coherent Grothendieck topology.
 -/
LightCondAb : Type 1
-- Qq.Macro
Qq.Impl.UnquoteState.withLevelNames : {α : Type} → Qq.Impl.UnquoteState → Lean.Elab.TermElabM (α × Array Lean.Name) → Lean.Elab.TermElabM α
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.noMaxOrder_rank_toType : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)], NoMaxOrder (Module.rank F E).ord.ToType
-- Mathlib.CategoryTheory.Galois.Basic
/-- The fiber of the equalizer of `f g : X ⟶ Y` is equivalent to the set of agreement of `f`
and `g`.  -/
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [inst_1 : CategoryTheory.PreGaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {X Y : C} →
            (f g : X ⟶ Y) →
              (F.obj (CategoryTheory.Limits.equalizer f g)).obj ≃
                { x //
                  (CategoryTheory.ConcreteCategory.hom (F.map f)) x =
                    (CategoryTheory.ConcreteCategory.hom (F.map g)) x }
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_mono : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : Polynomial R} {g : Polynomial S},
  f.support ⊆ g.support → f.degree ≤ g.degree
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.covariant_iff_contravariant : ∀ {N : Type u_2} {r : N → N → Prop} [inst : AddGroup N],
  Covariant N N (fun x1 x2 => x1 + x2) r ↔ Contravariant N N (fun x1 x2 => x1 + x2) r
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Pseudofunctor.leftZigzag_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.Pseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  CategoryTheory.Bicategory.leftZigzag
      (CategoryTheory.CategoryStruct.comp (F.mapId a).inv
        (CategoryTheory.CategoryStruct.comp (F.map₂ adj.unit) (F.mapComp f g).hom))
      (CategoryTheory.CategoryStruct.comp (F.mapComp g f).inv
        (CategoryTheory.CategoryStruct.comp (F.map₂ adj.counit) (F.mapId b).hom)) =
    CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f))
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv
        (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftZigzag adj.unit adj.counit))
          (CategoryTheory.bicategoricalComp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom))))
-- Init.System.IO
IO.FS.Stream.mk.sizeOf_spec : ∀ (flush : IO Unit) (read : USize → IO ByteArray) (write : ByteArray → IO Unit) (getLine : IO String)
  (putStr : String → IO Unit) (isTty : BaseIO Bool),
  sizeOf { flush := flush, read := read, write := write, getLine := getLine, putStr := putStr, isTty := isTty } = 1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
      (i j : Fin (f.insertRupUnits units).1.rupUnits.size),
      i ≠ j → (f.insertRupUnits units).1.rupUnits[i] ≠ (f.insertRupUnits units).1.rupUnits[j]
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The canonical mapping from probability measures to finite measures is an embedding.  -/
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding : ∀ (Ω : Type u_2) [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Topology.IsEmbedding MeasureTheory.ProbabilityMeasure.toFiniteMeasure
-- Batteries.Data.MLList.Basic
/-- Return the head of a monadic lazy list, as a value in the monad.
Fails if the list is empty.
 -/
MLList.head : {m : Type u_1 → Type u_1} → {α : Type u_1} → [AlternativeMonad m] → MLList m α → m α
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.weightedSumSquares_apply : ∀ {S : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_8} [inst_1 : Fintype ι] [inst_2 : Monoid S]
  [inst_3 : DistribMulAction S R] [inst_4 : SMulCommClass S R R] (w : ι → S) (v : ι → R),
  (QuadraticMap.weightedSumSquares R w) v = ∑ i, w i • (v i * v i)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isDetector_detector : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.HasDetector C],
  CategoryTheory.IsDetector (CategoryTheory.detector C)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffAt_extChartAt' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {x : M} [IsManifold I n M] {x' : M},
  x' ∈ (chartAt H x).source → ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(extChartAt I x)) x'
-- Mathlib.Order.Hom.Set
OrderIso.subsingleton_of_wellFoundedLT' : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] [WellFoundedLT β] [inst_2 : Preorder α], Subsingleton (α ≃o β)
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- A family `𝒜` of sets of a measure space is said to be measure-dense if it contains only
measurable sets and can approximate any measurable set with finite measure, in the sense that
for any measurable set `s` with finite measure the symmetric difference `s ∆ t` can be made
arbitrarily small when `t ∈ 𝒜`. We show below that such a family can be chosen to contain only
sets with finite measure.

The term "measure-dense" is justified by the fact that the approximating condition translates
to the usual notion of density in the metric space made by constant indicators of measurable sets
equipped with the `Lᵖ` norm.  -/
MeasureTheory.Measure.MeasureDense : {X : Type u_1} → [m : MeasurableSpace X] → MeasureTheory.Measure X → Set (Set X) → Prop
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedCommGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedCommGroup E],
  ULift.seminormedCommGroup =
    SeminormedCommGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.SimpleModule.Basic
isSimpleModule_iff_toSpanSingleton_surjective : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSimpleModule R M ↔ Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.cofibrations_eq_unop : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.cofibrations C = (HomotopicalAlgebra.fibrations Cᵒᵖ).unop
-- Mathlib.Order.Lattice
toDual_inf : ∀ {α : Type u} [inst : Min α] (a b : α), OrderDual.toDual (a ⊓ b) = OrderDual.toDual a ⊔ OrderDual.toDual b
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r),
  (match RBTree.RBNode.node RBTree.RBColor.black a y b with
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
    | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
    | r => h_3 r) =
    h_1 a y b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {fallback : β a}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Not registered as an instance because `R` is an `outParam` in `SMulMemClass S R M`.  -/
AddSubgroupClass.zsmulMemClass : ∀ {S : Type u_1} {M : Type u_2} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [AddSubgroupClass S M],
  SMulMemClass S ℤ M
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.isInvertible_comp_equiv : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {e : M₃ ≃L[R] M} {f : M →L[R] M₂}, (f ∘SL ↑e).IsInvertible ↔ f.IsInvertible
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Constructor for isomorphisms in `ModuleCat R` taking an isomorphism in `AddCommGrpCat`
and a compatibility condition.  -/
ModuleCat.isoMk : {R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N) →
        (∀ (r : R),
            CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom) →
          (M ≅ N)
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRcoSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRcoSlice._auto_1) →
      Std.Rco.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RcoSlice α β)
-- Mathlib.NumberTheory.GaussSum
/-- For a quadratic character `χ` and when the characteristic `p` of the target ring
is a unit in the source ring and `n` is a natural number, the `p^n`th power of the Gauss
sum of `χ` and `ψ` is `χ (p^n)` times the original Gauss sum.  -/
MulChar.IsQuadratic.gaussSum_frob_iter : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
  [fp : Fact (Nat.Prime p)] [hch : CharP R' p] (n : ℕ),
  IsUnit ↑p →
    ∀ {χ : MulChar R R'}, χ.IsQuadratic → ∀ (ψ : AddChar R R'), gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsRightUniformAddGroup.uniformity_eq : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : AddGroup G} [self : IsRightUniformAddGroup G],
  uniformity G = Filter.comap (fun x => x.2 + -x.1) (nhds 0)
-- Mathlib.Order.Category.Lat
/-- `OrderDual` as a functor.  -/
Lat.dual : CategoryTheory.Functor Lat Lat
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.UniversallyInjective.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x =>
          Function.Injective x).universally
      f →
    AlgebraicGeometry.UniversallyInjective f
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mkHom_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (x : M × ↥S),
  AddLocalization.mkHom x = AddLocalization.mk x.1 x.2
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {A : Type u_1} [inst_1 : Semiring A],
  1 ≤ p.natDegree →
    ∀ (f : R →+* A) (x : A),
      Commute (f p.leadingCoeff) x →
        (∀ {r r' : R}, Commute (f r) (f r')) →
          Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization =
            f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.ext_hom_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (φ : c.pt ≅ c'.pt)
  (winl :
    autoParam (CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl) CategoryTheory.Limits.BinaryBicones.ext._auto_1)
  (winr :
    autoParam (CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr) CategoryTheory.Limits.BinaryBicones.ext._auto_3)
  (wfst :
    autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst) CategoryTheory.Limits.BinaryBicones.ext._auto_5)
  (wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd)
      CategoryTheory.Limits.BinaryBicones.ext._auto_7),
  (CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).hom.hom = φ.hom
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.eq_1 : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] [inst_1 : TopologicalSpace ε] (f : α → ε)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.MemLp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLpNorm f p μ < ⊤)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (μ : MeasureTheory.Measure Ω)
  (f : MeasureTheory.Filtration ι m) [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.SigmaFiniteFiltration μ f
-- Mathlib.CategoryTheory.EssentiallySmall
/-- Help the typechecker by explicitly translating from `C` to `ShrinkHoms C`.  -/
CategoryTheory.ShrinkHoms.toShrinkHoms : {C' : Type u_2} → C' → CategoryTheory.ShrinkHoms.{u_2} C'
-- Mathlib.RepresentationTheory.Induced
Rep.indResHomEquiv.eq_1 : ∀ {k : Type u} {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{max w v' u, u, v} k G) (B : Rep.{max w v' u, u, v'} k H),
  Rep.indResHomEquiv φ A B =
    {
      toFun := fun f =>
        Rep.ofHom
          { toLinearMap := (Rep.Hom.hom f).toLinearMap ∘ₗ Representation.IndV.mk φ A.ρ 1, isIntertwining' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯,
      invFun := fun f =>
        Rep.ofHom
          {
            toLinearMap :=
              Representation.Coinvariants.lift
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                (TensorProduct.lift
                  (((Finsupp.lift (↑A →ₗ[k] ↑B) k H) fun h => B.ρ h⁻¹ ∘ₗ (Rep.Hom.hom f).toLinearMap) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)))
                ⋯,
            isIntertwining' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] (g : ↥(Subgroup.center (SpecialLinearGroup R V))),
  ↑↑↑g = SpecialLinearGroup.centerEquivRootsOfUnity g • LinearMap.id
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- A point on a line through a point on a sphere and a second point equals that point or
`secondInter`.  -/
EuclideanGeometry.Sphere.eq_or_eq_secondInter_iff_mem_of_mem_affineSpan_pair : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  p ∈ s → ∀ {p' : P}, p' ∈ line[ℝ, p, q] → (p' = p ∨ p' = s.secondInter p (q -ᵥ p) ↔ p' ∈ s)
-- Init.Data.List.Erase
List.eraseIdx_sublist : ∀ {α : Type u_1} (l : List α) (k : ℕ), (l.eraseIdx k).Sublist l
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concatRec_nil : ∀ {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1}
  (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
  (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) (u : V),
  SimpleGraph.Walk.concatRec Hnil Hconcat SimpleGraph.Walk.nil = Hnil
-- Batteries.Linter.UnreachableTactic
/-- Gets the value of the `linter.unreachableTactic` option.  -/
Batteries.Linter.UnreachableTactic.getLinterUnreachableTactic : Lean.Linter.LinterOptions → Bool
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_le_one : ∀ (x : ℝ), Real.sin x ≤ 1
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateContImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [inst_5 : IsAbelianGalois ℚ K]
  (F : IntermediateField ℚ K) (χ : DirichletCharacter R n),
  χ ∈ (IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R) F ↔
    ∀ σ ∈ F.fixingSubgroup, χ ↑((IsCyclotomicExtension.Rat.galEquivZMod n K) σ) = 1
-- Init.Data.Float.Model.Float32
Float32.Model.instDiv : Div Float32.Model
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_erase!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.erase! k t) k = none
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasProjectiveDimensionLT S.X₁ n →
        CategoryTheory.HasProjectiveDimensionLT S.X₃ n → CategoryTheory.HasProjectiveDimensionLT S.X₂ n