mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Two affine maps are equal if they coerce to the same function.  -/
AffineMap.ext : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2}, (∀ (p : P1), f p = g p) → f = g
-- Mathlib.Data.ENNReal.Inv
ENNReal.ofReal_div_le : ∀ {x y : ℝ}, 0 ≤ y → ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- We choose `CommGrpCat.of (G × H)` as the product of `G` and `H` and `CommGrpCat.of PUnit` as
the terminal object.  -/
CommGrpCat.cartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory CommGrpCat
-- Mathlib.Algebra.Order.Sub.Unbundled.Hom
/-- An order isomorphism between types with ordered subtraction preserves subtraction provided that
it preserves addition.  -/
OrderIso.map_tsub : ∀ {M : Type u_3} {N : Type u_4} [inst : Preorder M] [inst_1 : Add M] [inst_2 : Sub M] [OrderedSub M]
  [inst_4 : PartialOrder N] [inst_5 : Add N] [inst_6 : Sub N] [OrderedSub N] (e : M ≃o N),
  (∀ (a b : M), e (a + b) = e a + e b) → ∀ (a b : M), e (a - b) = e a - e b
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.tower_top : ∀ {R : Type u_1} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T), (g.comp f).IsIntegral → g.IsIntegral
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedAddHom`.

---

`inducedMap` as an additive homomorphism.  -/
LinearOrderedField.inducedAddHom : (α : Type u_2) →
  (β : Type u_3) →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [IsStrictOrderedRing α] →
          [inst_3 : Field β] →
            [inst_4 : ConditionallyCompleteLinearOrder β] → [IsStrictOrderedRing β] → [Archimedean α] → α →+ β
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.toRingEquiv_conjStarAlgAut : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u : ↥(unitary R)),
  ((Unitary.conjStarAlgAut S R) u).toRingEquiv =
    (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (Unitary.toUnits u))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey? k = m₁.getKey? k
-- Mathlib.Algebra.Group.Defs
IsAddCyclic.exists_zsmul_surjective : ∀ {G : Type u} {inst : SMul ℤ G} [self : IsAddCyclic G], ∃ g, Function.Surjective fun x => x • g
-- Init.Data.List.Control
/-- Applies the monadic action `f` to the corresponding elements of two lists, left-to-right, stopping
at the end of the shorter list. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)`
for lawful `Monad` instances.

This implementation is tail recursive. `List.zipWithM'` is a non-tail-recursive variant that may
be more convenient to reason about.
 -/
