mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Bool
Bool.decide_beq_decide : ∀ (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q], (decide p == decide q) = decide (p ↔ q)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofiltered_of_directed_ge_nonempty : ∀ (α : Type u) [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α], CategoryTheory.IsCofiltered α
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.centroidWeightsWithCircumcenter.eq_1 : ∀ {n : ℕ} (fs : Finset (Fin (n + 1))) (a : Fin (n + 1)),
  Affine.Simplex.centroidWeightsWithCircumcenter fs (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) =
    if a ∈ fs then (↑fs.card)⁻¹ else 0
-- Init.Data.Vector.Lemmas
Vector.all_congr : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n},
  xs = ys → ∀ {p q : α → Bool}, (∀ (a : α), p a = q a) → xs.all p = ys.all q
-- Mathlib.GroupTheory.Nilpotent
Subgroup.IsAscendingCentralSeries.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsAscendingCentralSeries H = (H 0 = ⊥ ∧ ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_add_eq_iff_add_mul_eq_mul : ∀ {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] {x : R} {y : ↥M} {z₁ z₂ : S},
  IsLocalization.mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.continue.inj : ∀ {e? e?_1 : Option Lean.Meta.Simp.Result},
  Lean.Meta.Simp.Step.continue e? = Lean.Meta.Simp.Step.continue e?_1 → e? = e?_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₁ : ∀ {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) (n : ℤ) (j : C), ((t.triangleLEGT n).obj j).mor₁ = (t.truncLEι n).app j
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.exists_realize_equivSentence_iff_realize_exClosure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [inst_1 : DecidableEq α] [Nonempty M]
  {φ : L.Formula α}, (∃ v, M ⊨ FirstOrder.Language.Formula.equivSentence φ) ↔ M ⊨ φ.exClosure
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalFVarId : Lean.Meta.ReduceEval Lean.FVarId
-- Mathlib.Data.Nat.Digits.Lemmas
List.sum_fixedLengthDigits_sum : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ), ∑ L ∈ List.fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_compl : ∀ {α : Type u_1} (s : Set α), Subtype.val ⁻¹' sᶜ = ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
/-- The isomorphism `X.functorN' ≅ X.functorN` for a nonsingular simplicial set `X`.  -/
SSet.functorN'Iso : (X : SSet) → [inst : X.Nonsingular] → X.functorN' ≅ X.functorN
-- Lean.Server.Requests
Lean.Server.RequestM.bindTaskCheap : {α : Type u_1} →
  {β : Type} →
    Lean.Server.ServerTask α →
      (α → Lean.Server.RequestM (Lean.Server.RequestTask β)) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.Logic.Embedding.Basic
Subtype.impEmbedding.congr_simp : ∀ {α : Type u_1} (p q : α → Prop) (h : ∀ (x : α), p x → q x), Subtype.impEmbedding p q h = Subtype.impEmbedding p q h
-- Mathlib.Order.Category.HeytAlg
HeytAlg.mk.inj : ∀ {carrier : Type u_1} {str : HeytingAlgebra carrier} {carrier_1 : Type u_1} {str_1 : HeytingAlgebra carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertMany_ind : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  {motive : (Std.DHashMap.Raw α fun x => β) → Prop} (m : Std.DHashMap.Raw α fun x => β) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Raw α fun x => β) (a : α) (b : β), motive m → motive (m.insert a b)) →
      motive (Std.DHashMap.Raw.Const.insertMany m l)
-- Mathlib.Topology.AlexandrovDiscrete
isClosed_iUnion₂ : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsClosed (f i j)) → IsClosed (⋃ i, ⋃ j, f i j)
-- Mathlib.Geometry.Euclidean.SignedDist
abs_signedDist_eq_dist_iff_vsub_mem_span : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), |((signedDist v) p) q| = dist p q ↔ q -ᵥ p ∈ ℝ ∙ v
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.functorPushforward (CategoryTheory.Functor.id C) R = R
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instSemiring : {R : Type u_1} → [Semiring R] → Semiring Rᵒᵈ
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The homomorphism from `IteratedWreathProduct G n` to `Perm (Fin n → G)`.  -/
iteratedWreathToPermHom : (G : Type u_3) → [inst : Group G] → (n : ℕ) → IteratedWreathProduct G n →* Equiv.Perm (Fin n → G)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_monomial : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) {n : ℕ}
  {r : R}, (Polynomial.aeval x) ((Polynomial.monomial n) r) = (algebraMap R A) r * x ^ n
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.mk : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [toIsOrderedMonoid : IsOrderedMonoid α],
  (∀ (a b c : α), a * b ≤ a * c → b ≤ c) → (∀ (a b c : α), b * a ≤ c * a → b ≤ c) → IsOrderedCancelMonoid α
