mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.sup_eq_prod_inf_factors`. -/
sup_eq_prod_inf_factors : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ →
    J ≠ ⊥ → I ⊔ J = (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J).prod
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.sup_apply : ∀ {E : Type u_3} [inst : AddGroup E] (p q : AddGroupNorm E) (x : E), (p ⊔ q) x = max (p x) (q x)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.OuterMeasure.pi.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] (m : (i : ι) → MeasureTheory.OuterMeasure (α i)),
  MeasureTheory.OuterMeasure.pi m = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.piPremeasure m)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_range : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {ι : Sort u_5} (a : α) (f : ι → β),
  a • Set.range f = Set.range fun i => a • f i
-- Mathlib.RingTheory.Regular.IsSMulRegular
IsSMulRegular.lTensor : ∀ {R : Type u_1} (M : Type u_3) {M' : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [Module.Flat R M] {r : R},
  IsSMulRegular M' r → IsSMulRegular (TensorProduct R M M') r
-- Batteries.Data.Vector.Lemmas
_private.Batteries.Data.Vector.Lemmas.0.Vector.scanr_eq_reverse_scanl_reverse : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  Vector.scanr f init as = (Vector.scanl (flip f) init as.reverse).reverse
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_iSup : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {ι : Sort u_1} (f : K →+* L)
  (s : ι → Subfield K), Subfield.map f (iSup s) = ⨆ i, Subfield.map f (s i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_sub_pi : ∀ (x : ℝ), Real.tan (x - Real.pi) = Real.tan x
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.prod_unique : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring T] (f : R →ₙ+* S × T),
  ((NonUnitalRingHom.fst S T).comp f).prod ((NonUnitalRingHom.snd S T).comp f) = f
-- Init.Data.Vector.Int
Vector.sum_eq_foldl_int : ∀ {n : ℕ} {xs : Vector ℤ n}, xs.sum = Vector.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Init.Data.Order.Ord
Std.instReflCmpOfOrientedCmp : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp], Std.ReflCmp cmp
-- Mathlib.Util.SynthesizeUsing
/-- `synthesizeUsing type tac` synthesizes an element of type `type` using tactic `tac`.

The tactic must solve for all goals, in contrast to `synthesizeUsing`.
 -/
synthesizeUsing' : {u : Lean.Level} → (type : Q(Sort u)) → Lean.Elab.Tactic.TacticM Unit → Lean.MetaM Q(«$type»)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_3.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_eq_empty_iff : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ico a b = ∅ ↔ ¬a < b
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_lineMap_right : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist ((AffineMap.lineMap p₁ p₂) c) p₂ = ‖1 - c‖₊ * nndist p₁ p₂
-- Init.Tactics
/-- Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`,
`e` must have type `t` in the context `ctx, h : t'`.

