mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.del.match_1.eq_1 : ∀ (motive : RBTree.RBColor → Sort u_1) (h_1 : Unit → motive RBTree.RBColor.black)
  (h_2 : Unit → motive RBTree.RBColor.red),
  (match RBTree.RBColor.black with
    | RBTree.RBColor.black => h_1 ()
    | RBTree.RBColor.red => h_2 ()) =
    h_1 ()
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.Transcendental.of_ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) [H : Algebra.Transcendental S B],
  Function.Injective ⇑f →
    Function.Surjective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → Algebra.Transcendental R A
-- Mathlib.Data.Nat.Log
Nat.log_one_right : ∀ (b : ℕ), Nat.log b 1 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k}
  [inst_2 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → ⟨k, v⟩ ∈ l → (t.insertMany l).get! k' = cast ⋯ v
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.namespaceId.sizeOf_spec : ∀ (stx : Lean.Syntax), sizeOf (Lean.Elab.CompletionInfo.namespaceId stx) = 1 + sizeOf stx
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.toEssImage_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), (F.toEssImage.obj X).obj = F.obj X
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.J.eq_1 : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R],
  Matrix.J l R = Matrix.fromBlocks 0 (-1) 1 0
-- Aesop.Frontend.Extension
Aesop.Frontend.eraseGlobalRules : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [MonadLiftT IO m] →
        [MonadLiftT Lean.CoreM m] → [Lean.MonadEnv m] → Aesop.RuleSetNameFilter → Aesop.RuleFilter → Bool → m Unit
-- Init.Data.BitVec.Lemmas
BitVec.cpop.eq_1 : ∀ {w : ℕ} (x : BitVec w), x.cpop = BitVec.ofNat w (x.cpopNatRec w 0)
-- Init.Data.SInt.Lemmas
Int8.lt_or_lt_of_ne : ∀ {a b : Int8}, a ≠ b → a < b ∨ b < a
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.support_gaussianPDF : ∀ {μ : ℝ} {v : NNReal}, v ≠ 0 → Function.support (ProbabilityTheory.gaussianPDF μ v) = Set.univ
-- Mathlib.Data.Finset.Image
Finset.image_val : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Finset α),
  (Finset.image f s).val = (Multiset.map f s.val).dedup
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulMonC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulMonC k m p c) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denote ctx p
-- Init.Data.String.Iterate
String.Slice.ByteIterator.instFiniteUInt8 : ∀ {m : Type → Type u_1} [inst : Pure m], Std.Iterators.Finite String.Slice.ByteIterator m
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.isRightCancelAdd : ∀ {α : Type u} [inst : Mul α] [IsRightCancelMul α], IsRightCancelAdd (Additive α)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.weight : (σ : Type u_1) → (R : Type u_2) → [inst : CommRing R] → ℕ → Finset σ × σ → MvPolynomial σ R
-- Mathlib.Data.Finset.Defs
Finset.forall_mem_not_eq' : ∀ {α : Type u_1} {s : Finset α} {a : α}, (∀ b ∈ s, ¬b = a) ↔ a ∉ s
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.isStableUnderCobaseChangeAgainst_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.IsStableUnderCobaseChangeAgainst ⊤ ↔ P.IsStableUnderCobaseChange
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.apply_zero : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P) (x : X), F (0, x) = f₀ x
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.toOpenPartialHomeomorph_mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  n ≠ 0 → OpenPartialHomeomorph.MDifferentiable I J h.toHomeomorph.toOpenPartialHomeomorph
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} [inst : UniformSpace X],
  IsCompact F → UniformContinuous T → U ∈ uniformity X → ∀ (n : ℕ), ∃ s, Dynamics.IsDynCoverOf T F U n ↑s
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.rank_toPSet : ∀ (o : Ordinal.{u_1}), o.toPSet.rank = o
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.comp_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7}
  [inst_9 : AddCommGroup W₂] [inst_10 : Module R W₂] [inst_11 : TopologicalSpace Q₂] [inst_12 : AddTorsor W₂ Q₂]
  (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q) (p : P), (f.comp g) p = f (g p)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sin_mul_sum_cos : ∀ (n : ℕ) (a b : ℝ),
  Real.sin (a / 2) * ∑ i ∈ Finset.range n, Real.cos (a * ↑i + b) =
    Real.sin (↑n * a / 2) * Real.cos ((↑n - 1) * a / 2 + b)
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.ack.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) → ((n : ℕ) → motive 0 n) → ((m : ℕ) → motive m.succ 0) → ((m n : ℕ) → motive m.succ n.succ) → motive x x_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
neg_mem_iff : ∀ {S : Type u_3} {G : Type u_4} [inst : InvolutiveNeg G] {x : SetLike S G} [NegMemClass S G] {H : S} {x_1 : G},
  -x_1 ∈ H ↔ x_1 ∈ H
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.isoMk_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src)
  (e₂ : X.tgt ≅ Y.tgt)
  (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel),
  (CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.f = e₁.inv
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.ne_of_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] {a b : α}, a < b → a ≠ b
-- Init.Data.Int.DivMod.Lemmas
Int.mul_dvd_mul_left : ∀ {b c : ℤ} (a : ℤ), b ∣ c → a * b ∣ a * c
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The real exponential function tends to `+∞` at `+∞`.  -/
Real.tendsto_exp_atTop : Filter.Tendsto Real.exp Filter.atTop Filter.atTop
-- Mathlib.Topology.Bases
/-- **Alias** of `TopologicalSpace.SeparableSpace.of_denseRange`.