-- Mathlib.Topology.WithTopology
WithTopology.instMax.eq_1 : ∀ {X : Type u_1} (t : TopologicalSpace X) [inst : Max X],
  WithTopology.instMax t = { max := fun x y => WithTopology.toTopology t (x.ofTopology ⊔ y.ofTopology) }
-- Mathlib.Tactic.MoveAdd
/-- `moveOperSimpCtx` is the `Simp.Context` for the reordering internal to `move_oper`.
To support a new binary operation, extend the list in this definition, so that it contains
enough lemmas to allow `simp` to close a generic permutation goal for the new binary operation.
 -/
Mathlib.MoveAdd.moveOperSimpCtx : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFaithfulUnderUnderForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T)
  [inst_1 : Q.IsMultiplicative], (CategoryTheory.MorphismProperty.Under.forget P Q X).Faithful
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurableSet_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → (MeasurableSet (f '' s) ↔ MeasurableSet s)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.shearAddRight_symm_coe : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  ⇑(Homeomorph.shearAddRight G).symm = fun z => (z.1, -z.1 + z.2)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.neg_of : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Neg A] (f : Matrix m n A),
  -CStarMatrix.ofMatrix f = CStarMatrix.ofMatrix (-f)
-- Mathlib.Topology.Constructions
isOpen_pi_iff' : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [Finite ι] {s : Set ((a : ι) → A a)},
  IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ Set.univ.pi u ⊆ s
-- Mathlib.MeasureTheory.Measure.AddContent
/-- Extend a content over `C` to the finite unions of elements of `C` by additivity.  -/
MeasureTheory.AddContent.supClosure : {α : Type u_1} →
  {C : Set (Set α)} →
    {G : Type u_2} →
      [inst : AddCommMonoid G] →
        MeasureTheory.AddContent G C → MeasureTheory.IsSetSemiring C → MeasureTheory.AddContent G (supClosure C)
-- Init.Data.String.OrderInstances
String.Pos.instLTCoOfNatIntHAddCastUtf8ByteSize : ∀ {s : String}, Lean.Grind.ToInt.LT s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))
-- Mathlib.GroupTheory.FreeGroup.Orbit
/-- All elements of the free Group that start with a certain letter.
 -/
FreeGroup.startsWith : {α : Type u_1} → [DecidableEq α] → α × Bool → Set (FreeGroup α)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHomClass.toMonoidHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : MulZeroOneClass α}
  {inst_1 : MulZeroOneClass β} {inst_2 : FunLike F α β} [self : MonoidWithZeroHomClass F α β], MonoidHomClass F α β
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constOfArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {a : Array (α × β)},
  (Std.DTreeMap.Raw.Const.ofArray a cmp).WF
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.anyMUnsafe.any : {α : Type u} → {m : Type → Type w} → [Monad m] → (α → m Bool) → Array α → USize → USize → m Bool
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- `FintypeCat.toLightProfinite` is fully faithful.  -/
FintypeCat.toLightProfiniteFullyFaithful : FintypeCat.toLightProfinite.FullyFaithful
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.isoMk_hom_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {x y : CategoryTheory.Core C} (e : x.of ≅ y.of),
  (CategoryTheory.Core.isoMk e).hom.iso = e
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The line derivative in direction `m` of the Fourier transform is given by the Fourier transform
of the multiplication with `-(2 * π * Complex.I) • (inner ℝ · m)`.  -/
SchwartzMap.lineDerivOp_fourier_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  (f : SchwartzMap V E) (m : V),
  LineDeriv.lineDerivOp m (FourierTransform.fourier f) =
    FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulLeftCLM E fun x => inner ℝ x m) f)
