mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.Fin.Lemmas
Fin.findRev?_rev : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.findRev? fun x => p x.rev) = Option.map Fin.rev (Fin.find? p)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.coprod.inl
-- Init.Data.Array.Find
Array.back!_filterMap : ∀ {β : Type u_1} {α : Type u_2} [inst : Inhabited β] {f : α → Option β} {xs : Array α},
  (Array.filterMap f xs).back! = (Array.findSomeRev? f xs).getD default
-- Mathlib.Analysis.ODE.Transform
isIntegralCurveOn_comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ}
  {dt : ℝ}, IsIntegralCurveOn (γ ∘ fun x => x + dt) (v ∘ fun x => x + dt) (-dt +ᵥ s) ↔ IsIntegralCurveOn γ v s
-- Mathlib.Order.Monotone.Monovary
monovaryOn_toDual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ AntivaryOn f g s
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.cons.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural)
  (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr)
  (e_1 : Mathlib.Tactic.BicategoryLike.Mor₂) (α_1 : Mathlib.Tactic.BicategoryLike.Structural)
  (η_1 : Mathlib.Tactic.BicategoryLike.WhiskerLeft) (ηs_1 : Mathlib.Tactic.BicategoryLike.NormalExpr),
  (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs =
      Mathlib.Tactic.BicategoryLike.NormalExpr.cons e_1 α_1 η_1 ηs_1) =
    (e = e_1 ∧ α = α_1 ∧ η = η_1 ∧ ηs = ηs_1)
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.isUnit_or_isUnit_one_sub_self : ∀ {R : Type u_1} [inst : CommRing R] [IsLocalRing R] (a : R), IsUnit a ∨ IsUnit (1 - a)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero.sizeOf_spec : sizeOf Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero = 1
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprTransitionRule : Repr Std.Time.TimeZone.TransitionRule
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasProd_map_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {L : SummationFilter γ} {g : γ → β} (hg : Function.Injective g),
  HasProd f a (L.map { toFun := g, inj' := hg }) ↔ HasProd (f ∘ g) a L
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_toUInt8 : ∀ (n : UInt64), n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist.eq_1 : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), Metric.infEDist x s = ⨅ y ∈ s, edist x y
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom.eq_1 : ∀ (σ : Type u_1) (R : Type u_3) (n : ℕ) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.esymmAlgHom σ R n = MvPolynomial.aeval fun i => ⟨MvPolynomial.esymm σ R (↑i + 1), ⋯⟩
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.prodUnits.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Monoid α] [inst_1 : TopologicalSpace α] [inst_2 : Monoid β]
  [inst_3 : TopologicalSpace β],
  Homeomorph.prodUnits = { toEquiv := MulEquiv.prodUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges.selectionRange : Lean.DeclarationRanges → Lean.DeclarationRange
-- Lean.Parser.Term
Lean.Parser.Term.logNamedErrorMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.eval₂_coe : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (φ : R →+* S) (a : S)
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] (f : Polynomial R),
  PowerSeries.eval₂ φ a ↑f = Polynomial.eval₂ φ a f
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.dist_le_distortion_mul : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (i : ι),
  dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)
-- Init.SizeOf
/-- The "size" of an element, a natural number which decreases on fields of
each inductive type.  -/
SizeOf.sizeOf : {α : Sort u} → [self : SizeOf α] → α → ℕ
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_iSup : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {ι : Sort u_12}
  {p : ι → Seminorm 𝕜 E},
  BddAbove (Set.range p) → ∀ (e : E) {r : ℝ}, 0 < r → (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r
-- Mathlib.Order.Grade
GradeOrder.natToInt : {α : Type u_3} → [inst : Preorder α] → [GradeOrder ℕ α] → GradeOrder ℤ α
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The kernel of a divided power morphism from `I` to `J` is a sub-dp-ideal of `I`.  -/
DividedPowers.isSubDPIdeal_ker : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  {J : Ideal B} (hJ : DividedPowers J) {f : A →+* B}, hI.IsDPMorphism hJ f → hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  CategoryTheory.IsIso (D.t i j)
-- Mathlib.Algebra.CharP.Quotient
/-- `CharP.quotient'` as an `Iff`.  -/
CharP.quotient_iff : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) [CharP R n] (I : Ideal R), CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Given a submodule, corestrict to the pairing on `M ⧸ W` by
simultaneously restricting to `W.dualAnnihilator`.

