mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsOneApply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], IsOneApplyEqSelf (M₁ →L[R₁] M₁) M₁
-- Mathlib.Tactic.ProxyType
/-- Name to use for the declaration for a type that is `Equiv` to the given type.  -/
Mathlib.ProxyType.ProxyEquivConfig.proxyName : Mathlib.ProxyType.ProxyEquivConfig → Lean.Name
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- morphisms `X ⟶ Y` in the category identify morphisms `𝟙_ V ⟶ (X ⟶[V] Y)` in `V`  -/
CategoryTheory.EnrichedOrdinaryCategory.homEquiv : {V : Type u'} →
  {inst : CategoryTheory.Category.{v', u'} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u} →
        {inst_2 : CategoryTheory.Category.{v, u} C} →
          [self : CategoryTheory.EnrichedOrdinaryCategory V C] →
            {X Y : C} → (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] Y)
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.dart_edge_eq_mk'_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Upgrading a functor `E ⥤ C` to a functor `E ⥤ StructuredArrow X F` and composing with the
forgetful functor `StructuredArrow X F ⥤ C` recovers the original functor.  -/
CategoryTheory.Functor.toStructuredArrowCompProj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (G : CategoryTheory.Functor E C) →
              (X : D) →
                (F : CategoryTheory.Functor C D) →
                  (f : (Y : E) → X ⟶ F.obj (G.obj Y)) →
                    (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) →
                      (G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) ≅ G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLED_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : (a : α) × β a},
          Std.DTreeMap.Internal.Impl.getEntryLED k t₁ fallback = Std.DTreeMap.Internal.Impl.getEntryLED k t₂ fallback
-- Mathlib.RingTheory.Extension.Basic
/-- The underlying algebra of an extension.  -/
Algebra.Extension.Ring : {R : Type u} →
  {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S → Type w
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_mul : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrLeft_refl : ∀ {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → UniformSpace (X i)],
  UniformEquiv.piCongrLeft (Equiv.refl ι) = UniformEquiv.refl ((i : ι) → X i)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- Convergence in Lp implies convergence in measure.  -/
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  {f : ι → α → E} {g : α → E} [inst : NormedAddCommGroup E] {l : Filter ι},
  p ≠ 0 →
    (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
      MeasureTheory.AEStronglyMeasurable g μ →
        Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0) →
          MeasureTheory.TendstoInMeasure μ f l g
-- Mathlib.Analysis.Normed.Group.Basic
NormedGroup.nhds_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), (nhds x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y⁻¹ * x‖ < ε}
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic : ∀ {K : Type u_1} [inst : Field K] (f : Polynomial K) {a : K},
  Polynomial.X - Polynomial.C a ∣ f /ₘ (Polynomial.X - Polynomial.C a) →
    Polynomial.X - Polynomial.C a ∣ Polynomial.derivative f
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.instIsIsoδ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
-- Std.Time.Format.Modifier
/-- `M`: Month of year as number or text (e.g., 7, 07, Jul, July, J).
 -/
Std.Time.Modifier.M : Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If `N` acts continuously and ergodically on `X` and `M` acts minimally on `N`,
then the corresponding action of `M` on `X` is ergodic.  -/
ErgodicSMul.trans_isMinimal : ∀ {M : Type u_1} {X : Type u_2} [inst : Monoid M] [inst_1 : SMul M X] [inst_2 : TopologicalSpace X] [R1Space X]
  [inst_4 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] (N : Type u_3) [inst_8 : MulAction M N] [inst_9 : Monoid N] [inst_10 : TopologicalSpace N]
  [MulAction.IsMinimal M N] [inst_12 : MulAction N X] [IsScalarTower M N X] [ContinuousSMul N X] [ErgodicSMul N X μ],
  ErgodicSMul M X μ
-- Mathlib.Data.Set.Insert
Set.singleton_injective : ∀ {α : Type u_1}, Function.Injective singleton
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The third morphism of a triangle, as a natural
transformation `π₃ ⟶ π₁ ⋙ shiftFunctor _ (1 : ℤ)`.  -/
CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Pretriangulated.Triangle.π₃ ⟶
        CategoryTheory.Pretriangulated.Triangle.π₁.comp (CategoryTheory.shiftFunctor C 1)
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness of intermediate fields is preserved by algebra homomorphisms.  -/
IntermediateField.LinearDisjoint.map : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B →
    ∀ {K : Type u_1} [inst_3 : Field K] [inst_4 : Algebra F K] (f : E →ₐ[F] K),
      (IntermediateField.map f A).LinearDisjoint ↥(IntermediateField.map f B)
