mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsCofibrantI : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_4 : CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood],
  HomotopicalAlgebra.IsCofibrant P.I
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : Z₂₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp v₁₃ (CategoryTheory.CategoryStruct.comp self.m₃ h) =
    CategoryTheory.CategoryStruct.comp v₂₃ h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {v : β}, (k, v) ∈ Std.DTreeMap.Const.toList t ↔ Std.DTreeMap.Const.get? t k = some v
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_trailing_coeff' : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → (Polynomial.trinomial k m n u v w).coeff k = u
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_max_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (hc : k ∈ t),
  (cmp k (t.max ⋯)).isLE = true
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousCore_mono : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜],
  Monotone (Ideal.homogeneousCore 𝒜)
-- Mathlib.RingTheory.HahnSeries.Basic
/-- The map of Hahn series induced by applying a zero-preserving map to each coefficient.  -/
HahnSeries.map : {Γ : Type u_1} →
  {R : Type u_3} →
    {S : Type u_4} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero R] →
          [inst_2 : Zero S] →
            HahnSeries Γ R → {F : Type u_5} → [inst_3 : FunLike F R S] → [ZeroHomClass F R S] → F → HahnSeries Γ S
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.post : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMat__obj_fintype : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C),
  (F.mapMat_.obj M).fintype = M.fintype
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior_subset_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n), s.interior ⊆ s.closedInterior
-- Mathlib.Algebra.Ring.Subsemiring.Basic
SubsemiringClass.instCharZero : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [hSR : SubsemiringClass S R] (s : S)
  [CharZero R], CharZero ↥s
-- Lean.Meta.Match.Basic
/-- Convert a expression occurring as the argument of a `match` motive application back into a `Pattern`
For example, we can use this method to convert `x::y::xs` at
```
...
(motive : List Nat → Sort u_1) (xs : List Nat) (h_1 : (x y : Nat) → (xs : List Nat) → motive (x :: y :: xs))
...
```
into a pattern object
 -/
Lean.Meta.Match.toPattern : Lean.Expr → Lean.MetaM Lean.Meta.Match.Pattern
-- Init.Data.Nat.Lemmas
Nat.div_eq_iff_eq_mul_left : ∀ {a b c : ℕ}, 0 < b → b ∣ a → (a / b = c ↔ a = c * b)
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_init : ∀ {M : Type u_2} [inst : AddMonoid M] {n : ℕ} {f : Fin (n + 1) → M} (i : Fin (n + 1)),
  Fin.partialSum (Fin.init f) i = Fin.partialSum f i.castSucc
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.isCentralScalar : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] [inst_5 : SMul Sᵐᵒᵖ R]
  [inst_6 : SMul Sᵐᵒᵖ M] [inst_7 : IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M], IsCentralScalar S ↥p
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.dualEquiv_functor : PartOrdEmb.dualEquiv.functor = PartOrdEmb.dual
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.assoc_comp_δ : ∀ {G : Type v} [inst : Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  ((↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y)
                (Representation.linearize k G Z))).comp
          (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z)
            (Representation.LinearizeMonoidal.δ X Y))).comp
      (Representation.LinearizeMonoidal.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) =
    ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X)
              (Representation.LinearizeMonoidal.δ Y Z)).comp
          (Representation.LinearizeMonoidal.δ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))).comp
      (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ),
  TensorProduct.map f g ^ n = TensorProduct.map (f ^ n) (g ^ n)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
cfcₙ_norm_nonneg : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A]
  [inst_2 : TopologicalSpace A] [inst_3 : Module 𝕜 A] [inst_4 : StarRing A] [inst_5 : PartialOrder A]
  [StarOrderedRing A] [inst_7 : IsScalarTower 𝕜 A A] [inst_8 : SMulCommClass 𝕜 A A]
  [inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A), 0 ≤ cfcₙ (fun x => ↑‖f x‖) a
-- Mathlib.Order.Partition.Basic
/-- There is a unique partition of `⊥`.  -/
Partition.instUniqueBot : {α : Type u_1} → [inst : CompleteLattice α] → Unique (Partition ⊥)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The pullback functor for categories of sheaves of modules over schemes.  -/
AlgebraicGeometry.Scheme.Modules.pullback : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → CategoryTheory.Functor Y.Modules X.Modules
-- Lean.Meta.Tactic.NormCast
/-- `addInfer decl` infers the label of `decl` (`elim`, `move`, or `squash`) and arranges for it to
be used by `norm_cast`.

* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
 -/
Lean.Meta.NormCast.addInfer : Lean.Name → optParam Lean.AttributeKind Lean.AttributeKind.global → optParam ℕ 1000 → Lean.MetaM Unit
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_rco_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n - m).toNat → (m...n).toList.getD i fallback = m + ↑i
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- When `[WellPowered C]` and `[HasWidePullbacks C]`, `Subobject A` has arbitrary infimums.
 -/
CategoryTheory.Subobject.sInf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasWidePullbacks C] →
          {A : C} → Set (CategoryTheory.Subobject A) → CategoryTheory.Subobject A
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.integerComplement_add_ne_zero : ∀ {x : ℂ}, x ∈ Complex.integerComplement → ∀ (a : ℤ), x + ↑a ≠ 0
-- Mathlib.Topology.ContinuousOn
ContinuousAt.comp_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ},
  ContinuousAt g (f x) → ContinuousWithinAt f s x → ContinuousWithinAt (g ∘ f) s x
-- Mathlib.Algebra.Notation.Defs
One.instNonempty : ∀ {α : Type u} [One α], Nonempty α
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with left composition by continuous linear maps.  -/
ContDiffAt.laplacian_CLM_comp_left_nhds : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E} {l : F →L[ℝ] G},
  ContDiffAt ℝ 2 f x → Laplacian.laplacian (⇑l ∘ f) =ᶠ[nhds x] ⇑l ∘ Laplacian.laplacian f
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.add_eq_eval₁ : ∀ {R : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : SMul R M] (a₁ : R × M) {a₂ : R × M}
  {l₁ l₂ l : Mathlib.Tactic.Module.NF R M},
  l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval → (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The divided power algebra of a module M is defined as the ring quotient of the polynomial ring
in the variables `ℕ × M` by the ring relation defined by `DividedPowerAlgebra.Rel`.
We will later show that that `DividedPowerAlgebra R M` has divided powers.
It satisfies a weak universal property for morphisms to rings with divided powers.  -/
DividedPowerAlgebra : (R : Type u_2) →
  (M : Type u_3) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_2 u_3)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.topEquiv_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : ↥⊤),
  Subalgebra.topEquiv a = ↑a
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.Monic.mem_nonZeroDivisors : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R}, p.Monic → p ∈ nonZeroDivisors (Polynomial R)
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A function on `ℍ` which is invariant under an arithmetic subgroup of `GL(2, ℝ)`, and satisfies
an `O((im τ) ^ t)` bound at all cusps for some `0 ≤ t`, is in fact uniformly bounded by a multiple
of `(max (im τ) (1 / im τ)) ^ t`.  -/
ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ},
      0 ≤ t →
        (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
            (fun τ => f (g • τ)) =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) →
          ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic],
            (∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) →
              ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
-- Mathlib.Tactic.Lift
Subtype.exists_pi_extension : ∀ {ι : Sort u_1} {α : ι → Sort u_2} [ne : ∀ (i : ι), Nonempty (α i)] {p : ι → Prop} (f : (i : Subtype p) → α ↑i),
  ∃ g, (fun i => g ↑i) = f
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.ind_aux : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (MvQPF.P F).A)
  (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α),
  MvQPF.Fix.mk (MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(MvQPF.P F).wMk a f' f⟧
-- Mathlib.GroupTheory.Perm.List
List.formPerm_pair : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α), [x, y].formPerm = Equiv.swap x y
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.induction_on : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  {φ : (i : ι) → H →* G i} {motive : Monoid.PushoutI φ → Prop} (x : Monoid.PushoutI φ),
  (∀ (i : ι) (g : G i), motive ((Monoid.PushoutI.of i) g)) →
    (∀ (h : H), motive ((Monoid.PushoutI.base φ) h)) →
      (∀ (x y : Monoid.PushoutI φ), motive x → motive y → motive (x * y)) → motive x
