mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral
add to π", for oriented angles mod π, with a "concyclic" conclusion.  -/
EuclideanGeometry.concyclic_of_two_zsmul_oangle_eq_of_not_collinear : ∀ {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₄ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
    ¬Collinear ℝ {p₁, p₂, p₄} → EuclideanGeometry.Concyclic {p₁, p₂, p₃, p₄}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C}, sq.IsPushout → sq.op.IsPullback
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- **Alias** of the forward direction of `toZ_le_toZ`. -/
le_of_toZ_le : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i ≤ toZ i0 j → i ≤ j
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.IsRoot.of_map : ∀ {S : Type v} [inst : CommSemiring S] {R : Type u_1} [inst_1 : Ring R] {f : R →+* S} {x : R} {p : Polynomial R},
  (Polynomial.map f p).IsRoot (f x) → Function.Injective ⇑f → p.IsRoot x
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- Endowing the space `PiLp p β` with the `L^p` pseudoemetric structure. This definition is not
satisfactory, as it does not register the fact that the topology and the uniform structure coincide
with the product one. Therefore, we do not register it as an instance. Using this as a temporary
pseudoemetric space instance, we will show that the uniform structure is equal (but not defeq) to
the product one, and then register an instance in which we replace the uniform structure by the
product one using this pseudoemetric space and `PseudoEMetricSpace.replaceUniformity`.  -/
PiLp.pseudoEmetricAux : (p : ENNReal) →
  {ι : Type u_2} →
    (β : ι → Type u_4) →
      [Fact (1 ≤ p)] → [(i : ι) → PseudoEMetricSpace (β i)] → [Fintype ι] → PseudoEMetricSpace (PiLp p β)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.vlt_one_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x : R}, x <ᵥ 1 ↔ v x < 1
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- If all the elements of a set `s` commute, then `closure s` is a commutative semiring.  -/
Subsemiring.closureCommSemiringOfComm : {R' : Type u_1} →
  [inst : Semiring R'] → {s : Set R'} → (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → CommSemiring ↥(Subsemiring.closure s)
-- Mathlib.CategoryTheory.Opposites
/-- If F is faithful then the `rightOp` of F is also faithful.  -/
CategoryTheory.Functor.rightOp_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} [F.Faithful], F.rightOp.Faithful
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.not_revMatchesAt_of_get : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.startPos},
  p ((pos.prev h).get ⋯) = false → ¬String.Slice.Pattern.Model.RevMatchesAt p pos
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.DefEqCacheKey.mk.sizeOf_spec : ∀ (lhs rhs : Lean.Expr) (configKey : UInt64),
  sizeOf { lhs := lhs, rhs := rhs, configKey := configKey } = 1 + sizeOf lhs + sizeOf rhs + sizeOf configKey
-- Mathlib.Algebra.Order.Interval.Basic
instZeroNonemptyInterval : {α : Type u_2} → [inst : Preorder α] → [Zero α] → Zero (NonemptyInterval α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.all_eq_true_iff_forall_mem_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p a (m.get a h) = true)
-- Mathlib.Order.Preorder.Chain
Flag.ext : ∀ {α : Type u_1} [inst : LE α] {s t : Flag α}, ↑s = ↑t → s = t
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `M ∗ N →* M × N`.  -/
Monoid.Coprod.toProd : {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst_1 : Monoid N] → Monoid.Coprod M N →* M × N
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.odds.eq_1 : ∀ (n : ℕ), Nat.Partition.odds n = Nat.Partition.restricted n fun x => ¬Even x
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousOn.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X},
  ContinuousOn g s → ContinuousOn f s → ContinuousOn (fun x => g x ∘SL f x) s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A)
  (U :
    (TopologicalSpace.Opens
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)ᵒᵖ)
  {Z : CommRingCat}
  (h :
    ((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base).obj
            ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf).obj
        U ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).inv
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).presheaf.map
          (CategoryTheory.homOfLE ⋯).op)
        (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).c.app U) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)
        (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.map (CategoryTheory.homOfLE ⋯).op))
      h
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- Recursion principle to reduce a result about the synonym to the original type.  -/
HahnModule.rec : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_5} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero V] →
          [inst_2 : SMul R V] →
            {motive : HahnModule Γ R V → Sort u_6} →
              ((x : HahnSeries Γ V) → motive ((HahnModule.of R) x)) → (x : HahnModule Γ R V) → motive x
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.concreteCategory : CategoryTheory.ConcreteCategory AlexDisc fun x1 x2 => C(↑x1.toTopCat, ↑x2.toTopCat)
-- Mathlib.Order.WithBot
WithBot.instTop.eq_1 : ∀ {α : Type u_1} [inst : Top α], WithBot.instTop = { top := ↑⊤ }
-- Mathlib.GroupTheory.HNNExtension
Con.lift.congr_simp : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (c : Con M) (f f_1 : M →* P)
  (e_f : f = f_1) (H : c ≤ Con.ker f), c.lift f H = c.lift f_1 ⋯
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {nextIdx n : ℕ} {inner : Std.IterM m β} {nextIdx_1 n_1 : ℕ}
  {inner_1 : Std.IterM m β},
  { nextIdx := nextIdx, n := n, inner := inner } = { nextIdx := nextIdx_1, n := n_1, inner := inner_1 } →
    nextIdx = nextIdx_1 ∧ n = n_1 ∧ inner = inner_1
