mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)}, (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).isEmpty = ((↑m).isEmpty && l.isEmpty)
-- Mathlib.Data.Set.Basic
Set.empty_ssubset : ∀ {α : Type u} {s : Set α}, ∅ ⊂ s ↔ s.Nonempty
-- Mathlib.CategoryTheory.Comma.Basic
/-- Taking the comma category of the identity `Discrete PUnit ⥤ Discrete PUnit`
and a functor `B ⥤ Discrete PUnit` results in a category equivalent to `B`.  -/
CategoryTheory.Comma.toIdPUnitEquiv : {B : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} B] →
    (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) →
      (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) → CategoryTheory.Comma L R ≌ B
-- Init.Control.Lawful.Instances
instLawfulMonadOption : LawfulMonad Option
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchesAt_iff_exists_isLongestRevMatchAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔
    ∃ startPos, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos pos
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : IsDedekindDomain S],
  Ideal.map (algebraMap R S) p ≠ ⊥ →
    P.IsPrime →
      P ≠ ⊥ → p.ramificationIdx' P = Multiset.count P (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p))
-- Mathlib.Logic.Equiv.Fintype
Equiv.extendSubtype_apply_of_mem : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : Finite ↑{x | p x}]
  (e : { x // p x } ≃ { x // q x }) (x : α) (hx : p x), e.extendSubtype x = ↑(e ⟨x, hx⟩)
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.eq_bot_of_rank_eq_zero : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsDomain R] (b : Module.Basis ι R M) (N : Submodule R M),
  (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0) → N = ⊥
-- Mathlib.Topology.MetricSpace.Cover
/-- A maximal `ε`-separated subset of a set `s` is an `ε`-cover of `s`.

[R. Vershynin, *High Dimensional Probability*][vershynin2018high], 4.2.6.  -/
Metric.IsCover.of_maximal_isSeparated : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s N : Set X},
  Maximal (fun N => N ⊆ s ∧ Metric.IsSeparated (↑ε) N) N → Metric.IsCover ε s N
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- A contravariant functor on `C` satisfies `EqualizerCondition` if it takes kernel pairs of effective
epimorphisms to equalizer diagrams.
 -/
