mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<$>`, general version.  -/
SatisfiesM.map : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α_1 : Type u_1} {q : α_1 → Prop} {f : α → α_1}
  [inst : Functor m] [LawfulFunctor m] {x : m α}, SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <$> x)
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.preimage_setOfPred_dist : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (p : ℝ → Prop), f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.inter_left_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ M.E → Y ∩ X ⊆ M.E
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr.eq_2 : ∀ (e : ONote) (n : ℕ+) (a : ONote), (e.oadd n a).repr = Ordinal.omega0 ^ e.repr * ↑↑n + a.repr
-- Mathlib.CategoryTheory.Galois.Full
/-- Let `X` be an object of a Galois category with fiber functor `F` and `Y` a sub-`Aut F`-set
of `F.obj X`, on which `Aut F` acts transitively (i.e. which is connected in the Galois category
of finite `Aut F`-sets). Then there exists a connected sub-object `Z` of `X` and an isomorphism
`Y ≅ F.obj X` as `Aut F`-sets such that the obvious triangle commutes.

For a version without the connectedness assumption, see `exists_lift_of_mono`.
 -/
CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (Y : Action FintypeCat (CategoryTheory.Aut F)) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X)
  [CategoryTheory.Mono i] [CategoryTheory.PreGaloisCategory.IsConnected Y],
  ∃ Z f u,
    CategoryTheory.PreGaloisCategory.IsConnected Z ∧
      CategoryTheory.Mono f ∧
        i = CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.toSolution' : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ → FermatLastTheoremForThreeGen.Solution'✝ hζ
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSpace.pi : {δ : Type u_4} → {X : δ → Type u_6} → [m : (a : δ) → MeasurableSpace (X a)] → MeasurableSpace ((a : δ) → X a)
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instGroupWithZero : {K : Type v} → [inst : Field K] → (f : Polynomial K) → GroupWithZero f.SplittingField
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- The function `Real.arsinh` is real analytic.  -/
Real.analyticOnNhd_arsinh : ∀ {s : Set ℝ}, AnalyticOnNhd ℝ Real.arsinh s
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
_private.Mathlib.RingTheory.Perfectoid.FontaineTheta.0.«term_♭» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_id : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], ↑(ContinuousAlgHom.id R A) = AlgHom.id R A
-- Mathlib.Order.KrullDimension
/-- **Alias** of the reverse direction of `Order.height_eq_zero`.

---

The elements of height zero are the minimal elements.  -/
Order.IsMin.height_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, IsMin x → Order.height x = 0
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.skeletal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  CategoryTheory.Skeletal (CategoryTheory.Subobject X)
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
Finset.Rat.den_sum_dvd_prod_den : ∀ {ι : Type u_3} (s : Finset ι) (f : ι → ℚ), (∑ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_succ_self : ∀ {n : ℕ} (j : Fin n), j.succ.succAbove j = j.castSucc
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄}
  (f :
    (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A))
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f) =
    f i₁ i₂ i₃ h
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] → [inst_2 : CommSemiring R] → (v : AbsoluteValue R S) → CommSemiring (WithAbs v)
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
/-- The equivalence of categories between `CommGrpCat` and `AddCommGrpCat`.
 -/
commGroupAddCommGroupEquivalence : CommGrpCat ≌ AddCommGrpCat
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toSkeletonFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.toSkeletonFunctor C).obj X = CategoryTheory.toSkeleton X
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.revAtFun.eq_1 : ∀ (N i : ℕ), Polynomial.revAtFun N i = if i ≤ N then N - i else i
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.zero_of_eq : ∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    needlePos = pat.rawEndPos → String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s 0 stackPos
-- Init.Prelude
/-- Constructs a synthetic `atom` with source info coming from `src`.  -/
Lean.mkAtomFrom : Lean.Syntax → String → optParam Bool false → Lean.Syntax
-- Std.Internal.UV.Loop
Std.Internal.UV.Loop.Options.mk.injEq : ∀ (accumulateIdleTime blockSigProfSignal accumulateIdleTime_1 blockSigProfSignal_1 : Bool),
  ({ accumulateIdleTime := accumulateIdleTime, blockSigProfSignal := blockSigProfSignal } =
      { accumulateIdleTime := accumulateIdleTime_1, blockSigProfSignal := blockSigProfSignal_1 }) =
    (accumulateIdleTime = accumulateIdleTime_1 ∧ blockSigProfSignal = blockSigProfSignal_1)
-- Mathlib.Algebra.Group.Hom.Basic
negAddMonoidHom.eq_1 : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α], negAddMonoidHom = { toFun := Neg.neg, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.instIsTransParallel : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], IsTrans (AffineSubspace k P) AffineSubspace.Parallel
-- Init.Data.List.Lemmas
List.get_mem : ∀ {α : Type u_1} (l : List α) (n : Fin l.length), l.get n ∈ l
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_comm : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y ↔ y =ᵥ x
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.nhds_hasBasis : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) (x₀ : G),
  (nhds x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ + y) '' V
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.comp_symm_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : N → α) (g : M → α), g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.nnrat_rawCast : ∀ {n d : ℕ} {R : Type u_2} [inst : DivisionSemiring R], NNRat.rawCast n d = n.rawCast / d.rawCast
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.restrictScalars_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {S : Submodule A M}
  [Module.Finite R A], (Submodule.restrictScalars R S).FG ↔ S.FG
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.opIso_inv_app_hom_apply : ∀ (n : SimplexCategory) (X : SimplexCategoryᵒᵖ) (x : (SSet.stdSimplex.obj n).obj X),
  (CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.opIso n).inv.app X)) x = SSet.stdSimplex.opObjEquiv.symm x
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addRightReflectLE : ∀ {α : Type u} [inst : LE α] [inst_1 : Add α] [AddRightReflectLE α], AddRightReflectLE αᵒᵈ
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.kerLift_injective : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H),
  Function.Injective ⇑(QuotientAddGroup.kerLift φ)
-- Lean.SubExpr
Lean.SubExpr.instToJsonGoalsLocation.toJson : Lean.SubExpr.GoalsLocation → Lean.Json
-- Lean.Parser.Syntax
Lean.Parser.Syntax.binary.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.List.Lemmas
List.findIdx_mem_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.findIdx p xs < xs.length → List.findIdx p xs ∈ List.findIdxs p xs
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.PrelocalPredicate.sheafifyOf : ∀ {X : TopCat} {T : ↑X → Type u_2} {P : TopCat.PrelocalPredicate T} {U : TopologicalSpace.Opens ↑X}
  {f : (x : ↥U) → T ↑x}, P.pred f → P.sheafify.pred f
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
/-- Given two morphisms `f` and `g` in `A.toFunctor ⟶ F₂`, this is the monomorphism
of functors corresponding to the inclusion `Subfunctor.equalizer f g ≤ A`.  -/
CategoryTheory.Subfunctor.equalizer.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₁ F₂ : CategoryTheory.Functor C (Type w)} →
      {A : CategoryTheory.Subfunctor F₁} →
        (f g : A.toFunctor ⟶ F₂) → (CategoryTheory.Subfunctor.equalizer f g).toFunctor ⟶ A.toFunctor
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The current state of the tape  -/
Turing.TM1.Cfg.Tape : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → [inst : Inhabited Γ] → Turing.TM1.Cfg Γ Λ σ → Turing.Tape Γ
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_natCast : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (k : ℕ),
  (↑k).charpoly = (Polynomial.X - ↑k) ^ Fintype.card n
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.add_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.add h').h₁ = h.h₁ + h'.h₁
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- An arbitrarily chosen small model for a finally small category.  -/
CategoryTheory.FinalModel : (J : Type u) → [inst : CategoryTheory.Category.{v, u} J] → [CategoryTheory.FinallySmall J] → Type w
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toDualProdHom_apply : ∀ {α : Type u_1} [inst : LE α] (a : NonemptyInterval α), NonemptyInterval.toDualProdHom a = a.toDualProd
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
_private.Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete.0.CategoryTheory.Functor.toPseudofunctor.match_3.eq_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {b b' : CategoryTheory.LocallyDiscrete C}
  (motive : (b ⟶ b') → Sort u_3) (f : b.as ⟶ b'.as) (h_1 : (f : b.as ⟶ b'.as) → motive { as := f }),
  (match { as := f } with
    | { as := f } => h_1 f) =
    h_1 f
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_limZero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {x : β}, (CauSeq.const abv x).LimZero ↔ x = 0
-- Batteries.Control.Nondet.Basic
Nondet.mk : {σ : Type} → {m : Type → Type} → [inst : Lean.MonadBacktrack σ m] → {α : Type} → MLList m (α × σ) → Nondet m α
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.id_appIso : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.appIso (CategoryTheory.CategoryStruct.id X) U =
    CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).op
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_op_comp_eqToHom_assoc : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) {Z : Xᵒᵖ}
  (h : Opposite.op c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hbc) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯).op h
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppEquivDFinsupp_apply : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : Zero N] (f : (i : ι) × η i →₀ N),
  ⇑(sigmaFinsuppEquivDFinsupp f) = f.split
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.support_prod_subset : ∀ {ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] (s : Finset ι) (f : ι → κ → M₀),
  (Function.support fun x => ∏ i ∈ s, f i x) ⊆ ⋂ i ∈ s, Function.support (f i)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_add_of_le_right : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b c : α}, a ≤ c → a ≤ b + c
-- Mathlib.Combinatorics.Additive.Dissociation
AddDissociated.subset : ∀ {α : Type u_1} [inst : AddCommGroup α] {s t : Set α}, s ⊆ t → AddDissociated t → AddDissociated s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryLT! t₁ k = Std.DTreeMap.Const.getEntryLT! t₂ k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addU_smul : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {u v : F},
        u ≠ 0 →
          v ≠ 0 → WeierstrassCurve.Jacobian.addU (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addU P Q
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_constOfIsEmpty : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι] (x : G),
  ‖ContinuousMultilinearMap.constOfIsEmpty 𝕜 E x‖ = ‖x‖
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist.match_1.eq_3 : ∀ {X : Type u_1} {Y : Type u_2} (motive : X ⊕ Y → X ⊕ Y → Sort u_3) (x : X) (y : Y)
  (h_1 : (x y : X) → motive (Sum.inl x) (Sum.inl y)) (h_2 : (x y : Y) → motive (Sum.inr x) (Sum.inr y))
  (h_3 : (x : X) → (y : Y) → motive (Sum.inl x) (Sum.inr y)) (h_4 : (x : Y) → (y : X) → motive (Sum.inr x) (Sum.inl y)),
  (match Sum.inl x, Sum.inr y with
    | Sum.inl x, Sum.inl y => h_1 x y
    | Sum.inr x, Sum.inr y => h_2 x y
    | Sum.inl x, Sum.inr y => h_3 x y
    | Sum.inr x, Sum.inl y => h_4 x y) =
    h_3 x y
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_bot : ∀ {α : Type u} [inst : Add α] (x : WithBot α), x + ⊥ = ⊥
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_self : ∀ {β : Type u_3} [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] (b : β),
  ConditionallyCompleteLinearOrderedField.inducedMap β β b = b
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
/-- Given `R`-algebras `S,T`, there is a natural `R`-algebra isomorphism from `S ⊗[R] T` to
`S' ⊗[R] T'` where `S',T'` are the images of `S,T` in `S ⊗[R] T` respectively.  -/
Algebra.TensorProduct.algEquivIncludeRange : (R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring T] →
              [inst_4 : Algebra R T] →
                TensorProduct R S T ≃ₐ[R]
                  TensorProduct R ↥Algebra.TensorProduct.includeLeft.range ↥Algebra.TensorProduct.includeRight.range
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- The **universal property with parameters** of the topology on the restricted product:
for any topological space `Y` of "parameters", a map from `Y × Πʳ i, [R i, A i]` is continuous
*iff* its restriction to each `Y × Πʳ i, [R i, A i]_[𝓟 S]` (with `S` cofinite) is continuous.  -/
RestrictedProduct.continuous_dom_prod_left : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {X : Type u_3} {Y : Type u_4} [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Y]
      {f : Y × RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite → X},
      Continuous f ↔
        ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S),
          Continuous (f ∘ Prod.map id (RestrictedProduct.inclusion R A hS))
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g.mop f
-- Mathlib.Order.Fin.Basic
Fin.top_eq_last : ∀ (n : ℕ), ⊤ = Fin.last n
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.limitToAlgEquiv_symm_apply : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (a : K),
  (InfiniteGalois.limitToAlgEquiv g).symm a = InfiniteGalois.toAlgEquivAux✝ g⁻¹ a
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.toScott_inj : ∀ {α : Type u_1} {a b : α}, Topology.WithScott.toScott a = Topology.WithScott.toScott b ↔ a = b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ},
  (Std.ExtDHashMap.filterMap f m).size = m.size ↔
    ∀ (k : α) (h : k ∈ m), (f (m.getKey k h) (Std.ExtDHashMap.Const.get m k h)).isSome = true
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.beqModel.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.beqModel l₁ l₂ =
    if l₁.length ≠ l₂.length then false else l₁.all fun x => Std.Internal.List.getValueCast? x.fst l₂ == some x.snd
-- Init.Data.BitVec.Lemmas
BitVec.le_toNat_of_msb_true : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → 2 ^ (w - 1) ≤ x.toNat
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm : ∀ {R : Type u} [inst : CommSemiring R] {A B C D : SemimoduleCat R},
  CategoryTheory.MonoidalCategory.tensorμ A B C D =
    SemimoduleCat.ofHom ↑(TensorProduct.tensorTensorTensorComm R ↑A ↑B ↑C ↑D)
-- Init.Data.Range.Polymorphic.Basic
/-- This typeclass ensures that a `HasSize` instance returns the correct size for all ranges.
 -/
Std.Rxi.LawfulHasSize : (α : Type u) → [Std.PRange.UpwardEnumerable α] → [Std.Rxi.HasSize α] → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.isCoskeletal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  X.IsCoskeletal n ↔
    CategoryTheory.Functor.IsRightKanExtension X
      (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X))
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_iUnion_memPartition : ∀ {α : Type u_1} (t : ℕ → Set α),
  MeasurableSpace.generateFrom (⋃ n, memPartition t n) = MeasurableSpace.generateFrom (Set.range t)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.linMulLin_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {f g : M →ₗ[R] R} (l r : M' →ₗ[R] M),
  (LinearMap.BilinForm.linMulLin f g).comp l r = LinearMap.BilinForm.linMulLin (f ∘ₗ l) (g ∘ₗ r)
-- Mathlib.Combinatorics.Hindman
Hindman.FS.add_two : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (i j : ℕ), i < j → a.get i + a.get j ∈ Hindman.FS a
-- Mathlib.RingTheory.Perfection
/-- A monoid homomorphism `M →* N` induces `Perfection M p →* Perfection N p`.  -/
Perfection.mapMonoidHom : (p : ℕ) →
  {M : Type u_2} →
    {N : Type u_3} → [inst : CommMonoid M] → [inst_1 : CommMonoid N] → (M →* N) → Perfection M p →* Perfection N p
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nnnorm_toLp : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] (f : α × β),
  ‖WithLp.toLp ⊤ f‖₊ = ‖f‖₊
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The measure equivalence between `WithLp 2 (U × V)` and `U × V` is volume preserving.  -/
WithLp.volume_preserving_symm_measurableEquiv_toLp_prod : ∀ (U : Type u_4) (V : Type u_5) [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : MeasurableSpace U] [inst_3 : BorelSpace U] [inst_4 : FiniteDimensional ℝ U] [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  [inst_9 : FiniteDimensional ℝ V],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (U × V)).symm) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `HasStrictFDerivAt.finsetProd`. -/
HasStrictFDerivAt.finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x) →
    HasStrictFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iSup_of_isEmpty : ∀ {ι : Sort u_1} [IsEmpty ι] (f : ι → ℝ), ⨆ i, f i = 0
-- Init.Data.Int.Order
Int.le_of_sub_le_sub_right : ∀ {a b c : ℤ}, a - c ≤ b - c → a ≤ b