mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Inversion.Basic
/-- Distance between the images of two points under an inversion.  -/
EuclideanGeometry.dist_inversion_inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x y : P},
  x ≠ c →
    y ≠ c →
      ∀ (R : ℝ),
        dist (EuclideanGeometry.inversion c R x) (EuclideanGeometry.inversion c R y) =
          R ^ 2 / (dist x c * dist y c) * dist x y
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.dvd_mul_right : ∀ {m n k : ℕ}, k.Coprime n → (k ∣ m * n ↔ k ∣ m)
-- Mathlib.Topology.Algebra.Order.Field
/-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_neg_atTop`.  -/
tendsto_pow_neg_atTop : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {n : ℕ}, n ≠ 0 → Filter.Tendsto (fun x => x ^ (-↑n)) Filter.atTop (nhds 0)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.IterM.toList_toTake : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β}, it.toTake.toList = it.toList
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.isoMk_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom))
      CategoryTheory.Oplax.LaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Oplax.LaxTrans.isoMk app naturality).inv.as.app a = (app a).inv
-- Mathlib.Algebra.CharP.Defs
ExpChar.exists_unique : ∀ (R : Type u_1) [inst : Ring R] [IsDomain R], ∃! q, ExpChar R q
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Reflective.toFull : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {R : CategoryTheory.Functor D C} [self : CategoryTheory.Reflective R], R.Full
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.mulDistribMulAction : {M : Type u_1} →
  {N : Type u_2} →
    {R : Type u_5} →
      [inst : Monoid R] →
        [inst_1 : Monoid M] →
          [inst_2 : Monoid N] → [MulDistribMulAction R M] → [MulDistribMulAction R N] → MulDistribMulAction R (M × N)
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Pi.instConvexSpaceForall : {R : Type u_2} →
  [inst : Semiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {ι : Type u_3} →
          {X : ι → Type u_4} → [(i : ι) → Convexity.ConvexSpace R (X i)] → Convexity.ConvexSpace R ((i : ι) → X i)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.symm_apply_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Equiv M N)
  (a : M), f.symm (f a) = a
-- Aesop.Rule.Name
Aesop.ScopeName.global.sizeOf_spec : sizeOf Aesop.ScopeName.global = 1
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.basisMatrix_eq_embeddingsMatrixReindex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.basisMatrix K =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(NumberField.integralBasis K) ∘ ⇑(NumberField.equivReindex K))
      (RingHom.equivRatAlgHom K ℂ)
-- Mathlib.Analysis.Normed.Module.Basic
NormedAlgebra.mk : {𝕜 : Type u_6} →
  {𝕜' : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedRing 𝕜'] →
        [toAlgebra : Algebra 𝕜 𝕜'] → (∀ (r : 𝕜) (x : 𝕜'), ‖r • x‖ ≤ ‖r‖ * ‖x‖) → NormedAlgebra 𝕜 𝕜'
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulR : Int.Internal.Linear.Expr → ℤ → Int.Internal.Linear.Expr
-- Mathlib.Topology.Hom.Open
instCoeTCContinuousOpenMapOfContinuousOpenMapClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : FunLike F α β] → [ContinuousOpenMapClass F α β] → CoeTC F (α →CO β)
-- Init.Data.Array.DecidableEq
/-- Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
 -/
Array.instDecidableEmpEq : {α : Type u_1} → (ys : Array α) → Decidable (#[] = ys)
-- Mathlib.Analysis.Convex.Mul
ConvexOn.smul'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F}
  [IsOrderedModule 𝕜 E],
  ConvexOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → AntivaryOn f g s → ConcaveOn 𝕜 s (f • g)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.exists_mem_sup : ∀ {N : Type u_4} [inst : CommMonoid N] {P : N → Prop} {s t : Submonoid N},
  (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instReprExpr.repr : Lean.Grind.Linarith.Expr → ℕ → Std.Format
-- Mathlib.Data.Rel
SetRel.isTrans_inter : ∀ {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsTrans] [R₂.IsTrans], (R₁ ∩ R₂).IsTrans
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.continuousLinearEquivalence_comp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] [inst_7 : TopologicalSpace F'] [inst_8 : AddCommMonoid F'] [inst_9 : Module R F']
  {f : E →L[R] F} {g : F ≃L[R] F'}, f.HasRightInverse → (↑g ∘SL f).HasRightInverse
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.zero_natPow : ∀ {b : ℕ}, Nat.pow 0 b.succ = 0
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, DifferentiableAt 𝕜 (g i) x) →
    fderiv 𝕜 (fun x => ∏ i ∈ u, g i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderiv 𝕜 (g i) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → List.Pairwise (fun a b => (a.fst == b.fst) = false) (↑m).toList
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.neg_pi_div_two_lt_arctan : ∀ (x : ℝ), -(Real.pi / 2) < Real.arctan x
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_toUInt32 : ∀ (n : UInt8), n.toUInt32.toUInt16 = n.toUInt16
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelSemigroup α],
  AddOpposite.instAddLeftCancelSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, toIsLeftCancelAdd := ⋯ }
-- Init.Data.Iterators.Basic
/-- Currently, `Shrink α` is just a wrapper around `α`.

In the future, `Shrink` should allow shrinking `α` into a potentially smaller universe,
given a proof that `α` is actually small, just like Mathlib's `Shrink`, except that
the latter's conversion functions are noncomputable. Until then, `Shrink α` is always in the
same universe as `α`.

This no-op type exists so that fewer breaking changes will be needed when the
real `Shrink` type is available and the iterators will be made more flexible with regard to
universes.

The conversion functions `Shrink.deflate` and
`Shrink.inflate` form an equivalence between
`α` and `Shrink α`, but this equivalence is intentionally not definitional.
 -/
Std.Shrink : Type u → Type u
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.Location.mk'.sizeOf_spec : ∀ (startPosLine startPosCharacter endPosLine endPosCharacter : ℕ) (parentDecl : String),
  sizeOf
      { startPosLine := startPosLine, startPosCharacter := startPosCharacter, endPosLine := endPosLine,
        endPosCharacter := endPosCharacter, parentDecl := parentDecl } =
    1 + sizeOf startPosLine + sizeOf startPosCharacter + sizeOf endPosLine + sizeOf endPosCharacter + sizeOf parentDecl
-- Init.Core
Relation.TransGen.below : {α : Sort u} →
  {r : α → α → Prop} →
    {a : α} → {motive : (a_1 : α) → Relation.TransGen r a a_1 → Prop} → {a_1 : α} → Relation.TransGen r a a_1 → Prop
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.refl_symm_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (a : A), (CoalgEquiv.refl R A).symm a = a
-- Mathlib.Algebra.Star.Module
StarAddMonoid.toStarModuleRat : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : Module ℚ R] [inst_2 : StarAddMonoid R], StarModule ℚ R
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → Array α → Sort u_2) (x : α) (xs : List α) (n : ℕ) (acc : Array α)
  (h_1 : (x : ℕ) → (x_1 : Array α) → motive [] x x_1)
  (h_2 : (head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc)
  (h_3 : (x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc),
  (match x :: xs, n.succ, acc with
    | [], x, x_1 => h_1 x x_1
    | head :: xs, 0, acc => h_2 head xs acc
    | x :: xs, n.succ, acc => h_3 x xs n acc) =
    h_3 x xs n acc
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.isOpen_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (y : Y), IsOpen {x | f x = y}
-- Mathlib.Topology.Order
TopologicalSpace.mkOfClosure_sets : ∀ {α : Type u} {s : Set (Set α)} {hs : {u | TopologicalSpace.GenerateOpen s u} = s},
  TopologicalSpace.mkOfClosure s hs = TopologicalSpace.generateFrom s
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_insertIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ {a : α} {b : β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.insertIfNewₘ a b)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.right_distrib : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X ((a + b) * c) (a * c + b * c)
-- Mathlib.Topology.LocallyConstant.Basic
/-- The map is locally constant.  -/
LocallyConstant.isLocallyConstant : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] (self : LocallyConstant X Y), IsLocallyConstant self.toFun
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.componentComplMk_mem_hom : ∀ {V : Type u} {K L : Set V} (G : SimpleGraph V) {v : V} (vK : v ∉ K) (h : L ⊆ K),
  v ∈ SimpleGraph.ComponentCompl.hom h (G.componentComplMk vK)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittOne_zero_eq_one : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittOne p 0 = 1
-- Mathlib.Topology.UrysohnsLemma
/-- Urysohn's lemma: if `s` and `t` are two disjoint closed sets in a normal topological space `X`,
then there exists a continuous function `f : X → ℝ` such that

* `f` equals zero on `s`;
* `f` equals one on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
 -/
exists_continuous_zero_one_of_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s → IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toAlternatingMap_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], Function.Injective ContinuousAlternatingMap.toAlternatingMap
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- If a set of points in an affine subspace is cospherical, then its image under the coercion
to the ambient space is cospherical.  -/
EuclideanGeometry.Cospherical.subtype_val : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {S : AffineSubspace ℝ P} [Nonempty ↥S] {ps : Set ↥S},
  EuclideanGeometry.Cospherical ps → EuclideanGeometry.Cospherical (Subtype.val '' ps)
-- Mathlib.Tactic.FieldSimp
/-- `field` is a `simp` set that clears denominators in (semi-)field (in)equalities.

The `field` simp set is a variant of the `field_simp` tactic. The latter operates recursively on
subexpressions, bringing every field-expression encountered to the form `n / d`, and then attempts
to clear the denominator. (For confluence reasons, the `field` simprocs also have a slightly
different normal form from `field_simp`'s.)

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression,
by repeatedly taking products or divisors. The discharger can be non-universal, i.e. can be specific
to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is known,
etc). See `field_simp_discharge` for full details of the discharger algorithm.

* `simp [field, t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for
  nonzeroness/positivity proofs.

Examples:
```
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
    (x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
  simp only [field]
  -- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
```
 -/
fieldLe : Lean.Meta.Simp.Simproc
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.seq1.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forget_obj : ∀ (C : CategoryTheory.Cat), CategoryTheory.ReflQuiv.forget.obj C = CategoryTheory.ReflQuiv.of ↑C
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The minimal tensor product is less than or equal to the maximal tensor product.  -/
PointedCone.minTensorProduct_le_maxTensorProduct : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  (C₁ : PointedCone R G) (C₂ : PointedCone R H), C₁.minTensorProduct C₂ ≤ C₁.maxTensorProduct C₂
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Raised.add_left : ∀ (k : ℕ) {n m : ℕ}, Ordnode.Raised n m → Ordnode.Raised (k + n) (k + m)
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instToFormat : {α : Type u_1} → [Std.ToFormat α] → Std.ToFormat (Ordnode α)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mul_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), I.mul J = I * J
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_eq_of_ne : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] {i i' : ι},
  i' ≠ i → ∀ (x : M i), Pi.mulSingle i x i' = 1
-- Init.Data.List.Lex
List.lex.eq_1 : ∀ {α : Type u} [inst : BEq α] (lt : α → α → Bool) (head : α) (tail : List α), [].lex (head :: tail) lt = true
-- Init.Data.SInt.Lemmas
ISize.sub_neg : ∀ {a b : ISize}, a - -b = a + b
-- Lean.Parser.Extra
Lean.Parser.symbol.parenthesizer : String → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}, ProbabilityTheory.evariance 0 μ = 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftComp_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (hl' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l'.app X.left) X.hom))
  (hll' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp l l').app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftComp R l l' hl hl' hll').hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_add : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x y : WithVal v), (x + y).ofVal = x.ofVal + y.ofVal
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey?.isSome = true
-- Mathlib.Analysis.Convex.MetricSpace
/-- When `X` is a bounded convex metric space, to check continuity of
`t ↦ f(t) • x(t) + (1 - f(t)) • y(t)` it suffices to show that `f` is continuous,
`x` is continuous away from `f(t) = 0`, and `y` is continuous away from `f(t) = 1`.  -/
Convexity.continuous_convexCombPair' : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] [BoundedSpace X]
  {T : Type u_3} [inst_4 : TopologicalSpace T] (f : T → ℝ),
  Continuous f →
    ∀ (hf0 : ∀ (t : T), 0 ≤ f t) (hf1 : ∀ (t : T), f t ≤ 1) (x y : T → X),
      ContinuousOn x (f ⁻¹' {0}ᶜ) →
        ContinuousOn y (f ⁻¹' {1}ᶜ) → Continuous fun i => Convexity.convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.unitOfList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α], Std.ExtDHashMap.Const.unitOfList [] = ∅
-- Std.Internal.Do.WP.Frame
/-- If `wp x` is conjunctive, then `x` frames `(F ⊓ ·)` when `F` holds before and after running `x`.  -/
Std.Internal.Do.WP.Frames.of_wp_conjunctive : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred]
  [Std.Internal.Do.WPConjunctive Prog Value Pred EPred] {x : Prog} {F : Pred},
  (∀ (E : EPred), Lean.Order.PartialOrder.rel F (Std.Internal.Do.wp x (fun x => F) E)) →
    Std.Internal.Do.WP.Frames (fun x1 x2 => Lean.Order.meet x1 x2) x F
-- Mathlib.Data.Stream.Init
Stream'.get_zip : ∀ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' β),
  (Stream'.zip f s₁ s₂).get n = f (s₁.get n) (s₂.get n)
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
closure_range_zpow_eq_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G),
  closure (Set.range fun x_1 => x ^ x_1) = closure (Set.range fun x_1 => x ^ x_1)