See `Subspace.dualCopairing_nondegenerate`.  -/
Submodule.dualCopairing : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (W : Submodule R M) → ↥W.dualAnnihilator →ₗ[R] M ⧸ W →ₗ[R] R
-- Mathlib.Data.Bool.Basic
Bool.le_iff_imp : ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.cancel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f₁ f₂ : C(β, γ)} {g : C(α, β)},
  Function.Surjective ⇑g → (f₁.comp g = f₂.comp g ↔ f₁ = f₂)
-- Mathlib.Topology.Basic
isClosed_biInter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X},
  (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋂ i ∈ s, f i)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
Filter.EventuallyEq.mfderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → mfderiv[s] f₁ x = mfderiv[s] f x
-- Lean.Elab.DocString
/-- A string  -/
Lean.Doc.DocArg.str : Lean.StrLit → Lean.Doc.DocArg
-- Mathlib.RingTheory.Flat.Equalizer
/-- Given surjection `f : N → P` with `P` flat, then `A ⊗ ker f ≃ ker (A ⊗ f)`.
Also see `LinearMap.tensorKerEquiv` for the version with `A` flat instead.  -/
LinearMap.kerLTensorEquivOfSurjective : {R : Type u_1} →
  [inst : CommRing R] →
    {N : Type u_4} →
      {P : Type u_5} →
        [inst_1 : AddCommGroup N] →
          [inst_2 : AddCommGroup P] →
            [inst_3 : Module R N] →
              [inst_4 : Module R P] →
                [Module.Flat R P] →
                  (f : N →ₗ[R] P) →
                    Function.Surjective ⇑f →
                      (A : Type u_6) →
                        [inst_6 : AddCommGroup A] →
                          [inst_7 : Module R A] → ↥(LinearMap.lTensor A f).ker ≃ₗ[R] TensorProduct R A ↥f.ker
-- Mathlib.Computability.DFA
DFA.evalFrom_nil : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ), M.evalFrom s [] = s
-- Mathlib.RingTheory.Ideal.Oka
/-- A predicate `P : Ideal R → Prop` over the ideals of a ring `R` is said to be Oka if R satisfies
it (`P ⊤`) and whenever we have `I : Ideal R`, `P (I.colon (span {a})` and `P (I ⊔ span {a})` for
some `a : R` then `P I`.  -/
Ideal.IsOka : {R : Type u_1} → [inst : CommSemiring R] → (Ideal R → Prop) → Prop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : α} {fallback : β},
  ∅.getD a fallback = fallback
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path_image_Ioc_union : ∀ {x y : Circle}, x ≠ y → ⇑(x.path y) '' Set.Ioc 0 1 ∪ ⇑(y.path x) '' Set.Ioc 0 1 = Set.univ
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.C_inj : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (r s : R), MvPowerSeries.C r = MvPowerSeries.C s ↔ r = s
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [inst : AlgebraicGeometry.LocallyOfFinitePresentation f],
  AlgebraicGeometry.Scheme.Hom.smoothLocus f = ⊤ ↔ AlgebraicGeometry.Smooth f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.mk.sizeOf_spec : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [inst_3 : SizeOf C] (I : Type w) (X : I → C)
  (coversTop : J.CoversTop X) (generators : (i : I) → (M.over (X i)).GeneratingSections),
  sizeOf { I := I, X := X, coversTop := coversTop, generators := generators } = 1 + sizeOf I
