mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
/-- `panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
`α` implements `Inhabited`.
At runtime, `msg` and the file position are printed to stderr unless the C
function `lean_set_panic_messages(false)` has been executed before. If the C
function `lean_set_exit_on_panic(true)` has been executed before, the process is
then aborted.
 -/
Lean.Parser.Term.panic : Lean.Parser.Parser
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.fvar.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {fvarId_1 : Lean.FVarId} {args_1 : Array (Lean.Compiler.LCNF.Arg pu)},
  Lean.Compiler.LCNF.LetValue.fvar fvarId args = Lean.Compiler.LCNF.LetValue.fvar fvarId_1 args_1 →
    fvarId = fvarId_1 ∧ args = args_1
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardRuleStateStats.default : Aesop.ForwardRuleStateStats
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is separable,
then $[K:F]_i = [K:E]_i$.
It is a special case of `Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it.  -/
Field.insepDegree_eq_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E],
  Field.insepDegree F K = Field.insepDegree E K
-- Init.GetElem
List.getElem?_eq_none_iff : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l[i]? = none ↔ l.length ≤ i
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.mul_natCast_lt : ∀ {a o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o → a < o → ∀ (n : ℕ), a * ↑n < o
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mulLeftRight_apply : ∀ {R : Type u_14} {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (a b x : A),
  (LinearMap.mulLeftRight R (a, b)) x = a * x * b
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If `f` is meromorphic, then the divisor of `f ^ n` is `n` times the divisor of `f`.
 -/
MeromorphicOn.divisor_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicOn f U → ∀ (n : ℤ), MeromorphicOn.divisor (f ^ n) U = n • MeromorphicOn.divisor f U
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.step_iterFromIdx : ∀ {β : Type w} {array : Array β} {pos : ℕ},
  (array.iterFromIdx pos).step =
    if h : pos < array.size then Std.PlausibleIterStep.yield (array.iterFromIdx (pos + 1)) array[pos] ⋯
    else Std.PlausibleIterStep.done ⋯
-- Init.Data.UInt.Lemmas
USize.neg_mul_neg : ∀ (a b : USize), -a * -b = a * b
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DHashMap.Internal.Raw₀ α β → Sort u_3) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size)
  (h_1 :
    (size : ℕ) →
      (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
        (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
          motive ⟨{ size := size, buckets := buckets }, hm⟩),
  (match ⟨{ size := size, buckets := buckets }, hm⟩ with
    | ⟨{ size := size, buckets := buckets }, hm⟩ => h_1 size buckets hm) =
    h_1 size buckets hm
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The map is alternating: if `v` has two equal coordinates, then `f v = 0`.  -/
AlternatingMap.map_eq_zero_of_eq' : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (self : M [⋀^ι]→ₗ[R] N) (v : ι → M) (i j : ι),
  v i = v j → i ≠ j → (↑self).toFun v = 0
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
/-- The inclusion `InjectiveObject C ⥤ C` of the full subcategory of
injective objects in `C`.  -/
CategoryTheory.InjectiveObject.ι : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.InjectiveObject C) C
-- Mathlib.Data.PEquiv
PEquiv.instInhabited : {α : Type u} → {β : Type v} → Inhabited (α ≃. β)
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.mk.inj : ∀ {R : Type u} {inst : Ring R} {n : ℕ} {S : Submodule R (Fin n → R)} {n_1 : ℕ} {S_1 : Submodule R (Fin n_1 → R)},
  { n := n, S := S } = { n := n_1, S := S_1 } → n = n_1 ∧ S ≍ S_1
-- Mathlib.Geometry.Euclidean.Triangle
EuclideanGeometry.angle_le_iff_dist_le : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P},
  ¬Collinear ℝ {a, b, c} → (EuclideanGeometry.angle a c b ≤ EuclideanGeometry.angle a b c ↔ dist a b ≤ dist a c)
-- Mathlib.Data.Num.Lemmas
Num.zero_add : ∀ (n : Num), 0 + n = n
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_toPreZeroHypercover : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D),
  (E.map F).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Any two measures satisfying `AddQuotientMeasureEqMeasurePreimage` are equal.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.unique : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [hasFun : MeasureTheory.HasAddFundamentalDomain G α ν]
  (μ μ' : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ'],
  μ = μ'
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)).hom
        h)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaObjObjEquiv_map_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X X' : C}
  {Y : Cᵒᵖ} (f : (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') {Z : C} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.shrinkYonedaObjObjEquiv
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.map g).app Y)) f))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaObjObjEquiv f)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.measurableSet_spanningSetsIndex : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
  Measurable (MeasureTheory.spanningSetsIndex μ)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.PComp.mk.inj : ∀ {c : Mathlib.Tactic.Linarith.Comp} {src : Mathlib.Tactic.Linarith.CompSource}
  {history effective implicit vars : Std.TreeSet ℕ compare} {c_1 : Mathlib.Tactic.Linarith.Comp}
  {src_1 : Mathlib.Tactic.Linarith.CompSource} {history_1 effective_1 implicit_1 vars_1 : Std.TreeSet ℕ compare},
  { c := c, src := src, history := history, effective := effective, implicit := implicit, vars := vars } =
      { c := c_1, src := src_1, history := history_1, effective := effective_1, implicit := implicit_1,
        vars := vars_1 } →
    c = c_1 ∧ src = src_1 ∧ history = history_1 ∧ effective = effective_1 ∧ implicit = implicit_1 ∧ vars = vars_1
