mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_eq_ordHom_of_coheight_eq_one : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {z : ↥X} (hz : Order.coheight z = 1) (f : ↑X.functionField),
  AlgebraicGeometry.Scheme.ord f z =
    Multiplicative.toAdd (WithZero.unzeroD 1 ((AlgebraicGeometry.Scheme.ordHom z hz) f))
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The identity morphism of a snake input.  -/
CategoryTheory.ShortComplex.SnakeInput.Hom.id : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.Hom S
-- Init.Data.Option.Lemmas
Option.isSome_of_eq_some : ∀ {α : Type u_1} {x : Option α} {y : α}, x = some y → x.isSome = true
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.add_fst : ∀ {q : ℕ} (x y : LucasLehmer.X q), (x + y).1 = x.1 + y.1
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.QuasiSeparated ⊤
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root enode in the equivalence class of `e`.  -/
Lean.Meta.Grind.getRootENode : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.ENode
-- Mathlib.RingTheory.Localization.Integral
/-- `integerNormalization p` normalizes `p` to have integer coefficients
by clearing the denominators  -/
IsLocalization.integerNormalization : {R : Type u_1} →
  [inst : CommRing R] →
    (M : Submonoid R) →
      {S : Type u_2} →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Polynomial S → Polynomial R
-- Mathlib.Topology.ContinuousMap.Units
/-- Equivalence between continuous maps into the additive units of an additive monoid with
continuous addition and the additive units of the additive monoid of continuous maps.  -/
ContinuousMap.addUnitsLift : {X : Type u_1} →
  {M : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : AddMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : ContinuousAdd M] → C(X, AddUnits M) ≃ AddUnits C(X, M)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Connecting two unreachable vertices by an edge preserves existing bridges,
provided the bridge is already an edge.  -/
SimpleGraph.IsBridge.sup_edge_of_not_reachable_of_isBridge : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {e : Sym2 V},
  ¬G.Reachable u v → G.IsBridge e → e ∈ G.edgeSet → (G ⊔ SimpleGraph.edge u v).IsBridge e
