mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.mem_submoduleImage : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_10}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {O : Submodule R M} {ϕ : ↥O →ₗ[R] M'} {N : Submodule R M} {x : M'},
  x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x
-- Mathlib.Logic.Equiv.Set
Equiv.symm_image_subset : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β), ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.div_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → DivInvMonoid (R i)] [inst_2 : ∀ (i : ι), SubgroupClass (S i) (R i)]
  (x y : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (x / y) i = x i / y i
-- Lean.Parser.Do
Lean.Parser.Term.doExpr : Lean.Parser.Parser
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- `Codiscrete.functorToCat` turns a type into a codiscrete category.  -/
CategoryTheory.Codiscrete.functorToCat : CategoryTheory.Functor (Type u) CategoryTheory.Cat
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Compacts.edist_eq : ∀ {α : Type u_1} [inst : EMetricSpace α] {s t : TopologicalSpace.Compacts α}, edist s t = Metric.hausdorffEDist ↑s ↑t
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.embedding_injective : ∀ (K : Type u_1) [inst : Field K], Function.Injective NumberField.InfinitePlace.embedding
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A ring with finite quotients has only finitely many ideals of bounded norm.  -/
Ring.HasFiniteQuotients.finite_absNorm_le : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] [inst_2 : IsDedekindDomain R]
  [inst_3 : Module.Free ℤ R] (B : ℕ), {I | Ideal.absNorm I ≤ B}.Finite
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- **Alias** of `Cardinal.le_range_of_union_finset_eq_univ`.

---

If an infinite type `β` can be expressed as a union of finite sets,
then the cardinality of the collection of those finite sets
must be at least the cardinality of `β`.  -/
Cardinal.le_range_of_union_finset_eq_top : ∀ {α : Type u_1} {β : Type u_2} [Infinite β] (f : α → Finset β),
  ⋃ a, ↑(f a) = Set.univ → Cardinal.mk β ≤ Cardinal.mk ↑(Set.range f)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.foldlM_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeSet.Raw.foldlM f init t₁ = Std.TreeSet.Raw.foldlM f init t₂
-- Mathlib.Tactic.Ring.Common
/-- Decides whether a coefficient is 1 and returns a proof if so.  -/
Mathlib.Tactic.Ring.Common.RingCompute.isOne : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          {x : Q(«$α»)} → BaseType x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1)
-- Init.System.IO
/-- The file can be executed.  -/
IO.AccessRight.execution : IO.AccessRight → Bool
-- Mathlib.Combinatorics.Graph.Basic
Graph.Adj.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α), G.Adj x y = ∃ e, G.IsLink e x y
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderUnitor.leftUnitor_inv_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderUnitor] (c : C),
  P (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).inv
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsHomeomorph id
-- Mathlib.Data.Set.Basic
Set.mem_powerset_iff : ∀ {α : Type u} (x s : Set α), x ∈ 𝒫 s ↔ x ⊆ s
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.nndist_set_exists : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, ∃ C, ∀ (x : α), nndist (f x) (g x) ≤ C
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)),
  CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (F.map φ) = CategoryTheory.CategoryStruct.id (F.obj j)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation.0.MeasureTheory.VectorMeasure.semivariation.eq_1 : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  (μ : MeasureTheory.VectorMeasure X E) (s : Set X),
  μ.semivariation s = ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
