mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The uniform equivalence `C(X, R)₀ ≃ᵤ C(Y, R)₀` induced by a homeomorphism of the domains
sending `0 : X` to `0 : Y`.  -/
UniformEquiv.arrowCongrLeft₀ : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : Zero R] →
          [inst_3 : UniformSpace R] →
            {Y : Type u_3} →
              [inst_4 : TopologicalSpace Y] →
                [inst_5 : Zero Y] → (f : X ≃ₜ Y) → f 0 = 0 → ContinuousMapZero X R ≃ᵤ ContinuousMapZero Y R
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toBitVec = BitVec.ofNat 64 n
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.F : {B : Type v} → B → CartanMatrix.Generators B
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.prod_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a : α}, a ≠ 0 → Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
-- Mathlib.GroupTheory.Focal
/-- The focal subgroup considered as a subgroup of `H`.
Note that `focalSubgroup H` is always contained in `H`.  -/
AddSubgroup.focalAddSubgroupOf : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → AddSubgroup ↥H
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mk.sizeOf_spec : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} [inst_4 : SizeOf E] [inst_5 : SizeOf F]
  (toFun : E → F) (contDiff' : ContDiff ℝ (↑n) toFun) (hasCompactSupport' : HasCompactSupport toFun)
  (tsupport_subset' : tsupport toFun ⊆ ↑Ω),
  sizeOf
      { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' } =
    1 + sizeOf contDiff'
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ),
  CategoryTheory.IsIso ((t.truncLT n).map f) ↔
    ∃ Z g h,
      ∃ (_ :
        CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) f) g h ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles),
        t.IsGE Z n
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form.  -/
Matrix.det_smul_inv_mulVec_eq_cramer : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α), IsUnit A.det → A.det • A⁻¹.mulVec b = A.cramer b
-- Batteries.Data.List.Lemmas
List.extractP.go.induct_unfolding : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (motive : List α → Array α → Option α × List α → Prop),
  (∀ (acc : Array α), motive [] acc (none, l)) →
    (∀ (x : α) (xs : List α) (acc : Array α), p x = true → motive (x :: xs) acc (some x, acc.toListAppend xs)) →
      (∀ (x : α) (xs : List α) (acc : Array α),
          p x = false →
            motive xs (acc.push x) (List.extractP.go p l xs (acc.push x)) →
              motive (x :: xs) acc (List.extractP.go p l xs (acc.push x))) →
        ∀ (a : List α) (a_1 : Array α), motive a a_1 (List.extractP.go p l a a_1)
-- Mathlib.Algebra.Group.Conj
IsAddConj.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] (a b : α), IsAddConj a b = ∃ c, AddSemiconjBy (↑c) a b
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is a regular measure, then any measurable set of finite measure can be approximated by a
compact subset. See also `MeasurableSet.exists_isCompact_lt_add` and
`MeasurableSet.exists_lt_isCompact_of_ne_top`.  -/
MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.Regular],
  μ.InnerRegularCompactLTTop
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toListRev_filter : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → Bool},
  (Std.Iter.filter f it).toListRev = List.filter f it.toListRev
-- Mathlib.Data.PNat.Prime
PNat.gcd_dvd_left : ∀ (n m : ℕ+), n.gcd m ∣ n
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.eq_mkNatTrans : ∀ {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]
  {F F' : CategoryTheory.Functor (CategoryTheory.Join C D) E} (α : F ⟶ F'),
  CategoryTheory.Join.mkNatTrans ((CategoryTheory.Join.inclLeft C D).whiskerLeft α)
      ((CategoryTheory.Join.inclRight C D).whiskerLeft α) ⋯ =
    α
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.smul_closure : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M] (a : α)
  (s : Set M), a • Submonoid.closure s = Submonoid.closure (a • s)