-- Mathlib.Logic.Equiv.PartialEquiv
/-- `Function.const` as a `PartialEquiv`.
It consists of two constant maps in opposite directions.  -/
PartialEquiv.single : {α : Type u_1} → {β : Type u_2} → α → β → PartialEquiv α β
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
/-- A predicate `C → Prop` on the objects of a category is closed under isomorphisms
if whenever `P X`, then all the objects `Y` that are isomorphic to `X` also satisfy `P Y`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyEntourage_monotone : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X), Monotone fun F => Dynamics.coverEntropyEntourage T F U
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.range_comp_le_range : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B]
  [inst_5 : NonUnitalNonAssocSemiring C] [inst_6 : Module R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C),
  NonUnitalAlgHom.range (g.comp f) ≤ NonUnitalAlgHom.range g
-- Mathlib.Computability.Ackermann
ack_injective_left : ∀ (n : ℕ), Function.Injective fun m => ack m n
-- Mathlib.GroupTheory.Focal
IsPGroup.powEquiv'.congr_simp : ∀ {p p_1 : ℕ} (e_p : p = p_1) {G : Type u_1} [inst : Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] {n n_1 : ℕ}
  (e_n : n = n_1) (hn : ¬p ∣ n), hG.powEquiv' hn = ⋯.powEquiv' ⋯
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_pow_le_of_le : ∀ {R : Type u} {m : ℕ} [inst : Semiring R] {p : Polynomial R} (n : ℕ), p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m
-- Mathlib.Order.ULift
ULift.instPartialOrder : {α : Type u} → [PartialOrder α] → PartialOrder (ULift.{v, u} α)
-- Lean.Data.Lsp.CodeActions
/-- The diagnostics that this code action resolves.  -/
Lean.Lsp.CodeAction.diagnostics? : Lean.Lsp.CodeAction → Option (Array Lean.Lsp.Diagnostic)
-- Mathlib.Order.Hom.Bounded
TopHom.instSemilatticeSup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β],
  TopHom.instSemilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_pair : ∀ {α : Type u} {x y : α} [inst : PseudoMetricSpace α], Metric.diam {x, y} = dist x y
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- Promote an equality to an isomorphism of `Under.map` functors.  -/
CategoryTheory.MorphismProperty.Under.mapCongr : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          [inst_2 : P.IsStableUnderComposition] →
            [Q.RespectsIso] →
              {X Y : T} →
                {f g : X ⟶ Y} →
                  (hfg : f = g) →
                    (hf : P f) →
                      CategoryTheory.MorphismProperty.Under.map Q hf ≅ CategoryTheory.MorphismProperty.Under.map Q ⋯
-- Mathlib.Tactic.FunProp.Types
/-- Log error message that will displayed to the user at the end.

Messages are logged only when `transitionDepth = 0` i.e. when `fun_prop` is **not** trying to infer
function property like continuity from another property like differentiability.
The main reason is that if the user forgets to add a continuity theorem for function `foo` then
`fun_prop` should report that there is a continuity theorem for `foo` missing. If we would log
messages `transitionDepth > 0` then user will see messages saying that there is a missing theorem
for differentiability, smoothness, ... for `foo`.  -/
Mathlib.Meta.FunProp.logError : String → Mathlib.Meta.FunProp.FunPropM Unit
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.idToMonad : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m], Std.Internal.LawfulMonadLiftFunction Std.Internal.idToMonad
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_zero : ∀ {x : ℝ}, Irrational x → x ≠ 0
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.instDecidableEqPartition.decEq : {n : ℕ} → (x x_1 : n.Partition) → Decidable (x = x_1)
-- Init.Data.Rat.Lemmas
Rat.floor_sub_one : ∀ {x : ℚ}, (x - 1).floor = x.floor - 1
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Embedding.to_isUniformEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [u : UniformSpace β] (f : α → β)
  (h : Topology.IsEmbedding f), IsUniformEmbedding f
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.GammaIntegral_conj : ∀ (s : ℂ), ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_ne_zero : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G ≠ 0 ↔ AddMonoid.ExponentExists G
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a field element is always at least `1`.  -/
Height.one_le_mulHeight₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K), 1 ≤ Height.mulHeight₁ x
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.allM : {α : Type u_1} →
  [inst : BEq α] →
    {m : Type → Type u_2} →
      [Monad m] → (α → m Bool) → (s : Aesop.UnorderedArraySet α) → optParam ℕ 0 → optParam ℕ s.size → m Bool
-- Mathlib.Algebra.Star.SelfAdjoint
IsUnit.isSelfAdjoint_conjugate_iff : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {a u : R},
  IsUnit u → (IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a)