CommGroup.is_simple_iff_prime_card : ∀ {α : Type u_1} [inst : CommGroup α], IsSimpleGroup α ↔ Nat.Prime (Nat.card α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A family of limiting binary fans on a partial order induces an inf-semilattice structure on it.
 -/
Preorder.semilatticeInfOfIsLimitBinaryFan : {C : Type u} →
  [inst : PartialOrder C] →
    (c : (X Y : C) → CategoryTheory.Limits.BinaryFan X Y) →
      ((X Y : C) → CategoryTheory.Limits.IsLimit (c X Y)) → SemilatticeInf C
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_map : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) {a b : B} (a_1 : a ⟶ b),
  (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map a_1 = (F' a b).obj a_1
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.ne_iff : ∀ {P : Type u_2} [inst : MetricSpace P] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius
-- Mathlib.Order.InitialSeg
InitialSeg.codRestrict_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : InitialSeg r s)
  (H : ∀ (a : α), f a ∈ p) (a : α), (InitialSeg.codRestrict p f H) a = ⟨f a, ⋯⟩
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_inv : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableInv G] [μ.IsInvInvariant] {f : G → F} {s : Set G},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn (fun x => f x⁻¹) s⁻¹ μ
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: If `R : Set G` and `H : Subgroup G` are complements with `1 ∈ R`, and if
`G` is generated by `S : Set G`, then `H` is generated by the `Set`
  `(R * S).image (fun g ↦ g * (hR.toRightFun g)⁻¹)`.  -/
Subgroup.closure_mul_image_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {R S : Set G} (hR : Subgroup.IsComplement (↑H) R),
  1 ∈ R → Subgroup.closure S = ⊤ → Subgroup.closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) = H
-- Mathlib.Data.Fin.Fin2
Fin2.castSucc.eq_1 : ∀ (n_1 : ℕ), Fin2.fz.castSucc = Fin2.fz
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq : Lean.Grind.AC.Expr → Lean.Grind.AC.Seq
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Const.ofList l cmp).getKeyD k' fallback = k
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {k : α} {v : β}, (m.insert k v).getKey! k = k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.fold_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w},
  m.WF →
    ∀ {f : δ → (a : α) → β a → δ} {init : δ},
      Std.DHashMap.Raw.fold f init m = List.foldl (fun a b => f a b.fst b.snd) init m.toList
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  Std.Internal.List.getEntry? k (Std.Internal.List.insertListIfNewUnit l toInsert) =
    (Std.Internal.List.getEntry? k l).or (Std.Internal.List.getEntry? k (List.map (fun x => ⟨x, ()⟩) toInsert))
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.IsHomological.mk : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] {F : CategoryTheory.Functor C A}
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [toPreservesZeroMorphisms : F.PreservesZeroMorphisms],
  (∀ (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact) →
    F.IsHomological
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.lsingle.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Module R S] (a : M),
  AddMonoidAlgebra.lsingle a = ↑(AddMonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle a
-- Mathlib.CategoryTheory.ObjectProperty.Comma
CategoryTheory.ObjectProperty.comma_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D]
  {F₁ : CategoryTheory.Functor C₁ D} {F₂ : CategoryTheory.Functor C₂ D} (P₁ : CategoryTheory.ObjectProperty C₁)
  (P₂ : CategoryTheory.ObjectProperty C₂) (X : CategoryTheory.Comma F₁ F₂),
  CategoryTheory.ObjectProperty.comma F₁ F₂ P₁ P₂ X ↔ P₁ X.left ∧ P₂ X.right
-- Mathlib.Tactic.Basic
Mathlib.Tactic.withResetServerInfo.Result.mk.injEq : ∀ {α : Type} (result? : Option α) (msgs : Lean.MessageLog) (trees : Lean.PersistentArray Lean.Elab.InfoTree)
  (result?_1 : Option α) (msgs_1 : Lean.MessageLog) (trees_1 : Lean.PersistentArray Lean.Elab.InfoTree),
  ({ result? := result?, msgs := msgs, trees := trees } = { result? := result?_1, msgs := msgs_1, trees := trees_1 }) =
    (result? = result?_1 ∧ msgs = msgs_1 ∧ trees = trees_1)
-- Mathlib.CategoryTheory.Opposites
/-- Take the "unopposite" of a functor is functorial.
 -/
CategoryTheory.Functor.opInv : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (CategoryTheory.Functor C D)ᵒᵖ
-- Std.Sat.CNF.Basic
/-- Variable `v` occurs in `CNF` formula `f`.
 -/
