mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Regular.Basic
/-- If an element `b` becomes add-right-regular after adding to it on the right
an add-right-regular element, then `b` is add-right-regular.  -/
IsAddRightRegular.of_add : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R}, IsAddRightRegular (b + a) → IsAddRightRegular b
-- Aesop.Tree.Data
Aesop.MVarCluster.provenGoal? : Aesop.MVarCluster → BaseIO (Option Aesop.GoalRef)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.mem_neighborFinset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] (w : V),
  w ∈ G.neighborFinset v ↔ G.Adj v w
-- Mathlib.Algebra.Lie.TraceForm
LieModule.trace_toEnd_mul_eq_zero_of_traceForm_eq_zero : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.traceForm R L M = 0 →
    ∀ (y : Module.End R M),
      (∀ z ∈ (LieModule.toEnd R L M).range, ⁅y, z⁆ ∈ (LieModule.toEnd R L M).range) →
        ∀ x ∈ LieAlgebra.derivedSeries R L 1, (LinearMap.trace R M) ((LieModule.toEnd R L M) x * y) = 0
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.monomial_dvd_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {r s : R} {i j : σ →₀ ℕ},
  (MvPolynomial.monomial i) r ∣ (MvPolynomial.monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s
-- Lean.Data.JsonRpc
Lean.JsonRpc.instOfNatRequestID : {n : ℕ} → OfNat Lean.JsonRpc.RequestID n
-- Lean.Util.Path
Lean.searchPathRef : IO.Ref Lean.SearchPath
-- Mathlib.GroupTheory.Exponent
Monoid.lcm_orderOf_dvd_exponent : ∀ (G : Type u) [inst : Monoid G] [inst_1 : Fintype G], Finset.univ.lcm orderOf ∣ Monoid.exponent G
-- Mathlib.Analysis.Complex.Trigonometric
Complex.two_sinh : ∀ (x : ℂ), 2 * Complex.sinh x = Complex.exp x - Complex.exp (-x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β] {a : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c)[a]! = default
-- Mathlib.Order.Filter.Lift
Filter.mem_lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {t : Set α}, t ∈ f → h t ∈ f.lift' h
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An induction principle for `FiniteMulArchimedeanClass`.  -/
FiniteMulArchimedeanClass.ind : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  {motive : FiniteMulArchimedeanClass M → Prop},
  (∀ (a : M) (ha : a ≠ 1), motive (FiniteMulArchimedeanClass.mk a ha)) → ∀ (x : FiniteMulArchimedeanClass M), motive x
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.mapComon_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (A : CategoryTheory.Comon C),
  (F.mapComon.obj A).X = F.obj A.X
-- Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Tactic.GCongr.ForwardExt.mk : (Lean.Expr → Lean.MVarId → Lean.MetaM Unit) → Mathlib.Tactic.GCongr.ForwardExt
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasDerivWithinAt.exp : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') s x
-- Init.Data.Int.Order
Int.sub_le_sub_left : ∀ {a b : ℤ}, a ≤ b → ∀ (c : ℤ), c - b ≤ c - a
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.instPowNat : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → Pow (GroupLike R A) ℕ
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom right map in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPrePost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPrePre' F)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableSimpCacheKey : Hashable Lean.Elab.Tactic.Grind.SimpCacheKey
-- Mathlib.CategoryTheory.Monad.Types
/-- The `Kleisli` category of a `Control.Monad` is equivalent to the `Kleisli` category of its
category-theoretic version, provided the monad is lawful.
 -/
CategoryTheory.kleisliCatEquivKleisli : (m : Type u → Type u) →
  [inst : Monad m] →
    [inst_1 : LawfulMonad m] → CategoryTheory.KleisliCat m ≌ CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)
