mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_le_iff_le_add'`. -/
sub_left_le_of_le_add : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a ≤ b + c → a - b ≤ c
-- Mathlib.Order.DirSupClosed
/-- A predicate for a set which is closed under directed suprema of nonempty sets.
This is the complement of a `DirSupInaccOn` set.  -/
DirSupClosedOn : {α : Type u_1} → [Preorder α] → Set (Set α) → Set α → Prop
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.AbsolutelyContinuous.comp_right : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ (κ : ProbabilityTheory.Kernel α γ), (μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑κ)
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.night.sizeOf_spec : sizeOf Std.Time.ExtendedDayPeriod.night = 1
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.lift_fst : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.fst f g) = a
-- Init.Data.String.Basic
String.Slice.Pos.cast_lt_cast_iff : ∀ {s t : String.Slice} {pos pos' : s.Pos} {h : s.copy = t.copy}, pos.cast h < pos'.cast h ↔ pos < pos'
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Fintype.piFinset_smul_finset : ∀ {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (β i)] [inst_3 : (i : ι) → SMul (α i) (β i)] (a : (i : ι) → α i)
  (s : (i : ι) → Finset (β i)), (Fintype.piFinset fun i => a i • s i) = a • Fintype.piFinset s
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_right_cancel' : ∀ {n a b : ℕ} (c : ℕ), a + c ≡ b + c [MOD n] → a ≡ b [MOD n]
-- Mathlib.Data.Sum.Order
OrderIso.sumComm_apply : ∀ (α : Type u_10) (β : Type u_11) [inst : LE α] [inst_1 : LE β] (a : α ⊕ β), (OrderIso.sumComm α β) a = a.swap
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Lean.Data.Options
Lean.OptionDecl.declName : Lean.OptionDecl → Lean.Name
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_eq_zero : ∀ {R : Type u_2} {S : Type u_3} [inst : DivisionSemiring R] [inst_1 : Semiring S] [Nontrivial S] (φ : PowerSeries R)
  (f : R →+* S), (PowerSeries.map f) φ = 0 ↔ φ = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateUnreach! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Expr → Lean.Compiler.LCNF.Code pu
-- Mathlib.Probability.Distributions.Beta
/-- The beta pdf is measurable.  -/
ProbabilityTheory.measurable_betaPDFReal : ∀ (α β : ℝ), Measurable (ProbabilityTheory.betaPDFReal α β)
-- Mathlib.Data.Finset.Max
Finset.max_erase_ne_self : ∀ {α : Type u_2} [inst : LinearOrder α] {x : α} {s : Finset α}, (s.erase x).max ≠ ↑x
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {s t : Set α},
  SemicontinuousWithinAt r s x → t ⊆ s → SemicontinuousWithinAt r t x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- If `f₁ = f₂` and `g₁ = g₂`, we may construct a canonical
isomorphism `pushout f₁ g₁ ≅ pullback f₂ g₂`  -/
CategoryTheory.Limits.pushout.congrHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f₁ f₂ : X ⟶ Y} →
        {g₁ g₂ : X ⟶ Z} →
          f₁ = f₂ →
            g₁ = g₂ →
              [inst_1 : CategoryTheory.Limits.HasPushout f₁ g₁] →
                [inst_2 : CategoryTheory.Limits.HasPushout f₂ g₂] →
                  CategoryTheory.Limits.pushout f₁ g₁ ≅ CategoryTheory.Limits.pushout f₂ g₂
-- Std.Tactic.Do.Syntax
/-- Like `refine`, but operating on stateful `Std.Do.SPred` goals.
```lean
example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
  mintro ⟨HP, HQ, HR⟩
  mrefine ⟨HP, HR⟩

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mrefine ⟨⌜42⌝, H⟩
```
 -/
Lean.Parser.Tactic.mrefine : Lean.ParserDescr
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.unify.congr_simp : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) {α : Type u_1} (x x_1 : α → FirstOrder.Language.Structure.Sigma f)
  (e_x : x = x_1) (i : ι) (h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (a a_1 : α),
  a = a_1 → FirstOrder.Language.DirectLimit.unify f x i h a = FirstOrder.Language.DirectLimit.unify f x_1 i ⋯ a_1
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeRight_symm_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : AddZeroClass H] (f : G ≃* Multiplicative H)
  (a : Additive G), (AddEquiv.toMultiplicativeRight.symm f) a = (MonoidHom.toAdditiveLeft f.toMonoidHom) a