CategoryTheory.regularTopology.EqualizerCondition : {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] → CategoryTheory.Functor Cᵒᵖ D → Prop
-- Lean.Meta.BinderNameHint
_private.Lean.Meta.BinderNameHint.0.Lean.rememberName : ℕ → Lean.Name → Array Lean.Name → Array Lean.Name
-- Lean.Environment
Lean.ImportStateM.run : {α : Type} → Lean.ImportStateM α → optParam Lean.ImportState default → IO (α × Lean.ImportState)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.coe_fn_coe : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B), ⇑↑f = ⇑f
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Equal characteristic implies not mixed characteristic.  -/
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.to_not_mixedCharZero : ∀ (R : Type u_1) [inst : CommRing R], (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → ∀ p > 0, ¬MixedCharZero R p
-- Mathlib.Analysis.Calculus.Implicit
/-- Implicit function `g` defined by `f (g z y) = z`.  -/
HasStrictFDerivAt.implicitFunction : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] →
      {E : Type u_2} →
        [inst_2 : NormedAddCommGroup E] →
          [inst_3 : NormedSpace 𝕜 E] →
            [CompleteSpace E] →
              {F : Type u_3} →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : NormedSpace 𝕜 F] →
                    [FiniteDimensional 𝕜 F] →
                      (f : E → F) →
                        (f' : E →L[𝕜] F) → {a : E} → HasStrictFDerivAt f f' a → (↑f').range = ⊤ → F → ↥(↑f').ker → E
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofLeftInverse_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse ⇑g ⇑f) (x : M), ↑((LinearEquiv.ofLeftInverse h) x) = f x
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.isNontrivial_congr : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v : AbsoluteValue R S} [IsDomain S] [Nontrivial R] {w : AbsoluteValue R S},
  v.IsEquiv w → (v.IsNontrivial ↔ w.IsNontrivial)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.involutiveNeg.eq_1 : ∀ {M₂ : Type u_2} {M₁ : Type u_3} [inst : Neg M₁] [inst_1 : InvolutiveNeg M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (inv : ∀ (x : M₁), f (-x) = -f x), Function.Injective.involutiveNeg f hf inv = { toNeg := inst, neg_neg := ⋯ }
-- Mathlib.Order.Heyting.Basic
HeytingAlgebra.toGeneralizedHeytingAlgebra : {α : Type u_4} → [self : HeytingAlgebra α] → GeneralizedHeytingAlgebra α
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- Converting a bundled commutative monoid to a commutative monoid object in `Type`.
 -/
CommMonTypeEquivalenceCommMon.inverse : CategoryTheory.Functor CommMonCat (CategoryTheory.CommMon (Type u))
-- Mathlib.Data.Int.Bitwise
Int.xor.eq_1 : ∀ (m n : ℕ), (Int.ofNat m).xor (Int.ofNat n) = ↑(m ^^^ n)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral.eq_1 : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.integral f =
    MeasureTheory.SimpleFunc.integral μ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Init.Core
/-- If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`). -/
«term_<->_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Graph.Delete
Graph.vertexSet_deleteVerts : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α), (G.deleteVerts X).vertexSet = G.vertexSet \ X
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_eq_one_iff`. -/
Ideal.ramificationIdx'_eq_one_iff : ∀ {S : Type u_1} [inst : CommRing S] {q : Ideal S} {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [inst_3 : q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsIntegral R S]
  [PerfectField (Ideal.under R q).ResidueField], q.ramificationIdx R = 1 ↔ Algebra.IsUnramifiedAt R q
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.val_zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, ↑0 = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.inhabitedOfVar : {L : FirstOrder.Language} → {α : Type u'} → [Inhabited α] → Inhabited (L.Term α)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_filterM : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o] [LawfulMonad o] [inst_10 : Std.IteratorLoop α m n]
  [inst_11 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o]
  [inst_14 : MonadLiftT m n] [inst_15 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
  {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.filterM f it) =
    Std.IterM.foldM
      (fun d b => do
        let __do_lift ← liftM (f b)
        if __do_lift.down = true then g d b else pure d)
      init it
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.nil_iff_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → (p.Nil ↔ u = v)
-- Init.Data.UInt.Bitwise
UInt8.not_neg_one : ~~~(-1) = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesCokernel.iso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.PreservesCokernel.iso G f =
    (CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit G f).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (G.map f) 0))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDHashMap.filterMap f m).get? k = (m.get? k).bind (f k)
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheaf_eq_pushforward : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] (A : C)
  [hd : (U : TopologicalSpace.Opens ↑(TopCat.of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)],
  skyscraperPresheaf p₀ A =
    (TopCat.Presheaf.pushforward C (TopCat.ofHom (ContinuousMap.const (↑(TopCat.of PUnit.{u + 1})) p₀))).obj
      (skyscraperPresheaf PUnit.unit A)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.instAddDistribAddActionSemiHomClassCoeAddMonoidHom : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (φ : M →* N) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] (B : Type u_5) [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B],
  DistribMulActionSemiHomClass (A →ₑ+[φ] B) (⇑φ) A B
-- Mathlib.Tactic.GRewrite.Core
/-- Whether the lemma rewrites right-to-left (i.e. whether it has a `←`).  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.symm : Mathlib.Tactic.GRewrite.GRewriteLemma✝ → Bool
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.mk.injEq : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : Star R] (toSubsemiring : Subsemiring R)
  (star_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → star a ∈ toSubsemiring.carrier) (toSubsemiring_1 : Subsemiring R)
  (star_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → star a ∈ toSubsemiring_1.carrier),
  ({ toSubsemiring := toSubsemiring, star_mem' := star_mem' } =
      { toSubsemiring := toSubsemiring_1, star_mem' := star_mem'_1 }) =
    (toSubsemiring = toSubsemiring_1)
-- Mathlib.NumberTheory.Divisors
Nat.toFinset_divisorsAntidiagonalList : ∀ {n : ℕ}, n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
/-- [Stacks Tag 01TB](https://stacks.math.columbia.edu/tag/01TB) ((1) => (2)) -/
AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType : ∀ {X : AlgebraicGeometry.Scheme} [JacobsonSpace ↥X] {x : ↥X},
  IsClosed {x} ↔ AlgebraicGeometry.LocallyOfFiniteType (X.fromSpecResidueField x)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.fixedPoint_lipschitz_in_map : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] {g : α → α} (hg : ContractingWith K g) {C : ℝ},
  (∀ (z : α), dist (f z) (g z) ≤ C) →
    dist (ContractingWith.fixedPoint f hf) (ContractingWith.fixedPoint g hg) ≤ C / (1 - ↑K)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_eq_fallback : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, a ∉ m → m.getD a fallback = fallback