The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`.
If `h :` is omitted, the name `this` is used.
  -/
Lean.Parser.Tactic.tacticSuffices_ : Lean.ParserDescr
-- Mathlib.Data.Matrix.Mul
dotProduct_smul : ∀ {m : Type u_2} {R : Type u_7} {α : Type v} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  [inst_3 : DistribSMul R α] [SMulCommClass R α α] (x : R) (v w : m → α), v ⬝ᵥ x • w = x • (v ⬝ᵥ w)
-- Lean.Expr
Lean.Expr.brecOn.eq : ∀ {motive : Lean.Expr → Sort u} (t : Lean.Expr) (F_1 : (t : Lean.Expr) → Lean.Expr.below t → motive t),
  Lean.Expr.brecOn t F_1 = F_1 t (Lean.Expr.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Limits.HasProducts A] [inst_3 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.firstMap R P) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.secondMap R P)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.range_map : ∀ {α : Type u} {β : Type v} {f : α → β}, (FreeGroup.map f).range = Subgroup.closure (FreeGroup.of '' Set.range f)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.toAddMonoidHom_injective : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
  Function.Injective NormedAddGroupHom.toAddMonoidHom
-- Mathlib.Analysis.Complex.Basic
RCLike.complexLinearIsometryEquiv_symm_apply : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (h : RCLike.im RCLike.I = 1) (a : ℂ),
  (RCLike.complexLinearIsometryEquiv h).symm a = (RCLike.complexRingEquiv h).invFun a
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than or equal to the given key.
 -/
Std.ExtTreeMap.getKeyGE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `Ring` instance for `type`  -/
Lean.Meta.Grind.Arith.CommRing.Ring.ringInst : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.Expr
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_edist_right : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {x : α},
  Measurable (edist x)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.exactly.go.eq_def : ∀ {α : Type} (parse : Std.Internal.Parsec.String.Parser α) (size : ℕ) (acc : Array α) (count : ℕ),
  Std.Time.exactly.go✝ parse size acc count =
    if count ≥ size then pure acc
    else do
      let res ← parse
      Std.Time.exactly.go✝ parse size (acc.push res) count.succ
-- Mathlib.Data.Fintype.Pigeonhole
/-- The strong pigeonhole principle for infinitely many pigeons in
finitely many pigeonholes.  If there are infinitely many pigeons in
finitely many pigeonholes, then there is a pigeonhole with infinitely
many pigeons.

See also: `Finite.exists_ne_map_eq_of_infinite`
 -/
Finite.exists_infinite_fiber : ∀ {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β] (f : α → β), ∃ y, Infinite ↑(f ⁻¹' {y})
-- Mathlib.Logic.Function.FiberPartition
/-- An arbitrary element of `a : Fiber f`.  -/
Function.Fiber.preimage : {Y : Type u_2} → {Z : Type u_3} → (f : Y → Z) → Function.Fiber f → Y
-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.equiv_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Functor.equiv.inverse = CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{w + 1})
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- The difference of the right morphisms factors through `hom`.  -/
CategoryTheory.Arrow.RightHomotopy.comm : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (self : CategoryTheory.Arrow.RightHomotopy f g),
  CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
    CategoryTheory.CategoryStruct.comp self.hom v.hom
-- Init.Control.Lawful.Basic
/-- A `bind` followed by `pure` composed with a function is equivalent to a functorial map.

This means that `pure` really is pure after a `bind` and has no effects.
 -/
LawfulMonad.bind_pure_comp : ∀ {m : Type u → Type v} {inst : Monad m} [self : LawfulMonad m] {α β : Type u} (f : α → β) (x : m α),
  (do
      let a ← x
      pure (f a)) =
    f <$> x
-- Init.Data.Int.Basic
/-- Strict inequality of integers, usually accessed via the `<` operator.

`a < b` when `a + 1 ≤ b`.
 -/
Int.lt : ℤ → ℤ → Prop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_hom_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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso C D).hom.app X =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
-- Mathlib.FieldTheory.RatFunc.Valuation
/-- The valuation at infinity on `F(t)`.  -/
RatFunc.inftyValuation : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → Valuation (RatFunc F) (WithZero (Multiplicative ℤ))
-- Mathlib.Order.Interval.Finset.Box
Finset.eq_zero_iff_eq_zero_of_mem_box : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : LocallyFiniteOrder α] {n : ℕ}
  [inst_4 : DecidableEq α] {x : α}, x ∈ Finset.box n → (x = 0 ↔ n = 0)
-- Lean.Parser.Basic
Lean.Parser.LeadingIdentBehavior.default.sizeOf_spec : sizeOf Lean.Parser.LeadingIdentBehavior.default = 1
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_mapDomainAddEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (e : M ≃ N)
  (x : AddMonoidAlgebra R M), ((AddMonoidAlgebra.mapDomainAddEquiv R e) x).coeff = Finsupp.equivMapDomain e x.coeff
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- This is the `iff` version of `Matrix.IsHermitian.fromBlocks`.  -/
Matrix.isHermitian_fromBlocks_iff : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : InvolutiveStar α] {A : Matrix m m α} {B : Matrix m n α}
  {C : Matrix n m α} {D : Matrix n n α},
  (Matrix.fromBlocks A B C D).IsHermitian ↔ A.IsHermitian ∧ B.conjTranspose = C ∧ C.conjTranspose = B ∧ D.IsHermitian
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.expr : Lean.Elab.Term.LevelMVarErrorInfo → Lean.Expr
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurve.continuous : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v → Continuous γ
-- Mathlib.Logic.Equiv.Defs
Equiv.existsUnique_congr_left : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β), (∃! a, p a) ↔ ∃! b, p (e.symm b)
-- Mathlib.Data.EReal.Basic
EReal.instMulZeroOneClass : MulZeroOneClass EReal
-- Lean.Parser.Types
Lean.Parser.argPrec : ℕ
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- The underlying set of boxes  -/
BoxIntegral.Prepartition.boxes : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → Finset (BoxIntegral.Box ι)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_inv.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] {a a' : Rack.PreEnvelGroup R} (ha : Rack.PreEnvelGroupRel' R a a'),
  sizeOf ha.congr_inv = 1 + sizeOf a + sizeOf a' + sizeOf ha
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.snd_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).2 = Convexity.iConvexComb w Prod.snd
-- Init.Data.Vector.Find
Vector.get_find?_mem : ∀ {α : Type} {n : ℕ} {p : α → Bool} {xs : Vector α n} (h : (Vector.find? p xs).isSome = true),
  (Vector.find? p xs).get h ∈ xs
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p` is a Taylor series up to `n`, and
`p (n + 1)` is a derivative of `p n`.  -/
hasFTaylorSeriesUpToOn_succ_iff_left : ∀ {𝕜 : 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} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ},
  HasFTaylorSeriesUpToOn (↑n + 1) f p s ↔
    HasFTaylorSeriesUpToOn (↑n) f p s ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y => p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x => p x (n + 1)) s
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushouts_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange], P.pushouts ≤ P
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Asymptotically, the logarithmic counting function for the zeros of `f * g` is less than or equal to
the sum of the logarithmic counting functions for the zeros of `f` and `g`, respectively.
 -/
