mathlib-initiative/mathlib-types huggingface dataset:
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshState.mk.inj : ∀ {curr : Thunk ProofWidgets.Html} {idx : ℕ} {next : Task (Option Unit)} {curr_1 : Thunk ProofWidgets.Html} {idx_1 : ℕ}
  {next_1 : Task (Option Unit)},
  { curr := curr, idx := idx, next := next } = { curr := curr_1, idx := idx_1, next := next_1 } →
    curr = curr_1 ∧ idx = idx_1 ∧ next = next_1
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.IsStableUnderBaseChange.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
      CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
        ∀ {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i),
          (∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) →
            CategoryTheory.Presieve.ofArrows P p₁ ∈ J.coverings Y) →
    J.IsStableUnderBaseChange
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_congr_ae' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  (∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ioc a b → f x = g x) →
    (∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ioc b a → f x = g x) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.grothendieckTopology_monotone : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  P ≤ Q → AlgebraicGeometry.Scheme.grothendieckTopology P ≤ AlgebraicGeometry.Scheme.grothendieckTopology Q
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.add.go.match_1.eq_3 : ∀ (motive : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Sort u_1) (k₁ : ℕ) (m₁ : Nat.Internal.SOM.Mon)
  (p₁ : List (ℕ × Nat.Internal.SOM.Mon)) (k₂ : ℕ) (m₂ : Nat.Internal.SOM.Mon) (p₂ : List (ℕ × Nat.Internal.SOM.Mon))
  (h_1 : (p₁ : Nat.Internal.SOM.Poly) → motive p₁ []) (h_2 : (p₂ : Nat.Internal.SOM.Poly) → motive [] p₂)
  (h_3 :
    (k₁ : ℕ) →
      (m₁ : Nat.Internal.SOM.Mon) →
        (p₁ : List (ℕ × Nat.Internal.SOM.Mon)) →
          (k₂ : ℕ) →
            (m₂ : Nat.Internal.SOM.Mon) →
              (p₂ : List (ℕ × Nat.Internal.SOM.Mon)) → motive ((k₁, m₁) :: p₁) ((k₂, m₂) :: p₂)),
  (match (k₁, m₁) :: p₁, (k₂, m₂) :: p₂ with
    | p₁, [] => h_1 p₁
    | [], p₂ => h_2 p₂
    | (k₁, m₁) :: p₁, (k₂, m₂) :: p₂ => h_3 k₁ m₁ p₁ k₂ m₂ p₂) =
    h_3 k₁ m₁ p₁ k₂ m₂ p₂
-- Mathlib.Topology.Sheaves.Sheaf
/-- Transfer the sheaf condition across an isomorphism of presheaves.
 -/
