mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WithBot
WithBot.linearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (WithBot α)
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] → (ρ : Representation k G V) → BoundedOrder ↥ρ.invtSubmodule
-- Init.System.IO
/-- Ordinary files that have contents and are not directories.  -/
IO.FS.FileType.file : IO.FS.FileType
-- Init.Data.Option.Lemmas
Option.some_le_some : ∀ {α : Type u_1} [inst : LE α] {a b : α}, some a ≤ some b ↔ a ≤ b
-- Mathlib.Order.Lattice
sup_right_idem : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α), a ⊔ b ⊔ b = a ⊔ b
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R →
    CircleIntegrable g c R → ∮ (z : ℂ) in C(c, R), f z + g z = (∮ (z : ℂ) in C(c, R), f z) + ∮ (z : ℂ) in C(c, R), g z
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.join.eq_1 : ∀ (l : List String), String.join l = List.foldl (fun r s => r ++ s) "" l
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_pow_mul : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ), (Polynomial.X ^ n * p).coeff (d + n) = p.coeff d
-- Mathlib.CategoryTheory.Abelian.Basic
/-- `Abelian.coimage` as a functor from the arrow category.  -/
CategoryTheory.Abelian.coim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Lean.Meta.Tactic.Induction
_private.Lean.Meta.Tactic.Induction.0.Lean.Meta.getTypeBody : Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.Simps.Basic
Simps.instToMessageDataProjectionData : Lean.ToMessageData Simps.ProjectionData
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.eq_bot_of_liesOver_bot : ∀ (A : Type u_1) [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] (P : Ideal B) [Nontrivial A] [IsDomain B] [h : P.LiesOver ⊥], P = ⊥
-- Mathlib.RingTheory.AlgebraTower
RingEquiv.ofBijective.congr_simp : ∀ {F : Type u_1} {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F)
  (e_f : f = f_1) (hf : Function.Bijective ⇑f), RingEquiv.ofBijective f hf = RingEquiv.ofBijective f_1 ⋯
-- Init.Data.Rat.Lemmas
Rat.le_trans : ∀ {a b c : ℚ}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.NumberTheory.Modular
/-- For any `y : ℝ`, the standard fundamental domain truncated at height `y` is compact.  -/
ModularGroup.isCompact_truncatedFundamentalDomain : ∀ (y : ℝ), IsCompact (ModularGroup.truncatedFundamentalDomain y)
-- Mathlib.Data.Finset.Density
Finset.natCast_card_mul_nnratCast_dens : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : Semifield 𝕜] [CharZero 𝕜] (s : Finset α),
  ↑(Fintype.card α) * ↑s.dens = ↑s.card
-- Mathlib.Topology.Maps.Proper.Basic
/-- A continuous map from a compact space to a T₂ space is a proper map.  -/
Continuous.isProperMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [CompactSpace X]
  [T2Space Y], Continuous f → IsProperMap f
-- Mathlib.Order.Atoms
isSimpleOrder_iff_isCoatom_bot : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α], IsSimpleOrder α ↔ IsCoatom ⊥
-- Init.Tactics
/-- A simp lemma specification is:
* optional `↑` or `↓` to specify use before or after entering the subterm
* optional `←` to use the lemma backward
* `thm` for the theorem to rewrite with
 -/