-- Init.Data.Array.InsertIdx
Array.insertIdx_eraseIdx_of_le : ∀ {α : Type u} {a : α} {i j : ℕ} {as : Array α} (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i w₁).size) (h : j ≤ i),
  (as.eraseIdx i w₁).insertIdx j a w₂ = (as.insertIdx j a ⋯).eraseIdx (i + 1) ⋯
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_rankFinite : ∀ {α : Type u_1} {β : Type u_2} (N : Matroid β) [N.RankFinite] (f : α → β), (N.comap f).RankFinite
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instModuleCarrierObjOppositeRingCatCarrierAbPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) → (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.presheaf.obj X)
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.universalHom_unique : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_3}
  [inst_2 : Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : OreLocalization S R →+* T),
  (∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) → φ = OreLocalization.universalHom f fS hf
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.le_omega_self : ∀ (o : Ordinal.{u_1}), o ≤ Ordinal.omega o
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF],
  W.Δ = -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆
-- Lean.Meta.Tactic.Assumption
/-- Return `true` if managed to close goal `mvarId` using an assumption.  -/
Lean.MVarId.assumptionCore : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Data.WSeq.Defs
_private.Mathlib.Data.WSeq.Defs.0.Stream'.WSeq.length.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (val : α) → (s' : Stream'.Seq (Option α)) → motive (some (some val, s'))),
  (match none with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some val, s') => h_3 val s') =
    h_1 ()
-- Mathlib.Order.Comparable
CompRel.of_ge : ∀ {α : Type u_1} {a b : α} [inst : LE α], b ≤ a → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Init.Data.UInt.Lemmas
UInt32.le_iff_toFin_le : ∀ {a b : UInt32}, a ≤ b ↔ a.toFin ≤ b.toFin
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.toStream.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode.Stream α → Sort u_2) (acc : RBTree.RBNode.Stream α)
  (h_1 : (acc : RBTree.RBNode.Stream α) → motive RBTree.RBNode.nil acc)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (v : α) → (r : RBTree.RBNode α) → (acc : RBTree.RBNode.Stream α) → motive (RBTree.RBNode.node c l v r) acc),
  (match RBTree.RBNode.nil, acc with
    | RBTree.RBNode.nil, acc => h_1 acc
    | RBTree.RBNode.node c l v r, acc => h_2 c l v r acc) =
    h_1 acc
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_subset_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β}
  [inst_1 : DecidableEq β], Finset.image₂ f s (t ∩ t') ⊆ Finset.image₂ f s t ∩ Finset.image₂ f s t'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.map_inl_inv_coprodComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)],
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_prod_of_prime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  [Subsingleton αˣ] {m : Multiset α}, (∀ p ∈ m, Prime p) → UniqueFactorizationMonoid.normalizedFactors m.prod = m
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instMetricSpace : {α : Type u_1} →
  {R : Type u_3} →
    [inst : TopologicalSpace α] →
      [CompactSpace α] →
        [inst_2 : Zero α] → [inst_3 : MetricSpace R] → [inst_4 : Zero R] → MetricSpace (ContinuousMapZero α R)
-- Mathlib.Data.Finset.Fold
Finset.fold_op_rel_iff_or : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {r : β → β → Prop},
  (∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z) → ∀ {c : β}, r c (Finset.fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
-- Mathlib.Data.Nat.Find
Nat.le_find_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ), n ≤ Nat.find h ↔ ∀ m < n, ¬p m
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- The identity functor on a site is cocontinuous.  -/
CategoryTheory.isCocontinuous_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Functor.id C).IsCocontinuous J J
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Removes the given declaration from `s`.  -/
Lean.Meta.Grind.SymbolPriorities.erase : Lean.Meta.Grind.SymbolPriorities → Lean.Name → Lean.Meta.Grind.SymbolPriorities
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite_of_lt : ∀ {n k : ℕ}, n < k → (Polynomial.hermite n).coeff k = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeAdjunction.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  PresheafOfModules.freeAdjunction R =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := fun x x_1 => PresheafOfModules.freeHomEquiv, homEquiv_naturality_left_symm := ⋯,
        homEquiv_naturality_right := ⋯ }
