mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Insert
Set.decidableSingleton : {α : Type u_1} → (a b : α) → [Decidable (a = b)] → Decidable (a ∈ {b})
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.mapLe h p).IsCycle ↔ p.IsCycle
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.symm_symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P), F.symm.symm = F
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a b : α}, a < b → frontier (Set.Ioc a b) = {a, b}
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely as `x` tends to `a` from the right or from the left,
then `u ↦ ∫ x in u..b, f x` has right (resp., left) derivative `-c` at `a`.  -/
intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
      StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
        Filter.Tendsto f (nhdsWithin a t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
          HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) s a
-- Init.System.IO
/-- Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file.
 -/
IO.FS.Metadata.type : IO.FS.Metadata → IO.FS.FileType
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_neg_eq_intMinSealed_sub : ∀ {n : ℕ} {x : BitVec n}, BitVec.Signed.rotate✝ (-x) = BitVec.Signed.intMinSealed✝ n - x
-- Mathlib.Algebra.Group.Subgroup.Defs
inv_mem_iff : ∀ {S : Type u_3} {G : Type u_4} [inst : InvolutiveInv G] {x : SetLike S G} [InvMemClass S G] {H : S} {x_1 : G},
  x_1⁻¹ ∈ H ↔ x_1 ∈ H
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For nonzero `I, I'`, `val_v(I*I') = val_v(I) + val_v(I')`.  -/
FractionalIdeal.count_mul : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {I I' : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 → I' ≠ 0 → FractionalIdeal.count K v (I * I') = FractionalIdeal.count K v I + FractionalIdeal.count K v I'
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacGen.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.RuleTacDescr.tacGen decl = Aesop.RuleTacDescr.tacGen decl_1) = (decl = decl_1)
-- Mathlib.Topology.IsLocalHomeomorph
isLocalHomeomorph_iff_isOpenEmbedding_restrict : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ nhds x, Topology.IsOpenEmbedding (U.domRestrict f)
-- Mathlib.Order.Interval.Set.Image
directedOn_le_Ioc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), DirectedOn (fun x1 x2 => x1 ≤ x2) (Set.Ioc a b)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
_private.Mathlib.RepresentationTheory.Homological.TateCohomology.Basic.0.CochainComplex.ConnectData.X.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Aesop.Stats.Basic
Aesop.instInhabitedGoalStats.default : Aesop.GoalStats
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- A Weierstrass curve `Y² + a₁XY + a₃Y = X³ + a₂X² + a₄X + a₆` with parameters `aᵢ`.  -/
WeierstrassCurve : Type u → Type u
-- Mathlib.Topology.EMetricSpace.Basic
SeparationQuotient.edist_mk : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (x y : X),
  edist (SeparationQuotient.mk x) (SeparationQuotient.mk y) = edist x y