Std.Sat.CNF.VarMem : {α : Type u_1} → α → Std.Sat.CNF α → Prop
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_univ : ∀ {α : Type u} [Nontrivial α], Set.univ.Nontrivial
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_equation : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (P : Fin 3 → R), (W'.map f).Equation (⇑f ∘ P) ↔ W'.Equation P
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_neg_right`. -/
MonovaryOn.of_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f (-g) s → AntivaryOn f g s
-- Mathlib.RingTheory.Complex
Algebra.trace_complex_apply : ∀ (z : ℂ), (Algebra.trace ℝ ℂ) z = 2 * z.re
-- Init.Data.List.MapIdx
List.mapIdx_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : ℕ → α → β} {g : ℕ → β → γ},
  List.mapIdx g (List.mapIdx f l) = List.mapIdx (fun i => g i ∘ f i) l
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.getUsedFVarsMap : Lean.Elab.Term.MutualClosure.FixPoint.M Lean.Elab.Term.MutualClosure.UsedFVarsMap
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target_subset_closure_interior : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M},
  (extChartAt I x).target ⊆ closure (interior (extChartAt I x).target)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompacts_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s t : TopologicalSpace.NonemptyCompacts α),
  (s ⊔ t).toCompacts = s.toCompacts ⊔ t.toCompacts
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ico_atBot_prod_atTop : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [NoTopOrder α],
  Filter.Tendsto (fun p => Finset.Ico p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop
-- Mathlib.Algebra.Group.Defs
add_right_injective : ∀ {G : Type u_1} [inst : Add G] [IsLeftCancelAdd G] (a : G), Function.Injective fun x => a + x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.semiconjBy_iff_semiconj : ∀ {f g₁ g₂ : CircleDeg1Lift}, SemiconjBy f g₁ g₂ ↔ Function.Semiconj ⇑f ⇑g₁ ⇑g₂
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integrable_sum_measure : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {μ : ι → MeasureTheory.Measure X} {f : X → E},
  (∀ (i : ι), MeasureTheory.Integrable f (μ i)) →
    (Summable fun i => ∫ (x : X), ‖f x‖ ∂μ i) → MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ)
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : LowerSet α) (t₁ t₂ : LowerSet β),
  s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- A reflexive module has a perfect pairing with its dual.  -/
LinearMap.IsPerfPair.dualEval : ∀ {R : Type u_1} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : Module R M]
  [Module.IsReflexive R M], (Module.Dual.eval R M).IsPerfPair
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_finset_range : Filter.Tendsto Finset.range Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The identity functor is also the identity on commutative monoid objects.  -/
CategoryTheory.Functor.mapCommMonIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (CategoryTheory.Functor.id C).mapCommMon ≅ CategoryTheory.Functor.id (CategoryTheory.CommMon C)
-- Init.Data.Int.Gcd
Int.natAbs_dvd_lcm_left : ∀ (a b : ℤ), a.natAbs ∣ a.lcm b
-- Mathlib.Data.Set.Subsingleton
Set.eq_empty_or_singleton_of_unique : ∀ {α : Type u} [inst : Unique α] (s : Set α), s = ∅ ∨ s = {default}
-- Mathlib.Analysis.ConstantSpeed
edist_naturalParameterization_eq_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.length_le : ∀ {n : ℕ} (c : Composition n), c.length ≤ n
-- Mathlib.FieldTheory.Separable
/-- A separable polynomial is square-free.

See `PerfectField.separable_iff_squarefree` for the converse when the coefficients are a perfect
field.  -/
Polynomial.Separable.squarefree : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R}, p.Separable → Squarefree p
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.crossing_pos_eq : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ},
  a < b →
    MeasureTheory.upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n =
        MeasureTheory.upperCrossingTime a b f N n ∧
      MeasureTheory.lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n =
        MeasureTheory.lowerCrossingTime a b f N n
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu → Bool
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_one_cast : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a ^ Nat.rawCast 1 = a
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ioc_eq_integral_Ioo : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Ioc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
-- Mathlib.Topology.Defs.Induced
/-- Given `f : X → Y` and a topology on `Y`,
the induced topology on `X` is the collection of sets
that are preimages of some open set in `Y`.
This is the coarsest topology that makes `f` continuous.  -/
TopologicalSpace.induced : {X : Type u_1} → {Y : Type u_2} → (X → Y) → TopologicalSpace Y → TopologicalSpace X
-- Mathlib.Data.Set.Basic
Set.eq_of_subset_of_subset : ∀ {α : Type u} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodProdProdComm_apply : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄]
  [inst_9 : TopologicalSpace M₁] [inst_10 : TopologicalSpace M₂] [inst_11 : TopologicalSpace M₃]
  [inst_12 : TopologicalSpace M₄] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) (p₄ : M₄),
  (ContinuousLinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄) ((p₁, p₂), p₃, p₄) = ((p₁, p₃), p₂, p₄)
-- Mathlib.Order.Fin.Basic
/-- The equivalence `Fin n ≃ {i // i < n}` is an order isomorphism.  -/
Fin.orderIsoSubtype : {n : ℕ} → Fin n ≃o { i // i < n }
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} (X : ℕ → C)
  (x : (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (X n))) (map : (n : ℕ) → X (n + 1) ⟶ X n)
  (effectiveEpi : ∀ (n : ℕ), CategoryTheory.EffectiveEpi (map n))
  (w :
    ∀ (n : ℕ),
      (CategoryTheory.ConcreteCategory.hom ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op (X (n + 1)))))
          (x (n + 1)) =
        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map (map n).op)) (x n))
  (X_1 : ℕ → C) (x_1 : (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (X_1 n)))
  (map_1 : (n : ℕ) → X_1 (n + 1) ⟶ X_1 n) (effectiveEpi_1 : ∀ (n : ℕ), CategoryTheory.EffectiveEpi (map_1 n))
  (w_1 :
    ∀ (n : ℕ),
      (CategoryTheory.ConcreteCategory.hom ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op (X_1 (n + 1)))))
          (x_1 (n + 1)) =
        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map (map_1 n).op)) (x_1 n)),
  ({ X := X, x := x, map := map, effectiveEpi := effectiveEpi, w := w } =
      { X := X_1, x := x_1, map := map_1, effectiveEpi := effectiveEpi_1, w := w_1 }) =
    (X = X_1 ∧ x ≍ x_1 ∧ map ≍ map_1)
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.unique_of_degree_le_degree_minpoly : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic → (Polynomial.aeval x) p = 0 → p.degree ≤ (minpoly A x).degree → p = minpoly A x
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      CategoryTheory.CategoryStruct.{max v₂ v₁, max u₂ u₁} F.Grothendieck
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.BoundedAtFilter.mul_zeroAtFilter : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedRing β] {l : Filter α} {f g : α → β},
  l.BoundedAtFilter f → l.ZeroAtFilter g → l.ZeroAtFilter (f * g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.flip_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g ↔ CategoryTheory.IsPullback snd fst g f
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.closure_range_inl_union_inr : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H],
  Subgroup.closure (Set.range ⇑Monoid.Coprod.inl ∪ Set.range ⇑Monoid.Coprod.inr) = ⊤
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.num : Lean.Meta.Grind.Result✝
-- Mathlib.Util.AtomM
/-- If an atomic expression has already been encountered, get the index and the stored form of the
atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
If the atomic expression has *not* already been encountered, store it in the list of atoms, and
return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by `addAtomQ` should be considered the normal form.

This is a strongly-typed version of `AtomM.addAtom` for code using `Qq`.
 -/
Mathlib.Tactic.AtomM.addAtomQ : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Mathlib.Tactic.AtomM (ℕ × { e' // «$e» =Q «$e'» })
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The canonical isomorphism relating `cospan f.unop g.unop` and `(span f g).leftOp`  -/
CategoryTheory.Limits.cospanUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          CategoryTheory.Limits.cospan f.unop g.unop ≅
            CategoryTheory.Limits.walkingSpanOpEquiv.inverse.comp (CategoryTheory.Limits.span f g).leftOp