-- Mathlib.Algebra.Module.BigOperators
Finset.cast_card : ∀ {α : Type u_3} {R : Type u_5} [inst : NonAssocSemiring R] (s : Finset α), ↑s.card = ∑ x ∈ s, 1
-- Init.Data.Option.Attach
Option.any_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }} {q : α → Bool},
  Option.any q o.unattach = Option.any (q ∘ Subtype.val) o
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditive_id : ∀ {α : Type u_3} [inst : MulOneClass α], MonoidHom.toAdditive (MonoidHom.id α) = AddMonoidHom.id (Additive α)
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular]
  [P.ι.IsDense] [CategoryTheory.LocallySmall.{w, v, u} C],
  P ≤ CategoryTheory.isCardinalPresentable C κ →
    ∀ [∀ (X : C), CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow P.ι X) κ],
      P.IsCardinalFilteredGenerator κ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mem_supp_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x : R), x ∈ v.supp ↔ v x = 0
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : α), ↑(Finset.Ioc b a) = Set.Ioc b a
-- Mathlib.Algebra.Group.Defs
CancelMonoid.toIsRightCancelMul : ∀ {M : Type u} [self : CancelMonoid M], IsRightCancelMul M
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.uniqueRingEquiv_symm_apply : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : Subsingleton M] (r : R),
  (AddMonoidAlgebra.uniqueRingEquiv M).symm r = AddMonoidAlgebra.single 0 r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_le_size_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF → ∀ {k : α} {f : Option β → Option β}, (↑m).size - 1 ≤ (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the left adjoint is faithful, then each component of the unit is a monomorphism.  -/
CategoryTheory.Adjunction.unit_mono_of_L_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Faithful] (X : C),
  CategoryTheory.Mono (h.unit.app X)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_le' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ), hτ.measurableSpace ≤ ⨆ t, ↑f t
-- Mathlib.Logic.Embedding.Basic
Equiv.toEmbedding_injective : ∀ {α : Sort u} {β : Sort v}, Function.Injective Equiv.toEmbedding
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.s : Std.Time.GenericFormat.DateBuilder✝ → Option (Std.Time.Second.Ordinal true)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.containsThenInsert.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.containsThenInsert a = m_1.containsThenInsert a_1
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.instSubtypeMemSubgroupTop : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [IsGaloisGroup G A B], IsGaloisGroup (↥⊤) A B
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_lt_one : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0}, ↑p < 1 ↔ p < 1
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.numMVars : Lean.Meta.AbstractMVarsResult → ℕ
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.subtype_coe : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (s : Set α), AntilipschitzWith 1 Subtype.val
-- Mathlib.Topology.ClusterPt
ClusterPt.of_le_nhds' : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f : Filter X}, f ≤ nhds x → f.NeBot → ClusterPt x f
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_sup_left : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A},
  x ∈ S → x ∈ S ⊔ T
-- Lean.Elab.PatternVar
/-- Check whether `stx` is a pattern variable or constructor-like (i.e., constructor or constant tagged with `[match_pattern]` attribute)  -/
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processId : Lean.Syntax → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.id_as : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (a : CategoryTheory.LocallyDiscrete C),
  (CategoryTheory.CategoryStruct.id a).as = CategoryTheory.CategoryStruct.id a.as
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_of_forall_inner : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [SecondCountableTopology E] {f : α → E},
  (∀ (c : E), (fun x => inner 𝕜 c (f x)) =ᵐ[μ] 0) → f =ᵐ[μ] 0
-- Init.Data.SInt.Lemmas
Int16.two_mul : ∀ {a : Int16}, 2 * a = a + a
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- An additive subgroup of `Lp E p μ`, consisting of the equivalence classes which contain a
bounded continuous representative.  -/
MeasureTheory.Lp.boundedContinuousFunction : {α : Type u_1} →
  (E : Type u_2) →
    {m0 : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : TopologicalSpace α] →
            [BorelSpace α] →
              [inst_2 : NormedAddCommGroup E] →
                [SecondCountableTopologyEither α E] → AddSubgroup ↥(MeasureTheory.Lp E p μ)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
