mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core.injEq : ∀ (e : Lean.Expr) (lhs rhs : Lean.Grind.CommRing.Expr) (e_1 : Lean.Expr) (lhs_1 rhs_1 : Lean.Grind.CommRing.Expr),
  (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core e_1 lhs_1 rhs_1) =
    (e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.ofNat_log : ∀ {n : ℕ} [inst : n.AtLeastTwo], ↑(Real.log (OfNat.ofNat n)) = Complex.log (OfNat.ofNat n)
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.mk.injEq : ∀ (mvarId : Lean.MVarId) (elems diseqs : Array Lean.FVarId) (subst : Lean.Meta.FVarSubst) (mvarId_1 : Lean.MVarId)
  (elems_1 diseqs_1 : Array Lean.FVarId) (subst_1 : Lean.Meta.FVarSubst),
  ({ mvarId := mvarId, elems := elems, diseqs := diseqs, subst := subst } =
      { mvarId := mvarId_1, elems := elems_1, diseqs := diseqs_1, subst := subst_1 }) =
    (mvarId = mvarId_1 ∧ elems = elems_1 ∧ diseqs = diseqs_1 ∧ subst = subst_1)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Tag.mk.inj : ∀ {declName : Lean.Name} {database : Mathlib.CrossRef.Database} {tag comment : String} {declName_1 : Lean.Name}
  {database_1 : Mathlib.CrossRef.Database} {tag_1 comment_1 : String},
  { declName := declName, database := database, tag := tag, comment := comment } =
      { declName := declName_1, database := database_1, tag := tag_1, comment := comment_1 } →
    declName = declName_1 ∧ database = database_1 ∧ tag = tag_1 ∧ comment = comment_1
-- Mathlib.Algebra.Category.BoolRing
BoolRing.hom_ext : ∀ {R S : BoolRing} {f g : R ⟶ S}, BoolRing.Hom.hom f = BoolRing.Hom.hom g → f = g
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_union_eq_top_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
  μ (s ∪ t) = ⊤ ↔ μ s = ⊤ ∨ μ t = ⊤
-- Mathlib.Order.WithBot
/-- A universe-polymorphic version of `EquivFunctor.mapEquiv WithTop e`.  -/
Equiv.withTopCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → WithTop α ≃ WithTop β
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.ext : ∀ {V : Type u} {G : SimpleGraph V} {x y : G.Subgraph}, x.verts = y.verts → x.Adj = y.Adj → x = y
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.Small.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{w, v, u} Q], P ≤ Q → CategoryTheory.ObjectProperty.Small.{w, v, u} P
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.opEquivOpUnder_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T),
  (CategoryTheory.Over.opEquivOpUnder X).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun Y => CategoryTheory.Over.mk (Opposite.unop Y).hom.op,
            map := fun {Z Y} f => CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f.unop).op ⋯, map_id := ⋯,
            map_comp := ⋯ }.comp
        { obj := fun Y => Opposite.op (CategoryTheory.Under.mk Y.hom.unop),
          map := fun {Z Y} f => Opposite.op (CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f).unop ⋯),
          map_id := ⋯, map_comp := ⋯ })
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.Pairing.AncestralRel.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x y : ↑P.II), P.AncestralRel x y = (x ≠ y ∧ ↑x < ↑(P.p y))
-- Init.While
Lean.instForInLoopUnitOfMonad : {m : Type u → Type v} → [Monad m] → ForIn m Lean.Loop Unit
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.«tactic_clause(Rule_sets:=[_])» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Real
Real.nnnorm_two : ‖2‖₊ = 2
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- A `ProjectiveResolution Z` consists of a bundled `ℕ`-indexed chain complex of projective objects,
along with a quasi-isomorphism to the complex consisting of just `Z` supported in degree `0`.
 -/
CategoryTheory.ProjectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → Type (max u v)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f f_1 : P.X ⟶ Q.X) (e_f : f = f_1)
  (comm : CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f Q.p) = f),
  { f := f, comm := comm } = { f := f_1, comm := ⋯ }
-- Mathlib.Algebra.Free
FreeMagmaAssocQuotientEquiv.eq_1 : ∀ (α : Type u),
  FreeMagmaAssocQuotientEquiv α =
    (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).toMulEquiv
      (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of)) ⋯ ⋯
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.unop.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.unop = AddMonoidHom.op.symm
-- Mathlib.Data.DFinsupp.Defs
/-- The composition of `f : β₁ → β₂` and `g : Π₀ i, β₁ i` is
  `mapRange f hf g : Π₀ i, β₂ i`, well defined when `f 0 = 0`.

