mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Oplax unity.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a).hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (self.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv h))
-- Mathlib.Order.Filter.Lift
Filter.lift'_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Nonempty ι] {f : ι → Filter α} {g : Set α → Set β},
  (∀ (s t : Set α), g (s ∩ t) = g s ∩ g t) → (iInf f).lift' g = ⨅ i, (f i).lift' g
-- Std.Time.Duration
/-- Subtracts a `Minute.Offset` from a `Duration`
 -/
Std.Time.Duration.subMinutes : Std.Time.Duration → Std.Time.Minute.Offset → Std.Time.Duration
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_eq_unop_limitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.colimitsOfShape J = (P.op.limitsOfShape Jᵒᵖ).unop
-- Mathlib.GroupTheory.Focal
AddSubgroup.map_focalAddSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  AddSubgroup.map H.subtype H.focalAddSubgroupOf = H.focalAddSubgroup
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.uniqueMDiffOn_image_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  n ≠ 0 → ∀ {s : Set M}, UniqueMDiff[s] → UniqueMDiff[⇑h '' s]
-- Mathlib.Analysis.Matrix.Hermitian
/-- A linear map is symmetric iff the corresponding matrix with an orthonormal basis is
Hermitian.  -/
LinearMap.isHermitian_toMatrix_iff : ∀ {n : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedAddCommGroup E] [inst_4 : InnerProductSpace 𝕜 E] {f : E →ₗ[𝕜] E} (b : OrthonormalBasis n 𝕜 E),
  ((LinearMap.toMatrix b.toBasis b.toBasis) f).IsHermitian ↔ f.IsSymmetric
-- Lean.Attributes
Lean.AttributeKind.scoped : Lean.AttributeKind
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_fst_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ) {Z : C}
  (h : K.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f p) h) =
    h
-- Mathlib.Data.Set.Lattice
Set.nonempty_iInter_Iic_iff : ∀ {α : Type u_1} {ι : Sort u_5} [inst : Preorder α] {f : ι → α}, (⋂ i, Set.Iic (f i)).Nonempty ↔ BddBelow (Set.range f)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
/-- Describes the counit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this
should give a map `M ⊗ Hom(M, N) ⟶ N`, so we flip the order of the arguments in the identity map
`Hom(M, N) ⟶ (M ⟶ N)` and uncurry the resulting map `M ⟶ Hom(M, N) ⟶ N.`  -/
ModuleCat.ihom_ev_app : ∀ {R : Type u} [inst : CommRing R] (M N : ModuleCat R),
  (CategoryTheory.ihom.ev M).app N =
    ModuleCat.ofHom
      ((TensorProduct.uncurry (RingHom.id R) ↑M ↑(M ⟹ N) ↑N)
        (LinearMap.lcomp R ↑N ↑ModuleCat.homLinearEquiv ∘ₗ LinearMap.id.flip))
-- Mathlib.Topology.Instances.Int
Int.preimage_closedBall : ∀ (x : ℤ) (r : ℝ), Int.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instFunLike : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : TopologicalSpace F] → (𝔖 : Set (Set E)) → FunLike (UniformConvergenceCLM σ F 𝔖) E F
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_symm_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  (F : SkewMonoidAlgebra k G →ₐ[k] A) (x : G),
  ((SkewMonoidAlgebra.lift k G A).symm F) x = F (SkewMonoidAlgebra.single x 1)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.ι_sigmaSpec : ∀ {ι : Type u} (R : ι → CommRingCat) (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun i => AlgebraicGeometry.Spec (R i)) i)
      (AlgebraicGeometry.sigmaSpec R) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i => ↑(R i)) i))