-- Std.Do.Triple.SpecLemmas
/-- Creates a cursor at the end of the list.
The prefix is the entire list and the suffix is empty.
 -/
List.Cursor.end : {α : Type u_1} → (l : List α) → l.Cursor
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.ext : ∀ {A : Type u_1} {inst : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {x y : hI.SubDPIdeal},
  x.carrier = y.carrier → x = y
-- Mathlib.Order.WellFounded
acc_def : ∀ {α : Sort u_1} {r : α → α → Prop} {a : α}, Acc r a ↔ ∀ (b : α), r b a → Acc r b
-- Init.Data.Vector.Algebra
Vector.add_assoc : ∀ {α : Type u_1} {n : ℕ} [inst : Add α],
  (∀ (x y z : α), x + y + z = x + (y + z)) → ∀ (xs ys zs : Vector α n), xs + ys + zs = xs + (ys + zs)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map.eq_1 : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (I : Ideal R), Ideal.map f I = Ideal.span (⇑f '' ↑I)
-- Mathlib.Data.Set.Image
Set.canLift : ∀ {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p],
  CanLift (Set α) (Set β) (fun x => c '' x) fun s => ∀ x ∈ s, p x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.neg_pi_lt_toReal : ∀ (θ : Real.Angle), -Real.pi < θ.toReal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ) (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) → (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n)
  (x_2 : ℕ),
  x = Std.DTreeMap.Internal.Impl.leaf →
    x_1 = x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
        | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) ≍
        h_1 x_2
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_comp : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] (p : GroupSeminorm E) (f : F →* E),
  ⇑(p.comp f) = ⇑p ∘ ⇑f
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
/-- Map over the bundled structure  -/
CategoryTheory.Bundled.map : {c d : Type u → Type v} → ({α : Type u} → c α → d α) → CategoryTheory.Bundled c → CategoryTheory.Bundled d
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- Let `f : M₁ →ₗ[R] M₂` be an `R`-linear map
between modules `M₁` and `M₂` with bases `b₁` and `b₂` respectively.
Then `LinearMap.toMvPolynomial b₁ b₂ f` is the family of multivariate polynomials over `R`
that evaluates on an element `x` of `M₁` (represented on the basis `b₁`)
to the element `f x` of `M₂` (represented on the basis `b₂`).  -/
LinearMap.toMvPolynomial : {R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      {ι₁ : Type u_4} →
        {ι₂ : Type u_5} →
          [inst : CommRing R] →
            [inst_1 : AddCommGroup M₁] →
              [inst_2 : AddCommGroup M₂] →
                [inst_3 : Module R M₁] →
                  [inst_4 : Module R M₂] →
                    [Fintype ι₁] →
                      [Finite ι₂] →
                        [DecidableEq ι₁] →
                          Module.Basis ι₁ R M₁ → Module.Basis ι₂ R M₂ → (M₁ →ₗ[R] M₂) → ι₂ → MvPolynomial ι₁ R
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.coe_id : ∀ {X : Semigrp}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_eq_of_nat : ∀ {ι : Type u_2} [inst : Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_5}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] (n : ℕ),
  p = ↑n → ∀ (f : PiLp p β), ‖f‖ = (∑ i, ‖f.ofLp i‖ ^ n) ^ (1 / ↑n)
-- Init.Prelude
/-- `Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`. -/
Not : Prop → Prop
-- Mathlib.MeasureTheory.Measure.Regular
/-- The measure of an open set is the supremum of the measures of compact sets it contains.  -/
IsOpen.measure_eq_iSup_isCompact : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
  IsOpen U → ∀ (μ : MeasureTheory.Measure α) [μ.Regular], μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ K
