mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.subgroup_strictAnti : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  StrictAnti FiniteMulArchimedeanClass.subgroup
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.mk.injEq : ∀ {m : Type u → Type u} (listM : Type u → Type u) (nil : {α : Type u} → listM α)
  (cons : {α : Type u} → α → listM α → listM α) (thunk : {α : Type u} → (Unit → listM α) → listM α)
  (squash : {α : Type u} → (Unit → m (listM α)) → listM α)
  (uncons : {α : Type u} → [Monad m] → listM α → m (Option (α × listM α)))
  (uncons? : {α : Type u} → listM α → Option (Option (α × listM α))) (listM_1 : Type u → Type u)
  (nil_1 : {α : Type u} → listM_1 α) (cons_1 : {α : Type u} → α → listM_1 α → listM_1 α)
  (thunk_1 : {α : Type u} → (Unit → listM_1 α) → listM_1 α)
  (squash_1 : {α : Type u} → (Unit → m (listM_1 α)) → listM_1 α)
  (uncons_1 : {α : Type u} → [Monad m] → listM_1 α → m (Option (α × listM_1 α)))
  (uncons?_1 : {α : Type u} → listM_1 α → Option (Option (α × listM_1 α))),
  ({ listM := listM, nil := nil, cons := cons, thunk := thunk, squash := squash, uncons := uncons,
        uncons? := uncons? } =
      { listM := listM_1, nil := nil_1, cons := cons_1, thunk := thunk_1, squash := squash_1, uncons := uncons_1,
        uncons? := uncons?_1 }) =
    (listM = listM_1 ∧
      nil ≍ nil_1 ∧ cons ≍ cons_1 ∧ thunk ≍ thunk_1 ∧ squash ≍ squash_1 ∧ uncons ≍ uncons_1 ∧ uncons? ≍ uncons?_1)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
deriv_circleMap_eq_zero_iff : ∀ {c : ℂ} {R θ : ℝ}, deriv (circleMap c R) θ = 0 ↔ R = 0
-- Mathlib.Tactic.Convert
/-- Internal elaborator for `Convert.ExpensiveConfig`: use `Convert.elabConfig` instead.  -/
Convert.elabExpensiveConfig : Lean.Syntax →
  optParam Convert.ExpensiveConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Convert.ExpensiveConfig
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.sndX_inrX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  ¬c.Rel i (c.next i) →
    ∀ {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ i ⟶ Z),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) h) =
        h
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The bijection `(X ⟶ Y) ≃ (𝟙_ C ⟶ (ihom X).obj Y)` in a monoidal closed category.  -/
CategoryTheory.MonoidalClosed.curryHomEquiv' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Closed X] → (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne : ∀ {σ : Type v} {g : σ → AlgebraicGeometry.Scheme} [inst : Small.{u, v} σ] {i j : σ} {Z : AlgebraicGeometry.Scheme}
  {a : Z ⟶ g i} {b : Z ⟶ g j},
  CategoryTheory.CommSq a b (CategoryTheory.Limits.Sigma.ι g i) (CategoryTheory.Limits.Sigma.ι g j) → i ≠ j → IsEmpty ↥Z
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- `localized'` as a `FrameHom`.  -/
Submodule.localized'FrameHom : {R : Type u_1} →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Module S N] →
                        [IsScalarTower R S N] →
                          (p : Submonoid R) →
                            [IsLocalization p S] →
                              (f : M →ₗ[R] N) → [IsLocalizedModule p f] → FrameHom (Submodule R M) (Submodule S N)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_congr_ae : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  {f g : α → ε}, f =ᵐ[μ] g → MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_iInf_mul : ∀ {ι : Type u_3} (u v : ι → ENNReal), (⨅ i, u i) * ⨅ i, v i ≤ ⨅ i, u i * v i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f)[k]? = f t[k]?
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center of a non-associative semiring `R` is the set of elements that commute and associate
with everything in `R`  -/
Subsemiring.center : (R : Type u) → [inst : NonAssocSemiring R] → Subsemiring R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_diff_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → Std.DHashMap.Internal.Raw₀.Const.get? (m₁.diff m₂) k = none
-- Mathlib.CategoryTheory.GradedObject.Associator
CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {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_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_6 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [inst_8 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_9 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J)
  (h : r (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 :
    CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) h_1) =
    CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1)
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
MeasurableEquiv.piSingleton.eq_1 : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)] (a : ℕ),
  MeasurableEquiv.piSingleton a =
    { toFun := fun x i => ⋯ ▸ x, invFun := fun x => x ⟨a + 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯,
      measurable_invFun := ⋯ }