-- Mathlib.Algebra.Group.Equiv.Defs
MulHom.toMulEquiv_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
  (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N), ⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.pow_const : ∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : Pow β γ] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → ∀ (c : γ), f ^ c =ᶠ[l] g ^ c
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_sup : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (I J : Ideal R),
  IsLocalization.coeSubmodule S (I ⊔ J) = IsLocalization.coeSubmodule S I ⊔ IsLocalization.coeSubmodule S J
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.diam_Ioo : ∀ {a b : ℝ}, a ≤ b → Metric.diam (Set.Ioo a b) = b - a
-- Mathlib.Topology.ContinuousMap.Algebra
RingHom.compLeftContinuous_apply_apply : ∀ (α : Type u_1) {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring β] [inst_3 : IsTopologicalSemiring β] [inst_4 : TopologicalSpace γ] [inst_5 : Semiring γ]
  [inst_6 : IsTopologicalSemiring γ] (g : β →+* γ) (hg : Continuous ⇑g) (f : C(α, β)) (a : α),
  ((RingHom.compLeftContinuous α g hg) f) a = g (f a)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.instDecidableEqDihedralGroup.decEq.match_1.eq_2 : ∀ {n : ℕ} (motive : DihedralGroup n → DihedralGroup n → Sort u_1) (a a_1 : ZMod n)
  (h_1 : (a b : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.r b))
  (h_2 : (a a_2 : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.sr a_2))
  (h_3 : (a a_2 : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.r a_2))
  (h_4 : (a b : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.sr b)),
  (match DihedralGroup.r a, DihedralGroup.sr a_1 with
    | DihedralGroup.r a, DihedralGroup.r b => h_1 a b
    | DihedralGroup.r a, DihedralGroup.sr a_2 => h_2 a a_2
    | DihedralGroup.sr a, DihedralGroup.r a_2 => h_3 a a_2
    | DihedralGroup.sr a, DihedralGroup.sr b => h_4 a b) =
    h_2 a a_1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The set of points of a face.  -/
Affine.Simplex.range_face_points : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1),
  Set.range (s.face h).points = s.points '' ↑fs
-- Mathlib.LinearAlgebra.Complex.Module
/-- An element in a non-unital star `ℂ`-algebra is normal if and only if its real and imaginary
parts commute.  -/
isStarNormal_iff_commute_realPart_imaginaryPart : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [IsScalarTower ℂ A A]
  [SMulCommClass ℂ A A] [inst_5 : StarModule ℂ A] {x : A}, IsStarNormal x ↔ Commute ↑(realPart x) ↑(imaginaryPart x)
-- Mathlib.RingTheory.PowerSeries.Trunc
/-- The `n`-th coefficient of `f*g` may be calculated
from the truncations of `f` and `g`.  -/
PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂ : ∀ {R : Type u_2} [inst : CommSemiring R] {n a b : ℕ} (f g : PowerSeries R),
  n < a →
    n < b →
      (PowerSeries.coeff n) (f * g) = (PowerSeries.coeff n) (↑((PowerSeries.trunc a) f) * ↑((PowerSeries.trunc b) g))
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- A uniform upper bound for `jacobiTheta₂_term` on compact subsets.  -/
norm_jacobiTheta₂_term_le : ∀ {S T : ℝ},
  0 < T →
    ∀ {z τ : ℂ},
      |z.im| ≤ S → T ≤ τ.im → ∀ (n : ℤ), ‖jacobiTheta₂_term n z τ‖ ≤ Real.exp (-Real.pi * (T * ↑n ^ 2 - 2 * S * ↑|n|))
