mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EToCycles_i_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.EToCycles_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.EToCycles_i._auto_3) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂₃ n₁) h) =
    CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) h)
-- Mathlib.LinearAlgebra.Dimension.Finrank
CommSemiring.finrank_self : ∀ (R : Type u_1) [inst : CommSemiring R], Module.finrank R R = 1
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {V W : HopfAlgCat R} {x y : V.Hom W}, x = y ↔ x.toBialgHom' = y.toBialgHom'
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
vectorSpan_prod_le : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s : Set P) (t : Set Q), vectorSpan k (s ×ˢ t) ≤ (vectorSpan k s).prod (vectorSpan k t)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T) (x : R) (y : ↥M),
  (IsLocalization.map Q g hy) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (g x) ⟨g ↑y, ⋯⟩
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_interpolate_lt : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
  Set.InjOn v ↑s → ((Lagrange.interpolate s v) r).degree < ↑s.card
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mul_pos : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] (a b : ℤ√↑d), 0 < a → 0 < b → 0 < a * b
-- Mathlib.Order.Filter.Extr
IsMinOn.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → ∀ {g : β → γ}, Monotone g → IsMinOn (g ∘ f) s a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a}, m.WF → (Std.DHashMap.Raw.map f m).isEmpty = m.isEmpty
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `f a ≤ B a`;
* `B` has derivative `B'` everywhere on `ℝ`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
  is bounded above by a function `f'`;
* we have `f' x < B' x` whenever `f x = B x`.