-- Init.Tactics
/-- `subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
replacing the left side of the equality with the right, until no more progress can be made.
 -/
Lean.Parser.Tactic.substEqs : Lean.ParserDescr
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multispanIndex_snd : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T}
  (d : CompleteLattice.MulticoequalizerDiagram x u v) (x_1 : (CategoryTheory.Limits.MultispanShape.prod ι).L),
  d.multispanIndex.snd x_1 = CategoryTheory.homOfLE ⋯
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_uIcc : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.uIcc i j = Set.uIcc (Fin.castLE h i) (Fin.castLE h j)
-- Mathlib.Topology.Constructions
Topology.IsCoinducing.restrictPreimage_of_isOpen : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsCoinducing f → ∀ {s : Set Y}, IsOpen s → Topology.IsCoinducing (s.restrictPreimage f)
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is non-strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a b ≤ slope f c b`.  -/
map_le_lineMap_iff_slope_le_slope_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < (1 - r) * (b - a) →
    (f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
      slope f a b ≤ slope f ((AffineMap.lineMap a b) r) b)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (Std.TreeMap.Raw.ofList l cmp).size = l.length
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_nil : ∀ {α : Type u} {instOrd : Ord α},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty [] ⋯) =
    Std.DTreeMap.Internal.Impl.empty
-- Mathlib.Order.Interval.Set.Infinite
Set.Ioi_infinite : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a : α), (Set.Ioi a).Infinite
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {m : α → β} {f : Filter α},
  Filter.Tendsto m f Filter.atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.comp_id : ∀ {R : Type u} [inst : CommSemiring R] {N : Type u_2} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {P : Type u_3}
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (g : N →ₚₗ[R] P), g.comp PolynomialLaw.id = g
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst_assoc : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.Limits.pullback.snd f g))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationPullback f g)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) h)
-- Init.Data.UInt.Lemmas
UInt16.ofInt_add : ∀ (x y : ℤ), UInt16.ofInt (x + y) = UInt16.ofInt x + UInt16.ofInt y
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs : Hashable Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsTheta.sqrt : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ},
  f =Θ[l] g → 0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → (fun x => √(f x)) =Θ[l] fun x => √(g x)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Finset.summable_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} (s : Finset β), (Summable fun x => f ↑x) ↔ Summable f
-- Mathlib.Data.EReal.Operations
EReal.top_sub_coe : ∀ (x : ℝ), ⊤ - ↑x = ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_extend_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {γ : Type u_4} {g : γ → β},
  Function.Injective g → ∀ (f : γ → α), ∏' (y : β), Function.extend g f 1 y = ∏' (x : γ), f x
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_iInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X),
  (∀ (i : ι), StableUnderGeneralization (S i)) → StableUnderGeneralization (⋂ i, S i)
-- Mathlib.Topology.Algebra.Module.IsWeak
LinearMap.IsWeak.eq_induced : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {inst : CommSemiring 𝕜} {inst_1 : TopologicalSpace 𝕜}
  {inst_2 : AddCommMonoid E} {inst_3 : Module 𝕜 E} {inst_4 : AddCommMonoid F} {inst_5 : Module 𝕜 F}
  {t : TopologicalSpace E} {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [self : B.IsWeak],
  t = TopologicalSpace.induced (fun x1 x2 => (B x1) x2) Pi.topologicalSpace
-- Mathlib.Analysis.SpecificLimits.Basic
/-- For any positive `m : ℕ`, `((n % m : ℕ) : ℝ) / (n : ℝ)` tends to `0` as `n` tends to `∞`.  -/
tendsto_mod_div_atTop_nhds_zero_nat : ∀ {m : ℕ}, 0 < m → Filter.Tendsto (fun n => ↑(n % m) / ↑n) Filter.atTop (nhds 0)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.trans : ∀ {V : Type u_1} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ u₃ v₃ : V} {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂}
  {p₃ : G.Walk u₃ v₃}, p₁.IsSubwalk p₂ → p₂.IsSubwalk p₃ → p₁.IsSubwalk p₃
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β} {hc : k ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKey k hc = k
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Int.closure_eq_zmultiples : ∀ (a b : ℤ), AddSubgroup.closure {a, b} = AddSubgroup.zmultiples ↑(a.gcd b)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.con_le_iff : ∀ {G : Type u_1} [inst : Group G] {N M : Subgroup G} [inst_1 : N.Normal] [inst_2 : M.Normal],
  QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M
-- Mathlib.Data.Num.Lemmas
Num.addMonoid : AddMonoid Num
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMapLI_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (self : E [⋀^ι]→L[𝕜] F),
  ContinuousAlternatingMap.toContinuousMultilinearMapLI self = self.toContinuousMultilinearMap
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instMul.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M],
  AddMonoidAlgebra.instMul = { mul := AddMonoidAlgebra.mul' }