-- Mathlib.Data.Nat.Find
/-- Find the smallest `n` satisfying `p n`. Returns a subtype.  -/
Nat.findX : {p : ℕ → Prop} → [DecidablePred p] → (∃ n, p n) → { n // p n ∧ ∀ m < n, ¬p m }
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_singleton : ∀ {α : Type u_1} {P : α → Prop} {x : α}, Ordnode.All P {x} ↔ P x
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.isZero_extend_X' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι'),
  e.r i' = none → CategoryTheory.Limits.IsZero ((K.extend e).X i')
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.vec : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {len : ℕ} → Std.Sat.AIG.RefVec.MapTarget aig len → aig.RefVec len
-- Mathlib.Algebra.Order.Module.Defs
pos_of_smul_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosReflectLT α β], 0 < a • b → 0 ≤ b → 0 < a
-- Mathlib.Order.Category.Semilat
/-- `OrderDual` as a functor.  -/
SemilatSupCat.dual : CategoryTheory.Functor SemilatSupCat SemilatInfCat
-- Mathlib.Order.RelIso.Basic
RelEmbedding.trans_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  {u : δ → δ → Prop} (f : r ↪r s) (g : s ↪r t) (h : t ↪r u), (f.trans g).trans h = f.trans (g.trans h)
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.toUInt64 : Lean.Meta.ProjReductionKind → UInt64
-- Mathlib.Algebra.Module.Equiv.Defs
/-- See Note [custom simps projection]  -/
LinearEquiv.Simps.symm_apply : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M ≃ₛₗ[σ] M₂) → M₂ → M
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctorRight_hom_app : ∀ {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 : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (X : D), (CategoryTheory.Join.mkFunctorRight F G α).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
-- Mathlib.Topology.GDelta.Basic
/-- The image of a meagre set through an inducing map is meagre.  -/
Topology.IsInducing.isMeagre_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → ∀ {s : Set X}, IsMeagre s → IsMeagre (f '' s)
-- Mathlib.Algebra.Module.Projective
Module.instProjectiveDFinsupp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_6} (A : ι → Type u_7) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [h : ∀ (i : ι), Module.Projective R (A i)], Module.Projective R (Π₀ (i : ι), A i)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.instCoeFunForallSmoothBumpFunctionC : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : Set M} → CoeFun (SmoothBumpCovering ι I M s) fun x => (i : ι) → SmoothBumpFunction I (x.c i)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.nonempty_orbit : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (a : α), (MulAction.orbit M a).Nonempty
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If there is a nonzero vector and every other vector is a multiple of it,
then the module has dimension one.  -/
finrank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [StrongRankCondition R] (v : M),
  v ≠ 0 → (∀ (w : M), ∃ c, c • v = w) → Module.finrank R M = 1
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} {_cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw._auto_1} [inst : SizeOf α]
  [inst_1 : (a : α) → SizeOf (β a)] (inner : Std.DTreeMap.Internal.Impl α β),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The morphism between base objects.  -/
CategoryTheory.Pseudofunctor.Grothendieck.Hom.base : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      {X Y : F.Grothendieck} → X.Hom Y → (X.base ⟶ Y.base)
-- Mathlib.Data.Fintype.Basic
Fintype.univ_pempty : Finset.univ = ∅
-- Mathlib.Order.RelSeries
/-- A relation series `a₀ -r→ a₁ -r→ ... -r→ aₙ` of `r` gives a relation series of the reverse of `r`
by reversing the series `aₙ ←r- aₙ₋₁ ←r- ... ←r- a₁ ←r- a₀`.
 -/
RelSeries.reverse : {α : Type u_1} → {r : SetRel α α} → RelSeries r → RelSeries r.inv
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `IsLocalization.AtPrime.under_maximalIdeal`. -/
IsLocalization.AtPrime.comap_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (h : optParam (IsLocalRing S) ⋯),
  Ideal.under R (IsLocalRing.maximalIdeal S) = I