-- Mathlib.Algebra.Group.Defs
LeftCancelMonoid.toIsLeftCancelMul : ∀ {M : Type u} [self : LeftCancelMonoid M], IsLeftCancelMul M
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_neg_eq_logb : ∀ (b x : ℝ), Real.logb b (-x) = Real.logb b x
-- Mathlib.Algebra.Group.Int.Even
Int.even_pow' : ∀ {m : ℤ} {n : ℕ}, n ≠ 0 → (Even (m ^ n) ↔ Even m)
-- Init.Notation
Lean.guardMsgsOrderingArg : Lean.ParserDescr
-- Batteries.Data.RunningStats
Batteries.RunningStats.init.inj : ∀ {count : ℕ} {mean var : Float} {count_1 : ℕ} {mean_1 var_1 : Float},
  { count := count, mean := mean, var := var } = { count := count_1, mean := mean_1, var := var_1 } →
    count = count_1 ∧ mean = mean_1 ∧ var = var_1
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one_one_comp_comm : ∀ (R : Type u_1) [inst : CommRing R] (m n : ℕ),
  (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n) =
    (Polynomial.dickson 1 1 n).comp (Polynomial.dickson 1 1 m)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensorInv_leftInverse : ∀ {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R),
  Function.LeftInverse ⇑(Module.Invertible.rTensorInv P Q e) ⇑(LinearMap.rTensorHom M)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C),
  CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A =
    (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).app A ≪≫
      CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (F.rightOp.comp CategoryTheory.coyoneda) A
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.resRec.match_1.splitter : {w : ℕ} →
  (s : ℕ) →
    (motive : (s' : ℕ) → s' + 1 < w → 0 < s' + 1 → s = s'.succ → Sort u_1) →
      (s' : ℕ) →
        (hs : s' + 1 < w) →
          (hslt : 0 < s' + 1) →
            (hs0 : s = s'.succ) →
              ((hs : 0 + 1 < w) → (hslt : 0 < 0 + 1) → (hs0 : s = Nat.succ 0) → s' = 0 → motive 0 hs hslt hs0) →
                ((s'' : ℕ) →
                    (hs : s'' + 1 + 1 < w) →
                      (hslt : 0 < s'' + 1 + 1) →
                        (hs0 : s = (s'' + 1).succ) → s' = s''.succ → motive s''.succ hs hslt hs0) →
                  motive s' hs hslt hs0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ =
    CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).inv
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).homologyπ
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- A number satisfying the Liouville condition with exponent `p > 1` is an irrational number.  -/
LiouvilleWith.irrational : ∀ {p x : ℝ}, LiouvilleWith p x → 1 < p → Irrational x
-- Mathlib.Analysis.Normed.Group.Basic
edist_zero_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), edist a 0 = ‖a‖ₑ
-- Lean.Expr
/-- Auxiliary definition for `getAppNumArgs'`.  -/
_private.Lean.Expr.0.Lean.Expr.getAppNumArgs'.go : Lean.Expr → ℕ → ℕ
-- Mathlib.Data.List.TakeDrop
List.takeD_length : ∀ {α : Type u} (n : ℕ) (l : List α) (a : α), (List.takeD n l a).length = n
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.mk.inj : ∀ {X : Type u_1} {Y : Type u_2} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {toFun : X → Y}
  {continuous_toFun : autoParam (Continuous toFun) ContinuousMap.continuous_toFun._autoParam} {toFun_1 : X → Y}
  {continuous_toFun_1 : autoParam (Continuous toFun_1) ContinuousMap.continuous_toFun._autoParam},
  { toFun := toFun, continuous_toFun := continuous_toFun } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1 } →
    toFun = toFun_1
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_to_nat : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℕ}, (∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f
-- Mathlib.Data.Num.Basic
/-- Addition of `ZNum`s.  -/
ZNum.add : ZNum → ZNum → ZNum
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.map_vertex : ∀ {n : ℕ} {X Y : SSet.Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) (i : Fin (m + 1)),
  (f.map σ).vertex i =
    (CategoryTheory.ConcreteCategory.hom (σ.app (Opposite.op { obj := { len := 0 }, property := ⋯ }))) (f.vertex i)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.toList.isEmpty = t.isEmpty
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.lt_and_eval_eq_eval_add_one_of_mem_isAdmissible : ∀ {m : ℕ} (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible m L →
    ∀ j ∈ L,
      j < m + L.length ∧ SimplexCategoryGenRel.simplicialEvalσ L j = SimplexCategoryGenRel.simplicialEvalσ L (j + 1)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.addValuation.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Padic.addValuation = AddValuation.of Padic.addValuationDef ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.Action.Basic
vadd_left_cancel : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α) {x y : β}, g +ᵥ x = g +ᵥ y → x = y
-- Mathlib.Analysis.Convex.Approximation
/-- A function `φ : E → ℝ` that is convex and lower-semicontinuous on a closed convex subset `s` is
the supremum of a family of functions that are the restrictions to `s` of continuous affine linear
functions in `E`.  -/
ConvexOn.sSup_affine_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c} =
          s.domRestrict φ
-- Mathlib.Data.Set.Card
Set.finite_of_ncard_pos : ∀ {α : Type u_1} {s : Set α}, 0 < s.ncard → s.Finite
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.toComma : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      CategoryTheory.MorphismProperty.Comma L R P Q W → CategoryTheory.Comma L R
-- Mathlib.CategoryTheory.Galois.Topology
/-- The image of `Aut F` in `∀ X, Aut (F.obj X)` is closed.  -/
CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  IsClosed (Set.range ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F))
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralMulAlgNorm_def : ∀ {K : Type u} [inst : NontriviallyNormedField K] {L : Type v} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [inst_4 : CompleteSpace K] (x : L),
  (spectralMulAlgNorm K L) x = spectralNorm K L x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.meas_biInter : ∀ {Ω : Type u_1} {ι : Type u_2} {π : ι → Set (Set Ω)} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.iIndepSets π μ →
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkConsistentParentChildLinks : Aesop.MVarClusterRef → Lean.CoreM Unit
-- Init.Data.Nat.Basic
Nat.add_sub_self_right : ∀ (a b : ℕ), a + b - b = a
-- Mathlib.Algebra.Order.Module.Field
/-- Left scalar multiplication as an order isomorphism.  -/
OrderIso.smulRightDual : {𝕜 : Type u_1} →
  (G : Type u_2) →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [inst_3 : AddCommGroup G] →
            [inst_4 : PartialOrder G] →
              [IsOrderedAddMonoid G] → [inst_6 : Module 𝕜 G] → {a : 𝕜} → [PosSMulMono 𝕜 G] → a < 0 → G ≃o Gᵒᵈ
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.omega0_le_of_isSuccLimit : ∀ {o : Ordinal.{u_4}}, Order.IsSuccLimit o → Ordinal.omega0 ≤ o
-- Aesop.Tree.AddRapp
Aesop.AddRapp.toRuleApplication : Aesop.AddRapp → Aesop.RuleApplication
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.subset_adjoin : ∀ (k : Type u_1) {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (s : Set K) [inst_4 : Finite ↑s], s ⊆ ↑(FiniteGaloisIntermediateField.adjoin k s).toIntermediateField
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Cartesian product of two formal multilinear series (with the same field `𝕜` and the same source
space, but possibly different target spaces).  -/
FormalMultilinearSeries.prod : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      {G : Type x} →
        [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 : AddCommMonoid G] →
                                [inst_12 : Module 𝕜 G] →
                                  [inst_13 : TopologicalSpace G] →
                                    [inst_14 : ContinuousAdd G] →
                                      [inst_15 : ContinuousConstSMul 𝕜 G] →
                                        FormalMultilinearSeries 𝕜 E F →
                                          FormalMultilinearSeries 𝕜 E G → FormalMultilinearSeries 𝕜 E (F × G)
-- Std.Data.DHashMap.RawLemmas
/-- Variant of `get?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Raw.Const.get?_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} (h : m.WF),
  Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.map f m) k =
    Option.pmap (fun v h' => f (m.getKey k h') v) (Std.DHashMap.Raw.Const.get? m k) ⋯
-- Mathlib.Tactic.Linarith.Frontend
/-- `linarith?` behaves like `linarith` but, on success, it prints a suggestion of
the form `linarith only [...]` listing a minimized set of hypotheses used in the
final proof.  Use `linarith?!` for the higher-reducibility variant and set the
`minimize` flag in the configuration to control whether greedy minimization is
performed.
 -/
Mathlib.Tactic.tacticLinarith?!_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomLeft : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ⟶ y) [CategoryTheory.IsIso f]
  (z : D), CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
-- Mathlib.CategoryTheory.Sites.CoversTop.Over
CategoryTheory.GrothendieckTopology.CoversTop.over : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C}
  {I : Type u_2} {X : I → C},
  J.CoversTop X →
    ∀ {I' : I → Type u} {Y : (i : I) → I' i → CategoryTheory.Over (X i)},
      (∀ (i : I), (J.over (X i)).CoversTop (Y i)) → J.CoversTop fun j => (Y j.fst j.snd).left
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.smul_tprodCoeff : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : DecidableEq ι] (z : R)
  (f : (i : ι) → s i) (i : ι) (r : R₁) [inst_4 : SMul R₁ R] [IsScalarTower R₁ R R] [inst_6 : SMul R₁ (s i)]
  [IsScalarTower R₁ R (s i)],
  PiTensorProduct.tprodCoeff R z (Function.update f i (r • f i)) = PiTensorProduct.tprodCoeff R (r • z) f
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.of_mulOpposite : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A)
      (MulOpposite.op b0) (MulOpposite.op a0) →
    UniqueMul A B a0 b0
-- Lean.Widget.InteractiveGoal
_private.Lean.Widget.InteractiveGoal.0.Lean.Widget.addInteractiveHypothesisBundle.ppLetValueExprTagged : Bool → Lean.Expr → Lean.MetaM Lean.Widget.CodeWithInfos
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNormClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} [inst : SeminormedCommRing R] {S : outParam (Type u_3)} [inst_1 : Ring S]
  [inst_2 : Algebra R S] [inst_3 : FunLike F S ℝ] [toMulRingNormClass : MulRingNormClass F S ℝ],
  (∀ (f : F) (a : R) (x : S), f (a • x) = ‖a‖ * f x) → MulAlgebraNormClass F R S
-- Init.Data.List.ToArray
Array.forIn'.loop.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (b : β) (x : 0 ≤ as.size), Array.forIn'.loop as f 0 x b = pure b
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.forall : ∀ {p : Complex.UnitClosedDisc → Prop},
  (∀ (z : Complex.UnitClosedDisc), p z) ↔ ∀ (z : ℂ) (hz : ‖z‖ ≤ 1), p (Complex.UnitClosedDisc.mk z hz)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.eq_of_inj_apply_eq_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F},
  CategoryTheory.Functor.CoconeTypes.IsColimit c →
    ∀ {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂), c.inj i₁ y₁ = c.inj i₂ y₂ → i₁ = i₂
-- Batteries.Lean.EStateM
EStateM.run_fromStateM : ∀ {σ α ε : Type} (x : StateM σ α) (s : σ),
  (EStateM.fromStateM x).run s = EStateM.Result.ok (StateT.run x s).1 (StateT.run x s).2
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = true → Std.Internal.List.getValueCast? k (List.filter (fun p => !l₂.contains p.fst) l₁) = none
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.hasSum_iff_of_support : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)),
  (∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x) → (HasSum f a ↔ HasSum g a)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- A subgraph is preconnected if it is preconnected when coerced to be a simple graph.

Note: This is a structure to make it so one can be precise about how dot notation resolves.  -/
SimpleGraph.Subgraph.Preconnected : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {h' : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.minKey h' = t₂.minKey ⋯