This preserves the structure on `f`, and exists in various bundled forms for when `f` is itself
bundled:

* `DFinsupp.mapRange.addMonoidHom`
* `DFinsupp.mapRange.addEquiv`
* `dfinsupp.mapRange.linearMap`
* `dfinsupp.mapRange.linearEquiv`
 -/
DFinsupp.mapRange : {ι : Type u} →
  {β₁ : ι → Type v₁} →
    {β₂ : ι → Type v₂} →
      [inst : (i : ι) → Zero (β₁ i)] →
        [inst_1 : (i : ι) → Zero (β₂ i)] →
          (f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i
-- Mathlib.Order.SymmDiff
bihimp_bihimp_bihimp_comm : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b c d : α),
  bihimp (bihimp a b) (bihimp c d) = bihimp (bihimp a c) (bihimp b d)
-- Init.Data.List.Erase
List.mem_of_mem_eraseIdx : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, a ∈ l.eraseIdx i → a ∈ l
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (i : ι), (∏ a, (P.RootForm (P.root a)) (P.root a)) • P.coroot i ∈ (P.Polarization.domRestrict (P.rootSpan R)).range
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The absolute error of the trapezoidal rule does not change when the endpoints are swapped.  -/
trapezoidal_error_symm : ∀ (f : ℝ → ℝ) {N : ℕ}, 0 < N → ∀ (a b : ℝ), trapezoidal_error f N a b = -trapezoidal_error f N b a
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (j : C), ((t.triangleω₁δ a b c hab hbc).obj j).obj₂ = (t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj j)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isLittleO_cobounded_of_degree_lt : ∀ {R : Type u_2} [inst : NormedRing R] [NormMulClass R] {P Q : Polynomial R},
  P.degree < Q.degree → (fun x => Polynomial.eval x P) =o[Bornology.cobounded R] fun x => Polynomial.eval x Q
-- Lean.Compiler.IR.Basic
Lean.IR.instReprParam.repr : Lean.IR.Param → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Complex.Module
Complex.mulAction : {R : Type u_1} → [inst : Monoid R] → [MulAction R ℝ] → MulAction R ℂ
-- Mathlib.Order.ConditionallyCompleteLattice.Group
add_ciSup_le : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : AddGroup α]
  [AddLeftMono α] {a g : α} {h : ι → α}, (∀ (j : ι), g + h j ≤ a) → g + iSup h ≤ a
-- Mathlib.Data.Set.Function
Set.SurjOn.inter_inter : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.SurjOn f s₁ t₁ → Set.SurjOn f s₂ t₂ → Set.InjOn f (s₁ ∪ s₂) → Set.SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofString.injEq : ∀ (s s_1 : String), (Lean.LeanOptionValue.ofString s = Lean.LeanOptionValue.ofString s_1) = (s = s_1)
-- Mathlib.Order.Fin.Basic
Fin.strictMono_castLE : ∀ {m n : ℕ} (h : n ≤ m), StrictMono (Fin.castLE h)
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.of_mul_left : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, (f * g).Separable → f.Separable
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldr_eq_foldr_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w} {f : α → δ → δ}
  {init : δ}, Std.DTreeMap.Raw.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.iterate : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α}, Measurable f → ∀ (n : ℕ), Measurable f^[n]
-- Mathlib.Dynamics.Transitive
IsOpen.dense_iUnion_preimage_smul : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [h : MulAction.IsTopologicallyTransitive M α] {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, (fun x => m • x) ⁻¹' U)
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.encard_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} [H.FiniteIndex],
  AddSubgroup.IsComplement S ↑H → S.encard = ↑H.index
-- Mathlib.Order.Hom.Basic
OrderIso.dualDual_apply : ∀ {α : Type u_2} [inst : LE α] (a : α), (OrderIso.dualDual α) a = OrderDual.toDual (OrderDual.toDual a)
-- Mathlib.GroupTheory.Commutator.Finite
/-- The commutator of a finite direct product is contained in the direct product of
the commutators.  -/
AddSubgroup.addCommutator_pi_pi_of_finite : ∀ {η : Type u_2} [Finite η] {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] (H K : (i : η) → AddSubgroup (Gs i)),
  ⁅AddSubgroup.pi Set.univ H, AddSubgroup.pi Set.univ K⁆ = AddSubgroup.pi Set.univ fun i => ⁅H i, K i⁆
