mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given a morphism `f : K ⟶ L`, this is the single cochain complex in degree `n`
which is given an injective object which contains `((cokernel f).truncGE n).X n`,
i.e. the object in degree `n` of the canonical truncation `≥ n` of `cokernel f`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.S : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (K ⟶ L) → [CategoryTheory.EnoughInjectives C] → ℤ → HomologicalComplex C (ComplexShape.up ℤ)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] ⦃f g : ZeroHom M N⦄, (∀ (x : M), f x = g x) → f = g
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff' : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  CategoryTheory.IsCardinalPresentable J κ ↔ HasCardinalLT (↑J.obj) κ
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainGoal : Lean.FromJson Lean.Lsp.PlainGoal
-- Mathlib.Order.Heyting.Hom
HeytingHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (f : HeytingHom α β),
  f.comp (HeytingHom.id α) = f
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**: if `f : ℂ → E` is complex analytic
on an open disk with center `c` and a positive radius `R₁`,
and it sends this disk to a closed ball with center `f c` and radius the same radius,
then the norm of the derivative of `f` at the center of this disk is at most `1`.
 -/
Complex.norm_deriv_le_one_of_mapsTo_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f : ℂ → E} {c : ℂ},
  DifferentiableOn ℂ f (Metric.ball c R) →
    Set.MapsTo f (Metric.ball c R) (Metric.closedBall (f c) R) → 0 < R → ‖deriv f c‖ ≤ 1
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instModelPreorderTheoryOfPartialOrderTheory : ∀ (L : FirstOrder.Language) {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [h : M ⊨ L.partialOrderTheory],
  M ⊨ L.preorderTheory
-- Init.Data.Vector.Basic
/-- `a ∈ v` is a predicate which asserts that `a` is in the vector `v`.  -/
Vector.Mem : {α : Type u_1} → {n : ℕ} → Vector α n → α → Prop
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
notMem_of_lt_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {x : α} {s : Set α}, x < sInf s → BddBelow s → x ∉ s
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.mk.inj : ∀ {J : Type u} {inst : CategoryTheory.Category.{v, u} J} {F : CategoryTheory.Functor J (Type w₀)} {pt : Type w₁}
  {ι : (j : J) → F.obj j → pt}
  {ι_naturality :
    autoParam (∀ {j j' : J} (f : j ⟶ j'), ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι j)
      CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam}
  {pt_1 : Type w₁} {ι_1 : (j : J) → F.obj j → pt_1}
  {ι_naturality_1 :
    autoParam (∀ {j j' : J} (f : j ⟶ j'), ι_1 j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι_1 j)
      CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam},
  { pt := pt, ι := ι, ι_naturality := ι_naturality } = { pt := pt_1, ι := ι_1, ι_naturality := ι_naturality_1 } →
    pt = pt_1 ∧ ι ≍ ι_1
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.e_lie_v_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] {i j : ι} {k : ↥b.support},
  P.root j = P.root ↑k + P.root i →
    ⁅RootPairing.GeckConstruction.e k, RootPairing.GeckConstruction.v b i⁆ =
      (↑(RootPairing.chainBotCoeff (↑k) i) + 1) • RootPairing.GeckConstruction.v b j
-- Mathlib.Analysis.Normed.Ring.Units
/-- The function `Ring.inverse` is continuous at each unit of `R`.  -/
NormedRing.inverse_continuousAt : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ), ContinuousAt Ring.inverse ↑x
-- Mathlib.Tactic.HigherOrder
Lean.Parser.Attr.higherOrder : Lean.ParserDescr
-- Mathlib.Probability.ProductMeasure
MeasureTheory.piContent_cylinder : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {I : Finset ι} {S : Set ((i : ↥I) → X ↑i)},
  MeasurableSet S →
    (MeasureTheory.piContent μ) (MeasureTheory.cylinder I S) = (MeasureTheory.Measure.pi fun i => μ ↑i) S
-- Mathlib.Data.Fin.Pigeonhole
/-- If we have an injective map from `Fin m` to `Fin n` whose image does not contain everything,
then `m < n`. See also `Fintype.card_lt_of_injective_of_notMem` for the generalisation to
arbitrary finite types.
 -/
Fin.lt_of_injective_of_notMem : ∀ {m n : ℕ} (f : Fin m → Fin n), Function.Injective f → ∀ {b : Fin n}, b ∉ Set.range f → m < n
-- Mathlib.Analysis.Convex.Gauge
/-- An alternative definition of the gauge using scalar multiplication on the element rather than on
the set.  -/
gauge_def' : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
  gauge s x = sInf {r | r ∈ Set.Ioi 0 ∧ r⁻¹ • x ∈ s}