Then `f x ≤ B x` everywhere on `[a, b]`.  -/
image_le_of_liminf_slope_right_lt_deriv_boundary : ∀ {f f' : ℝ → ℝ} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) →
      ∀ {B B' : ℝ → ℝ},
        f a ≤ B a →
          (∀ (x : ℝ), HasDerivAt B (B' x) x) →
            (∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
EuclideanGeometry.Sphere.coe_secondInter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (as : AffineSubspace ℝ P) [inst_4 : Nonempty ↥as] (s : EuclideanGeometry.Sphere ↥as)
  (p : ↥as) (v : ↥as.direction), ↑(s.secondInter p v) = { center := ↑s.center, radius := s.radius }.secondInter ↑p ↑v
-- Mathlib.Logic.Function.Basic
Function.Involutive.leftInverse_iff : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → ∀ {g : α → α}, Function.LeftInverse g f ↔ g = f
-- Init.Data.UInt.Lemmas
UInt16.mul_comm : ∀ (a b : UInt16), a * b = b * a
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.coe_toHomUnits : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : Monoid M] (f : G →* M) (g : G), ↑(f.toHomUnits g) = f g
-- Std.Data.Internal.List.Associative
Std.Internal.List.find?_map_eq_none_iff_containsKey_eq_false : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {k : α},
  List.find? (fun x => x.1 == k) (List.map (fun x => (x.fst, x.snd)) l) = none ↔
    Std.Internal.List.containsKey k l = false
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (b b_1 : β),
          b = b_1 →
            Std.ExtDHashMap.Const.getThenInsertIfNew? m a b = Std.ExtDHashMap.Const.getThenInsertIfNew? m_1 a_1 b_1
-- Mathlib.NumberTheory.FLT.Four
/-- a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` must have `a` and `b` coprime.  -/
Fermat42.coprime_of_minimal : ∀ {a b c : ℤ}, Fermat42.Minimal a b c → IsCoprime a b
-- Mathlib.Combinatorics.Matroid.Basic
/-- Every independent subset `I` of a set `X` for is contained in a maximal independent
subset of `X`.  -/
Matroid.maximality : ∀ {α : Type u_1} (self : Matroid α), ∀ X ⊆ self.E, Matroid.ExistsMaximalSubsetProperty self.Indep X
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_inv : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G]
  [inst_2 : DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G), ⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.smul_isLittleO : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedRing R] [inst_3 : NormedDivisionRing 𝕜'] {f' : α → E'}
  {g' : α → F'} {l : Filter α} [inst_4 : Module R E'] [IsBoundedSMul R E'] [inst_6 : Module 𝕜' F'] [NormSMulClass 𝕜' F']
  {k₁ : α → R} {k₂ : α → 𝕜'}, k₁ =O[l] k₂ → f' =o[l] g' → (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ_def : ∀ (s : ℂ), s.Gammaℝ = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2)
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.coe_zpow : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (x : ↥H)
  (n : ℤ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.cech_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y),
  U.cech.map f = U.mapPower (SimplexCategory.Hom.toOrderHom f.unop).toFun
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeS_codRestrict : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σS : Type u_2}
  [inst_2 : SetLike σS S] [inst_3 : SubsemiringClass σS S] {f : R →+* S} {s : σS} {h : ∀ (x : R), f x ∈ s},
  (f.codRestrict s h).rangeS = Subsemiring.comap (SubsemiringClass.subtype s) f.rangeS
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp_assoc : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (w : C) {x y z : D} (f : x ⟶ y) (g : y ⟶ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj w z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w
        (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w g)
        h)
-- Mathlib.Algebra.Module.Presentation.Cokernel
_private.Mathlib.Algebra.Module.Presentation.Cokernel.0.Module.Presentation.cokernelRelations.match_1.splitter : {A : Type u_4} →
  [inst : Ring A] →
    {M₂ : Type u_5} →
      [inst_1 : AddCommGroup M₂] →
        [inst_2 : Module A M₂] →
          (pres₂ : Module.Presentation A M₂) →
            {ι : Type u_2} →
              (motive : pres₂.R ⊕ ι → Sort u_6) →
                (x : pres₂.R ⊕ ι) → ((r : pres₂.R) → motive (Sum.inl r)) → ((i : ι) → motive (Sum.inr i)) → motive x
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- Variant of `fourδ₂Toδ₁` for preorders.  -/
CategoryTheory.ComposableArrows.fourδ₂Toδ₁' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ i₄ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            (hi₃₄ : i₃ ≤ i₄) →
              CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE ⋯)
                  (CategoryTheory.homOfLE hi₃₄) ⟶
                CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃)
                  (CategoryTheory.homOfLE hi₃₄)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.toLinearMap : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoid B] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A →ₗc[R] B) → A →ₗ[R] B
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.of_lanLift_comp_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} {h : x ⟶ c}
  [inst_2 : CategoryTheory.Bicategory.HasLeftKanLift f (CategoryTheory.CategoryStruct.comp h g)]
  (i :
    CategoryTheory.Bicategory.lanLift f (CategoryTheory.CategoryStruct.comp h g) ≅
      CategoryTheory.CategoryStruct.comp h (CategoryTheory.Bicategory.lanLift f g)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f (CategoryTheory.CategoryStruct.comp h g))
        (CategoryTheory.Bicategory.whiskerRight i.hom f) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.Bicategory.lanLiftUnit f g))
        (CategoryTheory.Bicategory.associator h (CategoryTheory.Bicategory.lanLift f g) f).inv →
    CategoryTheory.Bicategory.LanLift.CommuteWith f g h
-- Mathlib.Algebra.QuaternionBasis
/-- A quaternion basis contains the information both sufficient and necessary to construct an
`R`-algebra homomorphism from `ℍ[R,c₁,c₂,c₃]` to `A`; or equivalently, a surjective
`R`-algebra homomorphism from `ℍ[R,c₁,c₂,c₃]` to an `R`-subalgebra of `A`.

Note that for definitional convenience, `k` is provided as a field even though `i_mul_j` fully
determines it.  -/
QuaternionAlgebra.Basis : {R : Type u_1} → (A : Type u_2) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → R → R → R → Type u_2
-- Mathlib.Data.ENNReal.Operations
ENNReal.ofReal_sub : ∀ (p : ℝ) {q : ℝ}, 0 ≤ q → ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₀.Exact
-- Mathlib.Algebra.Category.Ring.Topology
/-- If `A ≅ B`, then `Hom(A, R)` is homeomorphic to `Hom(B, R)`.  -/
CommRingCat.HomTopology.precompHomeomorph : {R A B : CommRingCat} → [inst : TopologicalSpace ↑R] → (A ≅ B) → (B ⟶ R) ≃ₜ (A ⟶ R)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.comp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [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] {f : E →L[R] F} [inst_7 : TopologicalSpace G] [inst_8 : AddCommMonoid G] [inst_9 : Module R G]
  {g : F →L[R] G}, g.HasRightInverse → f.HasRightInverse → (g ∘SL f).HasRightInverse
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flip_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.flip.root = P.coroot
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Finset.Lattice.Fold
Finset.toDual_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β) (f : β → α),
  OrderDual.toDual (s.inf f) = s.sup (⇑OrderDual.toDual ∘ f)
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
MeasureTheory.IsHahnDecomposition.measurableSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsHahnDecomposition μ ν s → MeasurableSet s
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.pos : ∀ {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α}, (Ordnode.node s l x r).Sized → 0 < s
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.ιObj_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g : CategoryTheory.Arrow C} (φ : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιObj I κ f.hom)
      (CategoryTheory.SmallObject.objMap I κ φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left φ) (CategoryTheory.SmallObject.ιObj I κ g.hom)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isTangent_of_mem_tangentSet : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : EuclideanGeometry.Sphere P},
  as ∈ s.tangentSet → s.IsTangent as
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ},
  0 ≤ R → (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖(2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Slow.instDecidableOrdered : {α : Type u_1} →
  (cmp : α → α → Ordering) → [Std.TransCmp cmp] → (t : RBTree.RBNode α) → Decidable (RBTree.RBNode.Ordered cmp t)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions.mk.sizeOf_spec : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions) (resolveProvider? : Option Bool),
  sizeOf { toWorkDoneProgressOptions := toWorkDoneProgressOptions, resolveProvider? := resolveProvider? } =
    1 + sizeOf toWorkDoneProgressOptions + sizeOf resolveProvider?
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_subtype_le : ∀ {α : Type u} (p : α → Prop), Cardinal.mk (Subtype p) ≤ Cardinal.mk α
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.const_apply : ∀ (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (p : P2) (q : P1), (AffineMap.const k P1 p) q = p
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup_dite_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} (p : β → Prop)
  [inst_2 : DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β},
  b ∈ s → ∀ (h₁ : ¬p b), g b h₁ ≤ s.sup fun i => if h : p i then f i h else g i h
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.multiplicativeClosure = W.multiplicativeClosure'
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- `cyclotomic n ℤ` is irreducible.  -/
Polynomial.cyclotomic.irreducible : ∀ {n : ℕ}, 0 < n → Irreducible (Polynomial.cyclotomic n ℤ)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsMonHom.monoidHom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.IsMonHom.monoidHom (CategoryTheory.CategoryStruct.id M) X = MonoidHom.id (X ⟶ M)
-- Mathlib.Data.Sum.Order
Sum.Lex.toLexRelIsoLE_symm_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β], ⇑Sum.Lex.toLexRelIsoLE.symm = ⇑ofLex
-- Lean.Elab.InfoTree.Main
/-- Adds a node containing the `InfoTree`s generated by `x` to the `InfoTree`s in `m`.

If `x` succeeds and `mkInfo` yields an `Info`, the `InfoTree`s of `x` become subtrees of a node
containing the `Info` produced by `mkInfo`, which is then added to the `InfoTree`s in `m`.
If `x` succeeds and `mkInfo` yields an `MVarId`, the `InfoTree`s of `x` are discarded and a `hole`
node is added to the `InfoTree`s in `m`.
If `x` fails, the `InfoTree`s of `x` become subtrees of a node containing the `Info` produced by
`mkInfoOnError`, which is then added to the `InfoTree`s in `m`.

The `InfoTree`s in `m` are reset before `x` is executed and restored with the addition of a new tree
after `x` is executed.
 -/
Lean.Elab.withInfoContext' : {m : Type → Type} →
  [Monad m] →
    [Lean.Elab.MonadInfoTree m] →
      {α : Type} → [MonadFinally m] → m α → (α → m (Lean.Elab.Info ⊕ Lean.MVarId)) → m Lean.Elab.Info → m α
-- Mathlib.Data.Set.Lattice.Image
Set.seq_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} {u : Set β}, s.seq t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, f a ∈ u
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Families of power series which can be substituted  -/
MvPowerSeries.HasSubst : {σ : Type u_1} → {τ : Type u_4} → {S : Type u_5} → [CommRing S] → (σ → MvPowerSeries τ S) → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_iSup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Surjective ⇑f → ∀ (S : ι → Submonoid N), Submonoid.map f (⨆ i, Submonoid.comap f (S i)) = iSup S
-- Mathlib.Data.Finset.Card
Finset.card_eq_one : ∀ {α : Type u_1} {s : Finset α}, s.card = 1 ↔ ∃ a, s = {a}
-- Mathlib.RepresentationTheory.Basic
/-- The natural `k`-linear `G`-representation on `k[G]` induced by left multiplication in `G`.  -/
Representation.leftRegular : (k : Type u_1) → [inst : Semiring k] → (G : Type u_2) → [inst_1 : Monoid G] → Representation k G (MonoidAlgebra k G)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Small
CategoryTheory.CostructuredArrow.small_inverseImage_proj_of_locallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{v₁, v₁, u₁} P] [CategoryTheory.LocallySmall.{v₁, v₂, u₂} D],
  CategoryTheory.ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (CategoryTheory.CostructuredArrow.proj S T))
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.fintypeBot.eq_1 : ∀ {G : Type u_1} [inst : Group G], Subgroup.fintypeBot = { elems := {1}, complete := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Raw α fun x => Unit}, m₁.WF → m₂.WF → (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → m₁.Equiv m₂
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ofHom_id : ∀ {X : Type u} [inst : Group X], GrpCat.ofHom (MonoidHom.id X) = CategoryTheory.CategoryStruct.id (GrpCat.of X)
-- Mathlib.Order.Filter.Partial
Filter.rcomap'_rcomap' : ∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ) (l : Filter γ),
  Filter.rcomap' r (Filter.rcomap' s l) = Filter.rcomap' (r.comp s) l
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eval_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
  {l : Mathlib.Tactic.Module.NF R M} {x : M}, x = l.eval → ∀ (r : R), (r • l).eval = r • x
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_normalizer_closure_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {s : Set G},
  H ≤ Subgroup.normalizer ↑(Subgroup.closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ Subgroup.closure s
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.ofIdComp_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)),
  t.ofIdComp.right = t.lift
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.subset_shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)}, IsLowerSet ↑𝒜 → 𝒜 ⊆ 𝒜.shatterer
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.coinductiveFixpoint.sizeOf_spec : sizeOf Lean.Elab.PartialFixpointType.coinductiveFixpoint = 1
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `Cⁿ` within a set at a point as continuity within this set at this
point, and being `Cⁿ` in the corresponding extended chart in the target.  -/
contMDiffWithinAt_iff_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' (f x)) ∘ f) s x