-- Mathlib.Order.Directed
OrderTop.instIsDirectedOrder : ∀ {α : Type u_1} [inst : LE α] [OrderTop α], IsDirectedOrder α
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
CategoryTheory.Abelian.epiWithInjectiveKernel_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], CategoryTheory.Abelian.epiWithInjectiveKernel f
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.quotientToQuotientRangePowQuotSuccAux.congr_simp : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  {i : ℕ} {a a_1 : S} (e_a : a = a_1) (a_mem : a ∈ P ^ i) (a_2 a_3 : S ⧸ P),
  a_2 = a_3 → p.quotientToQuotientRangePowQuotSuccAux P a_mem a_2 = p.quotientToQuotientRangePowQuotSuccAux P ⋯ a_3
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_uSizeToBitVec : ∀ (n : USize), { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedOrigin : Inhabited Lean.Meta.Origin
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.injective_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [T2Space β] {s : Set α},
  Dense s → Function.Injective (ContinuousMap.restrict s)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.congr_F : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  {Φ₁ Φ₂ : S₁ ⟶ S₂}, Φ₁ = Φ₂ → Φ₁.f = Φ₂.f
-- Mathlib.Data.Num.Lemmas
PosNum.cmp_to_nat : ∀ (m n : PosNum), Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.coskAdj.reflective : (n : ℕ) → CategoryTheory.Reflective (SSet.Truncated.cosk n)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.le_eq_cancel_le : ∀ {M : Type u_1} [inst : MonoidWithZero M] [inst_1 : PartialOrder M] [PosMulMono M] [PosMulReflectLE M]
  {e₁ e₂ f₁ f₂ L : M}, e₁ = L * f₁ → e₂ = L * f₂ → 0 < L → (e₁ ≤ e₂) = (f₁ ≤ f₂)
-- Mathlib.CategoryTheory.EpiMono
/-- The chosen retraction of a split monomorphism.  -/
CategoryTheory.retraction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (f : Y ⟶ X) → [hf : CategoryTheory.IsSplitMono f] → X ⟶ Y
-- Mathlib.Topology.Algebra.Constructions
Topology.IsInducing.addUnits_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : AddMonoid N] {f : M →+ N}, Topology.IsInducing ⇑f → Topology.IsInducing ⇑(AddUnits.map f)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.mk : Std.Mutex Std.Http.Body.Channel.State✝ → Std.Http.Body.Stream
-- Mathlib.Order.Monotone.Defs
monotone_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {c : β}, Monotone fun x => c
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.convexSpaceSelf : {R : Type u_2} →
  [inst : Semiring R] → [inst_1 : PartialOrder R] → [inst_2 : IsStrictOrderedRing R] → Convexity.ConvexSpace R R
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.exists_matchesAt_iff_eq_append : ∀ {pat : String} {s : String.Slice},
  (∃ pos, String.Slice.Pattern.Model.MatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat ++ t₂
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_neg_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : AddGroup α] [inst_1 : StarAddMonoid α] {A : Matrix n n α},
  (-A).IsHermitian ↔ A.IsHermitian
-- Mathlib.Condensed.Light.InternallyProjective
/-- `P : LightCondMod R` is internally projective if and
only if, for all `A B : LightCondMod R`, for all epimorphisms `e : A ⟶ B`, for all
`S : LightProfinite` and all morphisms `g : R[S] ⊗ P ⟶ B`, there exists a `S' : LightProfinite`
with a surjection `π : S' ⟶ S` and a morphism `g' : R[S'] ⊗ P ⟶ A`, making the diagram
```
R[S'] ⊗ P --> A
  |           |
  v           v
R[S] ⊗ P  --> B
```
commute.
 -/