List.zipWithM : {m : Type u → Type v} →
  [Monad m] → {α : Type w} → {β : Type x} → {γ : Type u} → (α → β → m γ) → List α → List β → m (List γ)
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
ChainComplex.quasiIso_iff_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : ChainComplex C ℕ}
  [∀ (n : ℕ), CategoryTheory.Projective (K.X n)] [∀ (n : ℕ), CategoryTheory.Projective (L.X n)] (f : K ⟶ L),
  QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.down ℕ) f
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context.kind : Lean.Meta.FindSplitImpl.Context → Lean.Meta.SplitKind
-- Init.System.IO
/-- Configuration for the process' stdout handle.  -/
IO.Process.StdioConfig.stdout : IO.Process.StdioConfig → IO.Process.Stdio
-- Init.Data.Option.Lemmas
Option.pmap_pred_congr : ∀ {α : Type u} {p p' : α → Prop},
  (∀ (x : α), p x ↔ p' x) → ∀ {o o' : Option α}, o = o' → (∀ (x : α), o = some x → p x) → ∀ (x : α), o' = some x → p' x
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.NatTrans.CommShift F.mapDerivedCategoryFactorsh.hom ℤ
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : α) (xs : List α) (y : α) (ys : List α)
  (h_1 : (ys : List α) → motive [] ys) (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match x :: xs, y :: ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_3 x xs y ys
-- Init.Data.UInt.Bitwise
UInt32.toFin_or : ∀ (a b : UInt32), (a ||| b).toFin = a.toFin ||| b.toFin
-- Mathlib.Algebra.Order.Field.Power
/-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℤ)`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalZPow : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.Coprod.Basic
/-- Extensionality lemma for additive monoid homomorphisms `AddMonoid.Coprod M N →+ P`.
If two homomorphisms agree on the ranges of `AddMonoid.Coprod.inl` and `AddMonoid.Coprod.inr`,
then they are equal.  -/
AddMonoid.Coprod.hom_ext : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] {f g : AddMonoid.Coprod M N →+ P},
  f.comp AddMonoid.Coprod.inl = g.comp AddMonoid.Coprod.inl →
    f.comp AddMonoid.Coprod.inr = g.comp AddMonoid.Coprod.inr → f = g
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticOnNhd.zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOnNhd 𝕜 f s → 0 ≤ n → AnalyticOnNhd 𝕜 (f ^ n) s
-- Init.Data.BitVec.Lemmas
/-- Moves one-sided left toNat equality to BitVec equality.  -/
BitVec.toNat_eq_nat : ∀ {w : ℕ} {x : BitVec w} {y : ℕ}, x.toNat = y ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y
-- Init.Data.UInt.Lemmas
UInt8.ofNatTruncate_bitVecToNat : ∀ (n : BitVec 8), UInt8.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g g_1 : β → γ) (e_g : g = g_1) (hg : Continuous g)
  (f f_1 : α →ₘ[μ] β), f = f_1 → MeasureTheory.AEEqFun.comp g hg f = MeasureTheory.AEEqFun.comp g_1 ⋯ f_1
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_pure : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b : β},
  Filter.Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.kerParam.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Equiv.Perm.OnCycleFactors.kerParam g = Equiv.Perm.ofSubtype.noncommCoprod (Subgroup.noncommPiCoprod ⋯) ⋯
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.finrank_eq_zero_of_subsingleton : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] [Subsingleton M], Module.finrank R M = 0
-- Mathlib.Algebra.Regular.Prod
IsRightRegular.prodMk : ∀ {R : Type u_2} {S : Type u_3} [inst : Mul R] [inst_1 : Mul S] {a : R} {b : S},
  IsRightRegular a → IsRightRegular b → IsRightRegular (a, b)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.comap_exp_nhdsGT_zero : Filter.comap Real.exp (nhdsWithin 0 (Set.Ioi 0)) = Filter.atBot
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.monotone_prod_take : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [CanonicallyOrderedMul M] (L : List M),
  Monotone fun i => (List.take i L).prod
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_range_succ : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f : ℕ → M) (n : ℕ),
  ∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.iff_exponent_eq_card : ∀ {α : Type u_1} [inst : AddCommGroup α] [Finite α], IsAddCyclic α ↔ AddMonoid.exponent α = Nat.card α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).size =
    if k ∈ t ∧ (f (Std.DTreeMap.Const.get? t k)).isNone = true then t.size - 1
    else if k ∉ t ∧ (f (Std.DTreeMap.Const.get? t k)).isSome = true then t.size + 1 else t.size
-- Init.GrindInstances.Ring.UInt
UInt64.ofInt.eq_1 : ∀ (x : ℤ), UInt64.ofInt x = UInt64.ofNat (x % 2 ^ 64).toNat
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.remaining : {α : Type} → Std.Slot✝ α → ℕ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk_add : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a b : G), ↑(a + b) = ↑a + ↑b
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_eq_bot_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), Nonempty (α i)],
  Filter.coprodᵢ f = ⊥ ↔ f = ⊥
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical inclusion of rings `R →+* Unitization R A`.  -/
Unitization.inlRingHom : (R : Type u_1) →
  (A : Type u_2) → [inst : Semiring R] → [inst_1 : NonUnitalSemiring A] → [inst_2 : Module R A] → R →+* Unitization R A
-- Mathlib.Order.Heyting.Hom
CoheytingHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  [inst_2 : FunLike F α β] [toLatticeHomClass : LatticeHomClass F α β],
  (∀ (f : F), f ⊤ = ⊤) → (∀ (f : F) (a b : α), f (a \ b) = f a \ f b) → CoheytingHomClass F α β
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos` to be able to apply this.  -/
String.Slice.Pos.Splits.of_prev : ∀ {t₁ : String} {c : Char} {t₂ : String} {s : String.Slice} {p : s.Pos} {hp : p ≠ s.startPos},
  (p.prev hp).Splits t₁ (String.singleton c ++ t₂) → p.Splits (t₁ ++ String.singleton c) t₂
