mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_fun_sum_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_3}
  {f : ι → E → F} {u : Finset ι} {n : ℕ} {x : E},
  (∀ j ∈ u, ContDiffAt 𝕜 (↑n) (f j) x) →
    iteratedFDeriv 𝕜 n (fun z => ∑ j ∈ u, f j z) x = ∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RccSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxcIterator α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsZeroApply.zero_apply`. -/
zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_of_wellQuasiOrdered : ∀ {α : Type u_2} {r : α → α → Prop}, WellQuasiOrdered r → ∀ (s : Set α), s.PartiallyWellOrderedOn r
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.get!_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], m₁.Equiv m₂ → m₁.get! k = m₂.get! k
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_rooIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {t_ord : t.Ordered} {lowerBound upperBound : α},
  (Std.DTreeMap.Internal.rooIterator t lowerBound upperBound).toList =
    List.filter (fun e => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLT = true))
      t.toList
-- Mathlib.Topology.Defs.Basic
/-- The interior of a set `s` is the largest open subset of `s`.  -/
interior : {X : Type u} → [TopologicalSpace X] → Set X → Set X
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulToBackwardSearcherModel.defaultImplementation : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.StrictBackwardPattern pat] [inst_2 : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat],
  String.Slice.Pattern.Model.LawfulToBackwardSearcherModel pat
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.measure_sum_seq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [h : ProbabilityTheory.IsSFiniteKernel κ] (a : α), (MeasureTheory.Measure.sum fun n => (κ.seq n) a) = κ a
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_linMulLin : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Invertible 2] (f g : M →ₗ[R] R),
  QuadraticMap.associated (QuadraticMap.linMulLin f g) =
    ⅟2 • ((LinearMap.mul R R).compl₁₂ f g + (LinearMap.mul R R).compl₁₂ g f)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_pos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, 0 < a → 0 < a⁺
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.fintypePowers : {M : Type u_1} → [inst : Monoid M] → {a : M} → [Fintype M] → Fintype ↥(Submonoid.powers a)
-- Aesop.RuleTac
Aesop.RuleTacDescr.run : Aesop.RuleTacDescr → Aesop.RuleTac
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_decreaseBy : ∀ {p : String.Pos.Raw} {n : ℕ}, (p.decreaseBy n).byteIdx = p.byteIdx - n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1π_comp_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ 1))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π B))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ f φ)) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.ι₀_desc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₀ (SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) = f₀
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [Nonempty J], ⊥.limitsOfShape J = ⊥
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sshiftRight'_of_msb_false : ∀ {w : ℕ} {x y : BitVec w}, x.msb = false → (x.sshiftRight' y).toFin = Fin.ofNat (2 ^ w) (x.toNat >>> y.toNat)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Exp
_private.Mathlib.Analysis.Complex.UpperHalfPlane.Exp.0.term𝕢 : Lean.ParserDescr
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.module_of_finite`.

---

A module with a finite ring of scalars is torsion.  -/
AddMonoid.IsTorsion.module_of_finite : ∀ (R : Type u_3) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Ring R] [Finite R] [Module R M], IsAddTorsion M
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
commGroupAddCommGroupEquivalence_inverse : commGroupAddCommGroupEquivalence.inverse = AddCommGrpCat.toCommGrp
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- Given a subset `F`, an entourage `U` and an integer `n`, a subset `s` of `F` is a
`(U, n)`-dynamical net of `F` if no two orbits of length `n` of points in `s` shadow each other.  -/
Dynamics.IsDynNetIn : {X : Type u_1} → (X → X) → Set X → SetRel X X → ℕ → Set X → Prop
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.ncard_primesOver_mul_ncard_primesOver : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [FaithfulSMul A B]
  {p : Ideal A} (P : Ideal B) [P.IsPrime] [P.LiesOver p] (G : Type u_3) [inst_6 : Group G] [Finite G]
  [inst_8 : MulSemiringAction G B] [IsGaloisGroup G A B] (C : Type u_4) [inst_10 : CommRing C] [IsDomain C]
  [inst_12 : Algebra A C] [inst_13 : Algebra B C] [FaithfulSMul B C] [IsScalarTower A B C] (GAC : Type u_5)
  [inst_16 : Group GAC] [Finite GAC] [inst_18 : MulSemiringAction GAC C] [IsGaloisGroup GAC A C],
  (p.primesOver B).ncard * (P.primesOver C).ncard = (p.primesOver C).ncard
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.iso.congr_simp : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y), CategoryTheory.PreservesImage.iso L f = CategoryTheory.PreservesImage.iso L f
-- Mathlib.Data.EReal.Basic
EReal.toReal_one : EReal.toReal 1 = 1
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.isLeft_right : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {y : γ ⊕ δ} {a : α},
  Sum.LiftRel r s (Sum.inl a) y → y.isLeft = true