-- Mathlib.GroupTheory.Sylow
/-- A subgroup with cardinality `p ^ n` is a Sylow subgroup
where `n` is the multiplicity of `p` in the group order.  -/
Sylow.ofCard : {G : Type u_1} →
  [inst : Group G] →
    [Finite G] →
      {p : ℕ} → [Fact (Nat.Prime p)] → (H : Subgroup G) → Nat.card ↥H = p ^ (Nat.card G).factorization p → Sylow p G
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instForInOfMonad : {α : Type u} → {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForIn m (Std.TreeSet.Raw α cmp) α
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The conjugacy classes that are not trivial.  -/
ConjClasses.noncenter : (G : Type u_6) → [inst : Monoid G] → Set (ConjClasses G)
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_1.eq_3 : ∀ (motive : ℤ → Sort u_1) (d : ℕ) (h_1 : Unit → motive 0) (h_2 : (d d' : ℕ) → d = d' + 1 → motive (Int.ofNat d'.succ))
  (h_3 : (d : ℕ) → motive (Int.negSucc d)),
  (match Int.negSucc d with
    | 0 => h_1 ()
    | Int.ofNat d@hd:d'.succ => h_2 d d' hd
    | Int.negSucc d => h_3 d) =
    h_3 d
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddLeftMono : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  [inst_3 : AddZeroClass β] [inst_4 : ContinuousAdd β] [AddLeftMono β],
  AddLeftMono (CompactlySupportedContinuousMap α β)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.exists_ge_zero_eq_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [IsStrictOrderedRing S] [inst_8 : Algebra S R] [FaithfulSMul S R]
  [inst_10 : Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [inst_13 : Fintype ι],
  ∀ x ∈ Submodule.span S (Set.range ⇑P.root), ∃ s ≥ 0, (algebraMap S R) s = (P.RootForm x) x
-- Mathlib.FieldTheory.Finite.Basic
ZMod.frobenius_zmod : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], frobenius (ZMod p) p = RingHom.id (ZMod p)
-- Std.Time.Date.Unit.Week
/-- `Offset` represents an offset in weeks.
 -/
Std.Time.Week.Offset : Type
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indicator_indepFun_process_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P] {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ),
          ∫ (ω : Ω) in A, ∏ s, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X (↑s) ω) ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) (fun ω s => X s ω) P
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_mul_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] (a b c : α),
  gcd (a * b) (a * c) = normalize a * gcd b c
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.get? : {α : Type u} → {β : Type v} → [BEq α] → α → (Std.DHashMap.Internal.AssocList α fun x => β) → Option β
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3}
  [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [IsManifold I (↑⊤) M] [inst_10 : MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M → F}
  {μ : MeasureTheory.Measure M} [SigmaCompactSpace M] {U : Set M},
  IsOpen U →
    MeasureTheory.LocallyIntegrableOn f U μ →
      (∀ (g : M → ℝ),
          ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g →
            HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) →
        ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.tensor.injEq : ∀ {C : Type u} {W X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : W.Hom Y) (g : X.Hom Z) (f_1 : W.Hom Y)
  (g_1 : X.Hom Z), (f.tensor g = f_1.tensor g_1) = (f = f_1 ∧ g = g_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Eta-expanded form of `Measurable.comp` -/
Measurable.fun_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}
  {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable fun x => g (f x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.goto.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a a_1 : Γ → σ → Λ),
  (Turing.TM1.Stmt.goto a = Turing.TM1.Stmt.goto a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow h
-- Std.Internal.Do.Order.Basic
Lean.Order.le_of_right : ∀ (x y : Prop), y → Lean.Order.PartialOrder.rel x y
-- Init.SimpLemmas
false_or : ∀ (p : Prop), (False ∨ p) = p
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e` that `u : S.obj d ⟶ e`
induces via `CostructuredArrow.map₂` can be expressed up to isomorphism by
`CostructuredArrow.preEquivalence` and `CostructuredArrow.proj`.  -/
CategoryTheory.CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj : {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] →
            (T : CategoryTheory.Functor C D) →
              (S : CategoryTheory.Functor D E) →
                (d : D) →
                  (e : E) →
                    (u : S.obj d ⟶ e) →
                      CategoryTheory.CostructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (T.comp S)) u ≅
                        (CategoryTheory.CostructuredArrow.preEquivalence T
                                (CategoryTheory.CostructuredArrow.mk u)).inverse.comp
                          (CategoryTheory.CostructuredArrow.proj (CategoryTheory.CostructuredArrow.pre T S e)
                            (CategoryTheory.CostructuredArrow.mk u))
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.mk.sizeOf_spec : ∀ (decl : Lean.Declaration) (indFvars : Array Lean.Expr) (numParams : ℤ)
  (rs : Array Lean.Elab.Command.PreElabHeaderResult),
  sizeOf { decl := decl, indFvars := indFvars, numParams := numParams, rs := rs } =
    1 + sizeOf decl + sizeOf indFvars + sizeOf numParams + sizeOf rs
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.linear_inv_isBigO_right : ∀ (c : ℤ) (z : ℂ), (fun d => (↑c * z + ↑d)⁻¹) =O[Filter.cofinite] fun n => (↑n)⁻¹
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.innerSL_norm : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [Nontrivial E], ‖innerSL 𝕜‖ = 1
-- Init.Core
_private.Init.Core.0.Quotient.rel.refl : ∀ {α : Sort u} {s : Setoid α} (q : Quotient s), Quotient.rel✝ q q
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- If `P` lies over `p`, then `R / p` has a canonical map to `S / P`.

This can't be an instance since the map `f : R → S` is generally not inferable.
 -/
Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) → (P : Ideal S) → [hfp : NeZero (p.ramificationIdx' P)] → Algebra (R ⧸ p) (S ⧸ P)
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.Pushforward.comp_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z)
  (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ),
  (TopCat.Presheaf.Pushforward.comp f g ℱ).hom.app U =
    CategoryTheory.CategoryStruct.id
      (((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ).obj U)
-- Mathlib.Order.Directed
DirectedOn.snd : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r₂ : β → β → Prop} {d : Set (α × β)},
  DirectedOn (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) d → DirectedOn (fun x1 x2 => r₂ x1 x2) (Prod.snd '' d)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- See `AddAction.isBlock_subgroup` for a version that works for the left action
of a group on itself.  -/
AddAction.isBlock_addSubgroup' : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_3} {H : Type u_4} [inst_1 : AddGroup H] [inst_2 : SetLike S H]
  [AddSubgroupClass S H] {s : S} [inst_4 : AddAction G H] [VAddAssocClass G Hᵃᵒᵖ H], AddAction.IsBlock G ↑s
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The `SlashInvariantForm` associated to a `CuspForm`.  -/
CuspForm.toSlashInvariantForm : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → CuspForm Γ k → SlashInvariantForm Γ k
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The wide equalizer morphism in any limit cone is a monomorphism.  -/
CategoryTheory.Limits.mono_of_isLimit_parallelFamily : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  {c : CategoryTheory.Limits.Cone (CategoryTheory.Limits.parallelFamily f)} (i : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Mono (CategoryTheory.Limits.Trident.ι c)
-- Mathlib.Data.List.AList
AList.mk.injEq : ∀ {α : Type u} {β : α → Type v} (entries : List (Sigma β)) (nodupKeys : entries.NodupKeys) (entries_1 : List (Sigma β))
  (nodupKeys_1 : entries_1.NodupKeys),
  ({ entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := nodupKeys_1 }) =
    (entries = entries_1)
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult.mk : Option Lean.ModuleHeader → Array String → Lean.PrintImportResult
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The graph resulting from removing a vertex of degree one from a connected graph is connected.  -/
SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.Connected → ∀ {v : V} [inst : Fintype ↑(G.neighborSet v)], G.degree v = 1 → (SimpleGraph.induce {v}ᶜ G).Connected
-- Mathlib.Algebra.CubicDiscriminant
Cubic.mem_roots_iff : ∀ {R : Type u_1} {P : Cubic R} [inst : CommRing R] [inst_1 : IsDomain R],
  P.toPoly ≠ 0 → ∀ (x : R), x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
-- Init.Data.Bool
Bool.and_or_distrib_left : ∀ (x y z : Bool), (x && (y || z)) = (x && y || x && z)
-- Mathlib.RingTheory.WittVector.InitTail
/-- `init_ring` is an auxiliary tactic that discharges goals factoring `init` over ring operations.
 -/
WittVector.initRing : Lean.ParserDescr
-- Mathlib.Order.BoundedOrder.Basic
ULift.down_bot : ∀ {α : Type u} [inst : Bot α], ⊥.down = ⊥
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- `tensorProd R S` preserves the limit of the canonical fan on `P`.  -/
CommRingCat.Under.piFanTensorProductIsLimit : {R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    {ι : Type u} →
      (P : ι → CategoryTheory.Under R) →
        [Finite ι] → CategoryTheory.Limits.IsLimit ((R.tensorProd S).mapCone (CommRingCat.Under.piFan P))
-- Init.Data.Ord.Basic
Ordering.then.eq_2 : ∀ (a b : Ordering), (a = Ordering.eq → False) → a.then b = a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound : Inhabited Lean.Meta.Grind.Arith.Cutsat.SymbolicBound
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_eq_zero_of_eq : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) (v : ι → M) {i j : ι}, v i = v j → i ≠ j → f v = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.hom_inv_apply : ∀ {A B : ProfiniteGrp.{u}} (e : A ≅ B) (x : ↑B.toProfinite.toTop),
  (ProfiniteGrp.Hom.hom e.hom) ((ProfiniteGrp.Hom.hom e.inv) x) = x
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_eq_zero_iff_eq_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R},
  p.totalDegree = 0 ↔ p = MvPolynomial.C (MvPolynomial.coeff 0 p)
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.avgRisk_fintype' : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [inst : Fintype 𝓨] [MeasurableSingletonClass 𝓨],
  Measurable ℓ → ProbabilityTheory.avgRisk ℓ P κ π = ∑ y, ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π
-- Mathlib.Data.ENNReal.Basic
ENNReal.top_ne_natCast : ∀ (n : ℕ), ⊤ ≠ ↑n
-- Mathlib.LinearAlgebra.Ray
/-- `SameRay` is transitive unless the vector in the middle is zero and both other vectors are
nonzero.  -/
SameRay.trans : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y z : M},
  SameRay R x y → SameRay R y z → (y = 0 → x = 0 ∨ z = 0) → SameRay R x z
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Convolution semiring structure on linear maps from a coalgebra to an algebra.  -/
LinearMap.convSemiring : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid C] → [inst_4 : Module R C] → [Coalgebra R C] → Semiring (WithConv (C →ₗ[R] A))
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- **Alias** of `IsCyclic.isMulCommutative`. -/
IsCyclic.commutative : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α], IsMulCommutative α
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- The bottom `IntermediateField` is isomorphic to the field.  -/
IntermediateField.botEquiv : (F : Type u_1) → [inst : Field F] → (E : Type u_2) → [inst_1 : Field E] → [inst_2 : Algebra F E] → ↥⊥ ≃ₐ[F] F
-- Mathlib.Analysis.Convex.Between
Sbtw.mem_image_Ioo : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Sbtw R x y z → y ∈ ⇑(AffineMap.lineMap x z) '' Set.Ioo 0 1
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_le_tdiv : ∀ {a b c : ℤ}, 0 < c → a ≤ b → a.tdiv c ≤ b.tdiv c
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H]
  [inst_2 : AddAction G α] [inst_3 : MeasurableSpace α] [inst_4 : AddAction H β] [inst_5 : MeasurableSpace β]
  {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ {f : β → α},
      MeasureTheory.Measure.QuasiMeasurePreserving f ν μ →
        ∀ {e : G → H},
          Function.Bijective e →
            (∀ (g : G), Function.Semiconj f (fun x => e g +ᵥ x) fun x => g +ᵥ x) →
              MeasureTheory.IsAddFundamentalDomain H (f ⁻¹' s) ν
-- Mathlib.Analysis.Analytic.Order
analyticOrderNatAt.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (z₀ : 𝕜), analyticOrderNatAt f z₀ = (analyticOrderAt f z₀).toNat
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.Mon C} {x y : M.Hom N}, x.hom = y.hom → x = y
-- Mathlib.Algebra.Lie.LieTheorem
/-- An auxiliary lemma used only in the definition `LieModule.weightSpaceOfIsLieTower` below.  -/
_private.Mathlib.Algebra.Lie.LieTheorem.0.LieModule.weightSpaceOfIsLieTower_aux : ∀ {R : Type u_1} {L : Type u_2} {A : Type u_3} {V : Type u_4} [inst : CommRing R] [IsPrincipalIdealRing R] [IsDomain R]
  [CharZero R] [inst_4 : LieRing L] [inst_5 : LieAlgebra R L] [inst_6 : LieRing A] [inst_7 : LieAlgebra R A]
  [inst_8 : Bracket L A] [inst_9 : Bracket A L] [inst_10 : AddCommGroup V] [inst_11 : Module R V] [Module.Free R V]
  [Module.Finite R V] [inst_14 : LieRingModule L V] [LieModule R L V] [inst_16 : LieRingModule A V]
  [inst_17 : LieModule R A V] [IsLieTower L A V] [IsLieTower A L V] (χ : A → R) (z : L),
  ∀ v ∈ LieModule.weightSpace V χ, ⁅z, v⁆ ∈ LieModule.weightSpace V χ
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivalenceFunctor_unitIso_inv_app : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (X_1 : X →o Y),
  OrderHom.equivalenceFunctor.unitIso.inv.app X_1 = CategoryTheory.CategoryStruct.id X_1
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.contains.eq_1 : ∀ (s : Substring.Raw) (c : Char), Substring.Raw.Legacy.contains s c = Substring.Raw.Legacy.any s fun a => a == c
-- Init.Data.UInt.Bitwise
UInt32.toUInt16_and : ∀ (a b : UInt32), (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
-- Lean.Parser.Extra
Lean.Parser.nameLit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) {Z : C}
  (h : (t.truncLE c).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE a b hab).app X)
      (CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE b c hbc).app X) h) =
    CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE a c ⋯).app X) h
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.le_triangEnvelopeIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (n : ℕ), P ≤ P.triangEnvelopeIter n
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRoiSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRoiSlice._auto_1) →
    Std.Roi.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RoiSlice α)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Constructing a linear map `M ⊗ N → P` given a bilinear map `M → N → P` with the property that
its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`.

This works for semilinear maps.  -/
TensorProduct.lift : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {M : Type u_7} →
            {N : Type u_8} →
              {P₂ : Type u_17} →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : AddCommMonoid P₂] →
                      [inst_5 : Module R M] →
                        [inst_6 : Module R N] →
                          [inst_7 : Module R₂ P₂] → (M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) → TensorProduct R M N →ₛₗ[σ₁₂] P₂
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.range'_eq_range'TR.go : ∀ (step : optParam ℕ 1) (s n m : ℕ),
  List.range'TR.go step n (s + step * n) (List.range' (s + step * n) m step) = List.range' s (n + m) step
-- Mathlib.Geometry.Euclidean.Incenter
/-- The signed distance between the incenter and its projection in the plane of each face is the
inradius.

In other words, the incenter is _internally_ tangent to the faces.  -/
Affine.Simplex.signedInfDist_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (s.signedInfDist i) s.incenter = s.inradius
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_loops_eq_removeLoops : ∀ {α : Type u_1} (M : Matroid α), M.delete M.loops = M.removeLoops
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.gammaPDF_eq : ∀ (a r x : ℝ),
  ProbabilityTheory.gammaPDF a r x =
    ENNReal.ofReal (if 0 ≤ x then r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x)) else 0)