-- Mathlib.Data.Set.Lattice
Set.iUnion_inter_of_monotone : ∀ {ι : Type u_12} {α : Type u_13} [inst : Preorder ι] [IsDirectedOrder ι] {s t : ι → Set α},
  Monotone s → Monotone t → ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
-- Mathlib.CategoryTheory.Iso
/-- Identity isomorphism.  -/
CategoryTheory.Iso.refl : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → X ≅ X
-- Mathlib.Order.Filter.Bases.Basic
/-- View a filter as a filter basis.  -/
Filter.asBasis : {α : Type u_1} → Filter α → FilterBasis α
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.coe_dual_one : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B], ↑(FractionalIdeal.dual A K 1) = Submodule.traceDual A K 1
-- Init.Prelude
MonadExceptOf.mk : {ε : semiOutParam (Type u)} →
  {m : Type v → Type w} → ({α : Type v} → ε → m α) → ({α : Type v} → m α → (ε → m α) → m α) → MonadExceptOf ε m
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_top : ∀ {α : Type u_2} [inst : TopologicalSpace α], ↑⊤ = Set.univ
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames.mk : Bool → List Lean.Name → Lean.Meta.AltVarNames
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_natCast : ∀ (n : ℕ), Ordinal.lift.{u, v} ↑n = ↑n
-- Init.Data.Format.Basic
Std.Format.tag.injEq : ∀ (a : ℕ) (a_1 : Std.Format) (a_2 : ℕ) (a_3 : Std.Format),
  (Std.Format.tag a a_1 = Std.Format.tag a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Lean.Setup
Lean.ModuleSetup.mk.injEq : ∀ (name : Lean.Name) (package? : Option Lean.PkgId) (isModule : Bool) (imports? : Option (Array Lean.Import))
  (importArts : Lean.NameMap Lean.ImportArtifacts) (dynlibs : Array System.FilePath) (plugins : Array Lean.Plugin)
  (options : Lean.LeanOptions) (name_1 : Lean.Name) (package?_1 : Option Lean.PkgId) (isModule_1 : Bool)
  (imports?_1 : Option (Array Lean.Import)) (importArts_1 : Lean.NameMap Lean.ImportArtifacts)
  (dynlibs_1 : Array System.FilePath) (plugins_1 : Array Lean.Plugin) (options_1 : Lean.LeanOptions),
  ({ name := name, package? := package?, isModule := isModule, imports? := imports?, importArts := importArts,
        dynlibs := dynlibs, plugins := plugins, options := options } =
      { name := name_1, package? := package?_1, isModule := isModule_1, imports? := imports?_1,
        importArts := importArts_1, dynlibs := dynlibs_1, plugins := plugins_1, options := options_1 }) =
    (name = name_1 ∧
      package? = package?_1 ∧
        isModule = isModule_1 ∧
          imports? = imports?_1 ∧
            importArts = importArts_1 ∧ dynlibs = dynlibs_1 ∧ plugins = plugins_1 ∧ options = options_1)
-- Mathlib.Analysis.CStarAlgebra.lpSpace
instNonUnitalCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal : {I : Type u_1} → {A : I → Type u_2} → [inst : (i : I) → NonUnitalCStarAlgebra (A i)] → NonUnitalCStarAlgebra ↥(lp A ⊤)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_prod_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'}
  {k' : α → G'} {l : Filter α},
  Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k' ↔
    Asymptotics.IsBigOWith c l f' k' ∧ Asymptotics.IsBigOWith c l g' k'
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_top : ⊤⁻¹ = 0
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.complexOfFunctorsToFunctorToComplex_map_app_f : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3}
  {c : ComplexShape ι} {X Y : HomologicalComplex (CategoryTheory.Functor T V) c} (f : X ⟶ Y) (t : T) (i : ι),
  ((HomologicalComplex.complexOfFunctorsToFunctorToComplex.map f).app t).f i = (f.f i).app t
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_apply_eq_zero_of_restrict_le_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  μ.restrict s ≤ ν.restrict s → MeasurableSet s → (μ - ν) s = 0
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The shadow of a family of `r`-sets is a family of `r - 1`-sets.  -/
Set.Sized.shadow : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {r : ℕ}, Set.Sized r ↑𝒜 → Set.Sized (r - 1) ↑𝒜.shadow