TopCat.Presheaf.isSheaf_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {F G : TopCat.Presheaf C X} (α : F ≅ G),
  F.IsSheaf → G.IsSheaf
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.explore.eq_2 : ∀ {α : Type u} {β : α → Type v} {γ : Type w} [inst : Ord α] (k : α → Ordering) (init : γ)
  (inner : γ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → γ) (size : ℕ) (k' : α) (v : β k')
  (l_2 r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.explore k init inner (Std.DTreeMap.Internal.Impl.inner size k' v l_2 r) =
    match h : k k' with
    | Ordering.lt =>
      Std.DTreeMap.Internal.Impl.explore k
        (inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' h v r.toListModel)) inner l_2
    | Ordering.eq =>
      inner init
        (Std.DTreeMap.Internal.Impl.ExplorationStep.eq l_2.toListModel (Std.DTreeMap.Internal.Cell.ofEq k' v ⋯)
          r.toListModel)
    | Ordering.gt =>
      Std.DTreeMap.Internal.Impl.explore k
        (inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.gt l_2.toListModel k' h v)) inner r
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.factorPowSucc_fontaineThetaModPPow_eq : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : WittVector p (PreTilt R p)),
  (Ideal.Quotient.factorPowSucc (Ideal.span {↑p}) (n + 1)) ((WittVector.fontaineThetaModPPow R p (n + 1)) x) =
    (WittVector.fontaineThetaModPPow R p n) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).get? k' = some (cast ⋯ v)
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_set_zero : ∀ {α : Type u_1} [inst : Zero α], Small.{u, u_1} ↑0
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instIsStrictlyGEI : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K : CochainComplex C ℤ} (n : ℤ) [K.IsStrictlyGE n],
  (CochainComplex.cm5b.I K).IsStrictlyGE n
-- Mathlib.Data.List.Defs
List.permutations'Aux.eq_1 : ∀ {α : Type u_1} (t : α), List.permutations'Aux t [] = [[t]]
-- Mathlib.Algebra.Group.AddChar
/-- Additive characters `A → M` are the same thing as monoid homomorphisms from `Multiplicative A`
to `M`.  -/
AddChar.toMonoidHomEquiv : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → AddChar A M ≃ (Multiplicative A →* M)
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.mk.injEq : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A} (F : CategoryTheory.Functor A C)
  (π : F.comp ι ⟶ CategoryTheory.Functor.id A)
  (epi_π_app :
    autoParam (∀ (X : A), CategoryTheory.Epi (π.app X)) CategoryTheory.Abelian.LeftResolution.epi_π_app._autoParam)
  (F_1 : CategoryTheory.Functor A C) (π_1 : F_1.comp ι ⟶ CategoryTheory.Functor.id A)
  (epi_π_app_1 :
    autoParam (∀ (X : A), CategoryTheory.Epi (π_1.app X)) CategoryTheory.Abelian.LeftResolution.epi_π_app._autoParam),
  ({ F := F, π := π, epi_π_app := epi_π_app } = { F := F_1, π := π_1, epi_π_app := epi_π_app_1 }) = (F = F_1 ∧ π ≍ π_1)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfRoot_symm : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0),
  (pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.rotate_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.rotate.obj₁ = T.obj₂
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.right_pos : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < q
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Transitivity of multiplication-preserving order isomorphisms  -/
OrderMonoidIso.trans : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            [inst_3 : Mul α] → [inst_4 : Mul β] → [inst_5 : Mul γ] → (α ≃*o β) → (β ≃*o γ) → α ≃*o γ
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization.iso.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A),
  CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a =
    CategoryTheory.Localization.liftNatIso L W (L.comp ((CategoryTheory.shiftFunctor D a).comp F'))
      (L.comp (F'.comp (CategoryTheory.shiftFunctor E a))) ((CategoryTheory.shiftFunctor D a).comp F')
      (F'.comp (CategoryTheory.shiftFunctor E a))
      ((L.associator (CategoryTheory.shiftFunctor D a) F').symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.commShiftIso L a).symm F' ≪≫
          (CategoryTheory.shiftFunctor C a).associator L F' ≪≫
            (CategoryTheory.shiftFunctor C a).isoWhiskerLeft (CategoryTheory.Localization.Lifting.iso L W F F') ≪≫
              CategoryTheory.Functor.commShiftIso F a ≪≫
                CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Localization.Lifting.iso L W F F').symm
                    (CategoryTheory.shiftFunctor E a) ≪≫
                  L.associator F' (CategoryTheory.shiftFunctor E a))
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.select.inj : ∀ {α : Type} {finished finished_1 : Std.Async.Waiter (Option α)},
  Std.CloseableChannel.Consumer.select✝ finished = Std.CloseableChannel.Consumer.select✝ finished_1 →
    finished = finished_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
cmp_div_one' : ∀ {α : Type u} [inst : Group α] [inst_1 : LinearOrder α] [MulRightMono α] (a b : α), cmp (a / b) 1 = cmp a b
-- Mathlib.Topology.Inseparable
subtype_specializes_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X → Prop} (x y : Subtype p), x ⤳ y ↔ ↑x ⤳ ↑y
-- Init.Data.List.Lemmas
List.eq_append_cons_of_mem : ∀ {α : Type u_1} {a : α} {xs : List α}, a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as
-- Init.Prelude
/-- Types that can be hashed into a `UInt64`.  -/
Hashable : Sort u → Sort (max 1 u)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.precomp_δ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left), (F.precomp f).δ₀ = F
-- Init.Data.Hashable
instHashableProd : {α : Type u_1} → {β : Type u_2} → [Hashable α] → [Hashable β] → Hashable (α × β)
-- Mathlib.Algebra.Opposites
MulOpposite.unop_surjective : ∀ {α : Type u_1}, Function.Surjective MulOpposite.unop
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Build a list of elements in ascending order from the tree.

```
toList {1, 2, 4} = [1, 2, 4]
toList {2, 1, 1, 4} = [1, 2, 4]
```  -/
Ordnode.toList : {α : Type u_1} → Ordnode α → List α
-- Mathlib.Algebra.Field.IsField
/-- Transferring from `Field` to `IsField`.  -/
Field.toIsField : ∀ (R : Type u) [inst : Field R], IsField R
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C}
  [self : CategoryTheory.HomRel.IsStableUnderPostcomp r] {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z),
  r f f' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g)
-- Mathlib.Data.ENNReal.Basic
ENNReal.recTopCoe_ofNNReal : ∀ {C : ENNReal → Sort u_2} (top : C ⊤) (coe : (x : NNReal) → C ↑x) (x : NNReal), ENNReal.recTopCoe top coe ↑x = coe x
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  (i : 𝒰.I₀), d.relativeGluingData.natTrans.app i = (d.cocone i).pt.hom
-- Mathlib.Topology.Algebra.UniformConvergence
instAddMonoidUniformFun : {α : Type u_1} → {β : Type u_2} → [AddMonoid β] → AddMonoid (UniformFun α β)
-- Mathlib.Data.Finset.Insert
Finset.mem_of_mem_insert_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ insert a s → b ≠ a → b ∈ s
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Line derivative of `f` at the point `x` in the direction `v` within the set `s`, if it exists.
Zero otherwise.

If the line derivative exists (i.e., `∃ f', HasLineDerivWithinAt 𝕜 f f' s x v`), then
`f (x + t v) = f x + t lineDerivWithin 𝕜 f s x v + o (t)` when `t` tends to `0` and `x + t v ∈ s`.
 -/
lineDerivWithin : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] → {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → Set E → E → E → F
-- Lean.Meta.Basic
Lean.Meta.PostponedEntry.rhs : Lean.Meta.PostponedEntry → Lean.Level
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.isPos_iff' : ∀ {ι : 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} (b : P.Base)
  [inst_5 : CharZero R] {i : ι}, b.IsPos i ↔ 0 ≤ b.height i
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.uncountable : Uncountable Cardinal.{u}
-- Mathlib.Data.List.Sort
List.map_orderedInsert : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : DecidableRel r] [inst_1 : DecidableRel s]
  (f : α → β) (l : List α) (x : α),
  (∀ a ∈ l, r a x ↔ s (f a) (f x)) →
    (∀ a ∈ l, r x a ↔ s (f x) (f a)) → List.map f (List.orderedInsert r x l) = List.orderedInsert s (f x) (List.map f l)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- `G` is cover-lifting w.r.t. the induced topology.  -/
CategoryTheory.Functor.instIsCocontinuousRestrictedTopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K], G.IsCocontinuous (G.restrictedTopology K) K
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsDense] (X : C),
  CategoryTheory.CategoryStruct.comp ((F.leftKanExtensionUnit F).app X)
      ((CategoryTheory.Functor.IsDense.leftKanExtensionIso F).hom.app (F.obj X)) =
    F.rightUnitor.inv.app X
-- Mathlib.Algebra.Order.Field.Basic
inv_le_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a⁻¹ ≤ b ↔ b⁻¹ ≤ a)
-- Init.MetaTypes
Lean.Meta.Simp.instInhabitedConfig : Inhabited Lean.Meta.Simp.Config
-- Mathlib.Algebra.Group.Even
even_op_iff : ∀ {α : Type u_2} [inst : Add α] {a : α}, Even (AddOpposite.op a) ↔ Even a
-- Mathlib.Topology.Connected.Basic
connectedComponentIn.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] (F : Set α) (x : α),
  connectedComponentIn F x = if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_smul_iff : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} {𝕜 : Type u_9} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  {f : X → E} (c : 𝕜), MeasureTheory.LocallyIntegrableOn (c • f) s μ ↔ c = 0 ∨ MeasureTheory.LocallyIntegrableOn f s μ