-- Mathlib.Topology.Algebra.Monoid
/-- If `f : α → M` and `g : β → M` are continuous and both tend to zero on the cocompact filter,
then `fun i : α × β ↦ f i.1 * g i.2` also tends to zero on the cocompact filter.  -/
tendsto_mul_cocompact_nhds_zero : ∀ {M : Type u_3} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M]
  [inst_3 : TopologicalSpace α] [inst_4 : TopologicalSpace β] {f : α → M} {g : β → M},
  Continuous f →
    Continuous g →
      Filter.Tendsto f (Filter.cocompact α) (nhds 0) →
        Filter.Tendsto g (Filter.cocompact β) (nhds 0) →
          Filter.Tendsto (fun i => f i.1 * g i.2) (Filter.cocompact (α × β)) (nhds 0)
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.toPrefunctor_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D}, F.toPrefunctor = G.toPrefunctor → F = G
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.zip_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α)
  (c₁ : OmegaCompletePartialOrder.Chain β) (n : ℕ), (c₀.zip c₁) n = (c₀ n, c₁ n)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.union : ∀ {α : Type u} {s t : Set α}, s.Finite → t.Finite → (s ∪ t).Finite
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.brecOn.eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : RingCat.Colimits.Prequotient F → Sort u} (t : RingCat.Colimits.Prequotient F)
  (F_1 : (t : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Prequotient.below t → motive t),
  RingCat.Colimits.Prequotient.brecOn t F_1 = F_1 t (RingCat.Colimits.Prequotient.brecOn.go t F_1).2
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Negation `x ↦ -x` as an `IsometryEquiv`.  -/
IsometryEquiv.neg : (G : Type v) →
  [inst : AddGroup G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricVAdd G G] → [IsIsometricVAdd Gᵃᵒᵖ G] → G ≃ᵢ G
-- Lean.Expr
_private.Lean.Expr.0.Lean.natPowFn : Lean.Expr
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff : ∀ {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] (J : Type u') [inst_2 : CategoryTheory.Category.{v', u'} J]
  (P : CategoryTheory.ObjectProperty D) [P.IsClosedUnderIsomorphisms] (e : C ≌ D),
  (P.inverseImage e.functor).IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J
-- Mathlib.Order.Interval.Finset.Nat
Nat.cauchy_induction' : ∀ {P : ℕ → Prop} (seed : ℕ),
  (∀ (n : ℕ), P (n + 1) → P n) → P seed → (∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y) → ∀ (n : ℕ), P n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan : ∀ (x : ℝ), Real.sin (Real.arctan x) = x / √(1 + x ^ 2)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : Semiring A] [inst_1 : Field B] [IsAlgClosed B] {f : A →+* B} {p : Polynomial A},
  f p.leadingCoeff ≠ 0 → (Polynomial.map f p).roots.card = p.natDegree
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_uIcc : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  a ≠ 0 → ∀ (b c : α), (fun x => x * a) ⁻¹' Set.uIcc b c = Set.uIcc (b / a) (c / a)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa.inj : ∀ {n : ℕ} {a a_1 : ZMod (2 * n)}, QuaternionGroup.xa a = QuaternionGroup.xa a_1 → a = a_1
-- Mathlib.Algebra.GCDMonoid.Basic
pow_dvd_of_mul_eq_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c d₁ d₂ : α},
  a ≠ 0 → IsUnit (gcd a b) → ∀ {k : ℕ}, a * b = c ^ k → c = d₁ * d₂ → d₁ ∣ a → d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Bijective affine maps are affine isomorphisms.  -/
