mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The ideal of `A` in which the two divided power structures `hI` and `hI'` coincide.  -/
DividedPowers.dpEqualizer : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → DividedPowers I → DividedPowers I → Ideal A
-- Mathlib.Data.Set.Image
Set.leftInverse_rangeFactorization_iff_injective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  Function.LeftInverse (Set.rangeSplitting f) (Set.rangeFactorization f) ↔ Function.Injective f
-- Mathlib.GroupTheory.Congruence.Defs
/-- The coercion to the quotient of a congruence relation commutes with multiplication (by
definition).  -/
Con.coe_mul : ∀ {M : Type u_1} [inst : Mul M] {c : Con M} (x y : M), ↑(x * y) = ↑x * ↑y
-- Std.Sat.AIG.CNF
/-- Produce a Tseitin style CNF for a `Decl.false`, using `output` as the tree node variable.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.falseToCNF : {α : Type u_1} → α → Std.Sat.CNF α
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.instSMulSubtypeMemSubringSubalgebraIntegralClosure : {K : Type u_3} →
  {L : Type u_4} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (A : Subring K) → SMul ↥A ↥(integralClosure (↥A) L)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.updateBucket.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β))
  (h : 0 < self.size) (k : α) (f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.updateBucket self h k f =
    match Std.DHashMap.Internal.mkIdx self.size h (hash k) with
    | ⟨i, h⟩ => self.uset i (f self[i]) h
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.squashSeq.match_1.eq_1 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) × Option (GenContFract.Pair K) → Sort u_2)
  (gp_n gp_succ_n : GenContFract.Pair K)
  (h_1 : (gp_n gp_succ_n : GenContFract.Pair K) → motive (some gp_n, some gp_succ_n))
  (h_2 : (x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K)) → motive x),
  (match (some gp_n, some gp_succ_n) with
    | (some gp_n, some gp_succ_n) => h_1 gp_n gp_succ_n
    | x => h_2 x) =
    h_1 gp_n gp_succ_n
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.not_noRepetition_append_of_left : ∀ {α : Type u} {a : α} {l m : List α}, ¬NoRepetition✝ a l → ¬NoRepetition✝ a (l ++ m)
-- Mathlib.Topology.Inseparable
IsOpen.continuous_piecewise_of_specializes : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f g : X → Y}
  [inst_2 : DecidablePred fun x => x ∈ s],
  IsOpen s → Continuous f → Continuous g → (∀ (x : X), f x ⤳ g x) → Continuous (s.piecewise f g)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.fiberwise_left : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α}
  {f : α × β → E} {g : α × β → F} {l' : Filter β},
  f =Θ[l ×ˢ l'] g → ∀ᶠ (y : β) in l', (fun x => f (x, y)) =Θ[l] fun x => g (x, y)
-- Mathlib.Data.Matrix.Basic
LinearEquiv.mapMatrix_apply : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [inst_6 : RingHomInvPair σᵣₛ σₛᵣ]
  [inst_7 : RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) (M : Matrix m n α), f.mapMatrix M = M.map ⇑f
-- Batteries.Data.List.Matcher
/-- Find all start and end positions of all infix sublists of `l` matching `m.pattern`.
The sublists may be overlapping.
 -/
List.Matcher.findAll : {α : Type u_1} → [BEq α] → List.Matcher α → List α → Array (ℕ × ℕ)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.mk.inj : ∀ {L : Type w} {R : Type w'} {fst snd : L → R} {L_1 : Type w} {R_1 : Type w'} {fst_1 snd_1 : L_1 → R_1},
  { L := L, R := R, fst := fst, snd := snd } = { L := L_1, R := R_1, fst := fst_1, snd := snd_1 } →
    L = L_1 ∧ R = R_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {t : Set X} {μ : MeasureTheory.Measure X}, (∀ x ∈ t, f x = 0) → ∫ (x : X) in t, f x ∂μ = 0
-- Mathlib.Algebra.Group.Defs
MulOne.mk : {M : Type u_2} → [toOne : One M] → [toMul : Mul M] → MulOne M
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instPreservesLimitOppositeDiscreteFunctorCompOpObjFunctorEvalOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A] (J : Type w) (f : J → CategoryTheory.Limits.FormalCoproduct C)
  (F : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor (Opposite.op ∘ f))
    ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_zero_measure : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ}, ProbabilityTheory.variance X 0 = 0
