mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Basic
/-- **Alias** of `ne_of_mem_of_not_mem`. -/
Membership.mem.ne_of_notMem : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → b ∉ s → a ≠ b
-- Init.PropLemmas
exists_eq' : ∀ {α : Sort u_1} {a' : α}, ∃ a, a' = a
-- Lean.Parser.Command
Lean.Parser.Command.declSig.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.UInt
UInt16.toUInt32_toNat : ∀ (x : UInt16), x.toUInt32.toNat = x.toNat
-- Mathlib.Topology.DiscreteSubset
/-- A set `s` is discrete iff for every `y ∈ s` there is an open `u` with `u ∩ s = {y}`.
See `isDiscrete_iff_forall_subset_exists_isOpen'` for a related version of this with subsets.  -/
isDiscrete_iff_forall_mem_exists_isOpen : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {s : Set Y}, IsDiscrete s ↔ ∀ y ∈ s, ∃ u, IsOpen u ∧ u ∩ s = {y}
-- Mathlib.Algebra.Category.ModuleCat.InjectiveDimension
_private.Mathlib.Algebra.Category.ModuleCat.InjectiveDimension.0.ModuleCat.hasInjectiveDimensionLE_iff_of_linearEquiv_aux : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) (n : ℕ),
  CategoryTheory.HasInjectiveDimensionLE M n ↔ CategoryTheory.HasInjectiveDimensionLE N n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)}
  {hc : k ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.get k hc = (f (t.get? k)).get ⋯
-- Mathlib.Order.Restriction
Preorder.frestrictLe₂_comp_frestrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b),
  Preorder.frestrictLe₂ hab ∘ Preorder.frestrictLe b = Preorder.frestrictLe a
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- If `x` is an element of a subgroup `s` of a seminormed group
`E`, its norm in `s` is equal to its norm in `E`.

This is a reversed version of the `simp` lemma `AddSubgroup.coe_norm` for use by `norm_cast`.  -/
AddSubgroup.norm_coe : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s), ‖↑x‖ = ‖x‖
-- Mathlib.Order.Interval.Set.UnorderedInterval
Antitone.image_uIcc_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  Antitone f → f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_refl : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (l : α →₀ M), Finsupp.equivMapDomain (Equiv.refl α) l = l
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.left.inj : ∀ {α : Type u} {c : RBTree.RBColor} {parent : RBTree.RBNode.Path α} {v : α} {r : RBTree.RBNode α} {c_1 : RBTree.RBColor}
  {parent_1 : RBTree.RBNode.Path α} {v_1 : α} {r_1 : RBTree.RBNode α},
  RBTree.RBNode.Path.left c parent v r = RBTree.RBNode.Path.left c_1 parent_1 v_1 r_1 →
    c = c_1 ∧ parent = parent_1 ∧ v = v_1 ∧ r = r_1
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.instNonempty : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J),
  Nonempty (d.Extension val₀ j)
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The top map in a valuative commutative map.  -/
AlgebraicGeometry.ValuativeCommSq.i₁ : {X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} → (self : AlgebraicGeometry.ValuativeCommSq f) → AlgebraicGeometry.Spec (CommRingCat.of self.K) ⟶ X
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_vadd' : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : Lex β) (a : α), ofLex b +ᵥ a = b +ᵥ a
-- Mathlib.Data.Matrix.Basic
/-- The `AlgEquiv` between spaces of square matrices induced by an `AlgEquiv` between their
coefficients. This is `Matrix.map` as an `AlgEquiv`.  -/
AlgEquiv.mapMatrix : {m : Type u_2} →
  {R : Type u_7} →
    {α : Type u_11} →
      {β : Type u_12} →
        [inst : Fintype m] →
          [inst_1 : DecidableEq m] →
            [inst_2 : CommSemiring R] →
              [inst_3 : Semiring α] →
                [inst_4 : Semiring β] →
                  [inst_5 : Algebra R α] → [inst_6 : Algebra R β] → (α ≃ₐ[R] β) → Matrix m m α ≃ₐ[R] Matrix m m β
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Define `I := √-1` as an element of the upper half plane.  -/
UpperHalfPlane.I : UpperHalfPlane
-- Mathlib.Order.Comparable
CompRel.of_rel_symm : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, r b a → CompRel r a b
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.map_injective_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (Q : Type u_4)
  [inst_2 : CommSemiring Q] [inst_3 : Algebra P Q] {S : Type u_5} [inst_4 : CommRing S] [inst_5 : Algebra R S]
  (f : R →+* P) (r : R) [inst_6 : IsLocalization.Away r S] [inst_7 : IsLocalization.Away (f r) Q],
  Function.Injective ⇑(IsLocalization.Away.map S Q f r) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
