mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Iterators
Std.Ric.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.Least? α] (r : Std.Ric α),
  Std.Ric.Internal.iter r = { internalState := { next := Std.PRange.least?, upperBound := r.upper } }
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The functor `(f : α → C) ↦ ∐ f`.  -/
CategoryTheory.Limits.Sigma.functor : (α : Type w₂) →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [CategoryTheory.Limits.HasCoproductsOfShape α C] → CategoryTheory.Functor (α → C) C
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Let `M` be a smooth σ-compact manifold with extended distance. Let `K : ι → Set M` be a locally
finite family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for
all `i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and
`x ∈ K i`, we have `Metric.closedEBall x (δ x) ⊆ U i`.  -/
Metric.exists_contMDiffMap_forall_closedEBall_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] {n : ℕ∞} {M : Type u_1}
  [inst_4 : EMetricSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] {K U : ι → Set M},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_min?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → t.min?.isSome = true
-- Mathlib.Order.Defs.PartialOrder
lt_of_ne_of_le' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≠ b → b ≤ a → b < a
-- Mathlib.Order.Disjoint
codisjoint_toDual_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α},
  Codisjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Disjoint a b
-- Mathlib.Order.Cofinal
/-- **Alias** of `GaloisConnection.map_isCofinal`. -/
GaloisConnection.map_cofinal : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {g : α → β},
  GaloisConnection f g → ∀ {s : Set α}, IsCofinal s → IsCofinal (g '' s)
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.isLocallyInjective_iff_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget D)],
  CategoryTheory.Sheaf.IsLocallyInjective φ ↔
    ∀ (X : Cᵒᵖ), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (φ.hom.app X))
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.differentiableOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → n ≠ 0 → DifferentiableOn 𝕜 f s
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃Obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) {X₂ Y₂ : C₂} (φ : X₂ ⟶ Y₂) (X₃ : C₃),
  ((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).map φ).app X₃ = (F.obj X₁).map ((G₂₃.map φ).app X₃)
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.ext_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  {A B : VertexOperator R V}, A = B ↔ ∀ (v : V), A v = B v
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.inj.sizeOf_spec : ∀ (thm : Lean.Meta.Grind.InjectiveTheorem), sizeOf (Lean.Meta.Grind.Entry.inj thm) = 1 + sizeOf thm
-- Mathlib.Analysis.Convex.Side
AffineSubspace.setOfPred_wOppSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.WOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instSetLike : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → SetLike (LieSubmodule R L M) M
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.mem.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Mathlib.Topology.Order.IsLUB
eventually_const_le_iff_forall_lt_eventually_const_lt : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [FirstCountableTopology α] {l : Filter γ} [CountableInterFilter l] {f : γ → α} {a : α},
  (∀ᶠ (x : γ) in l, a ≤ f x) ↔ ∀ b < a, ∀ᶠ (x : γ) in l, b < f x
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_X : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R), p %ₘ Polynomial.X = Polynomial.C (Polynomial.eval 0 p)
-- Mathlib.Order.RelClasses
IsTrans.swap : ∀ {α : Type u} (r : α → α → Prop) [IsTrans α r], IsTrans α (Function.swap r)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.mk.inj : ∀ {mctx : Lean.MetavarContext} {paramNames : Array Lean.Name} {nextParamIdx : ℕ}
  {cache : Std.HashMap Lean.ExprStructEq Lean.Expr} {mctx_1 : Lean.MetavarContext} {paramNames_1 : Array Lean.Name}
  {nextParamIdx_1 : ℕ} {cache_1 : Std.HashMap Lean.ExprStructEq Lean.Expr},
  { mctx := mctx, paramNames := paramNames, nextParamIdx := nextParamIdx, cache := cache } =
      { mctx := mctx_1, paramNames := paramNames_1, nextParamIdx := nextParamIdx_1, cache := cache_1 } →
    mctx = mctx_1 ∧ paramNames = paramNames_1 ∧ nextParamIdx = nextParamIdx_1 ∧ cache = cache_1
-- Init.Data.SInt.Lemmas
Int16.neg_mul : ∀ (a b : Int16), -a * b = -(a * b)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instSMulCommClassTensorProduct : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B], SMulCommClass A B (TensorProduct R A B)
-- Mathlib.Algebra.RingQuot
RingQuot.neg_quot : ∀ {R : Type uR} [inst : Ring R] (r : R → R → Prop) {a : R},
  -{ toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (-a) }
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_eq_zero_of_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {x : E}, V x = 0 → W x = 0 → VectorField.lieBracket 𝕜 V W x = 0
-- Mathlib.Order.Filter.Pointwise
Filter.tendsto_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {a : Filter β} {f : β → α},
  Filter.Tendsto f a 1 ↔ ∀ᶠ (x : β) in a, f x = 1
-- Init.Data.Nat.Lemmas
Nat.sub_eq_zero_iff_le : ∀ {n m : ℕ}, n - m = 0 ↔ n ≤ m
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.mul_prod_Ioc_eq_prod_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → f a * ∏ x ∈ Finset.Ioc a b, f x = ∏ x ∈ Finset.Icc a b, f x
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_rci : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo (Std.Slice.toList xs)
-- Init.Data.List.Lemmas
List.getLast_append_of_ne_nil : ∀ {α : Type u_1} {l' l : List α} (h₁ : l ++ l' ≠ []) (h₂ : l' ≠ []), (l ++ l').getLast h₁ = l'.getLast h₂
-- Mathlib.Data.EReal.Basic
/-- The multiplication on `EReal`. Our definition satisfies `0 * x = x * 0 = 0` for any `x`, and
picks the only sensible value elsewhere.  -/
EReal.mul : EReal → EReal → EReal
-- Mathlib.Analysis.Matrix.Normed
/-- Auxiliary construction; an element of norm 1 such that `a * unitOf a = ‖a‖`.  -/
_private.Mathlib.Analysis.Matrix.Normed.0.Matrix.unitOf : {α : Type u_5} → [inst : NormedDivisionRing α] → [NormedAlgebra ℝ α] → α → α
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (ψ : NormedAddGroupHom V₁ ↥(f.equalizer g)),
  ↑(NormedAddGroupHom.Equalizer.liftEquiv.symm ψ) = (NormedAddGroupHom.Equalizer.ι f g).comp ψ
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_intCast : ∀ {d : ℤ} (n : ℤ), (↑n).norm = n * n
-- Mathlib.Order.RelSeries
RelSeries.length_ne_zero : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r} [r.IsIrrefl], s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- A map in the opposite direction to `f` and `g`  -/
CategoryTheory.IsSplitCoequalizer.leftSection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f g : X ⟶ Y} → {Z : C} → {π : Y ⟶ Z} → CategoryTheory.IsSplitCoequalizer f g π → (Y ⟶ X)
-- Mathlib.Condensed.Discrete.Colimit
/-- To presheaves on `LightProfinite` whose restrictions to finite sets are isomorphic have isomorphic
left Kan extensions.
 -/
LightCondensed.lanPresheafExt : {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} →
  (FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G) →
    (LightCondensed.lanPresheaf F ≅ LightCondensed.lanPresheaf G)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.measurable_stoppedValue : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace β] [inst_9 : MeasurableSpace β]
  [BorelSpace β],
  MeasureTheory.IsStronglyProgressive f u →
    ∀ (hτ : MeasureTheory.IsStoppingTime f τ), Measurable (MeasureTheory.stoppedValue u τ)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- **Lebesgue dominated convergence theorem**: sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
`condExpL1`.  -/
MeasureTheory.tendsto_condExpL1_of_dominated_convergence : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (hm : m ≤ m₀) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {fs : ℕ → α → E} {f : α → E}
  (bound_fs : α → ℝ),
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ) →
    MeasureTheory.Integrable bound_fs μ →
      (∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x) →
        (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) →
          Filter.Tendsto (fun n => MeasureTheory.condExpL1 hm μ (fs n)) Filter.atTop
            (nhds (MeasureTheory.condExpL1 hm μ f))
-- Mathlib.Data.Finsupp.Defs
Finsupp.range_mapRange : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M → N) (he₀ : e 0 = 0),
  Set.range (Finsupp.mapRange e he₀) = {g | ∀ (i : α), g i ∈ Set.range e}
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.posOfAux.eq_def : ∀ (s : String) (c : Char) (stopPos pos : String.Pos.Raw),
  String.Legacy.posOfAux s c stopPos pos =
    if h : pos < stopPos then
      if (String.Pos.Raw.get s pos == c) = true then pos
      else
        have this := ⋯;
        String.Legacy.posOfAux s c stopPos (String.Pos.Raw.next s pos)
    else pos
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.differentiable_completedHurwitzZetaEven₀ : ∀ (a : UnitAddCircle), Differentiable ℂ (HurwitzZeta.completedHurwitzZetaEven₀ a)
-- Mathlib.Order.Partition.Basic
Partition.ne_bot_of_mem' : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] {P : Partition s}, x ∈ P → s ≠ ⊥
-- Mathlib.Topology.Algebra.Group.Defs
Filter.Tendsto.sub : ∀ {G : Type u_1} {α : Type u_2} [inst : TopologicalSpace G] [inst_1 : Sub G] [ContinuousSub G] {f g : α → G}
  {l : Filter α} {a b : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → Filter.Tendsto (fun x => f x - g x) l (nhds (a - b))
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_option : ∀ {α : Type u_1} [Finite α], Nat.card (Option α) = Nat.card α + 1
-- Mathlib.Data.List.Sort
List.orderedInsert_cons_of_le : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {a b : α} (l : List α),
  r a b → List.orderedInsert r a (b :: l) = a :: b :: l
-- Std.Async.Process
/-- Number of involuntary context switches (process preempted)
 -/
Std.IO.Process.ResourceUsageStats.involuntaryContextSwitches : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The element `a` such that `d = a ^ 2 - 1`, considered as an integer.  -/
Pell.az : ℕ → ℤ
-- Mathlib.Topology.Order.Basic
gt_mem_nhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a b : α},
  b < a → ∀ᶠ (x : α) in nhds b, x < a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSum.add.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)] {a b : Q(«$α»)} (a_1 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα a)
  (a_2 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα b),
  sizeOf (Mathlib.Tactic.Ring.Common.ExSum.add a_1 a_2) = 1 + sizeOf a + sizeOf b + sizeOf a_1 + sizeOf a_2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_coe_pi : (↑Real.pi).sin = 0
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.optionDeclsRef : IO.Ref Lean.OptionDecls
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk_mem_col_iff : ∀ {μ : YoungDiagram} {i j : ℕ}, (i, j) ∈ μ.col j ↔ (i, j) ∈ μ
-- Mathlib.RingTheory.Valuation.Integers
Valuation.mem_leIdeal_iff : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀}
  {x : ↥v.integer}, x ∈ v.leIdeal γ ↔ v ↑x ≤ γ
-- Mathlib.Algebra.Group.Units.Equiv
AddEquiv.isAddUnit_map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : EquivLike F M N]
  [AddEquivClass F M N] (f : F) {x : M}, IsAddUnit (f x) ↔ IsAddUnit x
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.whiskeringLeft_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : C ⥤ₑ D} (η : F ⟶ G) (H : D ⥤ₑ E),
  ((CategoryTheory.ExactFunctor.whiskeringLeft C D E).map η).app H =
    CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringLeft C D E).map η.hom).app H.obj)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coeIsScalarTower : (R : Type u_1) →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module S M] →
                      [inst_7 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.SuggestionText.string.injEq : ∀ (a a_1 : String),
  (Lean.Meta.Tactic.TryThis.SuggestionText.string a = Lean.Meta.Tactic.TryThis.SuggestionText.string a_1) = (a = a_1)
-- Mathlib.Data.Set.Basic
Set.empty_inter : ∀ {α : Type u} (a : Set α), ∅ ∩ a = ∅
-- Mathlib.Data.Sym.Sym2
Sym2.other_mem : ∀ {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z), Sym2.Mem.other h ∈ z
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_eq_expSeries_sum : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] [CharZero 𝕂], NormedSpace.exp = (NormedSpace.expSeries 𝕂 𝔸).sum
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {base : s.Pos}
  {startPos endPos : (s.sliceFrom base).Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos ↔
    String.Slice.Pattern.Model.IsLongestMatchAt pat (String.Slice.Pos.ofSliceFrom startPos)
      (String.Slice.Pos.ofSliceFrom endPos)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State.mk : Lean.Meta.KExprMap ℕ → Array Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.State
-- Mathlib.Data.Rat.Cast.CharZero
/-- Coercion `ℚ → α` as a `RingHom`.  -/
Rat.castHom : (α : Type u_3) → [inst : DivisionRing α] → [CharZero α] → ℚ →+* α
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.mk : ∀ {R : Type u} {K : Type v} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : Module.IsTorsionFree R K], IsAlgClosed K → Algebra.IsAlgebraic R K → IsAlgClosure R K
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} {k : β → α}
  {lb : Filter β}, f =O[𝕜; l] g → Filter.Tendsto k lb l → (f ∘ k) =O[𝕜; lb] (g ∘ k)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Subtype.borelSpace : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [hα : BorelSpace α] (p : α → Prop),
  BorelSpace (Subtype p)
-- Mathlib.RingTheory.Localization.Basic
Localization.algHom_ext_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {W : Submonoid A} {f g : Localization W →ₐ[R] B},
  f = g ↔ f.comp (Algebra.algHom R A (Localization W)) = g.comp (Algebra.algHom R A (Localization W))
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.comp_coeff_zero' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 0 → E),
  (q.comp p 0) v = (q 0) fun _i => 0
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (a : M), IsUnit a = ∃ u, ↑u = a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.lift_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : (CategoryTheory.Functor.const J).obj X ⟶ D) {X_1 Y : J} (f : X_1 ⟶ Y),
  (CategoryTheory.Under.lift D s).map f = CategoryTheory.Under.homMk (D.map f) ⋯
-- Init.Core
/-- An alternative recursion or induction principle for quotients that can be used when the target type
is a subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial,
so any function can be lifted.

`Quotient.rec` does not assume that the target type is a subsingleton.
 -/
Quotient.recOnSubsingleton : {α : Sort u} →
  {s : Setoid α} →
    {motive : Quotient s → Sort v} →
      [h : ∀ (a : α), Subsingleton (motive ⟦a⟧)] → (q : Quotient s) → ((a : α) → motive ⟦a⟧) → motive q
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The initial object in `Type u` is `PEmpty`.  -/
CategoryTheory.Limits.Types.initialIso : ⊥_ Type u ≅ PEmpty.{u + 1}
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp.eq_1 : FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp =
  { hom := @FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp._aux_1,
    ofHom := @FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp._aux_3,
    hom_ofHom := @FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp._proof_5,
    ofHom_hom := @FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp._proof_6,
    id_apply := @FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp._proof_7,
    comp_apply := @FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp._proof_8 }
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurableSet_support : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Zero β]
  [MeasurableSingletonClass β], Measurable f → MeasurableSet (Function.support f)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.zeroBasis.eq_1 : ∀ {𝕜 : Type u_1} {α : Type u_3} [inst : NormedRing 𝕜],
  lp.zeroBasis =
    {
      repr :=
        { toFun := fun x => Finsupp.ofSupportFinite ↑x ⋯, map_add' := ⋯, map_smul' := ⋯, invFun := fun x => ⟨⇑x, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ } }
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- A $C^n$ map is a $C^{k+(α)}$ map for any `k < n`.  -/
ContDiffAt.contDiffPointwiseHolderAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {f : E → F} {a : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f a → ↑k < n → ∀ (α : ↑unitInterval), ContDiffPointwiseHolderAt k α f a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- We have that `hζ.toInteger - 1` does not divide `2`.  -/
IsPrimitiveRoot.toInteger_sub_one_not_dvd_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))), p ≠ 2 → ¬hζ.toInteger - 1 ∣ 2
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_pi : ∀ {ι : Type u_4} {ι' : ι → Type u_6} {α : ι → Type u_7} {s : (i : ι) → Set (ι' i)} {f : (i : ι) → ι' i → Set (α i)},
  (∀ (i : ι), (s i).PairwiseDisjoint (f i)) → (Set.univ.pi s).PairwiseDisjoint fun I => Set.univ.pi fun i => f i (I i)
-- Mathlib.LinearAlgebra.QuadraticForm.Complex
QuadraticForm.complex_equivalent : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module ℂ M] [FiniteDimensional ℂ M] (Q₁ Q₂ : QuadraticForm ℂ M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q₁) →
    LinearMap.SeparatingLeft (QuadraticMap.associated Q₂) → QuadraticMap.Equivalent Q₁ Q₂