mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.unitOfList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {hd : α} {tl : List α},
  Std.ExtDTreeMap.Const.unitOfList (hd :: tl) cmp = Std.ExtDTreeMap.Const.insertManyIfNewUnit (∅.insertIfNew hd ()) tl
-- Mathlib.GroupTheory.Exponent
/-- If two commuting elements `x` and `y` of an additive monoid have order `n` and
`m`, there is an element of order `lcm n m`. The result actually gives an explicit (computable)
element, written as the sum of a multiple of `x` and a multiple of `y`. See also the result below
if you don't need the explicit formula.  -/
AddCommute.addOrderOf_add_nsmul_eq_lcm : ∀ {G : Type u} [inst : AddMonoid G] {x y : G},
  AddCommute x y →
    addOrderOf x ≠ 0 →
      addOrderOf y ≠ 0 →
        addOrderOf
            ((addOrderOf x / (addOrderOf x).factorizationLCMLeft (addOrderOf y)) • x +
              (addOrderOf y / (addOrderOf x).factorizationLCMRight (addOrderOf y)) • y) =
          (addOrderOf x).lcm (addOrderOf y)
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.yonedaPresheaf_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w')
  [inst_1 : TopologicalSpace Y] {X Y_1 : Cᵒᵖ} (f : X ⟶ Y_1),
  (ContinuousMap.yonedaPresheaf F Y).map f = TypeCat.ofHom fun g => g.comp (TopCat.Hom.hom (F.map f.unop))
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- `K∞` is notation for `NumberField.InfiniteAdeleRing K`.  -/
NumberField.AdeleRing.«term_∞» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_mapAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S ≃ₐ[R] T) (p : Polynomial S) (q : Polynomial T)
  (h : Associated (Polynomial.map (↑f) p) q), ⇑(AdjoinRoot.mapAlgEquiv f p q h) = ⇑(AdjoinRoot.map (↑f) p q ⋯)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_single : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β₁ i)]
  [inst_2 : (i : ι) → Zero (β₂ i)] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {i : ι} {b : β₁ i},
  (DFinsupp.mapRange f hf fun₀ | i => b) = fun₀ | i => f i b
-- Init.Data.UInt.Bitwise
USize.toUInt8_xor : ∀ (a b : USize), (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
-- Mathlib.Topology.AlexandrovDiscrete
nhdsKer_subset_iff : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α},
  nhdsKer s ⊆ t ↔ ∃ U, IsOpen U ∧ s ⊆ U ∧ U ⊆ t
-- Init.Data.String.Basic
String.replaceEnd : (s : String) → s.Pos → String.Slice
-- Std.Time.Format.Modifier
Std.Time.instReprModifier.repr : Std.Time.Modifier → ℕ → Std.Format
-- Mathlib.Algebra.Group.Conj
isConj_comm : ∀ {α : Type u} [inst : Monoid α] {g h : α}, IsConj g h ↔ IsConj h g
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.primeFactorsPiBij : (d n : ℕ) → (f : (a : ℕ) → a ∈ n.primeFactors → Fin d) → (f ∈ n.primeFactors.pi fun x => Finset.univ) → Fin d → ℕ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, a ∉ ∅
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weightOfEPs.eq_1 : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : V → V → R) {i j : V},
  Quiver.Path.weightOfEPs w = Quiver.Path.weight fun {i j} x => w i j
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- A cone is a limit cone iff it is terminal.  -/
CategoryTheory.Limits.Cone.isLimitEquivIsTerminal : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) → CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsTerminal c
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.pi_iff : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_6} {M : ι → Type u_7} [Finite ι]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)],
  Module.Finite R ((i : ι) → M i) ↔ ∀ (i : ι), Module.Finite R (M i)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_singleton : ∀ {α : Type u_1} (a : α) (r : α → α → Prop), {a}.Pairwise r