LightCondensed.internallyProjective_iff_tensor_condition' : ∀ (R : Type u) [inst : CommRing R] (P : LightCondMod R),
  CategoryTheory.InternallyProjective P ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : CategoryTheory.MonoidalCategoryStruct.tensorObj ((LightCondensed.free R).obj S.toCondensed) P ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π) P)
                g =
              CategoryTheory.CategoryStruct.comp g' e
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Rci α → Std.DTreeMap.Internal.RciSliceData α β
-- Lean.Meta.Tactic.Apply
/-- Partitions the given mvars in to two arrays (non-deps, deps)
according to whether the given mvar depends on other mvars in the array. -/
_private.Lean.Meta.Tactic.Apply.0.Lean.Meta.partitionDependentMVars : Array Lean.Expr → Lean.MetaM (Array Lean.MVarId × Array Lean.MVarId)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotal_map_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂)
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
  {Z : C} (h_1 : (L.total c₁₂).X i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h_1) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂)
      (CategoryTheory.CategoryStruct.comp (L.ιTotal c₁₂ i₁ i₂ i₁₂ h) h_1)
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- If `f` is torus integrable then `-f` is torus integrable.  -/
TorusIntegrable.neg : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ},
  TorusIntegrable f c R → TorusIntegrable (-f) c R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  (Std.ExtDHashMap.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- For every prepartition `π` of `I` there exists a prepartition that covers exactly
`I \ π.iUnion`.  -/
BoxIntegral.Prepartition.exists_iUnion_eq_sdiff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [Finite ι] (π : BoxIntegral.Prepartition I), ∃ π', π'.iUnion = ↑I \ π.iUnion
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.mk.injEq : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {S : C} (I₀ : Type w) (X : I₀ → C₀) (f : (i : I₀) → F.obj (X i) ⟶ S)
  (I₁ : I₀ → I₀ → Type w) (Y : ⦃i₁ i₂ : I₀⦄ → I₁ i₁ i₂ → C₀) (p₁ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₁)
  (p₂ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₂)
  (w :
    ∀ ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂),
      CategoryTheory.CategoryStruct.comp (F.map (p₁ j)) (f i₁) =
        CategoryTheory.CategoryStruct.comp (F.map (p₂ j)) (f i₂))
  (I₀_1 : Type w) (X_1 : I₀_1 → C₀) (f_1 : (i : I₀_1) → F.obj (X_1 i) ⟶ S) (I₁_1 : I₀_1 → I₀_1 → Type w)
  (Y_1 : ⦃i₁ i₂ : I₀_1⦄ → I₁_1 i₁ i₂ → C₀) (p₁_1 : ⦃i₁ i₂ : I₀_1⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ X_1 i₁)
  (p₂_1 : ⦃i₁ i₂ : I₀_1⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ X_1 i₂)
  (w_1 :
    ∀ ⦃i₁ i₂ : I₀_1⦄ (j : I₁_1 i₁ i₂),
      CategoryTheory.CategoryStruct.comp (F.map (p₁_1 j)) (f_1 i₁) =
        CategoryTheory.CategoryStruct.comp (F.map (p₂_1 j)) (f_1 i₂)),
  ({ I₀ := I₀, X := X, f := f, I₁ := I₁, Y := Y, p₁ := p₁, p₂ := p₂, w := w } =
      { I₀ := I₀_1, X := X_1, f := f_1, I₁ := I₁_1, Y := Y_1, p₁ := p₁_1, p₂ := p₂_1, w := w_1 }) =
    (I₀ = I₀_1 ∧ X ≍ X_1 ∧ f ≍ f_1 ∧ I₁ ≍ I₁_1 ∧ Y ≍ Y_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1)
-- Mathlib.Data.Finsupp.Basic
/-- The additive monoid isomorphism between `α × β →₀ M` and `α →₀ β →₀ M` given by
currying/uncurrying.  -/
Finsupp.curryAddEquiv : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : AddZeroClass M] → (α × β →₀ M) ≃+ (α →₀ β →₀ M)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_le_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalRing R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] {a : A} (ha : p a)
  {f g : ContinuousMapZero (↑(quasispectrum R a)) R}, (cfcₙHom ha) f ≤ (cfcₙHom ha) g ↔ f ≤ g