-- Mathlib.Analysis.Normed.Group.Real
NNReal.nnnorm_eq_self : ∀ (x : NNReal), ‖x‖₊ = x
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.mul_apply' : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] (x y : R),
  ((ContinuousLinearMap.mul 𝕜 R) x) y = x * y
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatClamp n).toFin = ⟨n, hn⟩
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_erase : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h : t.WF) {k a : α},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl a =
    if compare k a = Ordering.eq then default else Std.DTreeMap.Internal.Impl.Const.get! t a
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.isRkFinite_iff_cRk_lt_aleph0 : ∀ {α : Type u} {M : Matroid α} {X : Set α}, M.IsRkFinite X ↔ M.cRk X < Cardinal.aleph0
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The `NormedRing` structure on a ring `R` determined by a `RingNorm`.  -/
RingNorm.toNormedRing : {R : Type u_1} → [inst : Ring R] → RingNorm R → NormedRing R
-- Mathlib.Data.Part
Part.ofOptionDecidable : {α : Type u_1} → (o : Option α) → Decidable (↑o).Dom
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instSingletonSigma : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Singleton ((a : α) × β a) (Std.DTreeMap.Raw α β cmp)
-- Lean.Data.Lsp.Basic
Lean.Lsp.Command.mk.injEq : ∀ (title command : String) (arguments? : Option (Array Lean.Json)) (title_1 command_1 : String)
  (arguments?_1 : Option (Array Lean.Json)),
  ({ title := title, command := command, arguments? := arguments? } =
      { title := title_1, command := command_1, arguments? := arguments?_1 }) =
    (title = title_1 ∧ command = command_1 ∧ arguments? = arguments?_1)
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOneMeasure μ]
  {s t : Set α}, MeasurableSet s → MeasurableSet t → μ s = 1 → μ t = 1 → μ (s ∩ t) = 1
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.triangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Arrow C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Arrow C)) Y).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_span_mul_finite_of_mem_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P} {x : P}, x ∈ I * J → ∃ T T', ↑T ⊆ ↑I ∧ ↑T' ⊆ ↑J ∧ x ∈ Submodule.span R (↑T * ↑T')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.WeierstrassCurve.Projective.toAffine_negAddY_of_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    ∀ {n d : F},
      d ≠ 0 →
        W.toAffine.negAddY (P 0 / P 2) (P 0 / P 2) (P 1 / P 2) (-n / P 2 / d) =
          (-n * (n ^ 2 - W.a₁ * n * P 2 * d - W.a₂ * P 2 ^ 2 * d ^ 2 - 2 * P 0 * P 2 * d ^ 2 - P 0 * P 2 * d ^ 2) +
                P 1 * P 2 ^ 2 * d ^ 3) /
              P 2 ^ 2 /
            (P 2 * d ^ 3)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastZeroExtend : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α)
  (target : aig.ExtendTarget newWidth) (assign : α → Bool) (idx : ℕ) (hidx : idx < newWidth),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend aig target).vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧ else false
-- Std.Time.Format.Modifier
/-- Two-letter short form (e.g., "Tu"). Produced only by 6-letter weekday patterns (`EEEEEE`, `eeeeee`, `cccccc`).
 -/
Std.Time.Text.twoLetterShort : Std.Time.Text
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.prodMk : ∀ {α : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β₁]
  [inst_2 : AddCommMonoid β₂] {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ},
  IsAddFreimanHom n A B₁ f₁ → IsAddFreimanHom n A B₂ f₂ → IsAddFreimanHom n A (B₁ ×ˢ B₂) fun x => (f₁ x, f₂ x)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.nonempty_of_pos_dist : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, 0 < G.dist u v → Set.univ.Nonempty
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_1 : Inhabited (γ k)],
  (Std.ExtDHashMap.filterMap f m).get! k = ((m.get? k).bind (f k)).get!
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_add : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i) [inst_6 : DecidableEq ι] (i : ι) (u v : E i →L[𝕜] E' i),
  PiTensorProduct.mapL (Function.update f i (u + v)) =
    PiTensorProduct.mapL (Function.update f i u) + PiTensorProduct.mapL (Function.update f i v)
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBy_coe : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : Type v) [inst_1 : TopologicalSpace Y],
  ⇑(Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBy X Y) =
    ⇑Topology.WithGeneratedByTopology.equiv.symm
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_nsmul_subset : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddMonoid β] [inst_2 : FunLike F α β]
  [AddMonoidHomClass F α β] (f : F) (s : Set β) (n : ℕ), n • ⇑f ⁻¹' s ⊆ ⇑f ⁻¹' (n • s)
