mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Triangle diagrams for (left) lifts.
```
            b
          ◹ |
   lift /   |      △
      /     | f    | unit
    /       ▽
  c - - - ▷ a
       g
```
 -/
CategoryTheory.Bicategory.LeftLift : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (b ⟶ a) → (c ⟶ a) → Type (max v w)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool}, (Std.ExtTreeMap.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = true
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E}
  (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F), UniqueDiffWithinAt 𝕜 s x → extDerivWithin (c • ω) s x = c • extDerivWithin ω s x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_fst_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).fst.obj X_1 = (J.obj X_1).fst
-- Mathlib.Data.List.Infix
List.map_reverse_tails : ∀ {α : Type u_1} (l : List α), List.map List.reverse l.tails = l.reverse.inits.reverse
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) (φ : P.cocomplex ⟶ Q.cocomplex),
  CategoryTheory.CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {Z : D}
      (h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj Q.cocomplex).cycles 0 ⟶ Z),
      CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (Q.toRightDerivedZero' F) h) =
        CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F)
          (CategoryTheory.CategoryStruct.comp
            (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0) h)
-- Mathlib.Logic.Unique
PUnit.instUnique : Unique PUnit.{u}
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_top' : ∀ {a : ENNReal}, a * ⊤ = if a = 0 then 0 else ⊤
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_add : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : FreeAddGroup α),
  (x + y).toWord = FreeAddGroup.reduce (x.toWord ++ y.toWord)
-- Mathlib.Geometry.Manifold.ConformalGroupoid
/-- The pregroupoid of conformal maps.  -/
conformalPregroupoid : {X : Type u_1} → [inst : NormedAddCommGroup X] → [NormedSpace ℝ X] → Pregroupoid X
-- Mathlib.Algebra.Ring.Submonoid.Basic
/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
additive closure of `M`.  -/
MulMemClass.mul_mem_add_closure : ∀ {M : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R] [MulMemClass M R] {S : M}
  {a b : R}, a ∈ AddSubmonoid.closure ↑S → b ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