-- Mathlib.RingTheory.HahnSeries.Summable
/-- The summable family made of a constant Hahn series.  -/
HahnSeries.SummableFamily.const : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : PartialOrder Γ] →
      [inst_1 : AddCommMonoid R] → (ι : Type u_7) → [Finite ι] → HahnSeries Γ R → HahnSeries.SummableFamily Γ R ι
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- Any `ℤ`-basis of `L` is also a `K`-basis of `E`.  -/
Module.Basis.ofZLatticeBasis : (K : Type u_1) →
  [inst : NormedField K] →
    [inst_1 : LinearOrder K] →
      [IsStrictOrderedRing K] →
        [HasSolidNorm K] →
          [FloorRing K] →
            {E : Type u_2} →
              [inst_5 : NormedAddCommGroup E] →
                [inst_6 : NormedSpace K E] →
                  [FiniteDimensional K E] →
                    [ProperSpace E] →
                      (L : Submodule ℤ E) →
                        [inst_9 : DiscreteTopology ↥L] →
                          {ι : Type u_3} → [hs : IsZLattice K L] → Module.Basis ι ℤ ↥L → Module.Basis ι K E
-- Lean.Elab.PreDefinition.WF.Preprocess
/-- `f (wfParam x) ==> wfParam (f x)` if `f` is a projection  -/
Lean.Elab.WF.paramProj : Lean.Meta.Simp.DSimproc
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get? (m₁ \ m₂) k = none
-- Init.Data.UInt.Lemmas
UInt32.lt_or_le : ∀ (a b : UInt32), a < b ∨ b ≤ a
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafBotEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A],
  (CategoryTheory.sheafBotEquivalence A).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Sheaf ⊥ A))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTGEHSubIntOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (X : C) (a b : ℤ), t.IsLE ((t.truncLTGE a b).obj X) (b - 1)
