mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty =
    ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty && (f (t.get? k)).isNone)
-- Mathlib.Algebra.Group.Defs
IsDedekindFiniteMonoid.mul_eq_one_symm : ∀ {M : Type u_2} {inst : MulOne M} [self : IsDedekindFiniteMonoid M] {a b : M}, a * b = 1 → b * a = 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.arrowCongr_apply : ∀ {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  {V₄ : Type u_9} [inst : AddCommGroup V₁] [inst_1 : AddCommGroup V₂] [inst_2 : AddCommGroup V₃]
  [inst_3 : AddCommGroup V₄] [inst_4 : AddTorsor V₁ P₁] [inst_5 : AddTorsor V₂ P₂] [inst_6 : AddTorsor V₃ P₃]
  [inst_7 : AddTorsor V₄ P₄] {R : Type u_10} [inst_8 : CommRing R] [inst_9 : Module R V₁] [inst_10 : Module R V₂]
  [inst_11 : Module R V₃] [inst_12 : Module R V₄] (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : P₃ ≃ᵃ[R] P₄) (f : P₁ →ᵃ[R] P₃) (x : P₂),
  ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [P.IsClosedUnderIsomorphisms]
  [∀ (a : α), P.IsClosedUnderColimitsOfShape (J a)], P.colimitsClosure J = P
-- Mathlib.Algebra.GCDMonoid.Basic
normalize.eq_1 : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α), normalize x = x * ↑(normUnit x)
-- Mathlib.Order.Interval.Set.Image
AntitoneOn.mapsTo_Icc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  AntitoneOn f (Set.Icc a b) → Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLEFunctor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncLE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.CategoryWithHomology C]
  {X Y : HomologicalComplex C c'} (φ : X ⟶ Y), (e.truncLEFunctor C).map φ = HomologicalComplex.truncLEMap φ e
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.mem_fieldRange : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {f : K →+* L} {y : L},
  y ∈ f.fieldRange ↔ ∃ x, f x = y
-- Mathlib.Order.Filter.Pointwise
Filter.mulAction.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : MulAction α β],
  Filter.mulAction = { toSMul := Filter.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Data.Nat.Factorization.PrimePow
exists_ordCompl_eq_one_iff_isPrimePow : ∀ {n : ℕ}, n ≠ 1 → (IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.Data.Set.Sups
Set.infs_union_left : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s₁ s₂ t : Set α}, (s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_add : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : FunLike F α β] [AddHomClass F α β] (f : F) {s t : Finset α} [inst_5 : DecidableEq β],
  Finset.image (⇑f) (s + t) = Finset.image (⇑f) s + Finset.image (⇑f) t
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_η_fst : ∀ {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] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.OplaxMonoidal],
  (CategoryTheory.Functor.OplaxMonoidal.η (F.prod' G)).1 = CategoryTheory.Functor.OplaxMonoidal.η F
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_notMem_affineSpan_pair : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i j : Fin (n + 1)), s.incenter ∉ line[ℝ, s.points i, s.points j]
-- Mathlib.Probability.Independence.Basic
/-- Two measurable space structures (or σ-algebras) `m₁, m₂` are independent with respect to a
measure `μ` (defined on a third σ-algebra) if for any sets `t₁ ∈ m₁, t₂ ∈ m₂`,
`μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)`  -/
ProbabilityTheory.Indep : {Ω : Type u_1} →
  MeasurableSpace Ω →
    MeasurableSpace Ω →
      {_mΩ : MeasurableSpace Ω} → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.Indep._auto_1 → Prop
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
lt_ciSup_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {a : α} [Nonempty ι] {f : ι → α},
  BddAbove (Set.range f) → (a < iSup f ↔ ∃ i, a < f i)
-- Std.Http.Data.Status
/-- A custom HTTP status with a numeric code and a reason phrase. Used to represent status codes
not enumerated as dedicated constructors in `Status`. The code must be in the range 100–999
(a three-digit integer per RFC 9112 §4) and must not correspond to any named constructor.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.CustomStatus : Type
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.cast_pos : ∀ {R : Type u_1} [inst : CommSemiring R] {a : R} {n : ℕ}, Mathlib.Meta.NormNum.IsNat a n → a = n.rawCast + 0
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The quadrant in `ℝ^n`, used to model manifolds with corners, made of all vectors with nonnegative
coordinates.
 -/
EuclideanQuadrant : ℕ → Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_insert_perm : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β}, (m.insert k v).toList.Perm ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) m.toList)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (le : startPos ≤ endPos),
  String.Slice.Pattern.Model.IsLongestRevMatch pat (endPos.sliceTo startPos le) →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos
-- Init.Data.Int.DivMod.Lemmas
Int.lt_ediv_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < c → c ∣ b → (a < b / c ↔ c * a < b)
-- Mathlib.Geometry.Manifold.Bordism
/-- The canonical singular manifold associated to the empty set (seen as a smooth manifold)  -/
SingularManifold.empty : (X : Type u_1) →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_4} →
        {H : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  (M : Type u) →
                    [inst_5 : TopologicalSpace M] →
                      [inst_6 : ChartedSpace H M] →
                        (I : ModelWithCorners ℝ E H) → [IsManifold I k M] → [IsEmpty M] → SingularManifold X k I
-- Mathlib.Algebra.Ring.Parity
Nat.even_or_odd' : ∀ (n : ℕ), ∃ k, n = 2 * k ∨ n = 2 * k + 1
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.truncate.eq_2 : ∀ {F : PFunctor.{uA, uB}} (a : ℕ) (i : F.A) (f : F.B i → PFunctor.Approx.CofixA F (a + 1)),
  PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro i f) =
    PFunctor.Approx.CofixA.intro i (PFunctor.Approx.truncate ∘ f)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- A group that is finite  -/
FiniteGrp.toGrp : FiniteGrp.{u} → GrpCat
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMulZeroClass : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [MulZeroClass Y] → MulZeroClass (LocallyConstant X Y)
-- Init.Data.Int.Order
Int.max_eq_right : ∀ {a b : ℤ}, a ≤ b → max a b = b
-- Mathlib.Algebra.Order.Module.Field
smul_inv_le_iff_of_neg : ∀ {𝕜 : Type u_1} {G : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G}
  [PosSMulMono 𝕜 G], a < 0 → (b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁)
-- Mathlib.SetTheory.Cardinal.Defs
/-- `lift.{max u v, u}` equals `lift.{v, u}`.

Unfortunately, the simp lemma doesn't work.  -/
Cardinal.lift_umax : Cardinal.lift.{max u v, u} = Cardinal.lift.{v, u}
-- Mathlib.Topology.Separation.Basic
isClosedEmbedding_update : ∀ {ι : Type u_3} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → TopologicalSpace (β i)]
  (x : (i : ι) → β i) (i : ι) [∀ (i : ι), T1Space (β i)], Topology.IsClosedEmbedding (Function.update x i)
-- Lean.Data.DeclarationRange
Lean.DeclarationRange.endPos : Lean.DeclarationRange → Lean.Position
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.TestHandler : Type
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) (x : α), (g.comp f) x = g (f x)
-- Aesop.Stats.Basic
Aesop.instToJsonGoalKind.toJson : Aesop.GoalKind → Lean.Json
-- Mathlib.Topology.CompactOpen
Filter.HasBasis.nhds_continuousMapConst : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {ι : Type u_6} {c : Y}
  {p : ι → Prop} {U : ι → Set Y},
  (nhds c).HasBasis p U →
    (nhds (ContinuousMap.const X c)).HasBasis (fun Ki => IsCompact Ki.1 ∧ p Ki.2) fun Ki =>
      {f | Set.MapsTo (⇑f) Ki.1 (U Ki.2)}
-- Mathlib.Data.Fintype.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons and pigeonholes.
This is the `Fintype` version of `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`.
 -/
Fintype.exists_ne_map_eq_of_card_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Fintype.card β < Fintype.card α → ∃ x y, x ≠ y ∧ f x = f y
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_toSignedMeasure : ∀ {X : Type u_2} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G]
  {μ : MeasureTheory.Measure X} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {f : X → G},
  ∫ᵛ (x : X), f x ∂<•μ.toSignedMeasure = ∫ (x : X), f x ∂μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.diseq_norm : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = true →
    Lean.Grind.CommRing.Expr.denote ctx lhs ≠ Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p ≠ 0
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.injective_noncommPiCoprod_of_iSupIndep : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → AddGroup (H i)]
  (ϕ : (i : ι) → H i →+ G) [inst_2 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)},
  (iSupIndep fun i => (ϕ i).range) →
    (∀ (i : ι), Function.Injective ⇑(ϕ i)) → Function.Injective ⇑(AddMonoidHom.noncommPiCoprod ϕ hcomm)
-- Init.Data.List.Nat.Perm
/-- Helper lemma for `set_set_perm` -/
_private.Init.Data.List.Nat.Perm.0.List.set_set_perm' : ∀ {α : Type u_1} {as : List α} {i j : ℕ} (h₁ : i < as.length) (h₂ : i + j < as.length),
  0 < j → ((as.set i as[i + j]).set (i + j) as[i]).Perm as
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- The object in the category of `R`-coalgebras associated to an `R`-coalgebra.  -/
CoalgCat.of : (R : Type u) →
  [inst : CommRing R] → (X : Type v) → [inst_1 : AddCommGroup X] → [inst_2 : Module R X] → [Coalgebra R X] → CoalgCat R