-- Mathlib.Algebra.Star.Unitary
Unitary.map_id : ∀ {R : Type u_2} [inst : Monoid R] [inst_1 : StarMul R],
  Unitary.map (StarMonoidHom.id R) = StarMonoidHom.id ↥(unitary R)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_lt : ∀ {a b c : Ordinal.{u_4}}, b ≠ 0 → (a / b < c ↔ a < b * c)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.self_sub_C_mul_X_pow : ∀ {R : Type u_2} [inst : Ring R] (f : Polynomial R),
  f - Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f.eraseLead
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.match_1.eq_3 : ∀ (motive : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Sort u_1) (a b : ℤ)
  (h_1 : (a a_1 b b_1 : ℤ) → motive (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1))
  (h_2 : (a b : ℤ) → motive (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b))
  (h_3 : (a b : ℤ) → motive (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii)
  (h_5 : (x x_1 : Lean.Grind.IntInterval) → motive x x_1),
  (match Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b with
    | Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 => h_1 a a_1 b b_1
    | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => h_2 a b
    | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => h_3 a b
    | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_3 a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_periodic : Function.Periodic Real.Angle.tan ↑Real.pi
-- Mathlib.RingTheory.Derivation.Lie
Derivation.commutator_apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {D1 D2 : Derivation R A A} (a : A), ⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a)
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.coprime_of_ne : ∀ {α : Type u} [inst : Semiring α] {M M' : Ideal α}, M.IsMaximal → M'.IsMaximal → M ≠ M' → M ⊔ M' = ⊤
-- Init.Data.Int.Order
Int.sign_pos_iff : ∀ {x : ℤ}, 0 < x.sign ↔ 0 < x
-- Mathlib.Analysis.Normed.Group.Basic
enorm_mul_le_of_le' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedMonoid E] {r₁ r₂ : ENNReal} {a₁ a₂ : E},
  ‖a₁‖ₑ ≤ r₁ → ‖a₂‖ₑ ≤ r₂ → ‖a₁ * a₂‖ₑ ≤ r₁ + r₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_erase_eq_iff_not_compare_eq_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).min? = t.min? ↔ ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instOrderedAddQ : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Lean.Grind.OrderedAdd (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A preorder with a terminal object has a greatest element.  -/
Preorder.orderTopOfHasTerminal : {C : Type u} → [inst : Preorder C] → [CategoryTheory.Limits.HasTerminal C] → OrderTop C
-- Mathlib.Data.Vector.Basic
List.Vector.append_nil : ∀ {α : Type u_1} {n : ℕ} (xs : List.Vector α n), xs ++ List.Vector.nil = xs
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.mk_of_charts : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
  x ∈ domChart.source →
    f x ∈ codChart.source →
      domChart ∈ IsManifold.maximalAtlas I n M →
        codChart ∈ IsManifold.maximalAtlas J n N →
          domChart.source ⊆ f ⁻¹' codChart.source →
            Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x => (x, 0))
                (domChart.extend I).target →
              Manifold.IsImmersionAt I J n f x
-- Batteries.Data.List.Perm
List.subperm_cons_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (l : List α), l.Subperm (a :: l.erase a)
-- Init.Data.Iterators.Basic
/-- The iterator is a plausible indirect successor of one of the current iterator's successors.  -/
Std.Iter.IsPlausibleIndirectSuccessorOf.cons_right : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it'' it' it : Std.Iter β},
  it''.IsPlausibleIndirectSuccessorOf it' → it'.IsPlausibleSuccessorOf it → it''.IsPlausibleIndirectSuccessorOf it
-- Init.Data.List.TakeDrop
List.head?_dropWhile_not : ∀ {α : Type u_1} (p : α → Bool) (l : List α),
  match (List.dropWhile p l).head? with
  | some x => p x = false
  | none => True
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.mem_adjoinNegOne_iff : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] {𝒢 : Subgroup (GL n R)}
  {g : GL n R}, g ∈ 𝒢.adjoinNegOne ↔ g ∈ 𝒢 ∨ -g ∈ 𝒢
-- Init.Prelude
/-- The `` `group `` kind is used for nodes that result from `Lean.Parser.group`. This avoids confusion
with the null kind when used inside `optional`.
 -/
Lean.groupKind : Lean.SyntaxNodeKind
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.uniqueLinearEquiv_apply : ∀ (R : Type u_1) {α : Type u_3} (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
  [inst_3 : Subsingleton α] (a : α) (a_1 : α →₀ M), (Finsupp.uniqueLinearEquiv R M a) a_1 = a_1 a
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_eq_of_gradedMonoid_eq : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : (i : ι) → AddCommMonoid (A i)] {i j : ι} {a : A i}
  {b : A j}, GradedMonoid.mk i a = GradedMonoid.mk j b → (DirectSum.of A i) a = (DirectSum.of A j) b
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fppfPrecoverage : AlgebraicGeometry.Scheme.zariskiPrecoverage ≤ AlgebraicGeometry.Scheme.fppfPrecoverage
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.cofibration_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CochainComplex.Plus C} (f : X ⟶ Y), HomotopicalAlgebra.Cofibration f ↔ CategoryTheory.Mono f
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ioo : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [inst : LinearOrder α] (f : ι → α) (g : ι' → α),
  IsPiSystem {S | ∃ l u, f l < g u ∧ Set.Ioo (f l) (g u) = S}
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft.congr_simp : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E], ZMod.dft = ZMod.dft
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_zero_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α),
  μ.compProd 0 = 0
-- Mathlib.FieldTheory.Tower
/-- **Alias** of `Module.Finite.right`.

---

[Stacks Tag 09G5](https://stacks.math.columbia.edu/tag/09G5) -/
FiniteDimensional.right : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : Module F K]
  [inst_3 : AddCommMonoid A] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [hf : Module.Finite F A],
  Module.Finite K A