ValueDistribution.logCounting_mul_top_eventuallyLE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜},
  Meromorphic f₁ →
    (∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) →
      Meromorphic f₂ →
        (∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) →
          ValueDistribution.logCounting (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop]
            ValueDistribution.logCounting f₁ ⊤ + ValueDistribution.logCounting f₂ ⊤
-- Mathlib.Algebra.Order.UpperLower
_private.Mathlib.Algebra.Order.UpperLower.0.UpperSet.zero_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s : UpperSet α),
  0 + s = s
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.congr_fun : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₐc[R] B}, φ₁ = φ₂ → ∀ (x : A), φ₁ x = φ₂ x
-- Mathlib.RingTheory.Length
Module.length_pi_of_fintype : ∀ (R : Type u_1) [inst : Ring R] {ι : Type u_5} [inst_1 : Fintype ι] (M : ι → Type u_6)
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module R (M i)],
  Module.length R ((i : ι) → M i) = ∑ i, Module.length R (M i)
-- Mathlib.Topology.Inseparable
specializingMap_iff_closure_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → (SpecializingMap f ↔ ∀ (x : X), f '' closure {x} = closure {f x})
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.mem_of : ∀ {α : Type u_1} {m n : α}, m ∈ FreeMonoid.of n ↔ m = n
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.inclusion.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] {H K : S} (h : H ≤ K),
  AddSubgroupClass.inclusion h = AddMonoidHom.mk' (fun x => ⟨↑x, ⋯⟩) ⋯
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk'_comp_subtype : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], (QuotientGroup.mk' N).comp N.subtype = 1
-- Batteries.Data.BitVec.Lemmas
BitVec.getLsbD_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ), (BitVec.ofFnBE f).getLsbD i = if h : i < n then f ⟨i, h⟩.rev else false
-- Mathlib.NumberTheory.Dioph
/-- The set of places where two Diophantine functions are unequal is Diophantine.  -/
Dioph.ne_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v ≠ g v}
-- Mathlib.GroupTheory.Commutator.Basic
/-- The set of commutator elements `⁅g₁, g₂⁆` in `G`.  -/
commutatorSet : (G : Type u_1) → [Group G] → Set G
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₂ : ∀ (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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₂ = F.comp CategoryTheory.ShortComplex.π₂
-- Lean.Elab.Binders
Lean.Elab.Term.elabLetDecl : Lean.Elab.Term.TermElab
-- Mathlib.GroupTheory.OrderOfElement
mem_powers_iff_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x y : G} [Finite G], y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.vadd.eq_1 : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G β],
  Function.Embedding.vadd = { vadd := fun g f => f.trans (Equiv.toEmbedding (AddAction.toPerm g)) }
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.eq_of_false : ∀ {a b : Prop}, ¬a → ¬b → a = b
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_preimage : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ (f : α ≃ α) (Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s),
        (∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs) →
          ∀ {A : Set α},
            (MeasureTheory.inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (MeasureTheory.inducedOuterMeasure m P0 m0) A
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.instModelField : ∀ {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K], K ⊨ FirstOrder.Language.Theory.field
-- Init.Control.StateRef
/-- Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
lifting](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monad-lifting).
 -/