-- Mathlib.FieldTheory.Galois.Infinite
/-- The Galois correspondence as a `GaloisInsertion`  -/
InfiniteGalois.GaloisInsertionIntermediateFieldClosedSubgroup : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [inst_3 : IsGalois k K] →
            GaloisInsertion (⇑OrderDual.toDual ∘ fun E => { toSubgroup := E.fixingSubgroup, isClosed' := ⋯ })
              ((fun H => IntermediateField.fixedField ↑H) ∘ ⇑OrderDual.toDual)
-- Mathlib.Data.ZMod.Basic
Prod.fst_zmod_cast : ∀ {n : ℕ} {R : Type u_1} [inst : AddGroupWithOne R] {S : Type u_2} [inst_1 : AddGroupWithOne S] (a : ZMod n),
  a.cast.1 = a.cast
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulLeft_toEquiv : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] (a : α),
  (OrderIso.mulLeft a).toEquiv = Equiv.mulLeft a
-- Mathlib.Topology.Connected.PathConnected
Subgroup.pathComponentOne.eq_1 : ∀ (G : Type u_4) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  Subgroup.pathComponentOne G = { toSubmonoid := Submonoid.pathComponentOne G, inv_mem' := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_eq_of_max : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p : AddMonoidAlgebra R A} [inst_3 : AddZeroClass A] {b : B},
  b ∈ Set.range D →
    Function.invFun D b ∈ p.coeff.support → (∀ a ∈ p.coeff.support, D a ≤ b) → AddMonoidAlgebra.supDegree D p = b
-- Lean.Meta.Tactic.Grind.Types
/-- Copy `parents` to the parents of `root`.
`root` must be the root of its equivalence class.
 -/
Lean.Meta.Grind.copyParentsTo : Lean.Meta.Grind.ParentSet → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.M.mk.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (x : (j : J) × ↑(F.obj j)),
  MonCat.FilteredColimits.M.mk F x = (F.comp (CategoryTheory.forget MonCat)).ιColimitType x.fst x.snd
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_of_ae_nnnorm_bound : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : α →ₘ[μ] E} (C : NNReal),
  (∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ C) → f ∈ MeasureTheory.Lp E p μ
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.tensorCotangentInvFun_smul_mk : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {P : Algebra.Extension R S}
  {Q : Algebra.Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring]
  (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
  (H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))) (x : Q.Ring) (y : ↥P.ker),
  (Algebra.Extension.tensorCotangentInvFun f halg H) (x • Algebra.Extension.Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) =
    x • 1 ⊗ₜ[S] Algebra.Extension.Cotangent.mk y
-- Lean.Setup
/-- The name of the plugin initialization function symbol.
  If `none`, the symbol is derived from the file name of the shared library.
   -/
Lean.Plugin.initFn? : Lean.Plugin → Option String
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.map_esymm : ∀ {S : Type u_4} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Fintype σ]
  (n : ℕ) (f : R →+* S), (MvPolynomial.map f) (MvPolynomial.esymm σ R n) = MvPolynomial.esymm σ S n
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_update_le : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R), (p.update n a).degree ≤ max p.degree ↑n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ),
  (CategoryTheory.simplicialCosimplicialEquiv C).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op
-- Mathlib.Data.Set.Subset
/-- **Alias** of `Set.image_val_sdiff`. -/
Set.image_val_diff : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, Subtype.val '' (D \ E) = Subtype.val '' D \ Subtype.val '' E
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraphReindexIso_apply : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} (A : Matrix V V α) [inst : MulZeroOneClass α] [inst_1 : Nontrivial α]
  (h : A.IsAdjMatrix) (f : V ≃ W) (a : W), (Matrix.IsAdjMatrix.toGraphReindexIso A h f) a = f.symm a
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.exceptT : Lean.Elab.Do.MonadInfo →
  Lean.Name →
    Lean.Name →
      Lean.Elab.Do.DoElabM Lean.Elab.Do.ReturnCont → Lean.Expr → Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack
-- Init.Data.Int.LemmasAux
Int.toNat_le_toNat : ∀ {n m : ℤ}, n ≤ m → n.toNat ≤ m.toNat
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.eq_class_eq_leftCoset : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : α), {x | ↑x = ↑g} = g +ᵥ ↑s
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_neg : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R),
  WittVector.ghostFun✝ (-x) = -WittVector.ghostFun✝ x