-- Mathlib.Tactic.FieldSimp
/-- Given `e₁` and `e₂`, cancel positive factors to construct a new inequality which is logically
equivalent to `e₁ ≤ e₂`.  -/
Mathlib.Tactic.FieldSimp.reduceLeQ : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      (iM : Q(CommGroupWithZero «$M»)) →
        (iM' : Q(PartialOrder «$M»)) →
          Q(PosMulStrictMono «$M») →
            Q(PosMulReflectLE «$M») →
              Q(ZeroLEOneClass «$M») →
                (e₁ e₂ : Q(«$M»)) →
                  Mathlib.Tactic.AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» ≤ «$e₂») = («$f₁» ≤ «$f₂»)))
-- Init.Data.Ord.Basic
Ordering.isLE_eq : Ordering.eq.isLE = true
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
/-- Simplifies `Nat.digitChar n = c` to `False` when `c` is a concrete character
not in the range of `digitChar` (i.e., not one of `'0'`-`'9'`, `'a'`-`'f'`, `'*'`).  -/
Char.Nat.reduceDigitCharEq : Lean.Meta.Simp.Simproc
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedContInfo.default : Lean.Elab.Do.ContInfo
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.iUnion_skeletonLT_eq_complex`. -/
Topology.CWComplex.iUnion_skeletonLT_eq_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ⋃ n, ↑(Topology.RelCWComplex.skeletonLT C ↑n) = C
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.eq_top_iff_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F), G = ⊤ ↔ CategoryTheory.IsIso G.ι
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.starEquivCostar_symm_apply : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasInvolutiveReverse U] {u v : U} (e : u ⟶ v),
  (Quiver.starEquivCostar v).symm (Quiver.Costar.mk e) = Quiver.Star.mk (Quiver.reverse e)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_ofENat : ∀ (n : ℕ∞), (↑n).toENatAux = n
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.hasFPowerSeriesWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E}, HasFPowerSeriesAt f p x → HasFPowerSeriesWithinAt f p s x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.not_nil_of_tail_not_nil : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, ¬p.tail.Nil → ¬p.Nil
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.mk : {D : Type u_5} →
  [inst : CategoryTheory.Category.{v_5, u_5} D] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : CategoryTheory.HasShift D M] →
          (toTwistShiftData :
              CategoryTheory.TwistShiftData
                (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M)) (M × M)) →
            autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (0, m₁) (0, m₂) = 1)
                CategoryTheory.CommShift₂Setup.z_zero₁._autoParam →
              autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (m₁, 0) (m₂, 0) = 1)
                  CategoryTheory.CommShift₂Setup.z_zero₂._autoParam →
                (ε : M → M → (CategoryTheory.CatCenter D)ˣ) →
                  autoParam
                      (∀ (m n : M), ε m n = (toTwistShiftData.z (0, n) (m, 0))⁻¹ * toTwistShiftData.z (m, 0) (0, n))
                      CategoryTheory.CommShift₂Setup.hε._autoParam →
                    CategoryTheory.CommShift₂Setup D M
-- Init.Data.Order.PackageFactories
/-- This structure contains all the data needed to create a `PreorderPackage α` instance. Its fields
are automatically provided if possible. For the detailed rules how the fields are inferred, see
`PreorderPackage.ofLE`.
 -/
Std.Packages.PreorderOfLEArgs : Type u → Type u
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_1.eq_2 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁] {it₁ : Std.IterM m β₁}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β₁) (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.skip it₁', hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_2 it₁' hp
-- Init.Data.UInt.Basic
/-- Converts word-sized unsigned integers to 32-bit unsigned integers. Wraps around on overflow, which
might occur on 64-bit architectures.

This function is overridden at runtime with an efficient implementation.
 -/
USize.toUInt32 : USize → UInt32
-- Init.Core
/-- If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). -/
Iff : Prop → Prop → Prop
-- Mathlib.ModelTheory.Syntax
/-- Turns all the in-scope bound variables into free variables.  -/
FirstOrder.Language.BoundedFormula.toFormula : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.Formula (α ⊕ Fin n)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_top : ∀ {α : Type u_1} (s : Set α), s.Pairwise ⊤
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.IsEmbedding.inr : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Zero R],
  Topology.IsEmbedding TrivSqZeroExt.inr
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.prodProdProdComm_symm : ∀ (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W],
  (Homeomorph.prodProdProdComm X Y W Z).symm = Homeomorph.prodProdProdComm X W Y Z
-- Mathlib.Algebra.Divisibility.Basic
IsLeftRegular.dvd_cancel_left : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, IsLeftRegular a → (a * b ∣ a * c ↔ b ∣ c)
-- Init.Meta.Defs
/-- Creates syntax representing a Lean term application, but avoids degenerate empty applications.
 -/
Lean.Syntax.mkApp : Lean.Term → Lean.TSyntaxArray `term → Lean.Term
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toListRev_iter : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β}, m.iter.toListRev = m.toList.reverse
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeForwardRule.injEq : ∀ (r₁ : Aesop.ForwardRule) (r₂ : Aesop.SafeRule) (r₁_1 : Aesop.ForwardRule) (r₂_1 : Aesop.SafeRule),
  (Aesop.BaseRuleSetMember.safeForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.safeForwardRule r₁_1 r₂_1) =
    (r₁ = r₁_1 ∧ r₂ = r₂_1)
-- Init.Data.Array.Count
Array.countP_push : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α},
  Array.countP p (xs.push a) = Array.countP p xs + if p a = true then 1 else 0
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.diagonal_fin_three : ∀ {α : Type u} [inst : Zero α] (d : Fin 3 → α), Matrix.diagonal d = !![d 0, 0, 0; 0, d 1, 0; 0, 0, d 2]
-- Mathlib.Analysis.Complex.AbsMax
Complex.norm_max_aux₁ : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] [CompleteSpace F] {f : ℂ → F} {z w : ℂ},
  DiffContOnCl ℂ f (Metric.ball z (dist w z)) → IsMaxOn (norm ∘ f) (Metric.closedBall z (dist w z)) z → ‖f w‖ = ‖f z‖
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instMax : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] → [inst_1 : Bot α] → [inst_2 : SemilatticeSup β] → [inst_3 : OrderBot β] → Max (SupBotHom α β)