-- Init.Data.Vector.Count
Vector.boole_getElem_le_count : ∀ {α : Type u_1} [inst : BEq α] {n i : ℕ} {a : α} {xs : Vector α n} (h : i < n),
  (if (xs[i] == a) = true then 1 else 0) ≤ Vector.count a xs
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
RootPairing.ncard_eq_finrank_of_linearIndepOn_of : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : CommRing R] [inst_3 : Module R M] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [P.IsRootSystem] [Nontrivial R] {s : Set ι},
  LinearIndepOn R (⇑P.root) s →
    (∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)) →
      s.ncard = Module.finrank R M
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.extendId`.

---

Extending a cocone by the identity does nothing.  -/
CategoryTheory.Limits.Cocones.extendId : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) → s.extend (CategoryTheory.CategoryStruct.id s.pt) ≅ s
-- Mathlib.Tactic.Abel
/-- A synonym for `•`, used internally in `abel`.  -/
Mathlib.Tactic.Abel.smul : {α : Type u_1} → [AddCommMonoid α] → ℕ → α → α
-- Mathlib.Analysis.Normed.Module.Ray
/-- If two points on the same ray have the same norm, then they are equal.  -/
SameRay.eq_of_norm_eq : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F}, SameRay ℝ x y → ‖x‖ = ‖y‖ → x = y
-- Mathlib.Data.Set.Lattice
Set.biUnion_and' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι' → Prop) (q : ι → ι' → Prop)
  (s : (x : ι) → (y : ι') → p y ∧ q x y → Set α),
  ⋃ x, ⋃ y, ⋃ (h : p y ∧ q x y), s x y h = ⋃ y, ⋃ (hy : p y), ⋃ x, ⋃ (hx : q x y), s x y ⋯
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- If `𝕜₁` is a normed field contained as subfield of a larger normed field `𝕜₂`, and if `a : A`
is an element whose `𝕜₂` spectrum restricts to `𝕜₁`, then the spectral radii over each scalar
field coincide.  -/
SpectrumRestricts.spectralRadius_eq : ∀ {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} {A : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedRing A] [inst_3 : NormedAlgebra 𝕜₁ A] [inst_4 : NormedAlgebra 𝕜₂ A] [inst_5 : NormedAlgebra 𝕜₁ 𝕜₂]
  [IsScalarTower 𝕜₁ 𝕜₂ A] {f : 𝕜₂ → 𝕜₁} {a : A}, SpectrumRestricts a f → spectralRadius 𝕜₁ a = spectralRadius 𝕜₂ a
-- Mathlib.Order.SuccPred.Tree
RootedTree.subtrees_disjoint : ∀ {t : RootedTree}, t.subtrees.PairwiseDisjoint SetLike.coe
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I → f.IsDistinguishedAt I
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_mul : ∀ (x y : ℝ), ↑(x * y) = ↑x * ↑y
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.fst_sConvexComb : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {X : Type u_3}
  {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (w : Convexity.StdSimplex R (X × Y)), (Convexity.sConvexComb w).1 = Convexity.iConvexComb w Prod.fst
-- Init.NotationExtra
«term_×__1» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.pi_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M₁ i)]
  [inst_2 : (i : ι) → Module R (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2} [inst_3 : (i : ι') → AddCommMonoid (M' i)]
  [inst_4 : (i : ι') → Module R (M' i)] (f : (i : ι') → MultilinearMap R M₁ (M' i)) (m : (i : ι) → M₁ i) (i : ι'),
  (MultilinearMap.pi f) m i = (f i) m
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The projection `∫ᶜ F ⥤ 𝒮` given by projecting both objects and homs to the first factor.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.forget : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) →
      CategoryTheory.Functor F.CoGrothendieck 𝒮
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instIsCancelAdd : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] [IsCancelAdd α], IsCancelAdd (Matrix m n α)
-- Batteries.Data.String.Basic
/-- Count the occurrences of a character in a string.  -/
String.count : String → Char → ℕ
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_eq_zero_iff_eq : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit b → (a - b = 0 ↔ a = b)
-- Mathlib.Topology.Separation.GDelta
PerfectlyNormalSpace.mk : ∀ {X : Type u} [inst : TopologicalSpace X] [toNormalSpace : NormalSpace X],
  (∀ ⦃h : Set X⦄, IsClosed h → IsGδ h) → PerfectlyNormalSpace X
-- Mathlib.Analysis.Analytic.Order
/-- The order of a function `f` at a `z₀` is infinity iff `f` vanishes locally around `z₀`.  -/
analyticOrderAt_eq_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, analyticOrderAt f z₀ = ⊤ ↔ ∀ᶠ (z : 𝕜) in nhds z₀, f z = 0
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.polarBilin_baseChange : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup M₂]
  [inst_3 : Algebra R A] [inst_4 : Module R M₂] [inst_5 : Invertible 2] [Invertible 2] (Q : QuadraticForm R M₂),
  QuadraticMap.polarBilin (QuadraticForm.baseChange A Q) = LinearMap.BilinForm.baseChange A (QuadraticMap.polarBilin Q)
-- Mathlib.Algebra.Group.Basic
add_eq_of_eq_neg_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, b = -a + c → a + b = c
-- Mathlib.FieldTheory.Normal.Basic
/-- If `x : L` is a root of `minpoly K y`, then we can find `(σ : Gal(L/K))` with `σ x = y`.
That is, `x` and `y` are Galois conjugates.  -/
minpoly.exists_algEquiv_of_root : ∀ {K : Type u_6} {L : Type u_7} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Normal K L] {x y : L},
  IsAlgebraic K y → (Polynomial.aeval x) (minpoly K y) = 0 → ∃ σ, σ x = y
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.pointwise_smul_le_pointwise_smul_iff : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] {g : G}
  {S T : ValuationSubring K}, g • S ≤ g • T ↔ S ≤ T
-- Mathlib.Topology.UniformSpace.Pi
/-- An infimum of complete uniformities is complete,
as long as the whole family is bounded by some common T2 topology.  -/
CompleteSpace.iInf : ∀ {ι : Type u_4} {X : Type u_5} {u : ι → UniformSpace X},
  (∀ (i : ι), CompleteSpace X) → (∃ t, T2Space X ∧ ∀ (i : ι), (u i).toTopologicalSpace ≤ t) → CompleteSpace X
-- Mathlib.Data.Matrix.Basic
AlgHom.mapMatrix_apply : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Algebra R α] [inst_6 : Algebra R β]
  (f : α →ₐ[R] β) (M : Matrix m m α), f.mapMatrix M = M.map ⇑f
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Cardinal.ord_eq_iInf`. -/
Cardinal.ord_eq_Inf : ∀ (α : Type u), (Cardinal.mk α).ord = ⨅ r, Ordinal.type ↑r
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instAddCommGroup : (A : Type u_3) → (E : Type u_4) → [AddCommGroup E] → AddCommGroup (WithCStarModule A E)
-- Mathlib.Algebra.GroupWithZero.WithZero
MonoidWithZeroHom.map_eq_zero_iff : ∀ {G₀ : Type u_1} {M₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MulZeroOneClass M₀] [Nontrivial M₀]
  {f : G₀ →*₀ M₀} {x : G₀}, f x = 0 ↔ x = 0
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.inf_eq_bot_of_commute : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → (∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) → A ⊓ B = ⊥
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_comp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {k : Type u_3}
  [inst_2 : DivisionRing k] [inst_3 : Module k M] [inst_4 : Module k N] {f : M →ₗ[k] N} {P : Type u_4}
  [inst_5 : AddCommGroup P] [inst_6 : Module k P] (g : N →ₗ[k] P) [FiniteDimensional k ↥f.ker]
  [FiniteDimensional k ↥g.ker] [FiniteDimensional k (N ⧸ f.range)] [FiniteDimensional k (P ⧸ g.range)],
  (g ∘ₗ f).index = g.index + f.index
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_iSup : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {ι : Sort u_1} (f : F) (s : ι → NonUnitalSubring R),
  NonUnitalSubring.map f (iSup s) = ⨆ i, NonUnitalSubring.map f (s i)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_zpow_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 1 ≤ a → m ≤ n → a ^ m ≤ a ^ n