AffineEquiv.ofBijective : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] → {φ : P₁ →ᵃ[k] P₂} → Function.Bijective ⇑φ → P₁ ≃ᵃ[k] P₂
-- Mathlib.Analysis.Complex.Circle
Circle.instCommGroup : CommGroup Circle
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.mul_prod_Ico_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 b * ∏ x ∈ Finset.Ico a b, f x = ∏ x ∈ Finset.Icc a b, f x
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.renameEquiv_symm : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ ≃ τ),
  (MvPowerSeries.renameEquiv R f).symm = MvPowerSeries.renameEquiv R f.symm
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.aleph0_mul_eq : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → Cardinal.aleph0 * a = a
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comap_obj : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I)
  (f : (i : I) → C i) (i : J), (CategoryTheory.Pi.comap C h).obj f i = f (h i)
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLT_succ_eq_degreeLE : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, Polynomial.degreeLT R (n + 1) = Polynomial.degreeLE R ↑n
-- Init.Grind.Ordered.Rat
Lean.Grind.instLawfulOrderLTRat : Std.LawfulOrderLT ℚ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_le_max_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.isEmpty = false}, (cmp (t.max he) ((t.insert k).max ⋯)).isLE = true
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.rotate_distinguished_triangle' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  ∀ T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C,
    T.rotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.uniqueAddUnits : {α : Type u_1} → Unique (AddUnits (FreeAddMonoid α))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.mul_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Mul (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] (i : ι) (x y : G i),
  ⟦⟨i, x⟩⟧ * ⟦⟨i, y⟩⟧ = ⟦⟨i, x * y⟩⟧
-- Mathlib.Algebra.Order.Hom.Ring
/-- `simp`-normal form of `trans_toRingEquiv`.  -/
OrderRingIso.trans_toRingEquiv_aux : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β]
  [inst_4 : Add β] [inst_5 : LE β] [inst_6 : Mul γ] [inst_7 : Add γ] [inst_8 : LE γ] (f : α ≃+*o β) (g : β ≃+*o γ),
  ↑(f.trans g) = f.trans g.toRingEquiv
-- Mathlib.Data.Set.Lattice.Image
Set.image_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β},
  Function.Bijective f → ∀ (s : ι → Set α), f '' ⋂ i, s i = ⋂ i, f '' s i
-- Init.Data.Int.Order
Int.lt_of_neg_lt_neg : ∀ {a b : ℤ}, -b < -a → a < b
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
/-- The subalgebra of functions that are bounded along a filter `l`.  -/
Filter.boundedFilterSubalgebra : (𝕜 : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : SeminormedCommRing 𝕜] →
        [inst_1 : SeminormedRing β] → [inst_2 : Algebra 𝕜 β] → [IsBoundedSMul 𝕜 β] → Filter α → Subalgebra 𝕜 (α → β)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂_hom_comp_i_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH2 A).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 2)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).hom h)
-- Qq.Macro
/-- Translates an arbitrary local context to a context of
Q-annotated expressions. Used by `by_elabq` and `run_tacq`.
 -/
Qq.Impl.quoteLCtx : Lean.LocalContext → List Lean.Name → Qq.Impl.UnquoteM (Lean.LocalContext × Array Lean.Expr)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_cos : Measurable Real.cos
-- Mathlib.Topology.Path
Path.continuous_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Continuous Path.symm
-- Mathlib.Data.NNRat.Defs
NNRat.divNat_mul_divNat : ∀ (n₁ n₂ : ℕ) {d₁ d₂ : ℕ}, NNRat.divNat n₁ d₁ * NNRat.divNat n₂ d₂ = NNRat.divNat (n₁ * n₂) (d₁ * d₂)
-- Mathlib.Analysis.SpecificLimits.Normed
/-- Partial sums of an alternating antitone series with an even number of terms provide
lower bounds on the limit.  -/
Antitone.alternating_series_le_tendsto : ∀ {E : Type u_4} [inst : Ring E] [inst_1 : PartialOrder E] [IsOrderedRing E] [inst_3 : TopologicalSpace E]
  [OrderClosedTopology E] {l : E} {f : ℕ → E},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l) →
    Antitone f → ∀ (k : ℕ), ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l
-- Mathlib.Order.Hom.Basic
OrderHom.const_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α →o β) (c : γ), ((OrderHom.const β) c).comp f = (OrderHom.const α) c
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.lift_X : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (x : S) (h : P.HasMap x), (P.lift x h) P.X = x
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.mk.inj : ∀ {carrier : Type u} {str : Group carrier} {carrier_1 : Type u} {str_1 : Group carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1