-- Mathlib.RingTheory.SimpleModule.Isotypic
eq_isotypicComponent_iff : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S] [IsSemisimpleModule R M] {m : Submodule R M},
  m ≠ ⊥ → (m = isotypicComponent R M S ↔ IsIsotypicOfType R (↥m) S ∧ m.IsFullyInvariant)
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderBot.ofIic.eq_1 : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : DecidableEq α] (finsetIci : α → Finset α)
  (mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ x ≤ a),
  LocallyFiniteOrderBot.ofIic α finsetIci mem_Ici =
    { finsetIio := fun a => {x ∈ finsetIci a | a ≠ x}, finsetIic := finsetIci, finset_mem_Iic := mem_Ici,
      finset_mem_Iio := ⋯ }
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.doubleCoset_union_rightCoset : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (a : G),
  ⋃ k, MulOpposite.op (a * ↑k) • ↑H = DoubleCoset.doubleCoset a ↑H ↑K
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.nontrivial : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → Nontrivial V
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel (β × α) γ` from a `Kernel (α × β) γ` by taking the comap of `Prod.swap`.  -/
ProbabilityTheory.Kernel.swapLeft : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel (α × β) γ → ProbabilityTheory.Kernel (β × α) γ
-- Lean.Language.Basic
Lean.Language.instToSnapshotTreeTransformedSnap : {α : Type} → [Lean.Language.ToSnapshotTree α] → Lean.Language.ToSnapshotTree (Lean.Language.TransformedSnap α)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instEpiFunctorColonπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C), CategoryTheory.Epi (Φ.colonπ Ψ)
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
convexOn_rpow_left : ∀ {b : ℝ}, 0 < b → ConvexOn ℝ Set.univ fun x => b ^ x
-- Mathlib.Data.Matrix.Basis
Matrix.ext_addMonoidHom_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} {β : Type u_8} [inst : DecidableEq m] [inst_1 : DecidableEq n] [Finite m]
  [Finite n] [inst_4 : AddCommMonoid α] [inst_5 : AddCommMonoid β] {f g : Matrix m n α →+ β},
  f = g ↔ ∀ (i : m) (j : n), f.comp (Matrix.singleAddMonoidHom i j) = g.comp (Matrix.singleAddMonoidHom i j)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.isValue.inj : ∀ {bvarIdx : ℕ} {strict : Bool} {bvarIdx_1 : ℕ} {strict_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremConstraint.isValue bvarIdx strict =
      Lean.Meta.Grind.EMatchTheoremConstraint.isValue bvarIdx_1 strict_1 →
    bvarIdx = bvarIdx_1 ∧ strict = strict_1
-- Init.Data.SInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 64-bit signed integers. Usually accessed via
the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so `Int64.complement a = -(a + 1)`.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.complement : Int64 → Int64
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_eq_top : ∀ {α : Type u} [inst : Add α] {x y : WithTop α}, x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
-- Mathlib.Algebra.Module.SpanRankOperations
TensorProduct.spanFinrank_top_eq_of_residueField : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [inst_3 : IsLocalRing R], N.FG → ⊤.spanFinrank = N.spanFinrank
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
/-- A preradical `Φ` is idempotent if `Φ.r ⋙ Φ.r ≅ Φ.r`.  -/
CategoryTheory.Abelian.Preradical.IsIdempotent : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Abelian.Preradical C → Prop
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instNoZeroDivisors : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [NoZeroDivisors A]
  [inst_3 : Module R A] [inst_4 : Star A] (S : NonUnitalStarSubalgebra R A), NoZeroDivisors ↥S
-- Std.Time.DateTime.WallTime
/-- Duration since `1970-01-01T00:00:00` in local (civil) time.
 -/
Std.Time.WallTime.val : Std.Time.WallTime → Std.Time.Duration
-- Mathlib.Algebra.Order.Field.Basic
lt_of_one_div_lt_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 1 / a < 1 / b → b < a
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mk_neg : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M} (ha : a ≠ 0),
  FiniteArchimedeanClass.mk (-a) ⋯ = FiniteArchimedeanClass.mk a ha
-- Mathlib.Data.List.Sym
List.sym2.eq_1 : ∀ {α : Type u_1}, [].sym2 = []
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.continuous_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsEmbedding g → (Continuous f ↔ Continuous (g ∘ f))
-- Lean.Expr
Lean.Expr.lam.injEq : ∀ (binderName : Lean.Name) (binderType body : Lean.Expr) (binderInfo : Lean.BinderInfo) (binderName_1 : Lean.Name)
  (binderType_1 body_1 : Lean.Expr) (binderInfo_1 : Lean.BinderInfo),
  (Lean.Expr.lam binderName binderType body binderInfo = Lean.Expr.lam binderName_1 binderType_1 body_1 binderInfo_1) =
    (binderName = binderName_1 ∧ binderType = binderType_1 ∧ body = body_1 ∧ binderInfo = binderInfo_1)
-- Mathlib.Algebra.Category.FGModuleCat.Abelian
FGModuleCat.instAbelian : {k : Type u} → [inst : Ring k] → [IsNoetherianRing k] → CategoryTheory.Abelian (FGModuleCat k)
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.mkNoindexAnnotation : Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- If for all `θ : ℝⁿ`, `‖f (torusMap c R θ)‖` is less than or equal to a constant `C : ℝ`, then
`‖∯ x in T(c, R), f x‖` is less than or equal to `(2 * π)^n * (∏ i, |R i|) * C`  -/
norm_torusIntegral_le_of_norm_le_const : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ}
  {R : Fin n → ℝ} {C : ℝ},
  (∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C) →
    ‖∯ (x : Fin n → ℂ) in T(c, R), f x‖ ≤ ((2 * Real.pi) ^ n * ∏ i, |R i|) * C
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.mk.inj : ∀ {ty : Option Q(Lean.Expr)} {fvarId : Lean.FVarId} {userName : Lean.Name} {ty_1 : Option Q(Lean.Expr)}
  {fvarId_1 : Lean.FVarId} {userName_1 : Lean.Name},
  { ty := ty, fvarId := fvarId, userName := userName } = { ty := ty_1, fvarId := fvarId_1, userName := userName_1 } →
    ty = ty_1 ∧ fvarId = fvarId_1 ∧ userName = userName_1
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.sInter_subset_sInter`. -/
Set.sInter_mono : ∀ {α : Type u_1} {S T : Set (Set α)}, S ⊆ T → ⋂₀ T ⊆ ⋂₀ S
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer.0.CategoryTheory.Limits.WalkingMultispan.instFinCategoryOfLOfDecidableEqR.match_4.eq_1 : ∀ {J : CategoryTheory.Limits.MultispanShape}
  (motive :
    (b : J.R) →
      (a : J.L) →
        (CategoryTheory.Limits.WalkingMultispan.left a ⟶ CategoryTheory.Limits.WalkingMultispan.right b) →
          J.fst a = b → J.snd a = b → Sort u_3)
  (a : J.L) (h₁ : J.fst a = J.fst a) (h₂ : J.snd a = J.fst a)
  (h_1 :
    (a : J.L) →
      (h₁ : J.fst a = J.fst a) →
        (h₂ : J.snd a = J.fst a) → motive (J.fst a) a (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) h₁ h₂)
  (h_2 :
    (a : J.L) →
      (h₁ : J.fst a = J.snd a) →
        (h₂ : J.snd a = J.snd a) → motive (J.snd a) a (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) h₁ h₂),
  (match J.fst a, a, CategoryTheory.Limits.WalkingMultispan.Hom.fst a, h₁, h₂ with
    | .(J.fst a), a, CategoryTheory.Limits.WalkingMultispan.Hom.fst .(a), h₁, h₂ => h_1 a h₁ h₂
    | .(J.snd a), a, CategoryTheory.Limits.WalkingMultispan.Hom.snd .(a), h₁, h₂ => h_2 a h₁ h₂) =
    h_1 a h₁ h₂
