mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.surjective : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (d : F.WellOrderInductionData) [inst_2 : OrderBot J] [WellFoundedLT J],
  Function.Surjective ((fun s => s (Opposite.op ⊥)) ∘ Subtype.val)
-- Mathlib.Order.BooleanSubalgebra
/-- An induction principle for closure membership. If `p` holds for `⊥` and all elements of `s`, and
is preserved under suprema and complement, then `p` holds for all elements of the closure of `s`.  -/
BooleanSubalgebra.closure_bot_sup_induction : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α} {p : (g : α) → g ∈ BooleanSubalgebra.closure s → Prop},
  (∀ (x : α) (hx : x ∈ s), p x ⋯) →
    p ⊥ ⋯ →
      (∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s) (y : α) (hy : y ∈ BooleanSubalgebra.closure s),
          p x hx → p y hy → p (x ⊔ y) ⋯) →
        (∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s), p x hx → p xᶜ ⋯) →
          ∀ {x : α} (hx : x ∈ BooleanSubalgebra.closure s), p x hx
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
/-- Subalgebra of functions that are bounded at infinity.  -/
UpperHalfPlane.boundedAtImInftySubalgebra : (α : Type u_1) → [inst : NormedField α] → Subalgebra α (UpperHalfPlane → α)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.order_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : MulZeroOneClass R],
  HahnSeries.order 1 = 0
-- Mathlib.Data.Sum.Order
Sum.Lex.toLex_le_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α ⊕ β},
  toLex a ≤ toLex b ↔ Sum.Lex (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Eta rule for costructured arrows. Prefer `CostructuredArrow.eta` for rewriting, as equality of
objects tends to cause problems.  -/
CategoryTheory.CostructuredArrow.eq_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T),
  f = CategoryTheory.CostructuredArrow.mk f.hom
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.map_tmul : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : AddCommMonoid Q] [inst_7 : Module R M] [inst_8 : Module R N]
  [inst_9 : Module R P] [inst_10 : Module R Q] [inst_11 : Module S M] [inst_12 : IsScalarTower R S M]
  [inst_13 : Coalgebra S M] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] [inst_16 : Coalgebra S N]
  [inst_17 : Coalgebra R P] [inst_18 : Coalgebra R Q] (f : M →ₗc[S] N) (g : P →ₗc[R] Q) (x : M) (y : P),
  (Coalgebra.TensorProduct.map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y
-- Mathlib.Order.Heyting.Hom
BiheytingHom.toLatticeHom : {α : Type u_6} →
  {β : Type u_7} → [inst : BiheytingAlgebra α] → [inst_1 : BiheytingAlgebra β] → BiheytingHom α β → LatticeHom α β
-- Mathlib.Data.List.Cycle
Cycle.instCoeList : {α : Type u_1} → Coe (List α) (Cycle α)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_zsmul_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : AddGroup Z] [inst_4 : IsTopologicalAddGroup Z] (f : C(X × Y, Z)) (n : ℤ)
  (x : X), (n • f).curry x = n • f.curry x
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.instField : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : UniformSpace K] →
      [IsTopologicalDivisionRing K] →
        [CompletableTopField K] → [IsUniformAddGroup K] → Field (UniformSpace.Completion K)