-- Mathlib.Topology.Homotopy.Product
Quotient.mk'.eq_1 : ∀ {α : Sort u} [s : Setoid α] (a : α), Quotient.mk' a = ⟦a⟧
-- Mathlib.Algebra.Homology.Homotopy
CategoryTheory.Functor.mapHomotopyEquiv_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive]
  (h : HomotopyEquiv C D), (F.mapHomotopyEquiv h).hom = (F.mapHomologicalComplex c).map h.hom
-- Init.SimpLemmas
true_or : ∀ (p : Prop), (True ∨ p) = True
-- Std.Http.Protocol.H1
/-- Takes and clears all accumulated events, returning the drained array.
 -/
Std.Http.Protocol.H1.Machine.takeEvents : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Array (Std.Http.Protocol.H1.Event dir)
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- If `G` is a finite Z-group, then `commutator G` is a Hall subgroup of `G`.  -/
IsZGroup.coprime_commutator_index : ∀ (G : Type u_1) [inst : Group G] [Finite G] [IsZGroup G], (Nat.card ↥(commutator G)).Coprime (commutator G).index
-- Mathlib.Algebra.Group.Basic
mul_inv_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b⁻¹ = 1 ↔ a = b
-- Init.Meta.Defs
/-- Interprets a numeric literal as a natural number.