-- Mathlib.Algebra.Ring.Units
Units.instHasDistribNeg : {α : Type u} → [inst : Monoid α] → [HasDistribNeg α] → HasDistribNeg αˣ
-- Std.Data.TreeSet.Raw.Basic
/-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
 -/
Std.TreeSet.Raw.get : {α : Type u} → {cmp : α → α → Ordering} → (t : Std.TreeSet.Raw α cmp) → (a : α) → a ∈ t → α
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperSemilinearSet.union : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsProperSemilinearSet s₁ → IsProperSemilinearSet s₂ → IsProperSemilinearSet (s₁ ∪ s₂)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Ric α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Ric α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Init.Omega.Constraint
Lean.Omega.Constraint.not_sat'_of_isImpossible : ∀ {c : Lean.Omega.Constraint}, c.isImpossible = true → ∀ {x y : Lean.Omega.Coeffs}, ¬c.sat' x y = true
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `includeLeftSubRight R S` vanishes in the range of `algebraMap R S`.  -/
Algebra.TensorProduct.includeLeftSubRight_zero_of_mem_range : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S] {s : S},
  s ∈ Set.range ⇑(algebraMap R S) → (Algebra.TensorProduct.includeLeftSubRight R S) s = 0
-- Mathlib.Data.Complex.Basic
Complex.conj_im : ∀ (z : ℂ), ((starRingEnd ℂ) z).im = -z.im
-- Mathlib.Order.KrullDimension
Order.height_le_coe_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ}, Order.height x ≤ ↑n ↔ ∀ y < x, Order.height y < ↑n
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a co-Heyting homomorphism preserves the top element.  -/
CoheytingHomClass.map_top : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : CoheytingAlgebra α} {inst_1 : CoheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : CoheytingHomClass F α β] (f : F), f ⊤ = ⊤
-- Init.Data.Queue
/-- `O(1)`. Push an element on the front of the queue.  -/
Std.Queue.enqueue : {α : Type u} → α → Std.Queue α → Std.Queue α
-- Lean.Compiler.IR.Basic
Lean.IR.args.alphaEqv : Lean.IR.IndexRenaming → Array Lean.IR.Arg → Array Lean.IR.Arg → Bool
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.fin_omega_proc : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.Compact
/-- If the product of continuous functions on a compact space is zero, then the norm of their sum
is the maximum of their norms.  -/
ContinuousMap.norm_add_eq_max : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4}
  [inst_2 : NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : C(α, R)}, f * g = 0 → ‖f + g‖ = max ‖f‖ ‖g‖
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.mk : Lean.Meta.Sym.AlphaShareCommon.State →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId) →
    Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo) →
      Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr →
        Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Level →
          Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.CongrInfo →
            Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool →
              Array Lean.Meta.Sym.SymExtensionState →
                List Lean.MessageData →
                  Lean.Meta.Sym.Canon.State → Lean.PHashMap Lean.Expr Lean.Expr → Bool → Lean.Meta.Sym.State
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- If `0 < n`, then `xa i` has order 4.
 -/
QuaternionGroup.orderOf_xa : ∀ {n : ℕ} [NeZero n] (i : ZMod (2 * n)), orderOf (QuaternionGroup.xa i) = 4
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.range.congr_simp : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f f_1 : α → ZFSet.{u}), f = f_1 → ZFSet.range f = ZFSet.range f_1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.op_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.op.snd = c.inr.op
-- Mathlib.Order.MinMax
AntitoneOn.map_max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α} {a b : α},
  AntitoneOn f s → a ∈ s → b ∈ s → f (max a b) = min (f a) (f b)
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
/-- **Alias** of `MonoidHom.finsetProd_apply`.

---

See also `Finset.prod_apply`, with the same conclusion but with the weaker hypothesis
`f : α → M → N`  -/
MonoidHom.finset_prod_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : CommMonoid N] (f : ι → M →* N)
  (s : Finset ι) (b : M), (∏ x ∈ s, f x) b = ∏ x ∈ s, (f x) b
-- Lean.Meta.Tactic.Grind.Types
/-- `match` auxiliary functions whose equations have already been created and activated.  -/
Lean.Meta.Grind.EMatch.State.matchEqNames : Lean.Meta.Grind.EMatch.State → Lean.PHashSet Lean.Name
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.swap_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α (β × γ)},
  (ProbabilityTheory.Kernel.swap β γ).comp κ = κ.map Prod.swap