-- Mathlib.Data.List.ModifyLast
_private.Mathlib.Data.List.ModifyLast.0.List.modifyLast.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((x : Array α) → motive [] x) →
          ((x : α) → (acc : Array α) → motive [x] acc) →
            ((x : α) → (xs : List α) → (acc : Array α) → (xs = [] → False) → motive (x :: xs) acc) → motive x x_1
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_eq_ramificationIdx`. -/
Ideal.ramificationIdx_eq_ramificationIdx' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] [q.LiesOver p] [hq : q.IsPrime],
  p ≠ ⊥ → p.ramificationIdx' q = q.ramificationIdx R
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_rankOne_eq_id : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E),
  ∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) (b i) = ContinuousLinearMap.id 𝕜 E
-- Lean.Server.References
Lean.Server.instInhabitedModuleImport : Inhabited Lean.Server.ModuleImport
-- Mathlib.RingTheory.Perfection
/-- The `n`-th coefficient of an element of the perfection.  -/
Perfection.coeffMonoidHom : (M : Type u_1) → [inst : CommMonoid M] → (p : ℕ) → ℕ → Perfection M p →* M
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.bound_aux' : ∀ (n d : ℕ), ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A version of `List.prod_inv_reverse` for `Matrix.inv`.  -/
Matrix.list_prod_inv_reverse : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (l : List (Matrix n n α)), l.prod⁻¹ = (List.map Inv.inv l.reverse).prod
-- Mathlib.Order.Disjoint
Complementeds.coe_inf : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] (a b : Complementeds α), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_mem_div_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, 1 ∈ s / t ↔ ¬Disjoint s t
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
Conformal.const_smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f : X → Y}, Conformal f → ∀ {c : ℝ}, c ≠ 0 → Conformal (c • f)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.null.sizeOf_spec : ∀ {α : Type u} {β : Type v} {σ : Type w} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ],
  sizeOf Lean.PersistentHashMap.Entry.null = 1
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : Monoid carrier], sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] [inst_2 : Inhabited α]
  {l : List α} {k : α},
  l.contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey! k = default
-- Mathlib.Order.WithBot
WithTop.instWellFoundedLT : ∀ {α : Type u_1} [inst : LT α] [WellFoundedLT α], WellFoundedLT (WithTop α)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
/-- The connecting homomorphism
`(singleFunctor C 0).obj S.X₃ ⟶ ((singleFunctor C 0).obj S.X₁)⟦(1 : ℤ)⟧` in the derived
category of `C` when `S` is a short exact short complex in `C`.  -/
CategoryTheory.ShortComplex.ShortExact.singleδ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex C} →
          S.ShortExact →
            ((DerivedCategory.singleFunctor C 0).obj S.X₃ ⟶
              (CategoryTheory.shiftFunctor (DerivedCategory C) 1).obj ((DerivedCategory.singleFunctor C 0).obj S.X₁))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] {f g : α →*o β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_trans_reindexLinearEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n')
  (e₁' : m' ≃ m'') (e₂' : n' ≃ n''),
  Matrix.reindexLinearEquiv R A e₁ e₂ ≪≫ₗ Matrix.reindexLinearEquiv R A e₁' e₂' =
    Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
-- Mathlib.Topology.Bornology.Real
NNReal.instIsOrderBornology : IsOrderBornology NNReal
-- Mathlib.FieldTheory.KummerExtension
autEquivZmod_symm_apply_intCast : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1)
  [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L},
  α ^ n = (algebraMap K L) a →
    ∀ [inst_4 : NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ),
      ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
-- Batteries.Data.List.Perm
/-- The list version of `add_tsub_cancel_of_le` for multisets.  -/
List.subperm_append_diff_self_of_count_le : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α},
  (∀ x ∈ l₁, List.count x l₁ ≤ List.count x l₂) → (l₁ ++ l₂.diff l₁).Perm l₂
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isLittleO_deriv_smoothingFn : deriv AkraBazziRecurrence.smoothingFn =o[Filter.atTop] fun x => x⁻¹
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm applied to a product is dominated by the sum of the seminorm applied to the
factors.  -/
GroupSeminorm.mul_le' : ∀ {G : Type u_6} [inst : Group G] (self : GroupSeminorm G) (x y : G), self.toFun (x * y) ≤ self.toFun x + self.toFun y
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.addBuilderOption : Aesop.RuleBuilderOptions → Aesop.Frontend.BuilderOption → Aesop.RuleBuilderOptions
-- Mathlib.Order.Filter.Pointwise
Filter.sub_pure : ∀ {α : Type u_2} [inst : Sub α] {f : Filter α} {b : α}, f - pure b = Filter.map (fun x => x - b) f
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.universalHom_commutes : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_3}
  [inst_2 : Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R},
  (OreLocalization.universalHom f fS hf) (OreLocalization.numeratorHom r) = f r
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tsum_symmetricIco_tsum_sub_eq : ∀ (z : UpperHalfPlane),
  ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
    -2 * ↑Real.pi * Complex.I / ↑z
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (↑(m.insertIfNew k v)).size ≤ (↑m).size + 1
-- Lean.Elab.Tactic.Config
_private.Lean.Elab.Tactic.Config.0.Lean.Elab.Tactic.mkConfigElaborator : Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
  Lean.Ident → Lean.Ident → Lean.Ident → Lean.Term → Lean.Term → Lean.MacroM (Lean.TSyntax `command)
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C) {Y Z : C}
  [HomotopicalAlgebra.IsCofibrant X] (g : Y ⟶ Z) [HomotopicalAlgebra.Fibration g]
  [HomotopicalAlgebra.WeakEquivalence g], Function.Bijective fun f => f.postcomp g