-- Init.Omega.Int
Lean.Omega.Int.ofNat_shiftLeft_eq : ∀ {x y : ℕ}, ↑(x <<< y) = ↑x * ↑(2 ^ y)
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.solved.sizeOf_spec : sizeOf Lean.Meta.Match.InjectionAnyResult.solved✝ = 1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.norm : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => ‖f x‖) p μ
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
zero_notMem_nonZeroDivisorsRight : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀], 0 ∉ nonZeroDivisorsRight M₀
-- Init.Data.List.Basic
/-- Decidability of lexicographic ordering.  -/
List.decidableLT : {α : Type u} → [DecidableEq α] → [inst : LT α] → [DecidableLT α] → (l₁ l₂ : List α) → Decidable (l₁ < l₂)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.liftWith_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : ({β : Type u} → OptionT m β → m (Option β)) → m α),
  (Std.Do.wp (MonadControl.liftWith f)).apply Q = (Std.Do.wp (f fun {β} x => x.run)).apply (Q.1, Q.2.2)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.exists_cos_eq_zero : 0 ∈ Real.cos '' Set.Icc 1 2
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_univ : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {f : ι → M} [inst_2 : Fintype ι],
  (Finset.univ.expect fun i => f i) = (↑(Fintype.card ι))⁻¹ • ∑ i, f i
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- In an exact short complex, if the two outer objects are zero objects, then so is the
middle object.  -/
CategoryTheory.ShortComplex.Exact.isZero_of_both_isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact → CategoryTheory.Limits.IsZero S.X₁ → CategoryTheory.Limits.IsZero S.X₃ → CategoryTheory.Limits.IsZero S.X₂
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- If `P : Cᵒᵖ ⥤ A` is a sheaf and `f i : X i ⟶ S` is a covering family, then
a morphism `E ⟶ P.obj (op S)` can be constructed from a compatible family of
morphisms `x : E ⟶ P.obj (op (X i))`.  -/
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {P : CategoryTheory.Functor Cᵒᵖ A} →
            CategoryTheory.Presheaf.IsSheaf J P →
              {I : Type u_1} →
                {S : C} →
                  {X : I → C} →
                    (f : (i : I) → X i ⟶ S) →
                      CategoryTheory.Sieve.ofArrows X f ∈ J S →
                        {E : A} →
                          (x : (i : I) → E ⟶ P.obj (Opposite.op (X i))) →
                            (∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
                                CategoryTheory.CategoryStruct.comp a (f i) =
                                    CategoryTheory.CategoryStruct.comp b (f j) →
                                  CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) =
                                    CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) →
                              (E ⟶ P.obj (Opposite.op S))
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.instCoeSubtypeMemSubringInteger.eq_1 : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete], Valuation.Uniformizer.instCoeSubtypeMemSubringInteger = { coe := fun π => π.val }
-- Init.Sym.Simp.SimprocDSL
Lean.Parser.Command.sym_simp_field.quot : Lean.ParserDescr
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.instGetElemProdNatRatAndLtFstSndOfUsableInSimplexAlgorithm : (n m : ℕ) →
  (matType : ℕ → ℕ → Type) →
    [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
      GetElem (matType n m) (ℕ × ℕ) ℚ fun x p => p.1 < n ∧ p.2 < m
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.go.eq_def : ∀ (n p : ℕ) (hp : 1 < p ∧ n ≠ 0),
  Nat.maxPowDvdDiv.go n p hp =
    if hmod : n % p = 0 then
      match Nat.maxPowDvdDiv.go n (p * p) ⋯ with
      | (e, q) => if q % p = 0 then (2 * e + 1, q / p) else (2 * e, q)
    else (0, n)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.mem_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  {f : α →o β}, ∀ x ∈ c, f x ∈ c.map f
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a = False`.
It assumes `a` and `False` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkEqFalseProof : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_neg_cancel_left_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a ≠ ⊤ → ∀ (b : α), a + (-a + b) = b
-- Mathlib.Condensed.Discrete.Module
/-- `functorToPresheaves` as a functor to condensed modules.  -/
CondensedMod.LocallyConstant.functor : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (CondensedMod R)
-- Mathlib.Data.Seq.Computation
Computation.tail_think : ∀ {α : Type u} (s : Computation α), s.think.tail = s
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.mapReverseId : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasReverse U], (𝟭q U).MapReverse
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth w : ℕ} (x : aig.RefVec w)
  (h : outWidth = w * w) (w_1 : ℕ) (x_1 : aig.RefVec w_1) (h_1 : outWidth = w_1 * w_1),
  ({ w := w, x := x, h := h } = { w := w_1, x := x_1, h := h_1 }) = (w = w_1 ∧ x ≍ x_1)
-- Mathlib.Geometry.Manifold.StructureGroupoid
Pregroupoid.mk.inj : ∀ {H : Type u_2} {inst : TopologicalSpace H} {property : (H → H) → Set H → Prop}
  {comp :
    ∀ {f g : H → H} {u v : Set H},
      property f u → property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v)}
  {id_mem : property id Set.univ}
  {locality :
    ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u}
  {congr : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u}
  {property_1 : (H → H) → Set H → Prop}
  {comp_1 :
    ∀ {f g : H → H} {u v : Set H},
      property_1 f u → property_1 g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property_1 (g ∘ f) (u ∩ f ⁻¹' v)}
  {id_mem_1 : property_1 id Set.univ}
  {locality_1 :
    ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property_1 f (u ∩ v)) → property_1 f u}
  {congr_1 : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property_1 f u → property_1 g u},
  { property := property, comp := comp, id_mem := id_mem, locality := locality, congr := congr } =
      { property := property_1, comp := comp_1, id_mem := id_mem_1, locality := locality_1, congr := congr_1 } →
    property = property_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.div` -/
MeasureTheory.AEStronglyMeasurable.fun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : Group β] [IsTopologicalGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i / g i) μ
-- Mathlib.Data.Nat.Log
Nat.clog_antitone_left : ∀ {n : ℕ}, AntitoneOn (fun b => Nat.clog b n) (Set.Ioi 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp)
  (e_t : t = t_1) (h : t ≠ ∅), t.minKey h = t_1.minKey ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The forgetful functor `PresheafOfModules R ⥤ Cᵒᵖ ⥤ Ab`.  -/
PresheafOfModules.toPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) →
      CategoryTheory.Functor (PresheafOfModules R) (CategoryTheory.Functor Cᵒᵖ Ab)