-- Mathlib.Order.Lex
ofLex_inj : ∀ {α : Type u_1} {a b : Lex α}, ofLex a = ofLex b ↔ a = b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `StructuredArrow.map` is a special case of `StructuredArrow.map₂` up to natural isomorphism.  -/
CategoryTheory.StructuredArrow.mapIsoMap₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : CategoryTheory.Functor C D} →
          {S S' : D} →
            (f : S ⟶ S') →
              CategoryTheory.StructuredArrow.map f ≅
                CategoryTheory.StructuredArrow.map₂ f (CategoryTheory.CategoryStruct.id T)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.mkCone_π_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none)
  (π : (j : J) → X ⟶ F.obj (some j))
  (w :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (π j) (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) = f)
  (j : CategoryTheory.Limits.WidePullbackShape J),
  (CategoryTheory.Limits.WidePullbackShape.mkCone f π w).π.app j =
    match j with
    | none => f
    | some j => π j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.union.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t₁ t₁_1 : Std.DTreeMap.Internal.Impl α β) (e_t₁ : t₁ = t₁_1)
  (t₂ t₂_1 : Std.DTreeMap.Internal.Impl α β) (e_t₂ : t₂ = t₂_1) (h₁ : t₁.Balanced) (h₂ : t₂.Balanced),
  t₁.union t₂ h₁ h₂ = t₁_1.union t₂_1 ⋯ ⋯
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a division monoid if `β` is a division monoid.  -/
FunLike.divisionMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Inv F] →
                [inst_5 : Div F] →
                  [inst_6 : Pow F ℤ] →
                    [inst_7 : DivisionMonoid β] →
                      [IsOneApply F α β] →
                        [IsMulApply F α β] →
                          [IsInvApply F α β] →
                            [IsDivApply F α β] → [IsPowApply ℕ F α β] → [IsPowApply ℤ F α β] → DivisionMonoid F
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.mk.inj : ∀ {name : Lean.Name} {scope : Aesop.ScopeName} {builders : Array Aesop.BuilderName} {phases : Array Aesop.PhaseName}
  {name_1 : Lean.Name} {scope_1 : Aesop.ScopeName} {builders_1 : Array Aesop.BuilderName}
  {phases_1 : Array Aesop.PhaseName},
  { name := name, scope := scope, builders := builders, phases := phases } =
      { name := name_1, scope := scope_1, builders := builders_1, phases := phases_1 } →
    name = name_1 ∧ scope = scope_1 ∧ builders = builders_1 ∧ phases = phases_1
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage_le_coverEntropyEntourage : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X),
  Dynamics.coverEntropyInfEntourage T F U ≤ Dynamics.coverEntropyEntourage T F U
-- Init.Data.SInt.Bitwise
Int32.xor_left_inj : ∀ {a b : Int32} (c : Int32), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.Algebra.Order.Field.Basic
div_le_one_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → (a / b ≤ 1 ↔ b ≤ a)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCancelMonoidOfMulOpposite : {M : Type u_1} → [CancelMonoid Mᵐᵒᵖ] → CancelMonoid Mᵈᵐᵃ