Returns `0` if the syntax is malformed.
 -/
Lean.TSyntax.getNat : Lean.NumLit → ℕ
-- Lean.Message
/-- Wrap the given message in parentheses `()`.  -/
Lean.MessageData.paren : Lean.MessageData → Lean.MessageData
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- **No wrap-around principle**.

The first `k + 1` elements of `Fin (n + 1)` are `m`-Freiman isomorphic to the first `k + 1` elements
of `ℕ` assuming there is no wrap-around.  -/
Fin.isAddFreimanIso_Iic : ∀ {k m n : ℕ}, m ≠ 0 → m * k ≤ n → IsAddFreimanIso m (Set.Iic ↑k) (Set.Iic k) Fin.val
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roc_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toArray[i]? = none ↔ (n - m).toNat ≤ i
-- Mathlib.Order.Monotone.Monovary
monovary_const_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β),
  Monovary f (Function.const ι b)
-- Std.Data.String.ToNat
String.toNat?_comp_toSlice : String.Slice.toNat? ∘ String.toSlice = String.toNat?
-- Mathlib.Data.Finset.Insert
Finset.singleton_subset_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, {a} ⊆ s ↔ a ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.whiskerRight : ∀ {J : Type u_1} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered α →
    ∀ (H : CategoryTheory.Functor C D)
      [∀ (i j : J) (f : j ⟶ i),
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (α.app i) (G.map f)) H],
      CategoryTheory.NatTrans.Equifibered (CategoryTheory.Functor.whiskerRight α H)
-- Init.Data.Order.Opposite
/-- Inverts an {name}`LT` instance.

The result is an {lean}`LT α` instance where {lit}`a < b` holds when {name}`lt` would have
{lit}`b < a` hold.

If {name}`lt` obeys laws, then {lean}`lt.opposite` obeys the opposite laws.
To automatically derive these laws, use {lit}`open scoped Std.OppositeOrderInstances`.

For example, one can use the derived instances to prove properties about the opposite {name}`LT`
instance:

```lean
open scoped Std.OppositeOrderInstances in
example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {x y : α} :
    letI : LE α := LE.opposite inferInstance
    letI : LT α := LT.opposite inferInstance
    ¬ y ≤ x ↔ x < y :=
  letI : LE α := LE.opposite inferInstance
  letI : LT α := LT.opposite inferInstance
  Std.not_le
```

Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLT α`
and {lit}`IsLinearOrder α` instances for the opposite order that are required by {name}`not_le`.
 -/
LT.opposite : {α : Type u_1} → LT α → LT α
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.loopRef.eq_def : ∀ (n : ℕ) (x : Lean.Meta.Grind.Action) (goal : Lean.Meta.Grind.Goal) (x_1 kp : Lean.Meta.Grind.ActionCont),
  Lean.Meta.Grind.Action.loopRef n x goal x_1 kp =
    match n with
    | 0 => kp goal
    | n.succ => x goal kp fun goal' => Lean.Meta.Grind.Action.loopRef n x goal' kp kp
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] [inst_7 : MeasurableSpace A] [inst_8 : BorelSpace A] (μ : MeasureTheory.Measure A)
  [inst_9 : μ.IsAddHaarMeasure] (g : G),
  μ.addHaarScalarFactor (DomMulAct.mk g • μ) = ((MeasureTheory.distribHaarChar A) g)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblU.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.dblU P = (MvPolynomial.eval P) W'.polynomialX
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_self_zsmul_atTop_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G)
  (m : ℤ), MapClusterPt (m • x) Filter.atTop fun x_1 => x_1 • x
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.map hj F τ j (Order.succ j) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso F X ⟨j, ⋯⟩).hom
      (CategoryTheory.CategoryStruct.comp τ (CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso hj F X).inv)