-- Mathlib.Analysis.Convex.Basic
Convex.add_smul_sub_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E} [AddRightMono 𝕜],
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → ∀ {t : 𝕜}, t ∈ Set.Icc 0 1 → x + t • (y - x) ∈ s
-- Lean.Data.Format
Lean.Std.Format.getUnicode : Lean.Options → Bool
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run'.match_1.splitter : {α : Type u_1} →
  (n : ℕ) →
    (motive : { l // l.length = (n + 2) / 2 } × { l // l.length = (n + 2 + 1) / 2 } → Sort u_2) →
      (x : { l // l.length = (n + 2) / 2 } × { l // l.length = (n + 2 + 1) / 2 }) →
        ((l : { l // l.length = (n + 2) / 2 }) → (r : { l // l.length = (n + 2 + 1) / 2 }) → motive (l, r)) → motive x
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.IsTotallyUnimodular.apply : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] {A : Matrix m n R},
  A.IsTotallyUnimodular → ∀ (i : m) (j : n), A i j ∈ Set.range SignType.cast
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_addY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_ofNat : ∀ (n : ℕ), (↑n).NF
-- Lean.Attributes
Lean.AttributeImplBuilderTable : Type
-- Init.Data.Array.Find
Array.find?_replicate : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α},
  Array.find? p (Array.replicate n a) = if n = 0 then none else if p a = true then some a else none
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β},
  StrictConvexOn 𝕜 s f → StrictConvexOn 𝕜 s g → StrictConvexOn 𝕜 s (f + g)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert!_fst_eq_containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsert! a b t).1 = (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).1
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
inTangentCoordinates_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_9} (f : N → H) (g : N → H') (ϕ : N → E →L[𝕜] E') (x₀ : N),
  inTangentCoordinates I I' f g ϕ x₀ = ϕ
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_filterM : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o]
  [inst_9 : Std.Internal.Do.Assertion Pred] [inst_10 : Std.Internal.Do.Assertion EPred]
  [inst_11 : Std.Internal.Do.WPMonad o Pred EPred] [inst_12 : Std.IteratorLoop α m n] [inst_13 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_16 : MonadLiftT m n] [inst_17 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ}
  {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← liftM (f b)
          if __do_lift.down = true then g d b else pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.filterM f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t₁ t₂ : Set β}, s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending
to `0`, indexed by any sequence of finite types.  -/
MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
  {ι : β → Type u_5} [inst_3 : (n : β) → Fintype (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal),
  Filter.Tendsto r l (nhds 0) →
    ∀ (t : (n : β) → ι n → Set X),
      (∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) →
        (∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
          (MeasureTheory.Measure.hausdorffMeasure d) s ≤ Filter.liminf (fun n => ∑ i, Metric.ediam (t n i) ^ d) l
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.addGroupSeminormClass : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  [NoZeroDivisors S], AddGroupSeminormClass (AbsoluteValue R S) R S
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.coconeOfHasColimitEval_ι_app_f : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] (j : J) (n : ι),
  ((HomologicalComplex.coconeOfHasColimitEval F).ι.app j).f n =
    CategoryTheory.Limits.colimit.ι (F.comp (HomologicalComplex.eval C c n)) j
-- Mathlib.Analysis.Complex.Basic
Complex.antilipschitz_equivRealProd : AntilipschitzWith (NNReal.sqrt 2) ⇑Complex.equivRealProd
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- Functor translating a monoid object in a functor category
to a functor into the category of monoid objects.
 -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor (CategoryTheory.Mon (CategoryTheory.Functor C D))
            (CategoryTheory.Functor C (CategoryTheory.Mon D))
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.prepareTriggers : Array Lean.Name → optParam Float 3.0 → Lean.MetaM (Lean.NameMap (List (Lean.Name × Float)))
-- Mathlib.Data.EReal.Operations
/-- If `-a < b` then `-b < a` on `EReal`.  -/
EReal.neg_lt_of_neg_lt : ∀ {a b : EReal}, -a < b → -b < a
-- Mathlib.Topology.Algebra.Constructions
Units.isOpenMap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : Monoid N] {f : M →* N}, Function.Injective ⇑f → IsOpenMap ⇑f → IsOpenMap ⇑(Units.map f)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_uIcc : ∀ {n : ℕ} (a b : Fin n), Finset.map Fin.valEmbedding (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.mk.sizeOf_spec : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : SizeOf 𝕜] [inst_16 : SizeOf E]
  [inst_17 : SizeOf H] [inst_18 : SizeOf M] [inst_19 : SizeOf F] [inst_20 : (a : M) → SizeOf (V a)]
  (toFun : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x)
  (isCovariantDerivativeOnUniv : IsCovariantDerivativeOn F toFun),
  sizeOf { toFun := toFun, isCovariantDerivativeOnUniv := isCovariantDerivativeOnUniv } =
    1 + sizeOf isCovariantDerivativeOnUniv
-- Aesop.Script.Step
Aesop.Script.LazyStep.mk.injEq : ∀ (preState : Lean.Meta.SavedState) (preGoal : Lean.MVarId) (tacticBuilders : Array Aesop.Script.TacticBuilder)
  (tacticBuilders_ne : autoParam (0 < tacticBuilders.size) Aesop.Script.LazyStep.tacticBuilders_ne._autoParam)
  (postState : Lean.Meta.SavedState) (postGoals : Array Lean.MVarId) (preState_1 : Lean.Meta.SavedState)
  (preGoal_1 : Lean.MVarId) (tacticBuilders_1 : Array Aesop.Script.TacticBuilder)
  (tacticBuilders_ne_1 : autoParam (0 < tacticBuilders_1.size) Aesop.Script.LazyStep.tacticBuilders_ne._autoParam)
  (postState_1 : Lean.Meta.SavedState) (postGoals_1 : Array Lean.MVarId),
  ({ preState := preState, preGoal := preGoal, tacticBuilders := tacticBuilders, tacticBuilders_ne := tacticBuilders_ne,
        postState := postState, postGoals := postGoals } =
      { preState := preState_1, preGoal := preGoal_1, tacticBuilders := tacticBuilders_1,
        tacticBuilders_ne := tacticBuilders_ne_1, postState := postState_1, postGoals := postGoals_1 }) =
    (preState = preState_1 ∧
      preGoal = preGoal_1 ∧ tacticBuilders = tacticBuilders_1 ∧ postState = postState_1 ∧ postGoals = postGoals_1)
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.continuous_multichoose : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ), Continuous fun x => Ring.multichoose x k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isSome_apply_of_mem_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : m.WF)
  (h' : k ∈ Std.DHashMap.Raw.filterMap f m), (f (m.getKey k ⋯) (Std.DHashMap.Raw.Const.get m k ⋯)).isSome = true
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Monoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G] (f : ContMDiffMap I I' N G n) (n_1 : ℕ), ⇑(f ^ n_1) = ⇑f ^ n_1
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Finite.algHom : ∀ (K : Type u_1) (M : Type u_2) (L : Type v) [inst : CommRing K] [inst_1 : Ring M] [inst_2 : Algebra K M]
  [Module.Free K M] [Module.Finite K M] [inst_5 : CommRing L] [IsDomain L] [inst_7 : Algebra K L], Finite (M →ₐ[K] L)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toList_rcc : ∀ {m n i : ℕ} (_h : i < (m...=n).toList.length), (m...=n).toList[i] = m + i
-- Mathlib.Data.ZMod.Basic
ZModModule.periodicPts_add_left : ∀ (n : ℕ) {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod n) G] [NeZero n] (x : G),
  (Function.periodicPts fun x_1 => x + x_1) = Set.univ