-- Mathlib.Data.ZMod.Aut
Units.mkOfMulEqOne.congr_simp : ∀ {α : Type u} [inst : Monoid α] [inst_1 : IsDedekindFiniteMonoid α] (a a_1 : α) (e_a : a = a_1) (b b_1 : α)
  (e_b : b = b_1) (hab : a * b = 1), Units.mkOfMulEqOne a b hab = Units.mkOfMulEqOne a_1 b_1 ⋯
-- Mathlib.Data.Rat.Floor
Rat.isInt_intCeil_ofIsRat_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (r : α)
  (n d : ℕ), Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsInt ⌈r⌉ (Int.negOfNat (n / d))
-- Mathlib.Data.List.Rotate
List.rotate_eq_drop_append_take : ∀ {α : Type u} {l : List α} {n : ℕ}, n ≤ l.length → l.rotate n = List.drop n l ++ List.take n l
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.toPartOrd : FinPartOrd → PartOrd
-- Mathlib.Topology.Algebra.Monoid
instContinuousMulOrderDual : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], ContinuousMul Mᵒᵈ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insertIfNew k v).isEmpty = false
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_mul' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s t : Set α},
  interior s * interior t ⊆ interior (s * t)
-- Init.Data.String.Length
_private.Init.Data.String.Length.0.Nat.repeat.match_1.splitter : {α : Type u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((a : α) → motive 0 a) → ((n : ℕ) → (a : α) → motive n.succ a) → motive x x_1
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.affineLocally_iff_affineOpens_le : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : AlgebraicGeometry.Scheme}
  (f : X ⟶ Y),
  AlgebraicGeometry.affineLocally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
      P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))
-- Mathlib.Tactic.Order.ToInt
/-- Translates a set of values in a linear ordered type to `ℤ`,
preserving all the facts except for `.isTop` and `.isBot`. We assume that these facts are filtered
at the preprocessing step.  -/
Mathlib.Tactic.Order.ToInt.translateToInt : {u : Lean.Level} →
  (type : Q(Type u)) →
    Q(LinearOrder «$type») →
      Array Mathlib.Tactic.Order.AtomicFact →
        Mathlib.Tactic.AtomM (Std.HashMap ℕ Q(ℤ) × Array Mathlib.Tactic.Order.AtomicFact)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.sInf_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S : Set (IntermediateField F E)), (sInf S).toSubfield = sInf (IntermediateField.toSubfield '' S)
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.constOn_of_comp : ∀ {X : Type u_1} {E : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace A] {p : E → X}
  {s : Set A} {g : A → E},
  IsSeparatedMap p →
    IsLocallyInjective p →
      IsPreconnected s →
        ContinuousOn g s → (∀ a ∈ s, ∀ a' ∈ s, p (g a) = p (g a')) → ∀ {a a' : A}, a ∈ s → a' ∈ s → g a = g a'
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A functor preserves effective epimorphic families if it maps effective epimorphic families to
effective epimorphic families.
 -/
CategoryTheory.Functor.PreservesEffectiveEpiFamilies.preserves : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D}
  [self : F.PreservesEffectiveEpiFamilies] {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B)
  [CategoryTheory.EffectiveEpiFamily X π], CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)