-- Mathlib.RingTheory.TensorProduct.Basic
Commute.tmul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] {a₁ a₂ : A} {b₁ b₂ : B},
  Commute a₁ a₂ → Commute b₁ b₂ → Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)
-- Mathlib.Topology.MetricSpace.Thickening
Disjoint.exists_thickenings : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Disjoint s t → IsCompact s → IsClosed t → ∃ δ, 0 < δ ∧ Disjoint (Metric.thickening δ s) (Metric.thickening δ t)
-- Mathlib.Topology.Separation.Basic
Set.Subsingleton.closure_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, s.Subsingleton → closure s = s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_zero : Real.Angle.sign 0 = 0
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_sumPiEquivProdPi_symm : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] {X : ι ⊕ ι' → Type u_4}
  {m : (i : ι ⊕ ι') → MeasurableSpace (X i)} (μ : (i : ι ⊕ ι') → MeasureTheory.Measure (X i))
  [∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
    ((MeasureTheory.Measure.pi fun i => μ (Sum.inl i)).prod (MeasureTheory.Measure.pi fun i => μ (Sum.inr i)))
    (MeasureTheory.Measure.pi μ)
-- Init.Data.SInt.Lemmas
ISize.toUSize_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toUSize = { toBitVec := b }
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.id_hComp_heq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)) η ≍ η
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.trivial_comon_comul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.ComonObj.comul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add : {α : Type u} → [Add α] → Add (WithTop α)
-- Mathlib.Data.List.Forall2
List.forall₂_take_append : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (l : List α) (l₁ l₂ : List β),
  List.Forall₂ R l (l₁ ++ l₂) → List.Forall₂ R (List.take l₁.length l) l₁
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.degree_mul_comm : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ (q : Polynomial R), (p * q).degree = (q * p).degree
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mk.injEq : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] (config : G → A) (support : Finset G)
  (condition : ∀ g ∉ support, config g = default) (config_1 : G → A) (support_1 : Finset G)
  (condition_1 : ∀ g ∉ support_1, config_1 g = default),
  ({ config := config, support := support, condition := condition } =
      { config := config_1, support := support_1, condition := condition_1 }) =
    (config = config_1 ∧ support = support_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- A multivariate power series is the sum (in the sense of summable families) of its monomials  -/
MvPowerSeries.WithPiTopology.hasSum_of_monomials_self : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] (f : MvPowerSeries σ R),
  HasSum (fun d => (MvPowerSeries.monomial d) ((MvPowerSeries.coeff d) f)) f
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α},
  e ∈ M.E → autoParam (I ⊆ M.E) Matroid.fundCircuit_subset_ground._auto_1 → M.fundCircuit e I ⊆ M.E
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpCacheKey.mk.inj : ∀ {variant : Lean.Name} {args : Lean.Elab.Tactic.Grind.DSimpArgs} {variant_1 : Lean.Name}
  {args_1 : Lean.Elab.Tactic.Grind.DSimpArgs},
  { variant := variant, args := args } = { variant := variant_1, args := args_1 } → variant = variant_1 ∧ args = args_1
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.pow_const` -/
Filter.EventuallyEq.fun_pow_const : ∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : Pow β γ] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → ∀ (c : γ), (fun i => f i ^ c) =ᶠ[l] fun i => g i ^ c
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_constVAdd : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (v : V),
  ⇑(AffineIsometryEquiv.constVAdd 𝕜 P v) = fun x => v +ᵥ x
-- Init.Data.Bool
Bool.bne_right_inj : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z
-- Lean.Meta.Iterator
Lean.Meta.Iterator.mk.inj : ∀ {α : Type} {next next_1 : Lean.MetaM (Option (α × Lean.Meta.SavedState))},
  { next := next } = { next := next_1 } → next = next_1
-- Mathlib.Order.Hom.Lattice
SupHom.bot_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : Bot β] (a : α), ⊥ a = ⊥
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.map_mkPrecomp_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X Y : C}
  {f : X ⟶ Y} {g g' : CategoryTheory.yoneda.obj Y ⟶ A} (h : g = g')
  {x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk g'))},
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CostructuredArrow.mkPrecomp g f).op))
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x) =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CostructuredArrow.mkPrecomp g' f).op)) x)
-- Batteries.CodeAction.Misc
/-- Returns the fields of a structure, unfolding parent structures.  -/
_private.Batteries.CodeAction.Misc.0.Batteries.CodeAction.instanceStub.collectFields : Lean.Environment → Lean.Name → Array (Lean.Name × Bool) → List Lean.Name → Array (Lean.Name × Bool)
-- Mathlib.Data.ENNReal.Basic
/-- Extension for the `positivity` tactic: `ENNReal.ofNNReal`.  -/
Mathlib.Meta.Positivity.evalENNRealOfNNReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofSubsingleton_map : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Subsingleton S]
  (x : PUnit.{u_1 + 1}), (Algebra.SubmersivePresentation.ofSubsingleton R S).map x = PUnit.unit
-- Std.Async.DNS
/-- Represents a resolved hostname and service name from a socket address.
 -/
Std.Async.DNS.NameInfo : Type
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G] [inst_4 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsHaarMeasure] [μ.InnerRegular] (g : G),
  MeasureTheory.Measure.map (fun x => x * g) μ = MeasureTheory.Measure.modularCharacterFun g • μ
-- Mathlib.Data.List.Sigma
List.keys_cons : ∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, (s :: l).keys = s.fst :: l.keys
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.default.sizeOf_spec : ∀ (e : Lean.Expr) (source : Lean.Meta.Grind.SplitSource),
  sizeOf (Lean.Meta.Grind.SplitInfo.default e source) = 1 + sizeOf e + sizeOf source
-- Mathlib.Analysis.Complex.Exponential
Complex.norm_exp_le_exp_norm : ∀ (x : ℂ), ‖Complex.exp x‖ ≤ Real.exp ‖x‖
-- Mathlib.Order.KrullDimension
Order.krullDim_lt_coe_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ}, Order.krullDim α < ↑n ↔ ∀ (l : LTSeries α), l.length < n
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.funLike : {R : Type u_5} →
  {S : Type u_6} →
    [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → FunLike (AbsoluteValue R S) R S
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.sum_ite_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (s : Finset ι)
  (f : ι → M), (∑ i, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.mk : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} →
                      (fst : x.fst ⟶ y.fst) →
                        (snd : x.snd ⟶ y.snd) →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F)
                                  y.iso.hom =
                                CategoryTheory.CategoryStruct.comp x.iso.hom
                                  (CategoryTheory.Functor.whiskerRight snd G))
                              CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam →
                            CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.primeFactorsPiBij_inj : ∀ (d n : ℕ) (f : (p : ℕ) → p ∈ n.primeFactors → Fin d) (hf : f ∈ n.primeFactors.pi fun x => Finset.univ)
  (g : (p : ℕ) → p ∈ n.primeFactors → Fin d) (hg : g ∈ n.primeFactors.pi fun x => Finset.univ),
  Nat.primeFactorsPiBij✝ d n f hf = Nat.primeFactorsPiBij✝ d n g hg → f = g
-- Init.Data.Order.Factories
/-- This lemma characterizes in terms of `LT α` when a `Min α` instance
"behaves like an infimum operator" with respect to `LE.ofLT α`.
 -/
Std.LawfulOrderInf.of_lt : ∀ {α : Type u} [inst : Min α] [inst_1 : LT α], (∀ (a b c : α), b ⊓ c < a ↔ b < a ∨ c < a) → Std.LawfulOrderInf α
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.neg_one_left : ∀ {R : Type u} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (x : R), SemiconjBy (-1) x x
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The `weightedTotalDegree'` of a polynomial `p` is `⊥` if and only if `p = 0`.  -/
MvPolynomial.weightedTotalDegree'_eq_bot_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] (w : σ → M) (p : MvPolynomial σ R), MvPolynomial.weightedTotalDegree' w p = ⊥ ↔ p = 0
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.mk.injEq : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toEquiv : X ≃ Y)
  (continuous_toFun : autoParam (Continuous toEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toEquiv.invFun) Homeomorph.continuous_invFun._autoParam)
  (toEquiv_1 : X ≃ Y)
  (continuous_toFun_1 : autoParam (Continuous toEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun_1 : autoParam (Continuous toEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam),
  ({ toEquiv := toEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toEquiv := toEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }) =
    (toEquiv = toEquiv_1)
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_shiftLeft : ∀ (a b : UInt16), (a <<< b).toUInt64 = a.toUInt64 <<< (b % 16).toUInt64 % 65536
-- Mathlib.MeasureTheory.Measure.Content
/-- Constructing the inner content of a content. From a content defined on the compact sets, we
obtain a function defined on all open sets, by taking the supremum of the content of all compact
subsets.  -/
MeasureTheory.Content.innerContent : {G : Type w} → [inst : TopologicalSpace G] → MeasureTheory.Content G → TopologicalSpace.Opens G → ENNReal
-- Mathlib.CategoryTheory.Shift.Basic
/-- a shift is a monoidal functor from `A` to `C ⥤ C`  -/
CategoryTheory.HasShift.shift : {C : Type u} →
  {A : Type u_2} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {inst_1 : AddMonoid A} →
        [self : CategoryTheory.HasShift C A] →
          CategoryTheory.Functor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)
-- Mathlib.Topology.Algebra.IsUniformGroup.Order
TendstoUniformlyOn.eventually_forall_le : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsUniformAddGroup β]
  [inst_3 : PartialOrder β] [OrderTopology β] [AddLeftMono β] [AddRightMono β] {f : ι → α → β} {g : α → β} {K : Set α}
  {p : Filter ι} {u v : β},
  u < v → TendstoUniformlyOn f g p K → (∀ x ∈ K, g x ≤ u) → ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x ≤ v
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableOn_add_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x}
  {u : Set B}, MDiff[u] (T% s) → MDiff[u] (T% t) → MDiff[u] fun x => ⟨x, (s + t) x⟩
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- **Alias** of `AddSemiconjBy.isTrans`.