DirectSum.SetLike.IsHomogeneous.mem_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] {R : Subsemiring A},
  DirectSum.SetLike.IsHomogeneous 𝒜 R → ∀ {a : A}, a ∈ R ↔ ∀ (i : ι), ↑(((DirectSum.decompose 𝒜) a) i) ∈ R
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift_of : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : α → β) (x : α),
  (FreeAddSemigroup.lift f) (FreeAddSemigroup.of x) = f x
-- Mathlib.Data.Set.Prod
Set.piMap_image_pi_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {f : (i : ι) → α i → β i} (t : (i : ι) → Set (α i)),
  Pi.map f '' s.pi t ⊆ s.pi fun i => f i '' t i
-- Mathlib.Topology.Algebra.FilterBasis
/-- `AddGroupFilterBasis` constructor in the additive commutative group case.  -/
addGroupFilterBasisOfComm : {G : Type u_1} →
  [inst : AddCommGroup G] →
    (sets : Set (Set G)) →
      sets.Nonempty →
        (∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) →
          (∀ U ∈ sets, 0 ∈ U) →
            (∀ U ∈ sets, ∃ V ∈ sets, V + V ⊆ U) →
              (∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x => -x) ⁻¹' U) → AddGroupFilterBasis G
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMkMor₂BicategoryM_1 : Mathlib.Tactic.BicategoryLike.MkMor₂ Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Order.Cover
WCovBy.Ioc_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → Set.Ioc a b ⊆ {b}
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.bddBelow_u_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {s : Set α}, BddBelow (u '' s) ↔ BddBelow s
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, Metric.eball x 0 = ∅
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The canonical map `Q →* D ≀ᵣ Q` sending `q` to `⟨1, q⟩`  -/
RegularWreathProduct.inl : {D : Type u_1} → {Q : Type u_2} → [inst : Group D] → [inst_1 : Group Q] → Q →* D ≀ᵣ Q
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The weak convergence of finite measures to a nonzero limit can be characterized by the weak
convergence of both their normalized versions (probability measures) and their total masses.  -/
MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
  [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.FiniteMeasure Ω},
  μ ≠ 0 →
    (Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize) ∧
        Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass) ↔
      Filter.Tendsto μs F (nhds μ))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α},
  (m₁ \ m₂).getKey! k = if k ∈ m₂ then default else m₁.getKey! k
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.Presentation.comp.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q Q_1 : Algebra.Presentation S T ι' σ'),
  Q = Q_1 →
    ∀ (P P_1 : Algebra.Presentation R S ι σ),
      P = P_1 → ∀ [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T], Q.comp P = Q_1.comp P_1
-- Mathlib.Data.List.DropRight
List.rdrop_append_of_le_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, ∀ k ≤ l₂.length, (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y Z : CategoryTheory.Over X),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z).left =
    CategoryTheory.ChosenPullbacksAlong.pullbackObj Y.hom Z.hom
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.append_left_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)),
  FreeGroup.Red.Step (L ++ L₁) (L ++ L₂) ↔ FreeGroup.Red.Step L₁ L₂
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.addNegClosureNhd.mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : AddGroup G],
  T ∈ nhds 0 → -T = T → IsOpen T → W + T ⊆ W → IsTopologicalAddGroup.addNegClosureNhd T W