-- Init.Data.Float.Float
/-- Computes the cube root of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`cbrt`.
 -/
Float.cbrt : Float → Float
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- In a complete space, the orthogonal complement of any submodule `K` is complete.  -/
Submodule.instOrthogonalCompleteSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [CompleteSpace E], CompleteSpace ↥Kᗮ
-- Mathlib.Data.Multiset.ZeroCons
Multiset.coe_eq_zero_iff_isEmpty : ∀ {α : Type u_1} (l : List α), ↑l = 0 ↔ l.isEmpty = true
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkNatIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (eₗ eₗ_1 : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G) (e_eₗ : eₗ = eₗ_1)
  (eᵣ eᵣ_1 : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G) (e_eᵣ : eᵣ = eᵣ_1)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
        ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G)),
  CategoryTheory.Join.mkNatIso eₗ eᵣ h = CategoryTheory.Join.mkNatIso eₗ_1 eᵣ_1 ⋯
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation.X : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)],
  (RatFunc.inftyValuation F) RatFunc.X = WithZero.exp 1
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqSimpCacheKey.beq : Lean.Elab.Tactic.Grind.SimpCacheKey → Lean.Elab.Tactic.Grind.SimpCacheKey → Bool
-- Mathlib.Algebra.Order.Group.Synonym
toLex_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : α), toLex (a - b) = toLex a - toLex b
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- Differentiability of `Θ z τ` in `τ`, for fixed `z`.  -/
differentiableAt_jacobiTheta₂_snd : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → DifferentiableAt ℂ (jacobiTheta₂ z) τ
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.withZeroUnitsEquiv_symm_apply : ∀ {G : Type u_4} [inst : GroupWithZero G] [inst_1 : DecidablePred fun a => a = 0] (a : G),
  WithZero.withZeroUnitsEquiv.symm a = if h : a = 0 then 0 else ↑(Units.mk0 a h)
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Formula.limplies_delete : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  {f : σ} {arr : Array ℕ},
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α f (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)
-- Mathlib.Tactic.CongrExclamation
/-- Accumulated goals that `congr!` could not handle.  -/
CongrState.goals : CongrState → Array Lean.MVarId
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instNoPrefixPatternModelForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.NoPrefixPatternModel p
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapAddEquiv.eq_1 : ∀ {R : Type u_3} {S : Type u_4} (M : Type u_6) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Add M] (e : R ≃+ S),
  AddMonoidAlgebra.mapAddEquiv M e =
    { toFun := AddMonoidAlgebra.map ↑e, invFun := AddMonoidAlgebra.map ↑e.symm, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of the 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Atom₁.src : Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.BicategoryLike.Obj
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.comp_left : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.CosimplicialObject.Augmented C}
  (a : X ⟶ Y) (a_1 : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp a a_1).left = CategoryTheory.CategoryStruct.comp a.left a_1.left
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
le_nonZeroDivisors_of_noZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [NoZeroDivisors M₀] {S : Submonoid M₀}, 0 ∉ S → S ≤ nonZeroDivisors M₀
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.tensorμ_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C]
  [inst_3 : P.IsStableUnderBraiding] (X Y Z T : CategoryTheory.WideSubcategory P),
  (CategoryTheory.MonoidalCategory.tensorμ X Y Z T).hom =
    CategoryTheory.MonoidalCategory.tensorμ X.obj Y.obj Z.obj T.obj
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_map : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → J)
  (g : J → M), Convexity.iConvexComb (Convexity.StdSimplex.map f s) g = Convexity.iConvexComb s fun i => g (f i)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.uniqueOfLeft : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → [Subsingleton M₁] → Unique (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedOrigin : Inhabited Mathlib.Meta.FunProp.Origin
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.contains a = false
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceOr : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.Associative.mk : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c],
  (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))) →
    (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
        c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) →
      (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
          c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
            c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) →
        (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
            c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)) →
          c₁.Associative c₂ c₃ c₁₂ c₂₃ c
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSlice.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → ℕ → List α → Sort u_2) (x x_1 : ℕ) (h_1 : (x x_2 : ℕ) → motive x x_2 [])
  (h_2 : (m : ℕ) → (xs : List α) → motive 0 m xs)
  (h_3 : (n m : ℕ) → (x : α) → (xs : List α) → motive n.succ m (x :: xs)),
  (match x, x_1, [] with
    | x, x_2, [] => h_1 x x_2
    | 0, m, xs => h_2 m xs
    | n.succ, m, x :: xs => h_3 n m x xs) =
    h_1 x x_1
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofNatList.congr_simp : ∀ (l l_1 : List ℕ) (e_l : l = l_1) (h : ∀ p ∈ l, Nat.Prime p),
  PrimeMultiset.ofNatList l h = PrimeMultiset.ofNatList l_1 ⋯
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_sub_st : ∀ {x : ℝ*}, ¬x.Infinite → (x - ↑x.st).Infinitesimal
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C),
  CategoryTheory.Grothendieck.ι F c =
    { obj := fun d => { base := c, fiber := d },
      map := fun {X Y} f =>
        { base := CategoryTheory.CategoryStruct.id { base := c, fiber := X }.base,
          fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_mul_right : ∀ {a b : Ordinal.{u_4}}, 0 < a → Order.IsSuccLimit b → Order.IsSuccLimit (a * b)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.sSup_lt_of_lt_cof : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}},
  Cardinal.mk ↑s < (Ordinal.lift.{u + 1, u} a).cof → (∀ i ∈ s, i < a) → sSup s < a
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries_mono : ∀ (G : Type u_1) [inst : AddGroup G], Monotone (AddSubgroup.upperCentralSeries G)
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_filter_le_vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f₁ f₂ : Filter β} {a : α}, f₁ ≤ f₂ → a +ᵥ f₁ ≤ a +ᵥ f₂
-- Mathlib.Algebra.Order.Ring.Abs
self_dvd_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a : α), a ∣ |a|
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atTop_basis_Ioi' : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [NoMaxOrder α] (a : α),
  Filter.atTop.HasBasis (fun x => a < x) Set.Ioi
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_sub_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Sub α] (s : ι → Set α) (t : Set α), (⋂ i, s i) - t ⊆ ⋂ i, s i - t
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Complex.exp` is complex analytic.  -/
analyticOnNhd_cexp : AnalyticOnNhd ℂ Complex.exp Set.univ
-- Init.System.IO
EIO.map : {α β ε : Type} → (α → β) → EIO ε α → EIO ε β
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat.div_pow : ∀ {p a b : ℕ} [hp : Fact (Nat.Prime p)], p ^ a ∣ b → padicValNat p (b / p ^ a) = padicValNat p b - a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.homEquiv_symm_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G}
  (f : A.ρ.IntertwiningMap B.ρ), Rep.homEquiv.symm f = Rep.ofHom f
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- A choice of a `OneHypercoverDenseData` structure when `F` is `1`-hypercover dense.  -/
CategoryTheory.Functor.oneHypercoverDenseData : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor C₀ C) →
          (J₀ : CategoryTheory.GrothendieckTopology C₀) →
            (J : CategoryTheory.GrothendieckTopology C) →
              [F.IsOneHypercoverDense J₀ J] → (X : C) → F.OneHypercoverDenseData J₀ J X
-- Lean.Meta.Sym.SymM
/-- Readonly context for the symbolic computation framework.  -/
Lean.Meta.Sym.Context : Type
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.justLoogleCmdImpl : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instHasFiniteLimits : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteLimits (HomologicalComplex C c)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copyBase_E : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E)
  (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B), (M.copyBase E IsBase hE h).E = E
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.mem_vonNeumann_succ : ∀ (x : ZFSet.{u_1}), x ∈ ZFSet.vonNeumann (Order.succ x.rank)
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.comp_convMul_distrib : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Semiring C] [inst_4 : Bialgebra R C] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (h : A →ₐ[R] B) (f g : WithConv (C →ₐ[R] A)),
  h.comp (f * g).ofConv = (WithConv.toConv (h.comp f.ofConv) * WithConv.toConv (h.comp g.ofConv)).ofConv
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.brecOn_1.go : {motive_1 : Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} →
  {motive_2 : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} →
    (t : List Lean.Elab.Tactic.RCases.RCasesPatt) →
      ((t : Lean.Elab.Tactic.RCases.RCasesPatt) → t.below → motive_1 t) →
        ((t : List Lean.Elab.Tactic.RCases.RCasesPatt) → Lean.Elab.Tactic.RCases.RCasesPatt.below_1 t → motive_2 t) →
          motive_2 t ×' Lean.Elab.Tactic.RCases.RCasesPatt.below_1 t