-- Init.Data.Float.Float
instNegFloat : Neg Float
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_undef : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  ¬CircleIntegrable f c R → ∮ (z : ℂ) in C(c, R), f z = 0
-- Mathlib.Order.Bounds.Image
/-- An antitone map sends a least element of a set to a greatest element of its
image.  -/
AntitoneOn.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  AntitoneOn f t → IsLeast t a → IsGreatest (f '' t) (f a)
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.eq_mem_ofPred`.

---

This lemma is intended for use with `rw` where a membership predicate is needed,
hence the explicit argument and the equality in the reverse direction from normal.
See also `Set.mem_ofPred_eq` for the reverse direction applied to an argument.  -/
Set.eq_mem_setOf : ∀ {α : Type u} (p : α → Prop), p = fun x => x ∈ {a | p a}
-- Init.Data.RArray
Lean.RArray.getImpl.eq_1 : ∀ {α : Type u} (n : ℕ) (x : α), (Lean.RArray.leaf x).getImpl n = x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instIsScalarTower' : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) [inst_4 : Semiring R'] [inst_5 : SMul R' R]
  [inst_6 : Module R' A] [inst_7 : IsScalarTower R' R A], IsScalarTower R' R ↥S
-- Std.Time.Format.Modifier
Std.Time.Number.mk : ℕ → Std.Time.Number
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Free bicategory over a quiver. Its objects are the same as those in the underlying quiver.  -/
CategoryTheory.FreeBicategory : Type u → Type u
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k' (Std.Internal.List.Const.modifyKey k f l) = true),
      Std.Internal.List.getKey k' (Std.Internal.List.Const.modifyKey k f l) h =
        if (k == k') = true then k else Std.Internal.List.getKey k' l ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharTwoJNeZeroNF_iff : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R), W.IsCharTwoJNeZeroNF ↔ W.a₁ = 1 ∧ W.a₃ = 0 ∧ W.a₄ = 0
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value `∞` instead, use `Metric.hausdorffEDist`, which takes values in `ℝ≥0∞`).  -/
Metric.hausdorffDist_empty' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist ∅ s = 0
-- Mathlib.Topology.Algebra.ConstMulAction
continuousAt_const_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G]
  [inst_2 : AddAction G α] [ContinuousConstVAdd G α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} (c : G),
  ContinuousAt (fun x => c +ᵥ f x) b ↔ ContinuousAt f b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
/-- **Alias** of `CategoryTheory.NatTrans.Coequifibered.of_isIso`. -/
CategoryTheory.NatTrans.Coequifibered_of_isIso : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [CategoryTheory.IsIso α], CategoryTheory.NatTrans.Coequifibered α
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- An additive group is finitely presented if it has a finite generating set such that the kernel
of the induced map from the free additive group on that set is the normal closure
of finitely many relations.  -/
AddGroup.IsFinitelyPresented : (G : Type u_5) → [AddGroup G] → Prop
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.mkCasesAndThen : Lean.TSyntax `grind → List (Lean.TSyntax `grind) → Lean.CoreM (Lean.TSyntax `grind)
-- Init.Data.SInt.Lemmas
ISize.lt_trans : ∀ {a b c : ISize}, a < b → b < c → a < c
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.errorName.sizeOf_spec : ∀ (stx partialId : Lean.Syntax),
  sizeOf (Lean.Elab.CompletionInfo.errorName stx partialId) = 1 + sizeOf stx + sizeOf partialId
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.eq_def : ∀ {s : String.Slice} (currPos : s.Pos) (l : List (String.Slice.Pattern.SearchStep s)),
  String.Slice.Pattern.Model.splitFromSteps✝ currPos l =
    match l with
    | [] => [s.subsliceFrom currPos]
    | String.Slice.Pattern.SearchStep.rejected startPos endPos :: l =>
      String.Slice.Pattern.Model.splitFromSteps✝ currPos l
    | String.Slice.Pattern.SearchStep.matched p q :: l =>
      s.subslice! currPos p :: String.Slice.Pattern.Model.splitFromSteps✝ q l
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W₁ W₂ : CategoryTheory.MorphismProperty C},
  W₁ ≤ W₂ →
    ∀ (J : Type u_2) [inst_1 : CategoryTheory.Category.{v_2, u_2} J], W₁.colimitsOfShape J ≤ W₂.colimitsOfShape J