-- Mathlib.Data.NNReal.Defs
NNReal.le_toNNReal_of_coe_le : ∀ {x : NNReal} {y : ℝ}, ↑x ≤ y → x ≤ y.toNNReal
-- Init.Data.Int.Order
Int.lt_sub_left_of_add_lt : ∀ {a b c : ℤ}, a + b < c → b < c - a
-- Lean.AuxRecursor
/-- Shape information for no confusion lemmas.
The `arity` does not include the final major argument (which is not there when the constructors differ)
The regular no confusion lemma marks the lhs and rhs arguments for the compiler to look at and
find the number of fields.
The per-constructor no confusion lemmas know the number of (non-prop) fields statically.
 -/
Lean.NoConfusionInfo : Type
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- A typeclass mixin for `MeasurableSpace`s such that each singleton is measurable.  -/
MeasurableSingletonClass : (α : Type u_7) → [MeasurableSpace α] → Prop
-- Std.Http.Data.Request
/-- Creates a new HTTP request builder with the default head
(method: GET, version: HTTP/1.1, target: `*`).
 -/
Std.Http.Request.new : Std.Http.Request.Builder
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
_private.Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal.0.PositiveLinearMap.gnsNonUnitalStarAlgHom_map_one : ∀ {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (f : A →ₚ[ℂ] ℂ),
  f.gnsNonUnitalStarAlgHom 1 = 1
-- Mathlib.Analysis.Analytic.Composition
/-- **Alias** of `AnalyticAt.fun_comp`.

---

Eta-expanded form of `AnalyticAt.comp`

---

If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
analytic at `x`.  -/
AnalyticAt.comp' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E},
  AnalyticAt 𝕜 g (f x) → AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (fun x => g (f x)) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keysArray_insertIfNew_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α},
  (t.insertIfNew k ()).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k)
-- Mathlib.Order.Ideal
Order.Ideal.instCompleteLattice : {P : Type u_1} → [inst : SemilatticeSup P] → [OrderBot P] → CompleteLattice (Order.Ideal P)
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.mk_pos : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a₁ a₂ : α},
  0 < Lean.Grind.Ring.OfSemiring.Q.mk (a₁, a₂) ↔ a₂ < a₁
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.finite_setOfPred_isIntegral_nat_mul_and_mulHeight₁_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 → ∀ (B : ℝ), {x | IsIntegral ℤ (↑n * x) ∧ Height.mulHeight₁ x ≤ B}.Finite
-- Mathlib.Algebra.Group.End
/-- Monoid hom from the group of multiplicative automorphisms to the group of permutations.  -/
AddAut.toPerm : (A : Type u_1) → [inst : Add A] → AddAut A →+ Additive (Equiv.Perm A)
-- Mathlib.Data.Fin.Parity
Fin.odd_iff_mod_of_even : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Even n → (Odd k ↔ ↑k % 2 = 1)
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.divX = 0 ↔ p = Polynomial.C (p.coeff 0)
-- Init.Data.Int.Gcd
Int.gcd_assoc : ∀ (a b c : ℤ), (↑(a.gcd b)).gcd c = a.gcd ↑(b.gcd c)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhdsGT_nat_neBot : ∀ (n : ℕ), (nhdsWithin (↑n) (Set.Ioi ↑n)).NeBot
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopologicalSpace.Opens.instIsContinuousCompGrothendieckTopology : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (F : CategoryTheory.Functor (TopologicalSpace.Opens X) (TopologicalSpace.Opens Y))
  (G : CategoryTheory.Functor (TopologicalSpace.Opens Y) (TopologicalSpace.Opens Z))
  [F.IsContinuous (Opens.grothendieckTopology X) (Opens.grothendieckTopology Y)]
  [G.IsContinuous (Opens.grothendieckTopology Y) (Opens.grothendieckTopology Z)],
  (F.comp G).IsContinuous (Opens.grothendieckTopology X) (Opens.grothendieckTopology Z)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.Raw.ofList l cmp).getKey? k = none
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sum_comp_sumInv : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι], AdicCompletion.sum I M ∘ₗ AdicCompletion.sumInv I M = LinearMap.id
-- Mathlib.Order.Monotone.Basic
/-- A monotone function `f : ℕ → ℕ` bounded by `b`, which is constant after stabilising for the
first time, stabilises in at most `b` steps.  -/
Nat.stabilises_of_monotone : ∀ {f : ℕ → ℕ} {b n : ℕ},
  Monotone f → (∀ (m : ℕ), f m ≤ b) → (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → b ≤ n → f n = f b
-- Init.Data.UInt.Lemmas
UInt16.ofNat_lt_iff : ∀ {n : UInt16} {m : ℕ}, m < UInt16.size → (UInt16.ofNat m < n ↔ m < n.toNat)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF],
  W.c₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