-- Lean.Hygiene
Lean.NameSanitizerState.mk.sizeOf_spec : ∀ (options : Lean.Options) (nameStem2Idx : Lean.NameMap ℕ) (userName2Sanitized : Lean.NameMap Lean.Name),
  sizeOf { options := options, nameStem2Idx := nameStem2Idx, userName2Sanitized := userName2Sanitized } =
    1 + sizeOf options + sizeOf nameStem2Idx + sizeOf userName2Sanitized
-- Mathlib.CategoryTheory.Monoidal.Functor.Types
/-- A lawful `Applicative` gives a category theory `LaxMonoidal` functor
between categories of types.  -/
CategoryTheory.instLaxMonoidalOfTypeFunctor : (F : Type u_1 → Type u_2) →
  [inst : Applicative F] → [inst_1 : LawfulApplicative F] → (CategoryTheory.ofTypeFunctor F).LaxMonoidal
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.continuous_toNNReal : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous ContinuousMap.toNNReal
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (f : NumberField.mixedEmbedding.mixedSpace K → ENNReal),
  ∫⁻ (x : NumberField.mixedEmbedding.polarSpace K) in (NumberField.mixedEmbedding.polarSpaceCoord K).target,
      (∏ w, ENNReal.ofReal (x.1 ↑w)) * f (↑(NumberField.mixedEmbedding.polarSpaceCoord K).symm x) =
    ∫⁻ (x : NumberField.mixedEmbedding.mixedSpace K), f x
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2 =>
      h_3 size k v l size_2 k_2 v_2 l_1 r h r_2) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_mul_complEDS₂ : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ),
  preNormEDS (b ^ 4) c d k * complEDS₂ b c d k = preNormEDS (b ^ 4) c d (2 * k) * if Even k then 1 else b
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- The pretopology on the category of schemes defined by covering families where the components
satisfy `P`.
 -/
AlgebraicGeometry.Scheme.pretopology : (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  [P.IsStableUnderBaseChange] → [P.IsMultiplicative] → CategoryTheory.Pretopology AlgebraicGeometry.Scheme
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- The root element of a W tree  -/
PFunctor.W.head : {P : PFunctor.{uA, uB}} → P.W → P.A
-- Mathlib.RingTheory.Perfectoid.Untilt
/-- The composition of the mod `p` map
with the untilt function equals taking the zeroth component of the perfection.
 -/
PreTilt.mk_untilt_eq_coeff_zero : ∀ {O : Type u_1} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) O] (x : PreTilt O p),
  (Ideal.Quotient.mk (Ideal.span {↑p})) (PreTilt.untilt x) = (PreTilt.coeff 0) x
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordMonoidWithZeroHom_eq_intValuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {x : R},
  x ∈ nonZeroDivisors R → (Ring.ordMonoidWithZeroHom R) x = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.toOption.match_1.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : String.Slice.SplitIterator pat s → Sort u_1) (currPos : s.Pos)
  (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) → motive (String.Slice.SplitIterator.operating currPos s_2))
  (h_2 : Unit → motive String.Slice.SplitIterator.atEnd),
  (match String.Slice.SplitIterator.operating currPos s_1 with
    | String.Slice.SplitIterator.operating currPos s => h_1 currPos s
    | String.Slice.SplitIterator.atEnd => h_2 ()) =
    h_1 currPos s_1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftId_hom_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapLeftId L R).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
_private.Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite.0.step4 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E),
  IsClosed ↑A →
    ∀ [A.CoFG],
      Disjoint (↑u).ker A →
        (Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔
          Topology.IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed ↑(↑(u.domRestrict A)).range)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.div : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Div Y] ⦃f g : X → Y⦄,
  IsLocallyConstant f → IsLocallyConstant g → IsLocallyConstant (f / g)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_univ : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞},
  ContMDiffOn I I' n f Set.univ ↔ ContMDiff I I' n f
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_empty : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E], Bornology.IsVonNBounded 𝕜 ∅
-- Mathlib.Data.W.Basic
WType.equivSigma_symm_apply : ∀ {α : Type u_1} (β : α → Type u_2) (a : (a : α) × (β a → WType β)), (WType.equivSigma β).symm a = WType.ofSigma a
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.structure : {α : Type u_1} →
  {M : α → Type u_2} →
    {u : Ultrafilter α} → {L : FirstOrder.Language} → [(a : α) → L.Structure (M a)] → L.Structure ((↑u).Product M)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Ioc : ∀ {n : ℕ} (i j : Fin n), Fin.rev ⁻¹' Set.Ioc i j = Set.Ico j.rev i.rev
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.bot_subgroupOf : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⊥.subgroupOf H = ⊥