-- Init.Data.Fin.Lemmas
Fin.ofNat_add : ∀ {n : ℕ} [inst : NeZero n] (x : ℕ) (y : Fin n), Fin.ofNat n x + y = Fin.ofNat n (x + ↑y)
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_empty_left : ∀ {α : Type u_2} (s : Finset α), Disjoint ∅ s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mkIso'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsMonHom e.hom],
  CategoryTheory.Mon.mkIso' e =
    { hom := { hom := e.hom, isMonHom_hom := inst_4 }, inv := { hom := e.inv, isMonHom_hom := ⋯ }, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
Fin.addRothNumber_eq_rothNumberNat : ∀ {n : ℕ} {k : Fin (n + 1)}, 2 * ↑k ≤ n → addRothNumber (Finset.Iio k) = rothNumberNat ↑k
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_diff_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.rnDeriv_ae_eq_condExp : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m ≤ m0}
  [hμm : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → ℝ},
  MeasureTheory.Integrable f μ →
    MeasureTheory.SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] μ[f | m]
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
/-- An absolute value `abv : R → S` is Euclidean if it is compatible with the
`EuclideanDomain` structure on `R`, namely `abv` is strictly monotone with respect to the well
founded relation `≺` on `R`.  -/
AbsoluteValue.IsEuclidean : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → Prop
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.proj.injEq : ∀ (typeName : Lean.Name) (idx nargs : ℕ) (typeName_1 : Lean.Name) (idx_1 nargs_1 : ℕ),
  (Lean.Meta.RefinedDiscrTree.Key.proj typeName idx nargs =
      Lean.Meta.RefinedDiscrTree.Key.proj typeName_1 idx_1 nargs_1) =
    (typeName = typeName_1 ∧ idx = idx_1 ∧ nargs = nargs_1)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_map : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {M : Type v} {N : Type w}
  (g : M → N) (f : Convexity.StdSimplex R M), (Convexity.StdSimplex.map g f).weights = Finsupp.mapDomain g f.weights
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffMul I n G] {f g : M → G}, ContMDiff I' I n f → ContMDiff I' I n g → ContMDiff I' I n (f * g)
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
/-- A variant of `isPivotedBy_iff` phrased with `Matrix.IsLeadingEntry`.  -/
Matrix.isPivotedBy_iff' : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n}
  [inst_1 : PartialOrder m] [inst_2 : LinearOrder n],
  A.IsPivotedBy l ↔
    Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_toSet : ∀ (a u : PSet.{u}), a ∈ u.toSet ↔ a ∈ u
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.sinh_arcosh : ∀ {x : ℝ}, 1 ≤ x → Real.sinh (Real.arcosh x) = √(x ^ 2 - 1)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instTypeNameElabImage : TypeName Lean.Doc.ElabImage✝
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm is subadditive.  -/
AddGroupSeminorm.add_le' : ∀ {G : Type u_6} [inst : AddGroup G] (self : AddGroupSeminorm G) (r s : G),
  self.toFun (r + s) ≤ self.toFun r + self.toFun s
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.inv_mem_inv : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] (s : NonemptyInterval α),
  ∀ a ∈ s, a⁻¹ ∈ s⁻¹
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.neg` -/
DifferentiableAt.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun i => -f i) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.rfl : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.Equiv t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_le_nsmul_iff_right : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M}
  {n : ℕ}, n ≠ 0 → (n • a ≤ n • b ↔ a ≤ b)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.principal_inf : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ (s' : Set α), (Filter.principal s' ⊓ l).HasBasis p fun i => s' ∩ s i
-- Mathlib.RingTheory.MvPolynomial.EulerIdentity
/-- Euler's identity for weighted homogeneous polynomials.  -/
MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {φ : MvPolynomial σ R} [inst_1 : Fintype σ] {n : ℕ} {w : σ → ℕ},
  MvPolynomial.IsWeightedHomogeneous w φ n → ∑ i, w i • (MvPolynomial.X i * (MvPolynomial.pderiv i) φ) = n • φ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_rpow_inv : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : NNReal), (x ^ y) ^ y⁻¹ = x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_ι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C}
  (h_1 : (t.truncGE b).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGTπ a).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGTIsoTruncGE a b h).hom.app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) h_1
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x}, VectorField.mpullback I I' f (-V) = -VectorField.mpullback I I' f V
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.IndepFun.mgf_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * Y ω)) μ →
        ProbabilityTheory.mgf (X + Y) μ t = ProbabilityTheory.mgf X μ t * ProbabilityTheory.mgf Y μ t
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_lt : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] (a b : WithZero (Multiplicative α)),
  WithZero.toMulBot a < WithZero.toMulBot b ↔ a < b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} (pullback : C)
  (p₁ : pullback ⟶ X₁) (p₂ : pullback ⟶ X₂)
  (condition : CategoryTheory.CategoryStruct.comp p₁ f₁ = CategoryTheory.CategoryStruct.comp p₂ f₂)
  (isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁ p₂ condition)) (p : pullback ⟶ S)
  (hp₁ : autoParam (CategoryTheory.CategoryStruct.comp p₁ f₁ = p) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam)
  (pullback_1 : C) (p₁_1 : pullback_1 ⟶ X₁) (p₂_1 : pullback_1 ⟶ X₂)
  (condition_1 : CategoryTheory.CategoryStruct.comp p₁_1 f₁ = CategoryTheory.CategoryStruct.comp p₂_1 f₂)
  (isLimit_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁_1 p₂_1 condition_1))
  (p_1 : pullback_1 ⟶ S)
  (hp₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp p₁_1 f₁ = p_1) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam),
  ({ pullback := pullback, p₁ := p₁, p₂ := p₂, condition := condition, isLimit := isLimit, p := p, hp₁ := hp₁ } =
      { pullback := pullback_1, p₁ := p₁_1, p₂ := p₂_1, condition := condition_1, isLimit := isLimit_1, p := p_1,
        hp₁ := hp₁_1 }) =
    (pullback = pullback_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1 ∧ isLimit ≍ isLimit_1 ∧ p ≍ p_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList.congr_simp : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α] (r r_1 : Std.Roc α),
  r = r_1 → r.toList = r_1.toList
-- Lean.Meta.Tactic.Grind.EMatch
/-- Matches arguments of pattern `p` with term `e`. Returns `some` if successful,
and `none` otherwise. It may update `c`s assignment and list of constraints to be
processed.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.matchArgs? : Lean.Meta.Grind.EMatch.Choice → Lean.Expr → Lean.Expr → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.match_1.eq_2 : ∀ {α : Type u_2} (n : ℕ) (motive : (x : ℕ) → x ≤ n → α → Sort u_1) (m : ℕ) (h : m.succ ≤ n) (a : α)
  (h_1 : (h : 0 ≤ n) → (a : α) → motive 0 h a) (h_2 : (m : ℕ) → (h : m.succ ≤ n) → (a : α) → motive m.succ h a),
  (match m.succ, h, a with
    | 0, h, a => h_1 h a
    | m.succ, h, a => h_2 m h a) =
    h_2 m h a
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverCoverOfIsIsoOfIsOver : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        [inst_2 : P.ContainsIdentities] →
          [inst_3 : P.RespectsIso] →
            {X Y : AlgebraicGeometry.Scheme} →
              (f : X ⟶ Y) →
                [inst_4 : X.Over S] →
                  [inst_5 : Y.Over S] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      [inst_7 : CategoryTheory.IsIso f] →
                        AlgebraicGeometry.Scheme.Cover.Over S (AlgebraicGeometry.Scheme.coverOfIsIso f)
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D},
  F.IsFinitelyAccessible ↔ CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
QuadraticForm.dualProdProdIsometry_invFun : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  (a : (Module.Dual R M × M) × Module.Dual R N × N),
  QuadraticForm.dualProdProdIsometry.invFun a = (LinearMap.coprod a.1.1 a.2.1, a.1.2, a.2.2)
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top : ∀ {𝕜 : 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'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → (↑(mfderiv% ↑e x)).range = ⊤
-- Init.Data.Dyadic.Basic
Dyadic.instLT : LT Dyadic
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_mk : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  (h : A.det = 1), ↑⟨A, h⟩ = A
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoind_coindToInd : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) [inst_3 : S.FiniteIndex],
  A.coindToInd ∘ₗ A.indToCoind = LinearMap.id
-- Init.Data.UInt.Lemmas
UInt32.mod_lt : ∀ (a : UInt32) {b : UInt32}, 0 < b → a % b < b
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocCommSemiring.toCommMagma : {α : Type u} → [self : NonUnitalNonAssocCommSemiring α] → CommMagma α
-- Mathlib.Analysis.Complex.Basic
Filter.Tendsto.ofReal : ∀ {α : Type u_2} {l : Filter α} {f : α → ℝ} {x : ℝ},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.singleAddHom.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M),
  MonoidAlgebra.singleAddHom m = { toFun := MonoidAlgebra.single m, map_zero' := ⋯, map_add' := ⋯ }