-- Mathlib.Algebra.Group.ULift
ULift.addLeftCancelMonoid : {α : Type u} → [AddLeftCancelMonoid α] → AddLeftCancelMonoid (ULift.{u_1, u} α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_inter_le_size_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], (t₁ ∩ t₂).size ≤ t₂.size
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.comp_add : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y')
  (eZ : L.obj Z ≅ Z') (f : X' ⟶ Y') (g₁ g₂ : Y' ⟶ Z'),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Localization.Preadditive.add W eY eZ g₁ g₂) =
    CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f g₁)
      (CategoryTheory.CategoryStruct.comp f g₂)
-- Mathlib.Topology.Maps.Strict.Group
/-- The isomorphism of topological groups `G ⧸ f.ker ≃ f.range` given by a strict group
homomorphism `f`. This is an avatar of the first isomorphism theorem.  -/
ContinuousMulEquiv.quotientKerEquivRange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group H] →
        {f : G →* H} →
          [inst_2 : TopologicalSpace G] →
            [inst_3 : TopologicalSpace H] → Topology.IsStrictMap ⇑f → G ⧸ f.ker ≃ₜ* ↥f.range
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_eq_bot : ∀ {R : Type u_2} [inst : NonAssocRing R] {S : Subring Rᵐᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Mathlib.Algebra.Group.Equiv.Defs
Monoid.End.equiv_apply : ∀ {M : Type u_9} [inst : MulOne M] (f : Monoid.End M) (x : M), ((Monoid.End.equiv M) f) x = f x
-- Mathlib.Tactic.Choose
/-- **Alias** of `Mathlib.Tactic.Choose.mkSometimes`.

---

Given `α : Sort u`, `nonemp : Nonempty α`, `p : α → Prop`, a context of free variables
`ctx`, and a pair of an element `val : α` and `spec : p val`,
`mkSometimes u α nonemp p ctx (val, spec)` produces another pair `val', spec'`
such that `val'` does not have any free variables from elements of `ctx` whose types are
propositions. This is done by applying `Function.sometimes` to abstract over all the propositional
arguments.  -/
Mathlib.Tactic.Choose.mk_sometimes : Lean.Level →
  Lean.Expr → Lean.Expr → Lean.Expr → List Lean.Expr → Lean.Expr × Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Data.Rat.Defs
Rat.zero_ne_one : 0 ≠ 1
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι)
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.CategoryWithHomology C] [inst_5 : CategoryTheory.CategoryWithHomology D]
  [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] [inst_7 : F.Additive] [inst_8 : F.PreservesHomology]
  [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_10 : c.QFactorsThroughHomotopy C]
  [inst_11 : c.QFactorsThroughHomotopy D]
  [inst_12 : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)],
  F.mapHomologicalComplexUpToQuasiIsoFactorsh c = F.mapHomologicalComplexUpToQuasiIsoFactorsh c
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Same as `getImportRewrites`, but for lemmas from the current file.  -/
Mathlib.Tactic.LibraryRewrite.getModuleRewrites : Lean.Expr → Lean.MetaM (Array (Array (Mathlib.Tactic.LibraryRewrite.Rewrite × Lean.Name)))
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsPreLocalizingSequence.isStoppingTime : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreLocalizingSequence._auto_1},
  ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P → ∀ (n : ℕ), MeasureTheory.IsStoppingTime 𝓕 (τ n)
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- The extension of an integral curve by another integral curve is an integral curve.

If two integral curves are defined on overlapping open intervals, and they agree at a point in
their common domain, then they can be patched together to form a longer integral curve.

This is stated for manifolds without boundary for simplicity. We actually only need to assume that
the images of `γ` and `γ'` lie in the interior of the manifold.
TODO: Generalise to manifolds with boundary.  -/
isMIntegralCurveOn_piecewise : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {a b a' b' : ℝ},
      IsMIntegralCurveOn γ v (Set.Ioo a b) →
        IsMIntegralCurveOn γ' v (Set.Ioo a' b') →
          ∀ {t₀ : ℝ},
            t₀ ∈ Set.Ioo a b ∩ Set.Ioo a' b' →
              γ t₀ = γ' t₀ → IsMIntegralCurveOn ((Set.Ioo a b).piecewise γ γ') v (Set.Ioo a b ∪ Set.Ioo a' b')