-- Mathlib.RepresentationTheory.Character
FDRep.char_dual : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] (V : FDRep k G) (g : G),
  (FDRep.of (Representation.dual V.ρ)).character g = V.character g⁻¹
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddCommMonoidCoeOfAddSubmonoidClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddCommMonoid (R i)] →
              [∀ (i : ι), AddSubmonoidClass (S i) (R i)] →
                AddCommMonoid (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)),
  t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑(ProjectiveSpectrum.vanishingIdeal t)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashSet.Raw.ofList l).isEmpty = l.isEmpty
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    (∀ a ∈ t, (List.map Sigma.fst l).contains a = false) → (t.insertMany l).size = t.size + l.length
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.union : ∀ {𝕜 : 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'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  HasMFDerivAt[s] f x f' → HasMFDerivAt[t] f x f' → HasMFDerivAt[s ∪ t] f x f'
-- Mathlib.Topology.Defs.Induced
/-- `WithTopology.ofTopology` and `WithTopology.toTopology` as an equivalence.  -/
WithTopology.equiv : (X : Type u_1) → (t : TopologicalSpace X) → WithTopology X t ≃ X
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.smul_trans : ∀ {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {G : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : Module S V]
  [inst_6 : ContinuousConstSMul S V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : Module S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddCommMonoid G] [inst_13 : Module R G]
  [inst_14 : TopologicalSpace G] [inst_15 : Module S G] [inst_16 : ContinuousConstSMul S G]
  [inst_17 : SMulCommClass R S W] [inst_18 : SMul S R] [inst_19 : IsScalarTower S R V] [inst_20 : IsScalarTower S R W]
  [inst_21 : SMulCommClass R S V] [inst_22 : IsScalarTower S R G] (α : Sˣ) (e : G ≃L[R] V) (f : V ≃L[R] W),
  (α • e).trans f = α • e.trans f
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.neg_to_not : ∀ (a : Bool), (¬a = true) = ((!a) = true)
-- Mathlib.MeasureTheory.Covering.LiminfLimsup
/-- Given a sequence of subsets `sᵢ` of a metric space, together with a sequence of radii `rᵢ`
such that `rᵢ → 0`, the set of points which belong to infinitely many of the closed
`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a uniformly locally doubling measure if
the `rᵢ` are all scaled by a positive constant.

This lemma is a generalisation of Lemma 9 appearing on page 217 of
[J.W.S. Cassels, *Some metrical theorems in Diophantine approximation. I*](cassels1950).

See also `blimsup_thickening_mul_ae_eq`.

NB: The `: Set α` type ascription is present because of
https://github.com/leanprover-community/mathlib/issues/16932.  -/
blimsup_cthickening_mul_ae_eq : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  (s : ℕ → Set α) {M : ℝ},
  0 < M →
    ∀ (r : ℕ → ℝ),
      Filter.Tendsto r Filter.atTop (nhds 0) →
        Filter.blimsup (fun i => Metric.cthickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ]
          Filter.blimsup (fun i => Metric.cthickening (r i) (s i)) Filter.atTop p
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.whiskerEquiv_inv : ∀ {J : Type w} {K : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f] [inst_3 : CategoryTheory.Limits.HasBiproduct g],
  (CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv =
    CategoryTheory.Limits.biproduct.desc fun k =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (w (e.symm k)).hom (CategoryTheory.Limits.biproduct.ι f (e.symm k)))
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁}
              (CategoryTheory.MonoidalCategory.DayFunctor C V)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_of_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsUnit a → UniqueFactorizationMonoid.radical a = 1
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_subtype : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), ⇑s.subtype = Subtype.val
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatterer_mono : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)}, 𝒜 ⊆ ℬ → 𝒜.shatterer ⊆ ℬ.shatterer
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapMap.eq_1 : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p] (j : J),
  CategoryTheory.GradedObject.mapMap φ p j =
    X.descMapObj p fun i hi => CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hi)
-- Mathlib.Algebra.Order.Module.Pointwise
lowerBounds_smul_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : GroupWithZero α] [inst_3 : Zero β]
  [inst_4 : MulActionWithZero α β] [PosSMulMono α β] [PosSMulReflectLE α β] {s : Set β} {a : α},
  0 < a → lowerBounds (a • s) = a • lowerBounds s
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {K : CategoryTheory.Precoverage C}
  (ι : C → Type (max u_1 u_2))
  (motive : (x : C) → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι x → Sort u_3) (x : C)
  (R : CategoryTheory.Presieve x) (hR : R ∈ K.coverings x)
  (h : ⦃W : C⦄ → (r : W ⟶ x) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W)
  (h_1 : (X : C) → (i : ι X) → motive X (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X i))
  (h_2 :
    (x Y : C) →
      (f : x ⟶ Y) →
        (i : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y) →
          motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i))
  (h_3 :
    (x : C) →
      (R : CategoryTheory.Presieve x) →
        (hR : R ∈ K.coverings x) →
          (h : ⦃W : C⦄ → (r : W ⟶ x) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W) →
            motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h)),
  (match x, CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h with
    | X, CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ .(X) i => h_1 X i
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i => h_2 x Y f i
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h => h_3 x R hR h) =
    h_3 x R hR h
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.satAssignment_inr : ∀ {x : ℕ} {aig : Std.Sat.AIG ℕ} {assign1 : ℕ → Bool} (h : x < aig.decls.size),
  Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1 x =
    ⟦assign1, { aig := aig, ref := { gate := x, invert := false, hgate := h } }⟧