mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.noConfusionType : Sort v✝ → Std.Tactic.BVDecide.LRAT.Internal.Result → Std.Tactic.BVDecide.LRAT.Internal.Result → Sort v✝
-- Init.Data.List.Lemmas
List.head_reverse : ∀ {α : Type u_1} {l : List α} (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote'.go.match_1.eq_3 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 : (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add 1 v p))
  (h_3 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (k = 1 → False) →
    (match Lean.Grind.Linarith.Poly.add k v p with
      | Lean.Grind.Linarith.Poly.nil => h_1 ()
      | Lean.Grind.Linarith.Poly.add 1 v p => h_2 v p
      | Lean.Grind.Linarith.Poly.add k v p => h_3 k v p) =
      h_3 k v p
-- Mathlib.Algebra.Group.Action.Defs
/-- An additive action of `M` on `α` and a function `N → M` induces an additive
action of `N` on `α`.  -/
VAdd.comp : {M : Type u_1} → {N : Type u_2} → (α : Type u_5) → [VAdd M α] → (N → M) → VAdd N α
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtensionUniqueOfIso_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] {G : CategoryTheory.Functor C H} (i : F ≅ G)
  (G' : CategoryTheory.Functor D H) (β : G ⟶ L.comp G') [inst_4 : G'.IsLeftKanExtension β],
  (F'.leftKanExtensionUniqueOfIso α i G' β).hom =
    F'.descOfIsLeftKanExtension α G' (CategoryTheory.CategoryStruct.comp i.hom β)
-- Mathlib.Data.Set.Operations
Set.mem_compl_iff : ∀ {α : Type u} (s : Set α) (x : α), x ∈ sᶜ ↔ x ∉ s
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.getElem?_zipWithAll.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (h_1 : Unit → motive none none)
  (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (match none, none with
    | none, none => h_1 ()
    | a?, b? => h_2 a? b?) =
    h_1 ()
-- Mathlib.Topology.ContinuousMap.Compact
/-- Distance between the images of any two points is at most twice the norm of the function.  -/
ContinuousMap.dist_le_two_norm : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) (x y : α), dist (f x) (f y) ≤ 2 * ‖f‖
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.repr_lt : ∀ {o : ONote} {b : Ordinal.{0}}, o.NFBelow b → o.repr < Ordinal.omega0 ^ b
-- Mathlib.FieldTheory.PerfectClosure
/-- `PerfectClosure.mk K p (n, x)` for `n : ℕ` and `x : K` is an element of `PerfectClosure K p`,
viewed as `x ^ (p ^ -n)`. Every element of `PerfectClosure K p` is of this form
(`PerfectClosure.mk_surjective`).  -/
PerfectClosure.mk : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → ℕ × K → PerfectClosure K p
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_le_of_ae_bound : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F} {C : ℝ}, (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.eLpNormEssSup f μ ≤ ENNReal.ofReal C
-- Std.Data.DTreeMap.Raw.Iterator
Std.DTreeMap.Raw.toList_iter : ∀ {α : Type u_1} {β : α → Type u_2} {cmp : α → α → Ordering} (m : Std.DTreeMap.Raw α β cmp), m.iter.toList = m.toList
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The opposite of the golden ratio is the inverse of its conjugate.  -/
Real.inv_goldenConj : Real.goldenConj⁻¹ = -Real.goldenRatio
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.cone.eq_1 : ∀ (P : ProfiniteAddGrp.{u}), P.cone = { pt := P, π := { app := ProfiniteAddGrp.proj, naturality := ⋯ } }
-- Aesop.Forward.State
Aesop.InstMap.mk.sizeOf_spec : ∀ (map : Lean.PHashMap Aesop.SlotIndex (Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp))),
  sizeOf { map := map } = 1 + sizeOf map
-- Init.Data.Bool
Bool.not_xor_self : ∀ (x : Bool), (!x ^^ x) = true
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toPermFiber_ext : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (e : ↑(f ⁻¹' {x})) {g g' : G},
  ((hf.toPermFiber x) g) e = ((hf.toPermFiber x) g') e → g = g'
-- Mathlib.Combinatorics.Hall.Basic
/-- This is a version of **Hall's Marriage Theorem** in terms of a relation to a finite type.
There is a transversal of the relation (an injective function `α → β` whose graph is a subrelation
of the relation) iff every subset of `k` terms of `α` is related to at least `k` terms of `β`.

It is like `Fintype.all_card_le_rel_image_card_iff_exists_injective` but uses `Finset.filter`
rather than `Rel.image`.
 -/
Fintype.all_card_le_filter_rel_iff_exists_injective : ∀ {α : Type u} {β : Type v} [inst : Fintype β] (r : α → β → Prop) [inst_1 : DecidableRel r],
  (∀ (A : Finset α), A.card ≤ {b | ∃ a ∈ A, r a b}.card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- `i : K ⟶ S.X₂` is a kernel of `g : S.X₂ ⟶ S.X₃`  -/
CategoryTheory.ShortComplex.LeftHomologyData.hi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (self : S.LeftHomologyData) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι self.i ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ) (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n),
  CochainComplex.HomComplex.δ n m (z₁ - z₂) = CochainComplex.HomComplex.δ n m z₁ - CochainComplex.HomComplex.δ n m z₂
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.induction₂ : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i),
  p 0 → (∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + fun₀ | i => b)) → p f
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Iio : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.succ (Finset.Iio i) = Finset.Ioo 0 i.succ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_nat_mul_pi_sub : ∀ (x : ℝ) (n : ℕ), Real.tan (↑n * Real.pi - x) = -Real.tan x
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_toUSize : ∀ (n : UInt64), n.toUSize.toUInt16 = n.toUInt16
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State.mk.inj : ∀ {keys results keys_1 results_1 : Array Lean.Expr},
  { keys := keys, results := results } = { keys := keys_1, results := results_1 } → keys = keys_1 ∧ results = results_1
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedMap.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : HasFibers.Fib p R} (f f_1 : R ⟶ S)
  (e_f : f = f_1) (ψ ψ_1 : (HasFibers.ι R).obj b' ⟶ a) (e_ψ : ψ = ψ_1) [inst_3 : p.IsCartesian f ψ]
  (φ φ_1 : (HasFibers.ι R).obj b ⟶ a) (e_φ : φ = φ_1) [inst_4 : p.IsHomLift f φ],
  HasFibers.inducedMap f ψ φ = HasFibers.inducedMap f_1 ψ_1 φ_1
-- Mathlib.Topology.Compactness.LocallyCompact
Topology.IsClosedEmbedding.weaklyLocallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [WeaklyLocallyCompactSpace Y]
  {f : X → Y}, Topology.IsClosedEmbedding f → WeaklyLocallyCompactSpace X
-- Init.Data.Range.Polymorphic.UInt
UInt64.succ?_ofBitVec : ∀ {x : BitVec 64}, Std.PRange.succ? { toBitVec := x } = UInt64.ofBitVec <$> Std.PRange.succ? x
-- Init.Data.String.Lemmas.Slice
String.Pos.get?_endPos : ∀ {s : String}, s.endPos.get? = none
-- Aesop.Tree.TreeM
Aesop.TreeM.Context : Type
-- Mathlib.Logic.Equiv.Finset
Denumerable.raise'.eq_def : ∀ (x : List ℕ) (x_1 : ℕ),
  Denumerable.raise' x x_1 =
    match x, x_1 with
    | [], x => []
    | m :: l, n => (m + n) :: Denumerable.raise' l (m + n + 1)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_zero : ∀ {w : ℕ} (x : BitVec w), x <<< 0 = x
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P Q : CategoryTheory.Idempotents.Karoubi C} →
      (f : P.X ⟶ Q.X) →
        autoParam (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f Q.p) = f)
            CategoryTheory.Idempotents.Karoubi.Hom.comm._autoParam →
          P.Hom Q
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Monad.comparisonForget_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x : D),
  (CategoryTheory.Monad.comparisonForget h).inv.app x = CategoryTheory.CategoryStruct.id (R.obj x)
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instOrd : {α : Type u_1} → [inst : AddMonoid α] → [Ord α] → Ord (AddUnits α)
-- Mathlib.Logic.Denumerable
Denumerable.instInfinite : ∀ {α : Type u_1} [Denumerable α], Infinite α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.unsat_eq_certC : Lean.Grind.CommRing.Poly → ℤ → ℕ → Bool
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Ico : ∀ (x y : NNReal), NNReal.toReal '' Set.Ico x y = Set.Ico ↑x ↑y
-- Mathlib.Data.Finset.NAry
Finset.image₂_image₂_image₂_comm : ∀ {α : Type u_1} {β : Type u_3} {ε : Type u_9} {ε' : Type u_10} {ζ : Type u_11} {ζ' : Type u_12} {ν : Type u_13}
  [inst : DecidableEq ε] [inst_1 : DecidableEq ε'] {s : Finset α} {t : Finset β} {γ : Type u_14} {δ : Type u_15}
  {u : Finset γ} {v : Finset δ} [inst_2 : DecidableEq ζ] [inst_3 : DecidableEq ζ'] [inst_4 : DecidableEq ν]
  {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ} {f' : ε' → ζ' → ν} {g' : α → γ → ε'} {h' : β → δ → ζ'},
  (∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)) →
    Finset.image₂ f (Finset.image₂ g s t) (Finset.image₂ h u v) =
      Finset.image₂ f' (Finset.image₂ g' s u) (Finset.image₂ h' t v)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- A `HomologyPretheory` is homotopy-invariant if its homology functor `Hₚ` takes homotopic maps to
the same map in homology  -/
TopPair.HomologyPretheory.IsHomotopyInvariant : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → TopPair.HomologyPretheory C c → Prop
-- Mathlib.RepresentationTheory.Coinvariants
Representation.finsuppToCoinvariants_single_mk : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} {α : Type u_9} (a : α) (x : V),
  ((ρ.finsuppToCoinvariants α) fun₀ | a => (Representation.Coinvariants.mk ρ) x) =
    (Representation.Coinvariants.mk (ρ.finsupp α)) fun₀ | a => x
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), f.toFun = ⇑f
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRel.swap : ∀ {α : Type u} {β : Type v} (R : α → β → Prop),
  Function.swap (Stream'.WSeq.LiftRel R) = Stream'.WSeq.LiftRel (Function.swap R)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.mem_iff_ultrafilter : ∀ {α : Type u} {f : Filter α} {s : Set α}, s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : PartialOrder carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Define the equalizing object  -/
CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryCoproducts C] →
      [CategoryTheory.Limits.HasPushouts C] → CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C → C
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J]
  [W.IsStableUnderTransfiniteComposition] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) {i j : J}
  (φ : i ⟶ j), W (h.F.map φ)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.instIsOpenImmersionAwayι : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given a co-Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and two morphisms