-- Mathlib.Algebra.Order.SuccPred
monotone_of_sub_one_le : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f (a - 1) ≤ f a) → Monotone f
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.tensorProductMap : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {S' : Type u_4} {T' : Type u_5} [inst_3 : CommRing S'] [inst_4 : CommRing T'] [inst_5 : Algebra R S]
  [inst_6 : Algebra R T] [inst_7 : Algebra R S'] [inst_8 : Algebra R T'] {f : S →ₐ[R] S'},
  f.SurjectiveOnStalks → ∀ {g : T →ₐ[R] T'}, g.SurjectiveOnStalks → (Algebra.TensorProduct.map f g).SurjectiveOnStalks
-- Mathlib.Algebra.Category.ModuleCat.Free
ModuleCat.disjoint_span_sum : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact →
    ∀ {v : ι → ↑S.X₁} {u : ι ⊕ ι' → ↑S.X₂},
      LinearIndependent R (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) →
        u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v →
          Disjoint (Submodule.span R (Set.range (u ∘ Sum.inl))) (Submodule.span R (Set.range (u ∘ Sum.inr)))
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- The canonical linear map from `(P →ₛₗ[σ₁₂] M₂) ⊗[R₂] N₂` to `P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂`.  -/
TensorProduct.rTensorHomToHomRTensor : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (P : Type u_9) →
            (M₂ : Type u_12) →
              (N₂ : Type u_14) →
                [inst_2 : AddCommMonoid P] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : AddCommMonoid N₂] →
                      [inst_5 : Module R₂ M₂] →
                        [inst_6 : Module R₂ N₂] →
                          [inst_7 : Module R P] →
                            TensorProduct R₂ (P →ₛₗ[σ₁₂] M₂) N₂ →ₗ[R₂] P →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.erase0 c = Lean.Meta.Grind.AC.EqCnstrProof.erase0 c_1 → c = c_1
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_modByMonic_le : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) {q : Polynomial R}, q.Monic → (p %ₘ q).degree ≤ q.degree
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.isHadamard_submatrix_equiv_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : Semiring R] [inst_5 : StarRing R] {A : Matrix n n R} (e₁ e₂ : m ≃ n),
  (A.submatrix ⇑e₁ ⇑e₂).IsHadamard ↔ A.IsHadamard
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.comp_toAlgHom : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : DecidableEq ι] [inst_8 : AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B}
  {𝒞 : ι → Submodule R C} [inst_9 : GradedAlgebra 𝒜] [inst_10 : GradedAlgebra ℬ] [inst_11 : GradedAlgebra 𝒞]
  (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ), ↑(g.comp f) = (↑g).comp ↑f
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.tensorUnit_ρ : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Rep.{u, u, v} k G)).ρ = Representation.trivial k G k
-- Mathlib.Analysis.Normed.Module.Ball.Action
mulActionClosedBallBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → MulAction ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Tactic.GRewrite.Elab
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.GRewrite.Config
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_inv : ∀ {α : Type u_2} [inst : Inv α] (S : Set (Set α)), (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toBoundedOrder : {α : Type u_8} → [self : CompleteLattice α] → BoundedOrder α
-- Std.Http.Data.Body.Length
/-- Size of the body of a response or request.
 -/
Std.Http.Body.Length : Type
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.mono : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ ν : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f t ν → s ⊆ t → μ ≤ ν → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.idv : ∀ {n : ℕ}, Nat.Primrec'.Vec id
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- If `F` is an equivalence and `F.map f` is a normal epi, then `f` is a normal epi.  -/
CategoryTheory.equivalenceReflectsNormalEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₁, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.IsEquivalence] →
                {X Y : C} → {f : X ⟶ Y} → CategoryTheory.NormalEpi (F.map f) → CategoryTheory.NormalEpi f
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.insert_isBase_of_insert_indep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e f : α},
  e ∉ I → f ∉ I → M.IsBase (insert e I) → M.Indep (insert f I) → M.IsBase (insert f I)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_17.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithInitial Cᵒᵖ) → (x ⟶ y) → Sort u_3) (x y : C)
  (f : CategoryTheory.WithInitial.of (Opposite.op x) ⟶ CategoryTheory.WithInitial.of (Opposite.op y))
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithInitial.of (Opposite.op x) ⟶ CategoryTheory.WithInitial.of (Opposite.op y)) →
        motive (CategoryTheory.WithInitial.of (Opposite.op x)) (CategoryTheory.WithInitial.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of (Opposite.op unop)) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of (Opposite.op unop)) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f with
    | CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x => h_2 unop x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_1 x y f
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.smul_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (a : σ → R), MvPowerSeries.HasSubst (a • MvPowerSeries.X)
-- Init.Data.Nat.Basic
Nat.mul_le_mul : ∀ {n₁ m₁ n₂ m₂ : ℕ}, n₁ ≤ n₂ → m₁ ≤ m₂ → n₁ * m₁ ≤ n₂ * m₂
-- Mathlib.Order.CompleteBooleanAlgebra
biSup_inter_of_pairwise_disjoint : ∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {f : ι → α},
  Pairwise (Function.onFun Disjoint f) → ∀ (s t : Set ι), ⨆ i ∈ s ∩ t, f i = (⨆ i ∈ s, f i) ⊓ ⨆ i ∈ t, f i
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₁) {X Y : C₃}
  (f : X ⟶ Y) (j : C₂), ((F.flip₂₃.obj G).map f).app j = ((F.obj G).obj j).map f
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.isRightInversion_mul_left_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ {w : W}, cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t
-- Init.Data.Hashable
instHashableBool : Hashable Bool
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.inhabited : {α : Type u} → Inhabited (WithOne α)
-- Mathlib.NumberTheory.LSeries.Positivity
/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1` is
positive, then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`.  -/
ArithmeticFunction.LSeries_positive : ∀ {a : ℕ → ℂ}, 0 ≤ a → 0 < a 1 → ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a < ↑x → 0 < LSeries a ↑x
-- Mathlib.Analysis.CStarAlgebra.Classes
instNonUnitalCStarAlgebraProd : {A : Type u_1} → {B : Type u_2} → [NonUnitalCStarAlgebra A] → [NonUnitalCStarAlgebra B] → NonUnitalCStarAlgebra (A × B)
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.le_normalClosure : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] (K : IntermediateField F L),
  K ≤ IntermediateField.normalClosure F (↥K) L