-- Init.Data.List.MinMaxOn
List.minOn_eq_head : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []), (∀ x ∈ xs, f (xs.head h) ≤ f x) → List.minOn f xs h = xs.head h
-- Mathlib.FieldTheory.Normal.Defs
Normal.algHomEquivAut_symm_apply : ∀ (F : Type u_1) [inst : Field F] (K₁ : Type u_3) [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra E K₁] [inst_6 : IsScalarTower F E K₁]
  [inst_7 : Normal F E] (σ : Gal(E/F)), (Normal.algHomEquivAut F K₁ E).symm σ = (IsScalarTower.toAlgHom F E K₁).comp ↑σ
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_eq : ∀ {a b : ℝ} (x : ↑(Set.Icc a b)) (t : ↑unitInterval), Set.Icc.convexComb x x t = x
-- Mathlib.Order.Atoms
/-- A complemented modular atomic lattice is strongly atomic.
Not an instance to prevent loops.  -/
ComplementedLattice.isStronglyAtomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α] [IsAtomic α],
  IsStronglyAtomic α
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k' (Std.Internal.List.Const.alterKey k f l) =
      if (k == k') = true then (f (Std.Internal.List.getValue? k l)).isSome else Std.Internal.List.containsKey k' l
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_eq_restrict_sUnion : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  {f g : UniformOnFun α β 𝔖},
  edist f g =
    edist (UniformFun.ofFun ((⋃₀ 𝔖).domRestrict ((UniformOnFun.toFun 𝔖) f)))
      (UniformFun.ofFun ((⋃₀ 𝔖).domRestrict ((UniformOnFun.toFun 𝔖) g)))
-- Lean.Environment
/-- `.ir.sig` (optional) + `.ir` (optional).  -/
_private.Lean.Environment.0.Lean.ImportedModule.irParts : Lean.ImportedModule✝ → Array (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q U : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (f : P ⟶ Q) (g : Q ⟶ U),
  (x.map f).map g = x.map (CategoryTheory.CategoryStruct.comp f g)
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.pu64 : Std.Internal.Parsec.ByteArray.Parser UInt64
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
CategoryTheory.CommSq.leftAdjointLiftStructEquiv.eq_1 : ∀ {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] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : B ⟶ A} {p : Y ⟶ X} {u : X ⟶ G.obj A} {v : Y ⟶ G.obj B}
  (sq : CategoryTheory.CommSq v p (G.map i) u) (adj : F ⊣ G),
  sq.leftAdjointLiftStructEquiv adj =
    { toFun := fun l => { l := (adj.homEquiv' B X) l.l, fac_left := ⋯, fac_right := ⋯ },
      invFun := fun l => { l := (adj.homEquiv' B X).symm l.l, fac_left := ⋯, fac_right := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.range_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M), (Fintype.linearCombination R v).range = Submodule.span R (Set.range v)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_smul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : HNNExtension G A B φ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.ReducedWord.prod φ (g • w).toReducedWord =
    g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f g : α → ENNReal},
  Measurable f →
    Measurable g →
      ∀ {s : Set α}, MeasurableSet s → ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
-- Mathlib.Topology.Defs.Induced
/-- The range of a closed embedding is a closed set.  -/
Topology.IsClosedEmbedding.isClosed_range : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → IsClosed (Set.range f)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_apply_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (a : A), e.symm (e a) = a
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.iSup_le_sum : ∀ {ι : Type u_1} (f : ι → Cardinal.{max u_1 u_2}), iSup f ≤ Cardinal.sum f
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Have.replace : ∀ {σs : List (Type u)} {P H H' PH PH' T : Std.Do.SPred σs},
  (PH ⊣⊢ₛ P ∧ H) → (P ∧ H' ⊣⊢ₛ PH') → (PH ⊢ₛ H') → (PH' ⊢ₛ T) → PH ⊢ₛ T
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.seq : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Monad m] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  {α β : Type u} {pre : Pred} {post : β → Pred} {epost : EPred} [LawfulMonad m] (x : m (α → β)) (y : m α),
  ⦃ pre ⦄ x ⦃ fun f => Std.Internal.Do.wp y (fun a => post (f a)) epost; epost ⦄ → ⦃ pre ⦄ x <*> y ⦃ post; epost ⦄
-- Mathlib.Computability.Ackermann
not_nat_primrec_ack_self : ¬Nat.Primrec fun n => ack n n
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddGrpCat.μ_forget_apply : ∀ {G H : AddGrpCat} (p : ↑G) (q : ↑H),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddGrpCat) G H))
      (p, q) =
    (p, q)
-- Init.Data.Order.Ord
Int.instLawfulEqOrd : Std.LawfulEqOrd ℤ
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.get?.match_1.eq_1 : ∀ {α : Type u_1} {δ : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => δ) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : δ) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => δ) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r => h_2 size k' v' l r) =
    h_1 ()
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.snd = κ.map Prod.snd
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurve.continuous : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v → Continuous γ
-- Mathlib.MeasureTheory.Group.Arithmetic
aemeasurable_const_smul_iff : ∀ {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  {μ : MeasureTheory.Measure α} {G : Type u_7} [inst_2 : Group G] [inst_3 : MulAction G β] [MeasurableConstSMul G β]
  (c : G), AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ
-- Init.Data.SInt.Lemmas
Int8.neg_mul : ∀ (a b : Int8), -a * b = -(a * b)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.updateAlt! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Alt pu →
    Array (Lean.Compiler.LCNF.Param pu) → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Alt pu
-- Lean.Exception
/-- Throw an error exception with the specified name, with position information from `getRef`.

Note: Use the macro `throwNamedError`, which validates error names, instead of calling this function
directly.
 -/
Lean.throwNamedError : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.Name → Lean.MessageData → m α
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g}
  (hc : CategoryTheory.Limits.IsColimit c),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ∀ (x₁ : X₁) (x₂ : X₂),
      (CategoryTheory.ConcreteCategory.hom c.inl) x₁ = (CategoryTheory.ConcreteCategory.hom c.inr) x₂ ↔
        ∃ s, (CategoryTheory.ConcreteCategory.hom f) s = x₁ ∧ (CategoryTheory.ConcreteCategory.hom g) s = x₂
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
/-- The adjunction in the bicategorical sense attached to an adjunction between functors.  -/
CategoryTheory.Adjunction.toCat : {C D : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      {F : CategoryTheory.Functor C D} →
        {G : CategoryTheory.Functor D C} → (F ⊣ G) → CategoryTheory.Bicategory.Adjunction F.toCatHom G.toCatHom
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncTotal : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R)
  {x : σ →₀ ℕ}, Finsupp.degree x < n → MvPolynomial.coeff x ((MvPowerSeries.truncTotal n) p) = (MvPowerSeries.coeff x) p
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape : ∀ (C : Type u₁) {inst : CategoryTheory.Category.{v₁, u₁} C} (κ : Cardinal.{w}) {inst_1 : Fact κ.IsRegular}
  [self : CategoryTheory.HasCardinalFilteredColimits C κ] (J : Type w) [inst_2 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsCardinalFiltered J κ], CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.support_C_mul_X_pow_subset`. -/
Polynomial.support_C_mul_X_pow' : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (c : R), (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
-- Init.Data.UInt.Bitwise
USize.toUInt64_shiftLeft_of_lt : ∀ (a b : USize),
  b.toNat < System.Platform.numBits → (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % UInt64.ofNat USize.size
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RioSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instIsScalarTower : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K γ]
  [inst_2 : SMul γ β] [inst_3 : SMul K β] [IsScalarTower K γ β], IsScalarTower K γ (MeasureTheory.SimpleFunc α β)
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.mapₐ.congr_simp : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A) [inst_5 : I.IsPrime] (J : Ideal B) [inst_6 : J.IsPrime]
  (f f_1 : A →ₐ[R] B) (e_f : f = f_1) (hf : I = Ideal.comap f.toRingHom J),
  Ideal.ResidueField.mapₐ I J f hf = Ideal.ResidueField.mapₐ I J f_1 ⋯
-- Mathlib.RingTheory.Kaehler.Basic
instModuleTensorProductKaehlerDifferential : (R : Type u_2) →
  (S : Type u_1) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Module (TensorProduct R S S) Ω[S⁄R]
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Iio_sub_Iio : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Iio b) μ →
    a ≤ b → ∫ (x : ℝ) in Set.Iio b, f x ∂μ - ∫ (x : ℝ) in Set.Iio a, f x ∂μ = ∫ (x : ℝ) in Set.Ico a b, f x ∂μ
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.mkStateOfTable : {γ : Type} → Lean.KeyedDeclsAttribute.Table γ → Lean.KeyedDeclsAttribute.ExtensionState γ
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context : Type
-- Lean.Server.Completion.EligibleHeaderDecls
/-- Checks whether this declaration can appear in completion results.  -/
Lean.Server.Completion.allowCompletion : Lean.Server.Completion.EligibleHeaderDecls → Lean.Environment → Lean.Name → Bool
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup.eq_2 : ∀ (x : Lean.Grind.AC.Var) (s_2 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s_2).eraseDup =
    match s_2.eraseDup with
    | Lean.Grind.AC.Seq.var y =>
      if Nat.beq x y = true then Lean.Grind.AC.Seq.var x else Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)
    | Lean.Grind.AC.Seq.cons y s' =>
      if Nat.beq x y = true then Lean.Grind.AC.Seq.cons y s' else Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s')
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.sup_toAddSubmonoid : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M), (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rco_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...n).toArray[i]! = 0 ↔ (n - m).toNat ≤ i ∨ m + ↑i = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.top_isNormal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C], ⊤.IsNormal
-- Mathlib.GroupTheory.RegularWreathProduct
/-- Define an isomorphism from `D₁ ≀ᵣ Q₁` to `D₂ ≀ᵣ Q₂`
given isomorphisms `D₁ ≀ᵣ Q₁` and `Q₁ ≃* Q₂`.  -/
RegularWreathProduct.congr : {D₁ : Type u_3} →
  {Q₁ : Type u_4} →
    {D₂ : Type u_5} →
      {Q₂ : Type u_6} →
        [inst : Group D₁] →
          [inst_1 : Group Q₁] → [inst_2 : Group D₂] → [inst_3 : Group Q₂] → D₁ ≃* D₂ → Q₁ ≃* Q₂ → D₁ ≀ᵣ Q₁ ≃* D₂ ≀ᵣ Q₂
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivWithinAt_iff_isLittleO`. -/
HasDerivWithinAt.isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → (fun x' => f x' - f x - (x' - x) • f') =o[nhdsWithin x s] fun x' => x' - x
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOnFunc.eq_1 : ∀ (α : Type u'), FirstOrder.Language.constantsOnFunc α 0 = α
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.revMatchesAt_iff_splits : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits (t₁ ++ pat.copy) t₂
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_sub : ∀ (a b : UInt8), (a - b).toUInt16 = (a.toUInt16 - b.toUInt16) % 256
-- Mathlib.Algebra.Group.Action.Defs
Add.toVAddAddOpposite.eq_1 : ∀ (α : Type u_9) [inst : Add α], Add.toVAddAddOpposite α = { vadd := fun a b => b + AddOpposite.unop a }
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumUniformly_iff_tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasSumUniformly f g ↔ TendstoUniformly (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_div_coe_angle : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → ↑(x / y).arg = ↑x.arg - ↑y.arg
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.epi_f_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → (CategoryTheory.Epi S.f ↔ S.g = 0)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.restrictScalars.eq_1 : ∀ (𝕜 : Type u) {𝕜' : Type u'} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : Semiring 𝕜'] [inst_12 : SMul 𝕜 𝕜'] [inst_13 : Module 𝕜' E]
  [inst_14 : ContinuousConstSMul 𝕜' E] [inst_15 : IsScalarTower 𝕜 𝕜' E] [inst_16 : Module 𝕜' F]
  [inst_17 : ContinuousConstSMul 𝕜' F] [inst_18 : IsScalarTower 𝕜 𝕜' F] (p : FormalMultilinearSeries 𝕜' E F) (n : ℕ),
  FormalMultilinearSeries.restrictScalars 𝕜 p n = ContinuousMultilinearMap.restrictScalars 𝕜 (p n)
-- Mathlib.RingTheory.Ideal.Maximal
/-- Krull's theorem: a nontrivial ring has a maximal ideal.  -/
Ideal.exists_maximal : ∀ (α : Type u) [inst : Semiring α] [Nontrivial α], ∃ M, M.IsMaximal
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_prod_le : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
  (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree
-- Mathlib.Order.Filter.SmallSets
Filter.eventually_smallSets_subset : ∀ {α : Type u_1} {l : Filter α} {s : Set α}, (∀ᶠ (t : Set α) in l.smallSets, t ⊆ s) ↔ s ∈ l
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAtFilter.const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasDerivAtFilter f f' L → HasDerivAtFilter (c • f) (c • f') L
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_isIso : ∀ {Y Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [CategoryTheory.IsIso g], AlgebraicGeometry.IsOpenImmersion g
-- Mathlib.RingTheory.Smooth.Kaehler
retractionOfSectionOfKerSqZero_tmul_D : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S] (g : S →ₐ[R] P)
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) (s : S)
  (t : P),
  ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (KaehlerDifferential.D R P) t)) =
    g s * t - g s * g ((algebraMap P S) t)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_mul_monomial' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R),
  MvPolynomial.coeff m (p * (MvPolynomial.monomial s) r) = if s ≤ m then MvPolynomial.coeff (m - s) p * r else 0
-- Init.Data.ByteArray.Lemmas
ByteArray.size_empty : ByteArray.empty.size = 0
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.finsetIntegerMultiple_image : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] [inst_4 : DecidableEq R] (s : Finset S),
  ⇑(algebraMap R S) '' ↑(IsLocalization.finsetIntegerMultiple M s) = IsLocalization.commonDenomOfFinset M s • ↑s
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.comap_uniformity_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
-- Mathlib.Algebra.Ring.Rat
Rat.divInt_pow : ∀ (num : ℕ) (den : ℤ) (n : ℕ), Rat.divInt (↑num) den ^ n = Rat.divInt (↑num ^ n) (den ^ n)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.lhs : (self : Std.Tactic.BVDecide.BVPred.ExprPair) → Std.Tactic.BVDecide.BVExpr self.w