---

If `f` has a dense range and its domain is countable, then its codomain is a separable space.
See also `DenseRange.separableSpace`.  -/
DenseRange.separableSpace' : ∀ {α : Type u} [t : TopologicalSpace α] {ι : Type u_2} [Countable ι] (u : ι → α),
  DenseRange u → TopologicalSpace.SeparableSpace α
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumcenter_restrict : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), ↑(s.restrict S hS).circumcenter = s.circumcenter
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_cons' : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s)
  (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun Commute f)),
  (Finset.cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- When `K` and `L` are both strictly `≥ n + 1`, this is the factorization `f ≫ 𝟙 L = f`
of a monomorphism `f : K ⟶ L` as a monomorphism that is a quasi-isomorphism in degrees `≤ n`
followed by a degreewise epimorphism with an injective kernel.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.zero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [CategoryTheory.Mono f] →
            (n : ℤ) →
              [K.IsStrictlyGE (n + 1)] →
                [L.IsStrictlyGE (n + 1)] →
                  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f (n + ↑0)
-- Mathlib.RingTheory.Coalgebra.MulOpposite
MulOpposite.comul_def : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A],
  CoalgebraStruct.comul =
    TensorProduct.map ↑(MulOpposite.opLinearEquiv R) ↑(MulOpposite.opLinearEquiv R) ∘ₗ
      CoalgebraStruct.comul ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm
-- Mathlib.Order.Atoms
Set.OrdConnected.isStronglyAtomic : ∀ {α : Type u_4} [inst : Preorder α] [IsStronglyAtomic α] {s : Set α}, s.OrdConnected → IsStronglyAtomic ↑s
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AContext.mk.inj : ∀ {fvars : Array Lean.Expr} {propToFVar : Lean.ExprMap Lean.Expr} {depth : ℕ} {initLCtx : Lean.LocalContext}
  {config : Batteries.Tactic.GeneralizeProofs.Config} {fvars_1 : Array Lean.Expr}
  {propToFVar_1 : Lean.ExprMap Lean.Expr} {depth_1 : ℕ} {initLCtx_1 : Lean.LocalContext}
  {config_1 : Batteries.Tactic.GeneralizeProofs.Config},
  { fvars := fvars, propToFVar := propToFVar, depth := depth, initLCtx := initLCtx, config := config } =
      { fvars := fvars_1, propToFVar := propToFVar_1, depth := depth_1, initLCtx := initLCtx_1, config := config_1 } →
    fvars = fvars_1 ∧ propToFVar = propToFVar_1 ∧ depth = depth_1 ∧ initLCtx = initLCtx_1 ∧ config = config_1
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.elabTryConfig : Lean.Syntax → optParam Lean.Try.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Try.Config
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α}, (m.insertManyIfNewUnit l)[k]? = if k ∈ m ∨ l.contains k = true then some () else none
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The additive homeomorphism from a topological ring to itself,
induced by right multiplication by a unit.  -/
ContinuousAddEquiv.mulRight : {R : Type u_1} → [inst : TopologicalSpace R] → [inst_1 : Semiring R] → [IsTopologicalSemiring R] → Rˣ → R ≃ₜ+ R
-- Lean.Elab.Binders
/-- Interprets a `Parser.Term.letConfig`.
 -/