`ψ ψ' : b ⟶ b'` lifting `𝟙 S` such that `φ ≫ ψ = φ ≫ ψ'`. Then we must have `ψ = ψ'`.  -/
CategoryTheory.Functor.IsCocartesian.ext : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] {b' : 𝒳}
  (ψ ψ' : b ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ]
  [p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ'],
  CategoryTheory.CategoryStruct.comp φ ψ = CategoryTheory.CategoryStruct.comp φ ψ' → ψ = ψ'
-- Init.Data.Array.MapIdx
Array.mapIdx_empty : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β}, Array.mapIdx f #[] = #[]
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).Q = cc.pt
-- Init.Data.String.Lemmas.FindPos
String.Pos.next_prev : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos}, (p.prev h).next ⋯ = p
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.nextCoeffUp.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  p.nextCoeffUp = if p.natTrailingDegree = 0 then 0 else p.coeff (p.natTrailingDegree + 1)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.commute : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → Commute f g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_iff_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∈ m ↔ m.contains a = true
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty : ∀ {X : AlgebraicGeometry.Scheme} [IsEmpty ↥X] (U : X.Opens), Subsingleton ↑(X.presheaf.obj (Opposite.op U))
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty' : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {G H : SimpleGraph α} {ε : 𝕜}
  [inst_2 : Fintype α] [inst_3 : DecidableRel G.Adj] [inst_4 : DecidableRel H.Adj] [inst_5 : DecidableEq α],
  H ≤ G →
    G.FarFromTriangleFree ε →
      ↑G.edgeFinset.card - ↑H.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) → (H.cliqueFinset 3).Nonempty
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeFpqcPrecoverage : AlgebraicGeometry.Scheme.fpqcPrecoverage.IsStableUnderBaseChange
-- Batteries.Util.Cache
Batteries.Tactic.DeclCache.mk'.injEq : ∀ {α : Type} (cache : Batteries.Tactic.Cache α)
  (addDecl addLibraryDecl : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) (cache_1 : Batteries.Tactic.Cache α)
  (addDecl_1 addLibraryDecl_1 : Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α),
  ({ cache := cache, addDecl := addDecl, addLibraryDecl := addLibraryDecl } =
      { cache := cache_1, addDecl := addDecl_1, addLibraryDecl := addLibraryDecl_1 }) =
    (cache = cache_1 ∧ addDecl = addDecl_1 ∧ addLibraryDecl = addLibraryDecl_1)
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.locallyLipschitzOn_iff_continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ},
  IsOpen C → ConvexOn ℝ C f → (LocallyLipschitzOn C f ↔ ContinuousOn f C)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.card_eq_card_functions_add_card_relations : ∀ {L : FirstOrder.Language},
  L.card =
    (Cardinal.sum fun l => Cardinal.lift.{v, u} (Cardinal.mk (L.Functions l))) +
      Cardinal.sum fun l => Cardinal.lift.{u, v} (Cardinal.mk (L.Relations l))
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (H : A.LinearDisjoint ↥B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type u_1} (b : Module.Basis ι F ↥B) (x : ↥B)
  (i : ι), (algebraMap (↥A) E) (((H.basisOfBasisRight H' b).repr ↑x) i) = (algebraMap F E) ((b.repr x) i)
-- Mathlib.Analysis.Calculus.FDeriv.Extend
/-- If a real function `f` has a derivative `g` everywhere but at a point, and `f` and `g` are
continuous at this point, then `g` is also the derivative of `f` at this point.  -/
hasDerivAt_of_hasDerivAt_of_ne : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ},
  (∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) → ContinuousAt f x → ContinuousAt g x → HasDerivAt f (g x) x
-- Mathlib.Data.Fin.Basic
Nat.forall_lt_iff_fin : ∀ {n : ℕ} {p : (k : ℕ) → k < n → Prop}, (∀ (k : ℕ) (hk : k < n), p k hk) ↔ ∀ (k : Fin n), p ↑k ⋯
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.card_interedges_comm : ∀ {α : Type u_4} {r : α → α → Prop} [inst : DecidableRel r] [Std.Symm r] (s t : Finset α),
  (Rel.interedges r s t).card = (Rel.interedges r t s).card
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_mul : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
  (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α),
  Matrix.of (Matrix.vecCons v A) * B = Matrix.of (Matrix.vecCons (Matrix.vecMul v B) (Matrix.of.symm (Matrix.of A * B)))
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR_loop_congr : ∀ {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → Bool) (j : ℕ) (h : j ≤ n),
  Nat.anyTR.loop✝ n f j h = Nat.anyTR.loop✝ m (fun i h => f i ⋯) j ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_involutive : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate),
  B.IsSymm → Function.Involutive (B.dualBasis hB)
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.one_div_pos' : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < 1 / r
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.hom_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁)
  (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
  CategoryTheory.CategoryStruct.comp (self.hom q f₁ f₂ hf₁ hf₂) (self.hom q f₂ f₃ hf₂ hf₃) = self.hom q f₁ f₃ hf₁ hf₃
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.continuous_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous ⇑DomAddAct.mk
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `RelIso.ordinalType_congr`. -/
RelIso.ordinal_type_eq : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (h : r ≃r s), Ordinal.type r = Ordinal.type s
-- Mathlib.Analysis.Complex.Circle
Circle.instUniformSpace : UniformSpace Circle
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.map_iConvexComb : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N]
  {f : M → N},
  Convexity.IsAffineMap R f →
    ∀ (s : Convexity.StdSimplex R I) (g : I → M), f (Convexity.iConvexComb s g) = Convexity.iConvexComb s (f ∘ g)