-- Mathlib.Order.CompleteLattice.Defs
isGLB_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] (s : Set α), IsGLB s (sInf s)
-- Mathlib.Data.List.Zip
List.zipWith3_same_mid : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → α → γ) (la : List α) (lb : List β),
  List.zipWith3 f la lb la = List.zipWith (fun a b => f a b a) la lb
-- Mathlib.Data.Setoid.Partition
/-- Combine functions with disjoint domains into a new function.
You can use the regular expression `def.*piecewise` to search for
other ways to define piecewise functions in mathlib4.  -/
IndexedPartition.piecewise : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → IndexedPartition s → {β : Type u_3} → (ι → α → β) → α → β
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocEntry.mk : Lean.Meta.Simp.SimprocOLeanEntry → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc → Lean.Meta.Simp.SimprocEntry
-- Mathlib.RingTheory.Perfection
Perfection.instCharP : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  CharP (Perfection R p) p
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.liftp_iff : ∀ {P : PFunctor.{uA, uB}} {α : Type u} (p : α → Prop) (x : ↑P α),
  Functor.Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)
-- Mathlib.Algebra.Lie.Engel
LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K : LieSubalgebra R L}, LieAlgebra.IsEngelian R ↥K → K < K.normalizer → ∃ K', LieAlgebra.IsEngelian R ↥K' ∧ K < K'