Lean.Elab.Term.mkLetConfig : Lean.Syntax → Lean.Elab.Term.LetConfig → Lean.Elab.TermElabM Lean.Elab.Term.LetConfig
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.iSup : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : ConditionallyCompleteLattice M] {ι : Sort u_3} [Nonempty ι]
  [Finite ι] {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteSupport (f i)) → Function.HasFiniteSupport fun a => ⨆ i, f i a
-- Mathlib.Topology.Instances.Matrix
Continuous.dotProduct : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Fintype n] [inst_3 : Mul R] [inst_4 : AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R]
  {A B : X → n → R}, Continuous A → Continuous B → Continuous fun x => A x ⬝ᵥ B x
-- Std.Time.DateTime.Timestamp
Std.Time.instDecidableEqTimestamp : DecidableEq Std.Time.Timestamp
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.IsLocallyFree.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R},
  (∃ q, q.IsLocallyFreeData) → M.IsLocallyFree
-- Lean.DocString.Markdown
/-- Splits off the leading run of whitespace from an inline tree, returning the whitespace as a plain
string and the remainder as a new inline. This allows emphasis to be applied to strings that start
or end with whitespace, taking the flanking rules of Markdown into account.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.trimLeft : {i : Type u_1} → Lean.Doc.Inline i → String × Lean.Doc.Inline i
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrict_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) (f : M →* N),
  MonoidHom.mker (f.domRestrict S) = Submonoid.comap S.subtype (MonoidHom.mker f)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.mk.inj : ∀ {toAddGrp : AddGrpCat} {isFinite : Finite ↑toAddGrp} {toAddGrp_1 : AddGrpCat} {isFinite_1 : Finite ↑toAddGrp_1},
  { toAddGrp := toAddGrp, isFinite := isFinite } = { toAddGrp := toAddGrp_1, isFinite := isFinite_1 } →
    toAddGrp = toAddGrp_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negDblY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objMk_bijective : ∀ {n : SimplexCategory} {m : SimplexCategoryᵒᵖ}, Function.Bijective SSet.stdSimplex.objMk
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_id_of_mono : ∀ {x : SimplexCategory} (i : x ⟶ x) [CategoryTheory.Mono i], i = CategoryTheory.CategoryStruct.id x
-- Mathlib.RepresentationTheory.Basic
Representation.subrepresentation_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (W : Submodule k V)
  (le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W) (g : G), (ρ.subrepresentation W le_comap) g = (ρ g).restrict ⋯