Lean.Parser.Tactic.simpLemma : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side, version subtracting vectors.  -/
Orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).tan * ‖x‖ = ‖y‖
-- Mathlib.Topology.Order.ExtendFrom
continuousOn_Ioc_extendFrom_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {lb : β} [RegularSpace β],
  ContinuousOn f (Set.Ioo a b) →
    Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb) → ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Ioc a b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_prodCongr : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_5} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] {M₃ : Type u_6}
  [inst_5 : TopologicalSpace M₃] [inst_6 : AddCommMonoid M₃] {M₄ : Type u_7} [inst_7 : TopologicalSpace M₄]
  [inst_8 : AddCommMonoid M₄] [inst_9 : Module R₁ M₁] [inst_10 : Module R₁ M₂] [inst_11 : Module R₁ M₃]
  [inst_12 : Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄), ↑(e.prodCongr e') = (↑e).prodMap ↑e'
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.instIsEmptyI₀Empty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C}, IsEmpty (CategoryTheory.PreZeroHypercover.empty S).I₀
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `lt_neg_add_iff_add_lt`. -/
lt_neg_add_of_add_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a + b < c → b < -a + c
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.reflection_apply_right : ∀ {ι : 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} {i j : ι},
  P.IsOrthogonal j i → (P.reflection j) (P.root i) = P.root i
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.eq_1 : ∀ (α : Type u_6), FreeAddMonoid α = List α
-- Mathlib.Order.ModularLattice
IsModularLattice.isModularLattice_Iic : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a : α}, IsModularLattice ↑(Set.Iic a)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.noConfusionType : Sort v✝ → CategoryTheory.Limits.WalkingReflexivePair → CategoryTheory.Limits.WalkingReflexivePair → Sort v✝
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- `UniqueMDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative.  -/
UniqueMDiffWithinAt.eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  UniqueMDiffAt[s] x → HasMFDerivAt[s] f x f' → HasMFDerivAt[s] f x f₁' → f' = f₁'
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_reverse : ∀ {T : Type u_1} (g : ContextFreeGrammar T), g.reverse.reverse = g
-- Mathlib.Order.Ideal
Order.Ideal.mem_principal_self : ∀ {P : Type u_1} [inst : Preorder P] {x : P}, x ∈ Order.Ideal.principal x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_min?_of_isSome_min?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).min?.isSome = true → t.min?.isSome = true
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_comp_homologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.homologyπ j) = 0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNegOfContinuousNeg : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Neg β] → [ContinuousNeg β] → Neg C(α, β)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_ExceptT_lift : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α ε' : Type u}
  [inst_4 : MonadExceptOf ε m] (err : ε) (post : α → Pred) (epost : EPost.Cons✝ (ε' → Pred) EPred),
  ⦃
    Std.Internal.Do.wp (MonadExceptOf.throw err)
      (fun r =>
        match r with
        | Except.ok a => post a
        | Except.error e => epost.head e)
      epost.tail ⦄
    MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsInducing.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsInducing f), Topology.IsInducing (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Init.Data.List.Lemmas
List.map_id : ∀ {α : Type u_1} (l : List α), List.map id l = l
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.of.injEq : ∀ (carrier : Type u) [str : TopologicalSpace carrier] (carrier_1 : Type u) (str_1 : TopologicalSpace carrier_1),
  (TopCat.of carrier = TopCat.of carrier_1) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_succ : ∀ (n k : ℕ), n.descFactorial (k + 1) = (n - k) * n.descFactorial k
-- Mathlib.Data.Multiset.Count
Multiset.count_pos : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, 0 < Multiset.count a s ↔ a ∈ s
-- Init.Data.String.OrderInstances
String.Pos.instLawfulOrderLT : ∀ {s : String}, Std.LawfulOrderLT s.Pos
-- Mathlib.GroupTheory.Nilpotent
/-- The preimage of a nilpotent additive group is nilpotent if the kernel of the
homomorphism is contained in the center.  -/
AddSubgroup.isNilpotent_of_ker_le_center : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (f : G →+ H),
  f.ker ≤ AddSubgroup.center G → ∀ [AddGroup.IsNilpotent H], AddGroup.IsNilpotent G
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.filterAt_basis_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X),
  (v.filterAt x).HasBasis (fun x => 0 < x) fun x_1 => {t | t ∈ v.setsAt x ∧ t ⊆ Metric.closedBall x x_1}
-- Mathlib.Analysis.Calculus.Deriv.Abs
deriv_abs_pos : ∀ {x : ℝ}, 0 < x → deriv (fun x => |x|) x = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorδ.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C),
  CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
          (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₂ Y₂).inv)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X₂ Y₁).inv Y₂))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
              (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₁ Y₂).hom)
            (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂
                (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)).inv)))
-- Mathlib.Data.Vector.Basic
List.Vector.not_empty_toList : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α (n + 1)), ¬v.toList.isEmpty = true
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_filter_mul_prod_map_filter_not : ∀ {α : Type u_2} {M : Type u_4} [inst : CommMonoid M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α → M)
  (l : List α),
  (List.map f (List.filter (fun b => decide (p b)) l)).prod * (List.map f (List.filter (fun x => decide ¬p x) l)).prod =
    (List.map f l).prod
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.ind_apply : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x ∈ s),
  (f (f.ind x hx)) x = 1
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapTrifunctorMapObj.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃)
  (j : J) (h : p (i₁, i₂, i₃) = j)
  [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p],
  CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_gt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.gt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.lt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        List.filter (fun x => k x.fst == Ordering.lt) r.toListModel
-- Mathlib.Topology.Algebra.Monoid
Specializes.mul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {a b c d : M},
  a ⤳ b → c ⤳ d → (a * c) ⤳ (b * d)
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- Any element semiconjugates `1` to `1`.  -/
SemiconjBy.one_right : ∀ {M : Type u_2} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1
-- Mathlib.Data.Sum.Basic
/-- The map from the second summand into a ternary sum.  -/
Sum3.in₁ : {α : Type u} → {β : Type v} → {γ : Type u_1} → β → α ⊕ β ⊕ γ
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.instFiniteInitial : (⊥_ SSet).Finite
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instInhabited : {α : Type u} → {β : Type v} → Inhabited (Std.HashMap.Raw α β)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mul_X_mem_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {p : MvPolynomial σ S} {s : σ},
  p * MvPolynomial.X s ∈ MvPolynomial.coeffsIn σ M ↔ p ∈ MvPolynomial.coeffsIn σ M
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.zero_mem_polar : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  0 ∈ B.polar s
-- Mathlib.Order.Filter.Map
Filter.le_comap_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β}, f ≤ Filter.comap m (Filter.map m f)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformly.add` -/
TendstoUniformly.fun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l →
    TendstoUniformly f' g' l → TendstoUniformly (fun i i_1 => f i i_1 + f' i i_1) (fun i => g i + g' i) l
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Icc_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ico a b ⊆ Finset.Icc a b
-- Std.Time.Zoned.ZoneRules
/-- The first `LocalTimeType` used as a fallback when no matching transition is found.
 -/