-- Mathlib.Algebra.Group.End
/-- Permutations on a subtype are equivalent to permutations on the original type that fix pointwise
the rest.  -/
Equiv.Perm.subtypeEquivSubtypePerm : {α : Type u_4} → (p : α → Prop) → [DecidablePred p] → Equiv.Perm (Subtype p) ≃ { f // ∀ (a : α), ¬p a → f a = a }
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.Equivalence_mk'_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse)
  (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D)
  (f :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) =
        CategoryTheory.CategoryStruct.id (functor.obj X)),
  { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso,
        functor_unitIso_comp := f }.counit =
    counit_iso.hom
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cooper_dvd_right_core : ∀ {a b c d s p q x : ℤ},
  a < 0 →
    0 < b →
      0 < d →
        a * x + p ≤ 0 →
          b * x + q ≤ 0 →
            d ∣ c * x + s →
              Int.Internal.Linear.OrOver (b.lcm (b * d / ↑((b * d).gcd c))) fun k =>
                b * p + -a * q + -a * ↑k ≤ 0 ∧ b ∣ q + ↑k ∧ b * d ∣ -c * q + b * s + -c * ↑k
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.close' : {m : Type → Type} →
  [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → [MonadLiftT BaseIO m] → Std.AtomicT Std.Http.Body.Channel.State✝ m Unit
-- Mathlib.Topology.Inseparable
inseparable_of_nhdsWithin_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X},
  x ∈ s → y ∈ s → nhdsWithin x s = nhdsWithin y s → Inseparable x y