-- Init.Data.Vector.Lemmas
Vector.mem_dite_empty_right : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : p → Vector α 0},
  (x ∈ if h : p then xs h else #v[]) ↔ ∃ (h : p), x ∈ xs h
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map_denom_ne_zero : ∀ {K : Type u} [inst : Field K] {L : Type u_1} {F : Type u_2} [inst_1 : Zero L] [inst_2 : FunLike F (Polynomial K) L]
  [ZeroHomClass F (Polynomial K) L] (φ : F), Function.Injective ⇑φ → ∀ (f : RatFunc K), φ f.denom ≠ 0
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulLeft.eq_1 : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G] (c : G),
  IsometryEquiv.mulLeft c = { toEquiv := Equiv.mulLeft c, isometry_toFun := ⋯ }
-- Mathlib.Data.Finset.NAry
Finset.image₂_mk_eq_product : ∀ {α : Type u_1} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] (s : Finset α) (t : Finset β),
  Finset.image₂ Prod.mk s t = s ×ˢ t
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- Two `AddMonoidHom`s from an additive quotient group are equal
if their compositions with `AddQuotientGroup.mk'` are equal.

See note [partially-applied ext lemmas].  -/
QuotientAddGroup.addMonoidHom_ext : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  ⦃f g : G ⧸ N →+ M⦄, f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N) → f = g
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasurableEmbedding.integrableOn_map_iff : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace β] {e : α → β},
  MeasurableEmbedding e →
    ∀ {f : β → ε} {μ : MeasureTheory.Measure α} {s : Set β},
      MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ
-- Mathlib.Order.Filter.Basic
Filter.join_mono : ∀ {α : Type u} {f₁ f₂ : Filter (Filter α)}, f₁ ≤ f₂ → f₁.join ≤ f₂.join
-- Mathlib.Tactic.DepRewrite
/-- `rewrite!` is like `rewrite`,
but can also insert casts to adjust types that depend on the LHS of a rewrite.
It is available as an ordinary tactic and a `conv` tactic.

The sort of casts that are inserted is controlled by the `castMode` configuration option.
By default, only proof terms are casted;
by proof irrelevance, this adds no observable complexity.

With `rewrite! +letAbs (castMode := .all)`, casts are inserted whenever necessary.
This means that the 'motive is not type correct' error never occurs,
at the expense of creating potentially complicated terms.
 -/
Mathlib.Tactic.DepRewrite.Conv.depRewrite : Lean.ParserDescr
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.extremalEpi_coproductFrom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator →
    ∀ (X : C) [inst_1 : CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)],
      CategoryTheory.ExtremalEpi (P.coproductFrom X)
-- Mathlib.Analysis.Complex.Basic
Complex.mem_slitPlane_iff : ∀ {z : ℂ}, z ∈ Complex.slitPlane ↔ 0 < z.re ∨ z.im ≠ 0
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β},
  f = g ↔ ∀ (x_2 : α), f x_2 = g x_2
