mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsSimpleGroup.isCyclic : ∀ {α : Type u_1} [inst : CommGroup α] [IsSimpleGroup α], IsCyclic α
-- Mathlib.Data.Rat.Sqrt
Rat.exists_mul_self : ∀ (x : ℚ), (∃ q, q * q = x) ↔ Rat.sqrt x * Rat.sqrt x = x
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits, then `F : C ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [CategoryTheory.CreatesLimits F.op] → CategoryTheory.CreatesColimits F
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_iUnion₀ : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {f : ι → Set α},
  Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f) →
    (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) → μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.indexEquiv.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.indexEquiv K = NumberField.mixedEmbedding.indexEquiv K
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.mem_finMulAntidiag : ∀ {d n : ℕ} {f : Fin d → ℕ}, f ∈ d.finMulAntidiag n ↔ ∏ i, f i = n ∧ n ≠ 0
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
MvQPF.Prj.inhabited : {n : ℕ} → (i : Fin2 n) → {v : TypeVec.{u} n} → [Inhabited (v i)] → Inhabited (MvQPF.Prj i v)
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.lt_iff : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LT α] [inst_2 : LT N] {a b : Colex (α →₀ N)},
  a < b ↔ ∃ i, (∀ (j : α), i < j → (ofColex a) j = (ofColex b) j) ∧ (ofColex a) i < (ofColex b) i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.self_le_maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (cmp k ((t.insert k).maxD fallback)).isLE = true
-- Std.Time.Date.Unit.Day
/-- Converts an `Ordinal` to an `Offset`.
 -/
Std.Time.Day.Ordinal.toOffset : Std.Time.Day.Ordinal → Std.Time.Day.Offset
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.smul_continuousOn`

---

If `f` is circle integrable and `g` is continuous on the circle `sphere c |R|`, then `f • g` is
circle integrable.
 -/
CircleIntegrable.fun_smul_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → 𝕜} {g : ℂ → F},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (fun i => f i • g i) c R
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable, then the product of the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is
`(∏' n, f n) * ∏' n, g n`.  -/
tprod_int_rec : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] [T2Space M] {f g : ℕ → M},
  Multipliable f → Multipliable g → ∏' (n : ℤ), Int.rec f g n = (∏' (n : ℕ), f n) * ∏' (n : ℕ), g n