-- Mathlib.Algebra.Order.Interval.Basic
instOneInterval : {α : Type u_2} → [inst : Preorder α] → [One α] → One (Interval α)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield_flatMap_pure : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ it₁' : Std.Iter β} {b : β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' b) →
    (Std.Iter.flatMapAfter f it₁ none).IsPlausibleStep (Std.IterStep.skip (Std.Iter.flatMapAfter f it₁' (some (f b))))
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.valuation_surjective : ∀ (K : Type u_1) [inst : Field K], Function.Surjective ⇑Valued.v
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The left-inverse of `algebraMap`.  -/
TensorAlgebra.algebraMapInv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorAlgebra R M →ₐ[R] R
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instLEOrdinal : LE Std.Time.Weekday.Ordinal
-- Mathlib.Order.Hom.Basic
OrderHom.uliftRightMap_coe_down : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (i : α),
  (f.uliftRightMap i).down = f i
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sep_subset : ∀ {x : ZFSet.{u_1}} {p : ZFSet.{u_1} → Prop}, ZFSet.sep p x ⊆ x
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_of_one_to_two : ∀ (f : { len := 1 } ⟶ { len := 2 }), (∃ i, f = SimplexCategory.δ i) ∨ ∃ a, f = { len := 1 }.const { len := 2 } a
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_sub : ∀ (a b : BitVec 8), Int8.ofBitVec (a - b) = Int8.ofBitVec a - Int8.ofBitVec b
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toAlgHom_ofComp_rename : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (p : P.Ring),
  (Q.ofComp P).toAlgHom ((MvPolynomial.rename Sum.inr) p) = MvPolynomial.C ((algebraMap P.Ring S) p)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommMonoidOfContinuousMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommMonoid β]
  [inst_3 : ContinuousMul β],
  ContinuousMap.instCommMonoidOfContinuousMul = { toMonoid := ContinuousMap.instMonoidOfContinuousMul, mul_comm := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_reverse : ∀ {w i : ℕ} {x : BitVec w}, x.reverse.getMsbD i = x.getLsbD i
-- Init.Tactics
/-- The `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 -/
Lean.Parser.Tactic.tacticHave__ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.toFinite_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α}, MeasureTheory.Measure.toFinite 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Real.differentiableOn_Gamma_Ioi : DifferentiableOn ℝ Real.Gamma (Set.Ioi 0)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply : ∀ (G : Type u_2) [inst : Group G] (n : ℕ) (v : ↑(Equiv.Perm.vectorsProdEqOne G (n + 1))),
  (Equiv.Perm.VectorsProdEqOne.vectorEquiv G n).symm v = (↑v).tail
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.map_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (K : Submodule 𝕜 E)
  (f : E →ₗᵢ[𝕜] F), Submodule.map f.toLinearMap Kᗮ = (Submodule.map f.toLinearMap K)ᗮ ⊓ f.range
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
List.formPerm_apply_mem_eq_next : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → ∀ (x : α) (hx : x ∈ l), l.formPerm x = l.next x hx
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsLeft_eq_right : ∀ (M₀ : Type u_2) [inst : CommMonoidWithZero M₀], nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.transnumAuxSeq_zero : ∀ (f : CircleDeg1Lift), f.transnumAuxSeq 0 = f 0
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_1 a a_1 f
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.val_singleSubSingle : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (r : R),
  ↑((LieAlgebra.SpecialLinear.singleSubSingle i j) r) = Matrix.single i i r - Matrix.single j j r
-- Mathlib.Order.Filter.Map
Filter.map_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β}, Filter.map m f = ⊥ ↔ f = ⊥
-- Lean.Util.CollectMVars
Lean.CollectMVars.State.mk : Lean.ExprSet → Array Lean.MVarId → Lean.CollectMVars.State
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_inverse_obj_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).left = X.left
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y')
  (f₁ f₂ : X' ⟶ Y'), f₁ + f₂ = CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂
-- Mathlib.Topology.Algebra.UniformConvergence
instModuleUniformFun : {α : Type u_1} →
  {β : Type u_2} →
    {R : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid β] → [Module R β] → Module R (UniformFun α β)
-- Mathlib.Algebra.Lie.Prod
/-- `Prod.map` of two Lie algebra homomorphisms.  -/
LieHom.prodMap : {R : Type u_1} →
  {L₁ : Type u_2} →
    {L₂ : Type u_3} →
      {L₃ : Type u_5} →
        {L₄ : Type u_6} →
          [inst : CommRing R] →
            [inst_1 : LieRing L₁] →
              [inst_2 : LieAlgebra R L₁] →
                [inst_3 : LieRing L₂] →
                  [inst_4 : LieAlgebra R L₂] →
                    [inst_5 : LieRing L₃] →
                      [inst_6 : LieAlgebra R L₃] →
                        [inst_7 : LieRing L₄] →
                          [inst_8 : LieAlgebra R L₄] → (L₁ →ₗ⁅R⁆ L₃) → (L₂ →ₗ⁅R⁆ L₄) → L₁ × L₂ →ₗ⁅R⁆ L₃ × L₄
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_substInvOfIsUnit_left : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R),
  PowerSeries.constantCoeff P = 0 →
    ∀ (hP' : IsUnit ((PowerSeries.coeff 1) P)), PowerSeries.subst P (P.substInvOfIsUnit hP') = PowerSeries.X
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDeriv_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {x : E},
  DifferentiableAt 𝕜 ω x →
    ∀ (v : Fin (n + 1) → E), (extDeriv ω x) v = ∑ i, (-1) ^ ↑i • (fderiv 𝕜 (fun x => (ω x) (i.removeNth v)) x) (v i)
-- Init.Core
/-- `insert x ∅ = {x}`  -/
LawfulSingleton.insert_empty_eq : ∀ {α : Type u} {β : Type v} {inst : EmptyCollection β} {inst_1 : Insert α β} {inst_2 : Singleton α β}
  [self : LawfulSingleton α β] (x : α), insert x ∅ = {x}
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (x x_1 : (n : ℕ) → X n ⟶ X (n + 1)),
  x = x_1 →
    ∀ (i j : ℕ) (a : i ≤ j),
      CategoryTheory.Functor.OfSequence.map x i j a = CategoryTheory.Functor.OfSequence.map x_1 i j a
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.isIso_of_source_target_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0), CategoryTheory.IsIso f
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- If `g` is an orientation reversing matrix with trace zero and `c ≠ 0`,
then its action on the upper half plane has a half-circle of fixed points.
In the hyperbolic geometry, this half-circle is a line.
If `c = 0`, then this line is a vertical half-line in the usual geometry,
see `gl_smul_eq_self_iff_re_eq`.  -/
UpperHalfPlane.gl_smul_eq_self_iff_dist_sq_eq : ∀ {g : GL (Fin 2) ℝ} {z : UpperHalfPlane},
  (↑g).det < 0 →
    (↑g).trace = 0 → ↑g 1 0 ≠ 0 → (g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2)
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.of.inj : ∀ {α : Type u} {isCommRing : CommRing α} {isTopologicalSpace : TopologicalSpace α}
  {isTopologicalRing : IsTopologicalRing α} {α_1 : Type u} {isCommRing_1 : CommRing α_1}
  {isTopologicalSpace_1 : TopologicalSpace α_1} {isTopologicalRing_1 : IsTopologicalRing α_1},
  TopCommRingCat.of α = TopCommRingCat.of α_1 →
    α = α_1 ∧ isCommRing ≍ isCommRing_1 ∧ isTopologicalSpace ≍ isTopologicalSpace_1
-- Mathlib.Algebra.Lie.Semisimple.Lemmas
LieAlgebra.trace_toEnd_eq_zero : ∀ {L : Type u_2} {M : Type u_3} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {R : Type u_4}
  [inst_3 : CommRing R] [inst_4 : LieAlgebra R L] [inst_5 : Module R M] [inst_6 : LieModule R L M] {s : Set L},
  (∀ x ∈ s, (LinearMap.trace R M) ((LieModule.toEnd R L M) x) = 0) →
    ∀ {x : L}, x ∈ LieSubalgebra.lieSpan R L s → (LinearMap.trace R M) ((LieModule.toEnd R L M) x) = 0
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `nontrivialTopology_iff_exists_nnnorm_ne_zero`. -/
NontrivialTopology.of_exists_nnnorm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (∃ x, ‖x‖₊ ≠ 0) → NontrivialTopology E
-- Mathlib.Data.Finset.Image
/-- A finset is nontrivial iff its image under a function injective on the finset is.  -/
Finset.image_nontrivial_iff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
  Set.InjOn f ↑s → ((Finset.image f s).Nontrivial ↔ s.Nontrivial)
-- Batteries.Data.Fin.Fold
Fin.dfoldlM_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] (f : Fin n → α → m α) (x : α),
  Fin.dfoldlM n (fun x => α) f x = Fin.foldlM n (fun x i => f i x) x
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget PartOrdEmb)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f]
  {t : CategoryTheory.Limits.PushoutCocone f f} (ht : CategoryTheory.Limits.IsColimit t), CategoryTheory.IsIso t.inl
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.MetrizableSpace.mk : ∀ {X : Type u_5} [t : TopologicalSpace X] [toPseudoMetrizableSpace : TopologicalSpace.PseudoMetrizableSpace X]
  [toT0Space : T0Space X], TopologicalSpace.MetrizableSpace X
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Lazy refined discrimination tree. It is an index from expressions to values of type `α`.

We store all of the nodes in one `Array`, `tries`, instead of using a 'normal' inductive type.
This is so that we can modify the tree globally, which is very useful when evaluating lazy
entries and saving the result globally.
 -/
Lean.Meta.RefinedDiscrTree : Type → Type
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) {X Y : B} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (x : Std.Sat.AIG.Decl α) →
      (x = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
        ((idx : α) → x = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx)) →
          ((lhs rhs : Std.Sat.AIG.Fanin) → x = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
            motive x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.restrict_carrier : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C)
  {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)), ↑(X.restrict h) = U
-- Init.Util
withPtrEq : {α : Type u} → (a b : α) → (k : Unit → Bool) → (a = b → k () = true) → Bool
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transEventuallyEqIsEquivalent : {α : Type u_1} →
  {β : Type u_2} →
    [inst : NormedAddCommGroup β] →
      {l : Filter α} → Trans l.EventuallyEq (Asymptotics.IsEquivalent l) (Asymptotics.IsEquivalent l)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_3 : HSub Std.Time.Nanosecond.Offset Std.Time.Hour.Offset Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.comp_toPrelaxFunctorStruct : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D),
  (F.comp G).toPrelaxFunctorStruct = F.comp G.toPrelaxFunctorStruct
-- Init.Data.SInt.Bitwise
ISize.toUSize_not : ∀ (a : ISize), (~~~a).toUSize = ~~~a.toUSize
-- Mathlib.NumberTheory.Bernoulli
bernoulliPowerSeries.eq_1 : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Algebra ℚ A],
  bernoulliPowerSeries A = PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli n / ↑n.factorial)
-- Batteries.Data.List.Lemmas
List.isChain_iff_pairwise : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} [Trans R R R], List.IsChain R l ↔ List.Pairwise R l
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- **Uniqueness of left-invariant measures**: In a second-countable locally compact group, any
σ-finite left-invariant measure is a scalar multiple of the Haar measure.
This is slightly weaker than assuming that `μ` is a Haar measure (in particular we don't require
`μ ≠ 0`).
See also `isMulLeftInvariant_eq_smul_of_regular`
for a statement not assuming second-countability.  -/
MeasureTheory.Measure.haarMeasure_unique : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SigmaFinite μ] [μ.IsMulLeftInvariant] (K₀ : TopologicalSpace.PositiveCompacts G),
  μ = μ ↑K₀ • MeasureTheory.Measure.haarMeasure K₀
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedSimpEntry : Inhabited Lean.Meta.SimpEntry
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_gcd_cert.eq_1 : ∀ (a b : ℤ) (p₂ p : Lean.Grind.CommRing.Poly) (k : ℤ) (v : Lean.Grind.CommRing.Mon) (p_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.add k v p_2) p₂ p = false
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.ext_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {w w' : CategoryTheory.TwoSquare T L R B},
  w = w' ↔ ∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the suprema and infima along a Galois coinsertion  -/
GaloisCoinsertion.liftLattice : {α : Type u} →
  {β : Type v} →
    {l : α → β} → {u : β → α} → [inst : PartialOrder β] → [inst_1 : Lattice α] → GaloisCoinsertion u l → Lattice β
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ} {r₁ : 𝕜}
  (s : Affine.Simplex 𝕜 P n) {p p₁o : P},
  p₁o ∈ affineSpan 𝕜 (Set.range s.points) →
    ↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑(s.orthogonalProjectionSpan p)) +ᵥ p₁o)) = p₁o