-- Init.PropLemmas
or_congr_left : ∀ {a b c : Prop}, (a ↔ b) → (a ∨ c ↔ b ∨ c)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r1_eq : ∀ (z : UpperHalfPlane), EisensteinSeries.r1 z = 1 / ((z.re / z.im) ^ 2 + 1)
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.instInhabitedContext : Inhabited Aesop.Script.DynStructureM.Context
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.bind_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] {X : C}
  (P : CategoryTheory.Limits.ColimitPresentation J X)
  (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j))
  [inst_3 : ∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [inst_4 : ∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)]
  (k : CategoryTheory.Limits.ColimitPresentation.Total Q),
  (P.bind Q).ι.app k = CategoryTheory.CategoryStruct.comp ((Q k.fst).ι.app k.snd) (P.ι.app k.fst)
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
_private.Mathlib.RingTheory.Polynomial.Hermite.Basic.0.Polynomial.hermite.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A linear isometry between finite-dimensional spaces of equal dimension can be upgraded
to a linear isometry equivalence.  -/
LinearIsometry.toLinearIsometryEquiv : {F : Type u_1} →
  {E₁ : Type u_2} →
    [inst : SeminormedAddCommGroup F] →
      [inst_1 : NormedAddCommGroup E₁] →
        {R₁ : Type u_3} →
          [inst_2 : Field R₁] →
            [inst_3 : Module R₁ E₁] →
              [inst_4 : Module R₁ F] →
                [FiniteDimensional R₁ E₁] →
                  [FiniteDimensional R₁ F] → (E₁ →ₗᵢ[R₁] F) → Module.finrank R₁ E₁ = Module.finrank R₁ F → E₁ ≃ₗᵢ[R₁] F
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.toSigma_s₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) (x : 𝒰.I₀), 𝒰.toSigma.s₀ x = default
-- Mathlib.Algebra.Order.Group.Synonym
isRegular_ofDual : ∀ {α : Type u_1} [inst : Monoid α] {a : αᵒᵈ}, IsRegular (OrderDual.ofDual a) ↔ IsRegular a
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Sieve S),
  F.IsPrestackFor R.arrows ↔
    ∀ (M N : ↑(F.obj { as := Opposite.op S })),
      CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N)
        ((CategoryTheory.Sieve.overEquiv (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S))).symm R).arrows
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- Note: this assumes `[IsLeftUniformGroup β] [IsRightUniformGroup β]` instead of the more typical
(and equivalent) `[IsUniformGroup β]` because this is used in the proof of said equivalence.  -/
Filter.Tendsto.conj_nhds_one : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β]
  {ι : Type u_3} {l : Filter ι} {x : ι → β},
  Filter.Tendsto x l (nhds 1) → ∀ (g : ι → β), Filter.Tendsto (g * x * g⁻¹) l (nhds 1)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_le_one_iff_adj_or_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
-- Init.Data.Array.Lemmas
Array.any_eq_false : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.any p = false ↔ ∀ (i : ℕ) (x : i < as.size), ¬p as[i] = true
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_naturality : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L)
  {n n' : ι} (h : n = n'),
  CategoryTheory.CategoryStruct.comp (φ.f n) (L.XIsoOfEq h).hom =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (φ.f n')
-- Mathlib.Data.Finset.Card
Finset.eq_of_subset_of_card_le : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → t.card ≤ s.card → s = t
-- Mathlib.Topology.Algebra.Group.Pointwise
IsCompact.mul_closure_one_eq_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {K : Set G},
  IsCompact K → K * closure {1} = closure K
-- Std.Data.HashSet.Lemmas
Std.HashSet.insertMany_append : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {l₁ l₂ : List α},
  m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.integrable_geometricMeasure_iff : ∀ {p : ↑unitInterval} {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℕ → E},
  p ≠ 0 →
    (MeasureTheory.Integrable f (ProbabilityTheory.geometricMeasure p) ↔ Summable fun n => (1 - ↑p) ^ n * ↑p * ‖f n‖)
-- Init.Data.Sum.Lemmas
Sum.getLeft?_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  (Sum.map f g x).getLeft? = Option.map f x.getLeft?
-- Mathlib.ModelTheory.Satisfiability
/-- An alternative statement of the Compactness Theorem. A formula `φ` is modeled by a
theory iff there is a finite subset `T0` of the theory such that `φ` is modeled by `T0`  -/
FirstOrder.Language.Theory.models_iff_finset_models : ∀ {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence}, T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_single_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Group G] [inst_2 : MulSemiringAction G k] (r : k) (x : G)
  (f : SkewMonoidAlgebra k G) (y : G), (SkewMonoidAlgebra.single x r * f).coeff y = r * x • f.coeff (x⁻¹ * y)
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.toAlternatingMap_curryLeft : ∀ {𝕜 : 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] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E), (f.curryLeft x).toAlternatingMap = f.toAlternatingMap.curryLeft x
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.requestStream : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Std.Http.Body.Stream
-- Mathlib.Logic.Function.Basic
eq_mp_bijective : ∀ {α β : Sort u_3} (h : α = β), Function.Bijective h.mp
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_nonempty : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), {w | w ∈ p.support}.Nonempty
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_zero_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F), TensorProduct.mapL 0 f = 0
-- Mathlib.RingTheory.KrullDimension.Basic
Prime.isMaximal_span_singleton : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] {a : R},
  Prime a → (Ideal.span {a}).IsMaximal