-- Init.Data.Vector.Basic
Vector.instForMOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → {n : ℕ} → [Monad m] → ForM m (Vector α n) α
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instReprOfYear : {leap : Bool} → Repr (Std.Time.Day.Ordinal.OfYear leap)
-- Mathlib.Data.Set.NAry
Set.image2_singleton : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {a : α} {b : β}, Set.image2 f {a} {b} = {f a b}
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.induction_on : ∀ {α : Type u_1} {rels : Set (FreeGroup α)} {C : PresentedGroup rels → Prop} (x : PresentedGroup rels),
  (∀ (z : FreeGroup α), C ((PresentedGroup.mk rels) z)) → C x
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_eq_one_iff : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ},
  (ClassGroup.mk K) I = 1 ↔ (↑↑I).IsPrincipal
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_symm_apply_eq_bot : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : WithBot m.syn), m.toWithBotSyn.symm a = ⊥ ↔ a = ⊥
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_eq_zero : ∀ {r : NNReal}, ↑r = 0 ↔ r = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- A trivial vector bundle over a manifold is a `C^n` vector bundle.  -/
Bundle.Trivial.contMDiffVectorBundle : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F], ContMDiffVectorBundle n F (Bundle.Trivial B F) IB
-- Mathlib.Algebra.Lie.Ideal
LieHom.range_subset_idealRange : ∀ {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] (f : L →ₗ⁅R⁆ L'), ↑f.range ⊆ ↑f.idealRange
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instFinite : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M],
  Finite (LieModule.Weight R L M)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.instNormalId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G : C} [inst_2 : CategoryTheory.AddGrpObj G], CategoryTheory.IsAddMonHom.Normal (CategoryTheory.CategoryStruct.id G)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.equiv_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : BEq β]
  [LawfulBEq α] [LawfulBEq β], Std.DHashMap.Const.beq m₁ m₂ = true → m₁.Equiv m₂
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.toAddCommGroup : {R : Type u} → [self : AddCommGroupWithOne R] → AddCommGroup R
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.int_algebraMap_surjective : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsFractionRing R ℚ],
  Function.Surjective ⇑(algebraMap ℤ R)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.maximumClique_card_eq_cliqueNum : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] (s : Finset α), G.IsMaximumClique s → s.card = G.cliqueNum
-- Mathlib.Algebra.Group.Basic
vadd_dite : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd β α] (p : Prop) [inst_1 : Decidable p] (a : p → α) (b : ¬p → α) (c : β),
  (c +ᵥ if h : p then a h else b h) = if h : p then c +ᵥ a h else c +ᵥ b h
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.one_le_finrank_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f] (x : ↥X),
  1 ≤ AlgebraicGeometry.Scheme.Hom.finrank f (f x)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- In a Dedekind domain, any ideal is spanned by two elements, where one of the element
could be any fixed non-zero element in the ideal.  -/
IsDedekindDomain.exists_eq_span_pair : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {I : Ideal R} {x : R},
  x ∈ I → x ≠ 0 → ∃ y, I = Ideal.span {x, y}
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The fundamental groupoid of a space `X` is defined to be a wrapper around `X`, and we
subsequently put a `CategoryTheory.Groupoid` structure on it.  -/
FundamentalGroupoid : Type u_3 → Type u_3
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.restrict_comap : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure β) (s : Set α),
      (MeasureTheory.Measure.comap f μ).restrict s = MeasureTheory.Measure.comap f (μ.restrict (f '' s))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp t.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Topology.CompactOpen
ContinuousMap.instR0Space : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [R0Space Y], R0Space C(X, Y)
-- Mathlib.Topology.Constructible
Topology.IsConstructible.inter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Topology.IsConstructible s → Topology.IsConstructible t → Topology.IsConstructible (s ∩ t)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.natDegree_preHilbertPoly : ∀ (F : Type u_1) [inst : Field F] [CharZero F] (d k : ℕ), (Polynomial.preHilbertPoly F d k).natDegree = d
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.forM_eq_forMUncurried : ∀ {α : Type u} {m' : Type w → Type w'} {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [inst : Monad m']
  [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  Std.DHashMap.Raw.forM f m = Std.DHashMap.Raw.Const.forMUncurried (fun a => f a.1 a.2) m
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.card_nthRoots : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ} {ζ : R},
  IsPrimitiveRoot ζ n → ∀ (a : R), (Polynomial.nthRoots n a).card = if ∃ α, α ^ n = a then n else 0
-- Batteries.Lean.EStateM
EStateM.dummyRestore_apply : ∀ {σ : Type u_1} (s : σ), EStateM.dummyRestore s = Function.const PUnit.{u_2} s
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_le_const_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  (∃ C, ∀ (x : α), f x ≤ C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop
-- Init.Data.List.Sort.Lemmas
List.length_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} (l : List α), (l.mergeSort le).length = l.length
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.addZ P P = 0