-- Mathlib.Order.LatticeIntervals
Set.Iic.eq_top_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {x : ↑(Set.Iic a)}, x = ⊤ ↔ ↑x = a
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.smul_orbit_eq_orbit_smul : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (N : Subgroup G) [nN : N.Normal] (a : X)
  (g : G), g • MulAction.orbit (↥N) a = MulAction.orbit (↥N) (g • a)
-- Mathlib.Topology.MetricSpace.Basic
SeparationQuotient.instMetricSpace : {α : Type u} → [inst : PseudoMetricSpace α] → MetricSpace (SeparationQuotient α)
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Ioc a b` and monotone on `Ici b`, then the minimum of `f` on `Ioi a` is
attained at `b`.  -/
isMinOn_Ioi_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  AntitoneOn f (Set.Ioc a b) → MonotoneOn f (Set.Ici b) → IsMinOn f (Set.Ioi a) b
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.ind_rec : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g₁ g₂ : QPF.Fix F → α),
  (∀ (x : F (QPF.Fix F)), g₁ <$> x = g₂ <$> x → g₁ (QPF.Fix.mk x) = g₂ (QPF.Fix.mk x)) → ∀ (x : QPF.Fix F), g₁ x = g₂ x
-- Mathlib.AlgebraicGeometry.Gluing
/-- The canonical morphism from the gluing of an open cover of `X` into `X`.
This is an isomorphism, as witnessed by an `IsIso` instance.  -/
AlgebraicGeometry.Scheme.Cover.fromGlued : {X : AlgebraicGeometry.Scheme} → (𝒰 : X.OpenCover) → (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).glued ⟶ X
-- Mathlib.Topology.Algebra.Monoid
finsum_eventually_eq_sum : ∀ {ι : Type u_1} {X : Type u_5} [inst : TopologicalSpace X] {M : Type u_6} [inst_1 : AddCommMonoid M] {f : ι → X → M},
  (LocallyFinite fun i => Function.support (f i)) →
    ∀ (x : X), ∃ s, ∀ᶠ (y : X) in nhds x, ∑ᶠ (i : ι), f i y = ∑ i ∈ s, f i y
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `aᶜ` is defined as `a ⇨ ⊥`  -/
CompletelyDistribLattice.himp_bot : ∀ {α : Type u} [self : CompletelyDistribLattice α] (a : α), a ⇨ ⊥ = aᶜ
-- Mathlib.Computability.TuringMachine.Tape
/-- The "inclusive" left side of the tape, including both `left` and `head`.  -/
Turing.Tape.left₀ : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Tape Γ → Turing.ListBlank Γ
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_bot : ∀ {G : Type u_1} [inst : Group G], ↑⊥ = {1}
-- Mathlib.Data.Finsupp.Option
Finsupp.some_apply : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : Option α →₀ M) (a : α), f.some a = f (some a)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.toAddEquiv : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : AddGroup E'] → {S' : AddGroupExtension N E' G} → S.Equiv S' → E ≃+ E'
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (K : CochainComplex C ℤ) {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (Φ : CategoryTheory.Functor C D)
  [inst_4 : Φ.Additive], (z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h
-- Mathlib.Algebra.Order.Floor.Ring
Int.abs_sub_lt_one_of_floor_eq_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a b : R},
  ⌊a⌋ = ⌊b⌋ → |a - b| < 1
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_roc : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : DecidableLE α] [inst_6 : LT α] [inst_7 : Std.PRange.UpwardEnumerable α] [inst_8 : Std.Rxc.IsAlwaysFinite α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerable α] [inst_10 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_11 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roc α} {init : β}
  {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The image of a set `s` under a linear map `f` has measure
equal to `μ s` times the absolute value of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_image_linearMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E →ₗ[ℝ] E) (s : Set E),
  μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatEraNarrow : Std.Time.DateFormatSymbols → Std.Time.Year.Era → String
-- Init.System.IO
/-- Creates a new mutable reference cell that contains `a`.
 -/
IO.mkRef : {α : Type} → α → BaseIO (IO.Ref α)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.measure_eq_top_of_lintegral_ne_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → μ {x | f x = ⊤} = 0
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier : ∀ {R : Type u} [inst : Ring R], (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).ReflectsIsomorphisms
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_replaceEntry_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  Std.Internal.List.containsKey k l = true →
    (k == a) = true → Std.Internal.List.getEntry? a (Std.Internal.List.replaceEntry k v l) = some ⟨k, v⟩
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (X : J)
  (hX : CategoryTheory.Limits.IsTerminal X), CategoryTheory.IsIso (c.ι.app X)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_toAdd : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (a b : Multiplicative X),
  nndist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = nndist a b
-- Mathlib.GroupTheory.Perm.Cycle.Factors
_private.Mathlib.GroupTheory.Perm.Cycle.Factors.0.Equiv.Perm.mem_support_cycleOf_iff'_aux : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α},
  f x ≠ x →
    ∀ [inst : DecidableRel f.SameCycle] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
      y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∈ t → (cmp t.minKey! k).isLE = true
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.hom_ext_iff : ∀ {R : Type u} [inst : Semiring R] {X Y : CategoryTheory.Mat R} {f g : X ⟶ Y},
  f = g ↔ ∀ (i : X.obj) (j : Y.obj), f i j = g i j
-- Lean.ErrorExplanation
Lean.ErrorExplanation.instFromJsonMetadata.fromJson : Lean.Json → Except String Lean.ErrorExplanation.Metadata
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.paddingLeft? : Lean.Lsp.InlayHint → Option Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_b₆ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).b₆ = ↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- If `f` is continuous alternating, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate.  -/
ContinuousAlternatingMap.map_sum : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {α : ι → Type u_7} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι]
  (g' : (i : ι) → α i → M) [inst_9 : (i : ι) → Fintype (α i)], (f fun i => ∑ j, g' i j) = ∑ r, f fun i => g' i (r i)
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- `FractionalIdeal.adjoinIntegral (S : Submonoid R) x hx` is `R[x]` as a fractional ideal,
where `hx` is a proof that `x : P` is integral over `R`.  -/
FractionalIdeal.adjoinIntegral : {R : Type u_1} →
  [inst : CommRing R] →
    (S : Submonoid R) →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] → [IsLocalization S P] → (x : P) → IsIntegral R x → FractionalIdeal S P
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.toByteArray_copy_eq_empty_iff : ∀ {s : String.Slice}, s.copy.toByteArray = ByteArray.empty ↔ s.isEmpty = true
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.smul_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {𝕜 : Type u_5} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₘ[μ] γ),
  (c • f).toGerm = c • f.toGerm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instInhabitedCooperSplit : Inhabited Lean.Meta.Grind.Arith.Cutsat.CooperSplit
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_ofAbs : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x : WithAbs v), WithAbs.toAbs v x.ofAbs = x