Std.Time.TimeZone.ZoneRules.initialLocalTimeType : Std.Time.TimeZone.ZoneRules → Std.Time.TimeZone.LocalTimeType
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Ico_iff : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ b₁ → (Finset.Icc a₁ b₁ ⊆ Finset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_right : ∀ {ι : 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 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ i (RootPairing.EmbeddedG2.twoShortAddLong P) =
    2 * P.pairingIn ℤ i (RootPairing.EmbeddedG2.short P) + 3 * P.pairingIn ℤ i (RootPairing.EmbeddedG2.long P)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.prodL_apply : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι]
  (a : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G'),
  (ContinuousMultilinearMap.prodL 𝕜 E G G') a = ContinuousMultilinearMap.prodEquiv.toFun a
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.arr_link : ∀ {self : Batteries.UnionFind} {x y : Fin self.size} {yroot : self.parent ↑y = ↑y},
  (self.link x y yroot).arr = Batteries.UnionFind.linkAux self.arr x y
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.zero.sizeOf_spec : sizeOf CategoryTheory.Limits.WalkingReflexivePair.zero = 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app : ∀ (R : CommRingCat), AlgebraicGeometry.Scheme.SpecΓIdentity.hom.app R = (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
-- Batteries.Data.List.Lemmas
List.findIdxNth_eq_findIdxNth_iff_of_right_lt_countP : ∀ {α : Type u_1} {m : ℕ} {p : α → Bool} {n : ℕ} {xs : List α},
  m < List.countP p xs → (List.findIdxNth p xs n = List.findIdxNth p xs m ↔ n = m)
-- Lean.Message
Lean.MessageData.trace.inj : ∀ {data : Lean.TraceData} {msg : Lean.MessageData} {children : Array Lean.MessageData} {data_1 : Lean.TraceData}
  {msg_1 : Lean.MessageData} {children_1 : Array Lean.MessageData},
  Lean.MessageData.trace data msg children = Lean.MessageData.trace data_1 msg_1 children_1 →
    data = data_1 ∧ msg = msg_1 ∧ children = children_1
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E], ‖0‖ = 0
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_inv_self : ∀ (β : Type u_3) (γ : Type u_4) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β]
  [inst_3 : Field γ] [inst_4 : ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] (b : β),
  ConditionallyCompleteLinearOrderedField.inducedMap γ β (ConditionallyCompleteLinearOrderedField.inducedMap β γ b) = b
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.aestabilizer_empty : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ], AddAction.aestabilizer G μ ∅ = ⊤
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.SymbolPriorities : Type
-- Init.Data.Vector.Lemmas
Vector.foldrM_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β},
  Vector.foldrM f init #v[] = pure init
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mop_inj_iff : ∀ {C : Type u₁} (x y : C), { unmop := x } = { unmop := y } ↔ x = y
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.ProofMode.elim_entails : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {φ : Prop} [Std.Do.SPred.Tactic.PropAsSPredTautology φ P], φ → ⊢ₛ P
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] (U : ↥(unitary R)), ↑(-U) = -↑U
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The first projection from the product.  -/
TopCat.prodFst : {X Y : TopCat} → TopCat.of (↑X × ↑Y) ⟶ X
-- Mathlib.CategoryTheory.Action.Monoidal
_private.Mathlib.CategoryTheory.Action.Monoidal.0.Action.diagonalSuccIsoTensorTrivial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
LinearMap.spectrum_toMatrix : ∀ {R : Type u_1} {n : Type u_2} {M : Type u_3} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (f : M →ₗ[R] M) (b : Module.Basis n R M),
  spectrum R ((LinearMap.toMatrix b b) f) = spectrum R f
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
/-- The image of the map sending a nonzero natural number `x ≤ p / 2` to the absolute value
of the integer in `(-p/2, p/2]` that is congruent to `a * x mod p` is the set
of nonzero natural numbers `x` such that `x ≤ p / 2`.  -/
ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ZMod p),
  a ≠ 0 →
    Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Finset.Ico 1 (p / 2).succ).val =
      Multiset.map (fun a => a) (Finset.Ico 1 (p / 2).succ).val
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.takeEndWhile_char_eq_takeEndWhile_beq : ∀ {c : Char} {s : String.Slice}, s.takeEndWhile c = s.takeEndWhile fun x => x == c
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instQuasiIsoAtIntπTruncGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ), QuasiIsoAt (K.πTruncGE n) n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDTreeMap.filterMap f t).contains k = Option.any (fun x => (f k x).isSome) (t.get? k)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.tryTactic : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM Bool