-- Aesop.Forward.LevelIndex
Aesop.instDecidableRelLevelIndexLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.Tactic.ToFun
_private.Mathlib.Tactic.ToFun.0.Mathlib.Tactic.toFunImpl : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Lean.Name
-- Aesop.Tree.Data
Aesop.TreeSpec.elimGoal : (self : Aesop.TreeSpec) → self.Goal → Aesop.GoalData self.Rapp self.MVarCluster
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.infClosed : ∀ {α : Type u_2} {s : Set α} [inst : SemilatticeInf α], CountableInfClosed s → InfClosed s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.associator_hom : ∀ (X Y Z : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    (((CategoryTheory.Prod.fst (↑X × ↑Y) ↑Z).comp (CategoryTheory.Prod.fst ↑X ↑Y)).prod'
        (((CategoryTheory.Prod.fst (↑X × ↑Y) ↑Z).comp (CategoryTheory.Prod.snd ↑X ↑Y)).prod'
          (CategoryTheory.Prod.snd (↑X × ↑Y) ↑Z))).toCatHom
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldCast_eq_dfoldCast_iff : ∀ {n i j : ℕ} {hi : i ≤ n} {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldCast_eq_dfoldCast_iff._auto_9✝ → Type u}
  {w₁ w₂ : i = j} {h : i ≤ n} {x : α i h}, Nat.dfoldCast✝ α w₁ x = Nat.dfoldCast✝ (fun i h => α i h) w₂ x ↔ w₁ = w₂
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_def : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure β), μ.prod ν = μ.bind fun x => MeasureTheory.Measure.map (Prod.mk x) ν
-- Mathlib.RepresentationTheory.Character
Representation.char_one : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [FiniteDimensional k V] (ρ : Representation k G V), ρ.character 1 = ↑(Module.finrank k V)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.cosh` is complex analytic.  -/
Complex.analyticWithinAt_cosh : ∀ {x : ℂ} {s : Set ℂ}, AnalyticWithinAt ℂ Complex.cosh s x
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_div : ∀ {α : Type u} [inst : Div α] (x y : α), Additive.ofMul (x / y) = Additive.ofMul x - Additive.ofMul y
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.isCompact_closure_image_ball : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}, IsCompactOperator ⇑f → ∀ (r : ℝ), IsCompact (closure (⇑f '' Metric.ball 0 r))
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_2 : ∀ (x : PosNum), (x = PosNum.one → False) → PosNum.one.sub' x = x.pred'.toZNumNeg
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.coe_op : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), ↑H.op = MulOpposite.unop ⁻¹' ↑H
-- Init.Data.List.Monadic
/-- We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
 -/
List.forIn_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  (f : α → β → m (ForInStep β)) (init : β),
  forIn l init f =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l
-- Mathlib.Order.OrderDual
/-- Type synonym to equip a type with the dual order: `≤` means `≥` and `<` means `>`. `αᵒᵈ` is
notation for `OrderDual α`.  -/
OrderDual : Type u_2 → Type u_2
-- Init.Data.Array.Lemmas
Array.replace_empty : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, #[].replace a b = #[]
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂) (s : R ⟶ R)
  (symmetry₁ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam)
  (symmetry₂ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam)
  (toJointlyMono₂_1 : CategoryTheory.JointlyMono₂ p₁ p₂) (s_1 : R ⟶ R)
  (symmetry₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam)
  (symmetry₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam),
  ({ toJointlyMono₂ := toJointlyMono₂, s := s, symmetry₁ := symmetry₁, symmetry₂ := symmetry₂ } =
      { toJointlyMono₂ := toJointlyMono₂_1, s := s_1, symmetry₁ := symmetry₁_1, symmetry₂ := symmetry₂_1 }) =
    (s = s_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)] {f : β k → β k},
  (t.modify k f).get! k = (Option.map f (t.get? k)).get!
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.oset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {i : ℕ} {y : Lean.Compiler.LCNF.Arg pu}
  {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_7} {fvarId_1 : Lean.FVarId}
  {i_1 : ℕ} {y_1 : Lean.Compiler.LCNF.Arg pu} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_7},
  Lean.Compiler.LCNF.Code.oset fvarId i y k h = Lean.Compiler.LCNF.Code.oset fvarId_1 i_1 y_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1 ∧ k = k_1
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.t2Space_iff_sInter_subset : ∀ {G : Type u} [inst : Group G] [t : TopologicalSpace G] (F : GroupFilterBasis G),
  F.topology = t → (T2Space G ↔ ⋂₀ F.sets ⊆ {1})
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (CategoryTheory.CategoryStruct.comp (K.D₁ c j j') h) =
    CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j')
      (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j') h)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w), (p.concat h).length = p.length + 1
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A subalgebra of a normed ring is also a normed ring, with the restriction of the
norm.  -/
SubalgebraClass.normedRing : {S : Type u_5} →
  {𝕜 : Type u_6} →
    {E : Type u_7} →
      [inst : CommRing 𝕜] →
        [inst_1 : NormedRing E] →
          [inst_2 : Algebra 𝕜 E] →
            [inst_3 : SetLike S E] → [SubringClass S E] → [SMulMemClass S 𝕜 E] → (s : S) → NormedRing ↥s
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod_lt : ∀ {m : ℕ} (u : UInt8), 0 < m → (u % UInt8.ofNat m).toNat < m
-- Mathlib.Data.Ordering.Basic
Ordering.compares_gt : ∀ {α : Type u_1} [inst : LT α] (a b : α), Ordering.gt.Compares a b = (a > b)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.compl_setOfPred_mem : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : (L.withConstants α).Sentence},
  {p | φ ∈ p}ᶜ = {p | FirstOrder.Language.Formula.not φ ∈ p}
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Split off the constant coefficient.  -/
PowerSeries.eq_shift_mul_X_add_const : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R),
  φ =
    (PowerSeries.mk fun p => (PowerSeries.coeff (p + 1)) φ) * PowerSeries.X +
      PowerSeries.C (PowerSeries.constantCoeff φ)
-- Mathlib.Order.Defs.Unbundled
RelLowerSet.mk.inj : ∀ {α : Type u_1} {inst : LE α} {P : α → Prop} {carrier : Set α} {isRelLowerSet' : IsRelLowerSet carrier P}
  {carrier_1 : Set α} {isRelLowerSet'_1 : IsRelLowerSet carrier_1 P},
  { carrier := carrier, isRelLowerSet' := isRelLowerSet' } =
      { carrier := carrier_1, isRelLowerSet' := isRelLowerSet'_1 } →
    carrier = carrier_1
-- Init.System.IOError
IO.Error.resourceBusy.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.resourceBusy osCode details = IO.Error.resourceBusy osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Init.Data.String.Lemmas.Basic
String.append_eq_empty_iff : ∀ {s t : String}, s ++ t = "" ↔ s = "" ∧ t = ""
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mk.injEq : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (toFun : (x : M) → V x)
  (contMDiff_toFun : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, toFun x⟩) (toFun_1 : (x : M) → V x)
  (contMDiff_toFun_1 : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, toFun_1 x⟩),
  ({ toFun := toFun, contMDiff_toFun := contMDiff_toFun } =
      { toFun := toFun_1, contMDiff_toFun := contMDiff_toFun_1 }) =
    (toFun = toFun_1)
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.Walk.IsCircuit.girth_le_length : ∀ {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a}, w.IsCircuit → G.girth ≤ w.length
-- Std.Data.HashSet.Basic
/-- Removes the element if it exists.  -/
Std.HashSet.erase : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Std.HashSet α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_obj : ∀ {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.Cocone F.rightOp),
  CategoryTheory.Limits.coconeRightOpOfConeEquiv.inverse.obj c =
    Opposite.op (CategoryTheory.Limits.coneOfCoconeRightOp c)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_castSucc_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) self.map = f.map
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp.eq_4 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.fix f k) =
    Turing.PartrecToTM2.codeSupp' f.fix k ∪ Turing.PartrecToTM2.contSupp k
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxcHasSize : Std.Rxc.HasSize Int16
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instUnique : {F : Type u_1} → [inst : Field F] → Unique (IntermediateField F F)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.whiskerLeft_add : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} (f g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (f + g) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f + CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g
-- Mathlib.Data.Multiset.Dedup
Multiset.le_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t.dedup ↔ s ≤ t ∧ s.Nodup
-- Mathlib.Analysis.Complex.Circle
Circle.coe_neg : ∀ (x : Circle), ↑(-x) = -↑x
-- Mathlib.Data.List.DropRight
List.rtake_eq_reverse_take_reverse : ∀ {α : Type u_1} (l : List α) (n : ℕ), l.rtake n = (List.take n l.reverse).reverse
-- Lean.Exception
/-- Convert an `Except` into a `m` monadic action, where `m` is any monad that
implements `MonadError`.
 -/
Lean.ofExcept : {m : Type → Type} → {ε α : Type} → [Monad m] → [Lean.MonadError m] → [Lean.ToMessageData ε] → Except ε α → m α
-- Init.Data.Int.Compare
Int.isGE_compare : ∀ {a b : ℤ}, (compare a b).isGE = true ↔ b ≤ a
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.GrothendieckTopology.HasEnoughPoints.exists_objectProperty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (J : CategoryTheory.GrothendieckTopology C)
  [self : J.HasEnoughPoints],
  ∃ P, CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P ∧ P.IsConservativeFamilyOfPoints
-- Init.Data.SInt.Lemmas
Int8.mul_sub : ∀ {a b c : Int8}, a * (b - c) = a * b - a * c
-- Init.Coe
CoeHTCT.mk : {α : Sort u} → {β : Sort v} → (α → β) → CoeHTCT α β
-- Batteries.Data.Array.Scan
Subarray.scanrM_eq_scanrM_extract : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → m β}
  {as : Subarray α}, Subarray.scanrM f init as = Array.scanrM f init (as.array.extract as.stop as.start)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_left_le_mk_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → ArchimedeanClass.mk a ≤ ArchimedeanClass.mk (a + b)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.rightAdjoint.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R R_1 : CategoryTheory.Functor D C) (e_R : R = R_1) [inst_2 : R.IsLeftAdjoint], R.rightAdjoint = R_1.rightAdjoint
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_uIcc : ∀ {n : ℕ} (a b : Fin n), (Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
-- Lean.Server.References
/-- All usage `Reference`s of the identifier in a single module.  -/
Lean.Server.RefInfo.usages : Lean.Server.RefInfo → Array Lean.Server.Reference
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The two projections `Δ_{X/Y} ⟶ X` form a kernel pair for `f : X ⟶ Y`.  -/
CategoryTheory.Limits.pullback.diagonal_isKernelPair : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.IsKernelPair f (CategoryTheory.Limits.pullback.fst f f) (CategoryTheory.Limits.pullback.snd f f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_of_isEmpty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {a : α}, (↑m).isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = none
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.isIso_of_ker_eq : ∀ {Z₁ Z₂ X : AlgebraicGeometry.Scheme} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [AlgebraicGeometry.IsClosedImmersion i₁]
  [AlgebraicGeometry.IsClosedImmersion i₂] (f : Z₁ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp f i₂ = i₁ →
    AlgebraicGeometry.Scheme.Hom.ker i₁ = AlgebraicGeometry.Scheme.Hom.ker i₂ → CategoryTheory.IsIso f
-- Lean.Server.References
/-- There are several different identifiers that should be considered equal for the purpose of finding
all references of an identifier:
- `FVarId`s of a function parameter in the function's signature and body
- Chains of helper definitions like those created for do-reassignment `x := e`
- Overlapping definitions like those defined by `where` declarations that define both an FVar
  (for local usage) and a constant (for non-local usage)
- Identifiers connected by `FVarAliasInfo` such as variables before and after `match` generalization

In the first three cases that are not explicitly denoted as aliases with an `FVarAliasInfo`, the
corresponding `Reference`s have the exact same range.
This function finds all definitions that have the exact same range as another definition or usage
and collapses them into a single identifier. It also collapses identifiers connected by
an `FVarAliasInfo`.
When collapsing identifiers, it prefers using a `RefIdent.const name` over a `RefIdent.fvar id` for
all identifiers that are being collapsed into one.
 -/
Lean.Server.combineIdents : Array Lean.Elab.InfoTree → Array Lean.Server.Reference → Array Lean.Server.Reference
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_not : ∀ (a : BitVec 32), { toBitVec := ~~~a } = ~~~{ toBitVec := a }
-- Qq.Macro
Qq.Impl.unquoteLevelLCtx : optParam Bool true → Qq.Impl.UnquoteM Unit
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (i : X ⟶ Y) (r : Y ⟶ X)
  (retract :
    autoParam (CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Retract.retract._autoParam)
  (i_1 : X ⟶ Y) (r_1 : Y ⟶ X)
  (retract_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 r_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Retract.retract._autoParam),
  ({ i := i, r := r, retract := retract } = { i := i_1, r := r_1, retract := retract_1 }) = (i = i_1 ∧ r = r_1)
-- Mathlib.Order.UpperLower.Closure
mem_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {x : α}, x ∈ lowerClosure s ↔ ∃ a ∈ s, x ≤ a
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.mk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F},
  (∀ (x : E), (p x 0).curry0 = f x) →
    (∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x) →
      (∀ (m : ℕ), ↑m ≤ n → Continuous fun x => p x m) → HasFTaylorSeriesUpTo n f p
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- A property is Zariski-local at target if it is local at target in the Zariski topology.  -/
AlgebraicGeometry.IsZariskiLocalAtTarget : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → Prop
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.Adjunction.homEquiv₂_symm_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : a ⟶ b} {h : a ⟶ c}
  (γ : g ⟶ CategoryTheory.CategoryStruct.comp h r),
  adj.homEquiv₂.symm γ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight γ l)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator h r l).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h adj.counit)
          (CategoryTheory.Bicategory.rightUnitor h).hom))
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Let `M` be a σ-compact Hausdorff finite-dimensional topological manifold. Let `t : M → Set F`
be a family of convex sets. Suppose that for each point `x : M` there exists a neighborhood
`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is $C^n$ smooth on `U` and `g y ∈ t y` for all
`y ∈ U`. Then there exists a $C^n$ smooth function `g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x`
for all `x`.

This is a special case of `exists_contMDiffSection_forall_mem_convex_of_local` where `V` is the
trivial bundle. See also `exists_contMDiffMap_mem_convex_of_local_const`.  -/
exists_contMDiffMap_forall_mem_convex_of_local : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM}
  [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M]
  [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞},
  (∀ (x : M), Convex ℝ (t x)) →
    (∀ (x : M), ∃ U ∈ nhds x, ∃ g, ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y) →
      ∃ g, ∀ (x : M), g x ∈ t x
-- Mathlib.Algebra.GroupWithZero.WithZero
MulEquiv.withZero_symm_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : Group β] (e : WithZero α ≃* WithZero β) (x : α),
  (MulEquiv.withZero.symm e) x = WithZero.unzero ⋯