---

The relation “there exists an element that semiconjugates `a` to `b`” on an
additive semigroup is transitive.  -/
AddSemiconjBy.transitive : ∀ {S : Type u_1} [inst : AddSemigroup S], IsTrans S fun a b => ∃ c, AddSemiconjBy c a b
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_copy : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B) (f' : A → B) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Prelude
/-- Add a new macro scope onto the name `n`, using the monad state to supply the
main module and current macro scope.
 -/
Lean.MonadQuotation.addMacroScope : {m : Type → Type} → [Lean.MonadQuotation m] → [Monad m] → Lean.Name → m Lean.Name
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkCoeWithErrorMsgs : Lean.Expr →
  Lean.Expr →
    (Option Lean.MessageData → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData) →
      (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_im_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.im (inner 𝕜 x y) = -RCLike.im (inner 𝕜 y x)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.iInf_mul : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I : Ideal A) {ι : Type u_4} [Nonempty ι] (J : ι → Ideal A),
  (⨅ i, J i) * I = ⨅ i, J i * I
-- Init.PropLemmas
eq_true_eq_id : Eq True = id
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.dist_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X} {x y : X}, HolderOnWith C r f s → x ∈ s → y ∈ s → ∀ {d : ℝ}, dist x y ≤ d → dist (f x) (f y) ≤ ↑C * d ^ ↑r
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The first leg of a pullback cone is a regular monomorphism if the left component is too.