-- Lean.Structure
Lean.instInhabitedStructureResolutionState.default : Lean.StructureResolutionState
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft_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]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {w x y : D} (f : w ⟶ x) (g : x ⟶ y) (z : C) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.comp f g)
        z)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft g z)
        h)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.PreservesLeftKanExtension.preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} A}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {inst_2 : CategoryTheory.Category.{v_3, u_3} C}
  {inst_3 : CategoryTheory.Category.{v_4, u_4} D} {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C} [self : G.PreservesLeftKanExtension F L] (F' : CategoryTheory.Functor C B)
  (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α],
  (F'.comp G).IsLeftKanExtension
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G) (L.associator F' G).hom)
-- Mathlib.Geometry.Manifold.Instances.Real
ModelWithCorners.mk.congr_simp : ∀ {𝕜 : 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]
  (toPartialEquiv toPartialEquiv_1 : PartialEquiv H E) (e_toPartialEquiv : toPartialEquiv = toPartialEquiv_1)
  (source_eq : toPartialEquiv.source = Set.univ)
  (convex_range' :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv) else Set.range ↑toPartialEquiv = Set.univ)
  (nonempty_interior' : (interior (Set.range ↑toPartialEquiv)).Nonempty) (continuous_toFun : Continuous ↑toPartialEquiv)
  (continuous_invFun : Continuous toPartialEquiv.invFun),
  { toPartialEquiv := toPartialEquiv, source_eq := source_eq, convex_range' := convex_range',
      nonempty_interior' := nonempty_interior', continuous_toFun := continuous_toFun,
      continuous_invFun := continuous_invFun } =
    { toPartialEquiv := toPartialEquiv_1, source_eq := ⋯, convex_range' := ⋯, nonempty_interior' := ⋯,
      continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : SMul G M] {n : WithTop ℕ∞} [ContMDiffSMul I I' n G M] {f : N → G} {g : N → M} {x : N},
  ContMDiffAt I'' I n f x → ContMDiffAt I'' I' n g x → ContMDiffAt I'' I' n (f • g) x
-- Init.Grind.AC
Lean.Grind.AC.Expr.var.inj : ∀ {x x_1 : Lean.Grind.AC.Var}, Lean.Grind.AC.Expr.var x = Lean.Grind.AC.Expr.var x_1 → x = x_1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) (i : Fin (m + 1)),
  (s.reindex e).touchpoint signs i = s.touchpoint (Finset.map e.symm.toEmbedding signs) (e.symm i)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_commonTangents_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s₁ s₂ : EuclideanGeometry.Sphere P},
  as ∈ s₁.commonTangents s₂ ↔ as ∈ s₁.tangentSet ∧ as ∈ s₂.tangentSet
-- Mathlib.Computability.Encoding
/-- Decoding and encoding are inverses of each other.  -/
Computability.Encoding.decode_encode : ∀ {α : Type u} {Γ : Type v} (self : Computability.Encoding α Γ) (x : α), self.decode (self.encode x) = some x
-- Std.Data.HashMap.Lemmas
Std.HashMap.fold_eq_foldl_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.HashMap.fold (fun d a x => f d a) init m = Array.foldl f init m.keysArray
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instRegularSpace : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [RegularSpace R], RegularSpace (ContinuousMapZero X R)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {toFunctor : CategoryTheory.Functor C C}
  {ε : toFunctor ⟶ CategoryTheory.Functor.id C} {δ : toFunctor ⟶ toFunctor.comp toFunctor}
  {coassoc :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (δ.app X)) =
          CategoryTheory.CategoryStruct.comp (δ.app X) (δ.app (toFunctor.obj X)))
      CategoryTheory.Comonad.coassoc._autoParam}
  {left_counit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (ε.app (toFunctor.obj X)) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj X))
      CategoryTheory.Comonad.left_counit._autoParam}
  {right_counit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (ε.app X)) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj X))
      CategoryTheory.Comonad.right_counit._autoParam}
  {toFunctor_1 : CategoryTheory.Functor C C} {ε_1 : toFunctor_1 ⟶ CategoryTheory.Functor.id C}
  {δ_1 : toFunctor_1 ⟶ toFunctor_1.comp toFunctor_1}
  {coassoc_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ_1.app X) (toFunctor_1.map (δ_1.app X)) =
          CategoryTheory.CategoryStruct.comp (δ_1.app X) (δ_1.app (toFunctor_1.obj X)))
      CategoryTheory.Comonad.coassoc._autoParam}
  {left_counit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ_1.app X) (ε_1.app (toFunctor_1.obj X)) =
          CategoryTheory.CategoryStruct.id (toFunctor_1.obj X))
      CategoryTheory.Comonad.left_counit._autoParam}
  {right_counit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ_1.app X) (toFunctor_1.map (ε_1.app X)) =
          CategoryTheory.CategoryStruct.id (toFunctor_1.obj X))
      CategoryTheory.Comonad.right_counit._autoParam},
  { toFunctor := toFunctor, ε := ε, δ := δ, coassoc := coassoc, left_counit := left_counit,
        right_counit := right_counit } =
      { toFunctor := toFunctor_1, ε := ε_1, δ := δ_1, coassoc := coassoc_1, left_counit := left_counit_1,
        right_counit := right_counit_1 } →
    toFunctor = toFunctor_1 ∧ ε ≍ ε_1 ∧ δ ≍ δ_1
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsCircuit.mem_closure_sdiff_singleton_of_mem`. -/
Matroid.IsCircuit.mem_closure_diff_singleton_of_mem : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α}, M.IsCircuit C → e ∈ C → e ∈ M.closure (C \ {e})
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.PulledChunk.mk.inj : ∀ {final incomplete : Bool} {chunk : Std.Http.Chunk} {final_1 incomplete_1 : Bool} {chunk_1 : Std.Http.Chunk},
  { final := final, incomplete := incomplete, chunk := chunk } =
      { final := final_1, incomplete := incomplete_1, chunk := chunk_1 } →
    final = final_1 ∧ incomplete = incomplete_1 ∧ chunk = chunk_1
-- Mathlib.Order.BoundedOrder.Basic
Ne.bot_lt' : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ ≠ a → ⊥ < a
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.instMonoidalCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : P.IsMonoidalStable] → CategoryTheory.MonoidalCategory (CategoryTheory.WideSubcategory P)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.inv.aux.eq_1 : ∀ {R : Type u_1} [inst : Ring R], PowerSeries.inv.aux = MvPowerSeries.inv.aux
-- Mathlib.Algebra.Notation.Pi.Basic
/-- Abbreviation for `single_eq_of_ne h.symm`, for ease of use by `simp`.  -/
Pi.single_eq_of_ne' : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] {i i' : ι},
  i ≠ i' → ∀ (x : M i), Pi.single i x i' = 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- Two oriented angles in right-angled triangles are equal if twice those angles are equal.  -/
EuclideanGeometry.oangle_eq_oangle_of_two_zsmul_eq_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  2 • EuclideanGeometry.oangle p₂ p₃ p₁ = 2 • EuclideanGeometry.oangle p₅ p₆ p₄ →
    EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
      EuclideanGeometry.angle p₄ p₅ p₆ = Real.pi / 2 →
        EuclideanGeometry.oangle p₂ p₃ p₁ = EuclideanGeometry.oangle p₅ p₆ p₄
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.flat_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Flat f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : SizeOf C] (of : C), sizeOf { of := of } = 1 + sizeOf of
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.le_add_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  AddLECancellable b → a ≤ a + b - b
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.lt.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (val : β)
  (h_1 : (val : β) → motive none (some val)) (h_2 : (x : α) → (y : β) → motive (some x) (some y))
  (h_3 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match none, some val with
    | none, some val => h_1 val
    | some x, some y => h_2 x y
    | x, x_1 => h_3 x x_1) =
    h_1 val
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μβ : MeasureTheory.Measure β)
  (a : α), (ProbabilityTheory.Kernel.const α μβ) a = μβ
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The functor `Ind C ⥤ Cᵒᵖ ⥤ Type v` is fully faithful.  -/
CategoryTheory.Ind.inclusion.fullyFaithful : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (CategoryTheory.Ind.inclusion C).FullyFaithful
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The affine subspace `as` is tangent to the sphere `s` at the point `p`.  -/
EuclideanGeometry.Sphere.IsTangentAt : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → EuclideanGeometry.Sphere P → P → AffineSubspace ℝ P → Prop
-- Mathlib.Order.UpperLower.Closure
LowerSet.erase_lt : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {a : α}, s.erase a < s ↔ a ∈ s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_link2 : ∀ {α : Type u} {β : α → Type v} [Ord α] {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced} {hr : r.Balanced},
  (l.link2 r hl hr).impl.toListModel = l.toListModel ++ r.toListModel
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_zero : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α},
  x ∉ Metric.thickening δ E → (thickenedIndicator δ_pos E) x = 0
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalarsEquiv_apply : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (p : Submodule R M)
  (a : ↥p), (Submodule.restrictScalarsEquiv S R M p) a = a
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_left_cancel : ∀ {n a b c d : ℕ}, a ≡ b [MOD n] → a + c ≡ b + d [MOD n] → c ≡ d [MOD n]
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableWithinAt.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableWithinAt 𝕜 φ s x →
    DifferentiableWithinAt 𝕜 φs s x → DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.natLog_le_logb : ∀ (a b : ℕ), ↑(Nat.log b a) ≤ Real.logb ↑b ↑a
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_and : ∀ {w x y : ℕ}, BitVec.ofNat w (x &&& y) = BitVec.ofNat w x &&& BitVec.ofNat w y
-- Mathlib.Data.Analysis.Topology
/-- A `Ctop α σ` is a realization of a topology (basis) on `α`,
represented by a type `σ` together with operations for the top element and
the intersection operation.  -/
Ctop : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.toFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            CategoryTheory.LaxMonoidalFunctor C D → CategoryTheory.Functor C D
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Overlap.zero.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  {x x_1 : Q(Mathlib.Meta.NormNum.IsNat «$e» 0)},
  Mathlib.Tactic.Ring.Common.Overlap.zero x = Mathlib.Tactic.Ring.Common.Overlap.zero x_1 → x = x_1
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.Nat.Partrec.Code.pappAck.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.divOf.congr_simp : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x x_1 : AddMonoidAlgebra k G), x = x_1 → ∀ (g g_1 : G), g = g_1 → x.divOf g = x_1.divOf g_1
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
/-- There are `n.totient` Dirichlet characters mod `n` with values in a ring that has enough
roots of unity.  -/
DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)],
  Nat.card (DirichletCharacter R n) = n.totient
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.d₂_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    ∀ (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂),
      K.d₂ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂')
            (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.pmap.match_1.splitter : {α : Type u_1} →
  {p : α → Prop} →
    (motive : (x : Option α) → (∀ (a : α), x = some a → p a) → Sort u_2) →
      (x : Option α) →
        (x_1 : ∀ (a : α), x = some a → p a) →
          ((x : ∀ (a : α), none = some a → p a) → motive none x) →
            ((a : α) → (H : ∀ (a_1 : α), some a = some a_1 → p a_1) → motive (some a) H) → motive x x_1
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.homOfEq_edge : ∀ {X : SSet.Truncated 2} {x₁ y₁ x₂ y₂ : SSet.OneTruncation₂ X} (f : x₁ ⟶ y₁) (hx : x₁ = x₂) (hy : y₁ = y₂),
  (Quiver.homOfEq f hx hy).edge = f.edge