-- Batteries.Tactic.Congr
_private.Batteries.Tactic.Congr.0.Batteries.Tactic.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Batteries.Tactic.Congr.Config
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.of_dvd_sub : ∀ {R : Type u_1} [inst : CommRing R] {a b r : Polynomial R} {m n : ℕ},
  n ≤ m →
    a.IsMonicOfDegree m →
      b.IsMonicOfDegree n → r.natDegree < m → b ∣ a - r → ∃ q, q.IsMonicOfDegree (m - n) ∧ a = q * b + r
-- Init.SimpLemmas
let_val_congr : ∀ {α : Sort u} {β : Sort v} {a a' : α} (b : α → β),
  a = a' →
    (have x := a;
      b x) =
      have x := a';
      b x
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {X Y : HopfAlgCat R} (f g : X ⟶ Y),
  HopfAlgCat.Hom.toBialgHom f = HopfAlgCat.Hom.toBialgHom g → f = g
-- Mathlib.Data.Ordmap.Invariants
Ordnode.foldr.eq_def : ∀ {α : Type u_1} {β : Sort u_2} (f : α → β → β) (x : Ordnode α) (x_1 : β),
  Ordnode.foldr f x x_1 =
    match x, x_1 with
    | Ordnode.nil, z => z
    | Ordnode.node size l x r, z => Ordnode.foldr f l (f x (Ordnode.foldr f r z))
-- Mathlib.Algebra.Lie.Basis.Prod
/-- A distinguished subalgebra of the product of two based Lie algebras with equivalent indexing
sets.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prod : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            ι₁ ≃ ι₂ →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          LieAlgebra.Basis ι₁ H₁ →
                            [inst : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} → LieAlgebra.Basis ι₂ H₂ → LieSubalgebra R (L₁ × L₂)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mkCLM_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [inst_8 : IsTopologicalAddGroup V] [inst_9 : ContinuousSMul ℝ V]
  [inst_10 : LocallyConvexSpace ℝ V] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V]
  [inst_14 : IsScalarTower ℝ 𝕜 V] (toFun : TestFunction Ω F n → V)
  (map_add : ∀ (f g : TestFunction Ω F n), toFun (f + g) = toFun f + toFun g)
  (map_smul : ∀ (c : 𝕜) (f : TestFunction Ω F n), toFun (c • f) = c • toFun f)
  (cont :
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (toFun ∘ TestFunction.ofSupportedIn K_sub_Ω))
  (a : TestFunction Ω F n), (TestFunction.mkCLM 𝕜 toFun map_add map_smul cont) a = toFun a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toList_eq_toList_rco : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_8 : Std.Rxc.IsAlwaysFinite α]
  [inst_9 : Std.Rxo.IsAlwaysFinite α] [inst_10 : Std.PRange.InfinitelyUpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α], r.toList = (r.lower...Std.PRange.succ r.upper).toList
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.ballInclusion.eq_1 : ∀ (n : ℕ),
  TopCat.ballInclusion n =
    TopCat.ofHom
      {
        toFun := fun x =>
          match x with
          | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ },
        continuous_toFun := ⋯ }
-- Mathlib.Tactic.Linter.DocString
_private.Mathlib.Tactic.Linter.DocString.0.Array.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Mathlib.RingTheory.Radical.Basic
/-- Division of an element by its radical in a Euclidean domain.  -/
EuclideanDomain.divRadical : {E : Type u_1} → [inst : EuclideanDomain E] → [NormalizationMonoid E] → [UniqueFactorizationMonoid E] → E → E
-- Init.Data.SInt.Lemmas
Int64.lt_iff_toBitVec_slt : ∀ {a b : Int64}, a < b ↔ a.toBitVec.slt b.toBitVec = true