See also `Pullback.fstOfMono` for the basic monomorphism version, and
`regularOfIsPullbackSndOfRegular` for the flipped version.
 -/
CategoryTheory.regularOfIsPullbackFstOfRegular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P Q R S : C} →
      {f : P ⟶ Q} →
        {g : P ⟶ R} →
          {h : Q ⟶ S} →
            {k : R ⟶ S} →
              CategoryTheory.RegularMono k →
                (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm) →
                    CategoryTheory.RegularMono f
-- Mathlib.Data.List.Basic
List.head!_cons : ∀ {α : Type u} [inst : Inhabited α] (a : α) (l : List α), (a :: l).head! = a
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_left.injEq : ∀ {B : Type u} [inst : Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c}
  (η η_1 : CategoryTheory.FreeBicategory.Hom₂ g h),
  (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η = CategoryTheory.FreeBicategory.Hom₂.whisker_left f η_1) =
    (η = η_1)
-- Batteries.Control.AlternativeMonad
seq_failure : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m]
  (x : m (α → β)), x <*> failure = x *> failure
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.coe_opLinearEquiv_symm : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑(MulOpposite.opLinearEquiv R).symm = MulOpposite.unop
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_int_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_eq_one_iff : ∀ {α : Type u_1} [inst : One α] (a : αˢʸᵐ), SymAlg.unsym a = 1 ↔ a = 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.id : {B : Type u} → [inst : Quiver B] → (a : B) → CategoryTheory.FreeBicategory.Hom a a