-- Batteries.Lean.AttributeExtra
Lean.TagAttributeExtra.mk : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet → Lean.NameHashSet → Lean.TagAttributeExtra
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
MulEquiv.isCyclic : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] (e : G ≃* G'), IsCyclic G ↔ IsCyclic G'
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.discreteTopology_of_forall_map_eq_one : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  (∀ (x : R), x ≠ 0 → Valued.v x = 1) → DiscreteTopology R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_filter_key_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter (fun a x => f a) t ⋯).impl = true ↔
    ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = true
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.IntInterval.lo?.match_1.eq_2 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (lo : ℤ) (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.ci lo with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_2 lo
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_congr : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f g : α → ε}, f =ᵐ[μ] g → (MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocDiv hp a (b - ↑m * p) = toIocDiv hp a b - ↑m
-- Mathlib.Order.Filter.Extr
IsMinFilter.isExtr : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsExtrFilter f l a
-- Mathlib.Order.InitialSeg
PrincipalSeg.transRelIso_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f : PrincipalSeg r s) (g : s ≃r t), (f.transRelIso g).top = g f.top
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.prodPUnit_apply : ∀ (α : Type u) [inst : UniformSpace α], ⇑(UniformEquiv.prodPUnit α) = fun p => p.1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getElem!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, t₁.Equiv t₂ → t₁[k]! = t₂[k]!
-- Mathlib.Order.Filter.Basic
Filter.eq_iInf_of_mem_iff_exists_mem : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} {l : Filter α}, (∀ {s : Set α}, s ∈ l ↔ ∃ i, s ∈ f i) → l = iInf f
-- Batteries.Data.ByteSlice
/-- Folds a monadic function over a `ByteSubarray` from left to right.  -/
ByteSlice.foldlM : {m : Type u_1 → Type u_2} → {β : Type u_1} → [Monad m] → ByteSlice → (β → UInt8 → m β) → β → m β
-- Mathlib.Topology.Category.Profinite.Product
/-- The projection maps in the limit cone `indexCone`.  -/
Profinite.IndexFunctor.π_app : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (C : Set ((i : ι) → X i)) → (J : ι → Prop) → C(↑C, ↑(Profinite.IndexFunctor.obj C J))
-- Std.Data.ExtDTreeMap.Basic
/-- Returns `true` if the tree map contains no mappings.  -/
Std.ExtDTreeMap.isEmpty : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.ExtDTreeMap α β cmp → Bool
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
/-- The multiplication on a finite-dimensional inner product space with a coalgebra structure
given by `x * y = (adjoint comul) (x ⊗ₜ y)`.

See note [reducible non-instances].  -/
InnerProductSpace.mulOfCoalgebra : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → [Coalgebra 𝕜 E] → Mul E
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_inv_eq_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z • f).inv h =
    CategoryTheory.CategoryStruct.comp f.inv (CategoryTheory.CategoryStruct.comp ((↑z⁻¹).app X) h)
-- Lean.Elab.App
Lean.Elab.Term.instReprElabElimInfo.repr : Lean.Elab.Term.ElabElimInfo → ℕ → Std.Format
-- Lean.Setup
Lean.instBEqImport : BEq Lean.Import
-- Init.Data.UInt.Lemmas
UInt16.neg_one_eq : -1 = 65535
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.const_subinterval_eq : ∀ {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin (l + 1)),
  CategoryTheory.CategoryStruct.comp ({ len := 0 }.const { len := l } i) (SimplexCategory.subinterval j l hjl) =
    { len := 0 }.const { len := n } ⟨j + ↑i, ⋯⟩
-- Mathlib.Order.Fin.Basic
Fin.castOrderIso.congr_simp : ∀ {m n : ℕ} (eq : n = m), Fin.castOrderIso eq = Fin.castOrderIso eq
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingProd_cons_cons : ∀ {G : Type u_7} [inst : DivInvMonoid G] (a b : G) (l : List G),
  (a :: b :: l).alternatingProd = a / b * l.alternatingProd
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.String.Slice.isNat_iff' : ∀ {s : String.Slice},
  s.isNat = true ↔
    s.copy.toList ≠ [] ∧
      (∀ c ∈ s.copy.toList, c.isDigit = true ∨ c = '_') ∧ NoRepetition✝ '_' ('_' :: s.copy.toList ++ ['_'])
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Assembles the full key matcher from the trie. Makes use of `item` in the current macro scope.
 -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.defEvalConfigItem.assemble : Lean.Ident → Lean.Elab.ConfigEval.HandlerTrie✝ → Lean.Term → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Data.Complex.Basic
Complex.ofReal_sub : ∀ (r s : ℝ), ↑(r - s) = ↑r - ↑s
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM : {m : Type → Type u_1} → [MonadLiftT m Lean.Elab.Command.CommandElabM] → ProofWidgets.HtmlEval (m ProofWidgets.Html)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCone.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cone (K.comp F)} [inst_3 : SizeOf C] [inst_4 : SizeOf D]
  [inst_5 : SizeOf J] (liftedCone : CategoryTheory.Limits.Cone K) (validLift : F.mapCone liftedCone ≅ c),
  sizeOf { liftedCone := liftedCone, validLift := validLift } = 1 + sizeOf liftedCone + sizeOf validLift
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isRamified_iff_card_stabilizer_eq_two : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  NumberField.InfinitePlace.IsRamified k w ↔ Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = 2