-- Mathlib.FieldTheory.Normal.Closure
IsNormalClosure.adjoin_rootSet : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} {inst : Field F} {inst_1 : Field K} {inst_2 : Field L}
  {inst_3 : Algebra F K} {inst_4 : Algebra F L} [self : IsNormalClosure F K L],
  ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
-- Mathlib.Data.Set.Function
Function.Injective.comp_injOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {s : Set α},
  Function.Injective g → Set.InjOn f s → Set.InjOn (g ∘ f) s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.normBound_pos : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S), 0 < ClassGroup.normBound abv bS
-- Mathlib.Order.RelSeries
RelSeries.length_eq_zero : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r} [r.IsIrrefl], s.length = 0 ↔ {x | x ∈ s}.Subsingleton
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} {l : List α} {k : α},
  (t.insertManyIfNewUnit l)[k]! = ()
-- Mathlib.Topology.Order.NhdsSet
Ioi_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  a < b → Set.Ioi a ∈ nhdsSet (Set.Icc b c)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_iInter_thickening' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ},
  0 ≤ δ →
    ∀ s ⊆ Set.Ioi δ,
      (∀ (ε : ℝ), δ < ε → (s ∩ Set.Ioc δ ε).Nonempty) →
        ∀ (E : Set α), Metric.cthickening δ E = ⋂ ε ∈ s, Metric.thickening ε E
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instIsUniformAddGroup : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3}, IsUniformAddGroup (CStarMatrix m n A)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p`-th cyclotomic extension of `ℚ` is a prime if
`p ≠ 2`.  -/
IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p),
  p ≠ 2 → Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- A version of `Pi.basisFun` for `PiLp`.  -/
PiLp.basisFun : (p : ENNReal) → (𝕜 : Type u_1) → (ι : Type u_2) → [Finite ι] → [inst : Ring 𝕜] → Module.Basis ι 𝕜 (PiLp p fun x => 𝕜)
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.toListRev_empty : ∀ {β : Type u_1}, (Std.Iter.empty β).toListRev = []
-- Batteries.Tactic.GeneralizeProofs
/-- Core implementation for `appArgExpectedTypes`.  -/
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.appArgExpectedTypes.go : Lean.Expr → Array Lean.Expr → Option Lean.Expr → Lean.MetaM (Array (Option Lean.Expr))
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_base_pow_mul : ∀ {b k m : ℕ}, 1 < b → 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.map_piSingle : ∀ {M : Type u_5} [inst : AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [inst_1 : Finite X] [inst_2 : Finite Y]
  [inst_3 : DecidableEq X] [inst_4 : DecidableEq Y] (f : X → Y) (x : X) (m : M),
  FunOnFinite.map f (Pi.single x m) = Pi.single (f x) m
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [inst_5 : F.CommShift A] (Y : D),
  (CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).inv.app Y =
    CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj (G.obj Y)))
      (CategoryTheory.CategoryStruct.comp
        (G.map
          ((CategoryTheory.shiftFunctorCompIsoId D b a h).inv.app
            (F.obj ((CategoryTheory.shiftFunctor C a).obj (G.obj Y)))))
        (CategoryTheory.CategoryStruct.comp
          (G.map
            ((CategoryTheory.shiftFunctor D a).map
              ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app (G.obj Y)))))
          (CategoryTheory.CategoryStruct.comp
            (G.map
              ((CategoryTheory.shiftFunctor D a).map
                ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y)))))
            (G.map ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y))))))
-- Mathlib.Algebra.Group.Action.Defs
SemiconjBy.smul_right : ∀ {M : Type u_1} {α : Type u_5} [inst : SMul M α] [inst_1 : Mul α] [SMulCommClass M α α] [IsScalarTower M α α]
  {x a b : α}, SemiconjBy x a b → ∀ (r : M), SemiconjBy x (r • a) (r • b)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMapSrc_functorObjTop_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πY) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ) h)