-- Mathlib.Data.PNat.Factors
instCanonicallyOrderedAddPrimeMultiset : CanonicallyOrderedAdd PrimeMultiset
-- Mathlib.Topology.Closure
interior_iInter₂_le_nat : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} (f : ℕ → Set X),
  interior (⋂ m, ⋂ (_ : m ≤ n), f m) = ⋂ m, ⋂ (_ : m ≤ n), interior (f m)
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.range_liftBaseChange : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] (l : M →ₗ[R] N),
  (LinearMap.liftBaseChange A l).range = Submodule.span A ↑l.range
-- Mathlib.Data.Seq.Defs
/-- It is decidable whether a sequence terminates at a given position.  -/
Stream'.Seq.terminatedAtDecidable : {α : Type u} → (s : Stream'.Seq α) → (n : ℕ) → Decidable (s.TerminatedAt n)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_equivProd_symm_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R), ((QuaternionAlgebra.equivProd c₁ c₂ c₃).symm a).imJ = a.2.2.1
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.compl_add : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [ContinuousMul α]
  {s : Set β}, Multipliable (f ∘ Subtype.val) → Multipliable (f ∘ Subtype.val) → Multipliable f
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.subsingleton_of_finrank_adjoin_le_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  (∀ (x : E), Module.finrank F ↥F⟮x⟯ ≤ 1) → Subsingleton (IntermediateField F E)
-- Mathlib.Data.Set.Lattice.Image
Set.biInter_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β},
  ⋂ x ∈ f '' s, g x = ⋂ y ∈ s, g (f y)
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.finrank_le_of_rank_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  Module.rank R M ≤ ↑n → Module.finrank R M ≤ n
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.abv_pos_of_not_limZero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : CauSeq β abv},
  ¬f.LimZero → ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (↑f j)
-- Init.Data.List.Find
List.finIdxOf?_eq_none_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, List.finIdxOf? a l = none ↔ a ∉ l
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_slice_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  p ≤ q.slice p₀ p₁ h₀ h₁ ↔ String.Slice.Pos.ofSlice p ≤ q
-- Aesop.Tree.Data
Aesop.MVarClusterData.parent? : {Goal Rapp : Type} → Aesop.MVarClusterData Goal Rapp → Option (IO.Ref Rapp)
-- Aesop.Forward.SlotIndex
Aesop.instDecidableEqSlotIndex : DecidableEq Aesop.SlotIndex
-- Mathlib.GroupTheory.Transfer
/-- Auxiliary lemma in order to state `transferSylow_eq_pow`.  -/
MonoidHom.transferSylow_eq_pow_aux : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G),
  Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P →
    ∀ [Fact (Nat.Prime p)] [Finite (Sylow p G)],
      ∀ g ∈ P, ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ P → g₀⁻¹ * g ^ k * g₀ = g ^ k
-- Mathlib.Order.Lattice
inf_right_le_sup_right : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, b ⊓ a ≤ b ⊔ c
-- Init.Grind.Lemmas
Lean.Grind.eqRec_heq : ∀ {α : Sort u_2} {a : α} {motive : (x : α) → a = x → Sort u_1} (v : motive a ⋯) {b : α} (h : a = b), h ▸ v ≍ v
-- Mathlib.MeasureTheory.Constructions.Pi
MeasurableEquiv.arrowProdEquivProdArrow.eq_1 : ∀ (α : Type u_8) (β : Type u_9) (γ : Type u_10) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  MeasurableEquiv.arrowProdEquivProdArrow α β γ =
    { toEquiv := Equiv.arrowProdEquivProdArrow γ (fun i => α) fun i => β, measurable_toFun := ⋯,
      measurable_invFun := ⋯ }
-- Mathlib.Algebra.Tropical.Basic
Tropical.instZeroTropical : {R : Type u} → [Top R] → Zero (Tropical R)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_6 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a : Lean.Grind.CommRing.Expr)
  (k : ℕ), Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.pow k) = Lean.Grind.CommRing.Expr.denoteSAsRing ctx a ^ k
-- Mathlib.Computability.Ackermann
ack_add_one_sq_lt_ack_add_three : ∀ (m n : ℕ), (ack m n + 1) ^ 2 ≤ ack (m + 3) n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams.fromJson : Lean.Json → Except String Lean.Lsp.CallHierarchyOutgoingCallsParams
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddMonoid.toContinuousENorm : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ESeminormedAddMonoid E] → ContinuousENorm E
-- Mathlib.Analysis.Seminorm
Seminorm.coe_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  (p q : Seminorm 𝕜 E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.separatingLeft_def : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0