StateRefT'.lift : {ω σ : Type} → {m : Type → Type} → {α : Type} → m α → StateRefT' ω σ m α
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature : Type
-- Init.Data.Fin.Lemmas
Fin.rev_lt_rev : ∀ {n : ℕ} {i j : Fin n}, i.rev < j.rev ↔ j < i
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformly.hasProdUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  MultipliableUniformly f → HasProdUniformly f fun x => ∏' (i : ι), f i x
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The cocone over the proposed colimit additive commutative group.  -/
AddCommGrpCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J AddCommGrpCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.Lie.Basic
LieEquiv.bijective : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), Function.Bijective ⇑e.toLieHom
-- Mathlib.Topology.NhdsSet
IsClosed.nhdsSet_le_sup' : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X) {t : Set X},
  IsClosed t → nhdsSet s ≤ nhdsSet (t ∩ s) ⊔ Filter.principal tᶜ
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ}
  {m : Type u → Type w} [inst_8 : Monad m] {r : Std.Roc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Roc.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_succ_succ : ∀ {m n : ℕ}, ((m + 1)...n + 1).toList = List.map (fun x => x + 1) (m...n).toList
-- Mathlib.Algebra.Module.Equiv.Defs
/-- Left scalar multiplication of a unit and a linear equivalence, as a linear equivalence.  -/
LinearEquiv.instSMulUnitsId : {S : Type u_14} →
  {R : Type u_15} →
    {V : Type u_16} →
      {W : Type u_17} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module R V] →
                [inst_4 : Module S V] →
                  [inst_5 : AddCommMonoid W] →
                    [inst_6 : Module R W] →
                      [inst_7 : Module S W] →
                        [SMulCommClass R S W] →
                          [inst_9 : SMul S R] → [IsScalarTower S R V] → [IsScalarTower S R W] → SMul Sˣ (V ≃ₗ[R] W)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The natural equivalence `E × (F × G) ≃ (E × F) × G` is smooth.

Warning: see remarks attached to `contDiff_prodAssoc`
 -/
contDiff_prodAssoc_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞},
  ContDiff 𝕜 n ⇑(Equiv.prodAssoc E F G).symm
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ofStarMonoidHom_symm_apply : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Star A] [inst_3 : Star B] (f : A →⋆* B)
  (g : B →⋆* A) (h₁ : g.comp f = StarMonoidHom.id A) (h₂ : f.comp g = StarMonoidHom.id B) (a : B),
  (StarMulEquiv.ofStarMonoidHom f g h₁ h₂).symm a = g a
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_ceil_map_map_zero : ∀ (f g : CircleDeg1Lift), ⌈f 0⌉ + ⌊g 0⌋ ≤ ⌈(f * g) 0⌉
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
AddSubgroup.intCast_mul_mem_zmultiples : ∀ {R : Type u_4} [inst : Ring R] (r : R) (k : ℤ), ↑k * r ∈ AddSubgroup.zmultiples r
-- Mathlib.Order.Hom.Lattice
InfHom.instInfHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β], InfHomClass (InfHom α β) α β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The canonical map `X ×ₛ Y ⟶ X ×ₜ Y` given `S ⟶ T`.  -/
CategoryTheory.Limits.pullback.mapDesc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y S T : C} →
      (f : X ⟶ S) →
        (g : Y ⟶ S) →
          (i : S ⟶ T) →
            [inst_1 : CategoryTheory.Limits.HasPullback f g] →
              [inst_2 :
                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i)
                    (CategoryTheory.CategoryStruct.comp g i)] →
                CategoryTheory.Limits.pullback f g ⟶
                  CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp f i)
                    (CategoryTheory.CategoryStruct.comp g i)
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec : ∀ {ι : Type u} (R : ι → CommRingCat) (I : Ideal ((i : ι) → ↑(R i)))
  (f : (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ AlgebraicGeometry.Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) =
      AlgebraicGeometry.sigmaSpec R →
    I = ⊥
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_neg : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E),
  ∫ (x : ℝ) in a..b, f (-x) = ∫ (x : ℝ) in -b..-a, f x
-- Mathlib.Data.Set.Insert
Set.empty_ne_singleton : ∀ {α : Type u_1} (a : α), ∅ ≠ {a}