-- Aesop.Tree.Data
Aesop.Goal.hasProvableRapp : Aesop.Goal → BaseIO Bool
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- If a `NonUnitalStarSubalgebra` over a field does not contain `1`, then its unitization is
isomorphic to its `StarAlgebra.adjoin`.  -/
NonUnitalStarSubalgebra.unitizationStarAlgEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Field R] →
        [inst_1 : StarRing R] →
          [inst_2 : Ring A] →
            [inst_3 : StarRing A] →
              [inst_4 : Algebra R A] →
                [inst_5 : StarModule R A] →
                  [inst_6 : SetLike S A] →
                    [hSA : NonUnitalSubringClass S A] →
                      [hSRA : SMulMemClass S R A] →
                        [inst_7 : StarMemClass S A] →
                          (s : S) → 1 ∉ s → Unitization R ↥s ≃⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
of `Γ(X, ⊤)` under `toΓSpec` agrees with the associated zero locus on `X`.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq : ∀ {X : AlgebraicGeometry.LocallyRingedSpace} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑(CategoryTheory.ConcreteCategory.hom X.toΓSpec.base) ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.Walk.setOfPred_length_eq_zero : ∀ {V : Type u} (G : SimpleGraph V) (u : V), {p | p.length = 0} = {SimpleGraph.Walk.nil}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_inter_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₂.contains k = true →
          Std.DHashMap.Internal.Raw₀.Const.getD (m₁.inter m₂) k fallback =
            Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.closure_singleton_one : ∀ {M : Type u_1} [inst : Monoid M], Submonoid.closure {1} = ⊥
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, (m.getKey? a).isSome = true ↔ a ∈ m
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.iff : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.ValuativeCriterion f ↔
    AlgebraicGeometry.ValuativeCriterion.Existence f ∧ AlgebraicGeometry.ValuativeCriterion.Uniqueness f
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsQuotientMap id
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_ulift_iff : ∀ (X : Type v) (κ : Cardinal.{w}), HasCardinalLT (ULift.{u, v} X) κ ↔ HasCardinalLT X κ
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.differentiableAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → k ≠ 0 → DifferentiableAt ℝ f a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- The base of a simplex shifted with parameter 0 intersects the closed interior only at the
vertex.  -/
Affine.Simplex.closedInterior_inter_shift_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedAddMonoid k]
  [inst_3 : AddCommGroup V] [inst_4 : AddTorsor V P] [inst_5 : Module k V] {n : ℕ} [NeZero n] (s : Affine.Simplex k P n)
  (i : Fin (n + 1)) [ZeroLEOneClass k],
  s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0) = {s.points i}
-- Mathlib.Algebra.Ring.BooleanRing
/-- Turn a bounded lattice homomorphism from Boolean algebras `α` to `β` into a ring homomorphism
from `α` to `β` considered as Boolean rings.  -/
BoundedLatticeHom.asBoolRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : BooleanAlgebra α] → [inst_1 : BooleanAlgebra β] → BoundedLatticeHom α β → AsBoolRing α →+* AsBoolRing β
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.mul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableMul₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f * g) μ