-- Init.Data.UInt.Bitwise
UInt32.xor_right_inj : ∀ {a b : UInt32} (c : UInt32), c ^^^ a = c ^^^ b ↔ a = b
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : Subtype p → α},
  BddBelow (Set.range f) → iInf f ≤ sInf ∅ → iInf f = ⨅ i, ⨅ (h : p i), f ⟨i, h⟩
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMul.contMDiff_mul : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Mul G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : ContMDiffMul I n G],
  ContMDiff (I.prod I) I n fun p => p.1 * p.2
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_self_add_left : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  (f + g).neLocus f = g.support
-- Mathlib.GroupTheory.Focal
/-- In the quotient `H / H*`, conjugation by any element of `G` preserves equivalence
classes. If `h ∈ H` and `g⁻¹ * h * g ∈ H`, then `g⁻¹hg ≡ h (mod H*)`.  -/
AddSubgroup.focalAddSubgroupOf.mk'_addConj_eq : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {h : G} (hh : h ∈ H) (g : G) (haddConj : -g + h + g ∈ H),
  (QuotientAddGroup.mk' H.focalAddSubgroupOf) ⟨-g + h + g, haddConj⟩ =
    (QuotientAddGroup.mk' H.focalAddSubgroupOf) ⟨h, hh⟩
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Cons.mk.sizeOf_spec : ∀ {eh : Type u} {et : Type v} [inst : SizeOf eh] [inst_1 : SizeOf et] (head : eh) (tail : et),
  sizeOf (EPost.Cons.mk✝ head tail) = 1 + sizeOf head + sizeOf tail
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.le_maximalIdeal_of_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] (p : Ideal R) [hp : p.IsPrime],
  p ≤ IsLocalRing.maximalIdeal R
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- The morphism `(X ⟶[V] Y) ⟶ (X ⟶[V] Y')` induced by a morphism `Y ⟶ Y'`.  -/
CategoryTheory.eHomWhiskerLeft : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] →
            (X : C) → {Y Y' : C} → (Y ⟶ Y') → ((X ⟶[V] Y) ⟶ X ⟶[V] Y')
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ},
  (CategoryTheory.CategoryStruct.id X).unmop = CategoryTheory.CategoryStruct.id X.unmop
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.instEvalExprCheapConfig.evalExpr : Lean.Expr → Lean.MetaM Convert.CheapConfig
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.appTop U.toSpecΓ =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom
      U.topIso.inv
-- Mathlib.Analysis.InnerProductSpace.Basic
parallelogram_law_with_norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E),
  ‖x + y‖ ^ 2 + ‖x - y‖ ^ 2 = 2 * (‖x‖ ^ 2 + ‖y‖ ^ 2)
-- Mathlib.Data.EReal.Inv
/-- Multiplicative inverse of an `EReal`. We choose `0⁻¹ = 0` to guarantee several good properties,
for instance `(a * b)⁻¹ = a⁻¹ * b⁻¹`.  -/
EReal.inv : EReal → EReal
-- Mathlib.GroupTheory.Sylow
Sylow.exists_comap_eq_of_injective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (P : Sylow p H) {f : H →* G},
  Function.Injective ⇑f → ∃ Q, Subgroup.comap f ↑Q = ↑P
-- Std.Sat.AIG.CNF
/-- The `State` invariant always holds when we have an empty CNF.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv_nil : ∀ {aig : Std.Sat.AIG ℕ}, Std.Sat.AIG.toCNF.State.Inv✝ aig Std.Sat.CNF.empty
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A simple graph `G` contains all `Subgraph G` coercions.  -/
SimpleGraph.Subgraph.coe_isContained : ∀ {V : Type u_1} {G : SimpleGraph V} (G' : G.Subgraph), G'.coe.IsContained G
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_of_mem_sphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x : P} {R : ℝ}, x ∈ Metric.sphere c R → EuclideanGeometry.inversion c R x = x
-- Init.Data.SInt.Lemmas
Int16.toInt32_ne_minValue : ∀ (a : Int16), a.toInt32 ≠ Int32.minValue
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_nonneg : ∀ {a : ENNReal}, 0 ≤ a.toReal
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.disjoint_splitLower_splitUpper : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ), Disjoint (I.splitLower i x) (I.splitUpper i x)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- The q-Expansion of normalised Eisenstein series of level one with `bernoulli` term.  -/
EisensteinSeries.q_expansion_bernoulli : ∀ {k : ℕ} (hk : 3 ≤ k),
  Even k →
    ∀ (z : UpperHalfPlane),
      (ModularForm.E hk) z =
        1 -
          2 * ↑k / ↑(bernoulli k) *
            ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).get k' h = cast ⋯ v
-- Mathlib.Order.Interval.Set.LinearOrder
Set.compl_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Iic a)ᶜ = Set.Ioi a