mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.mk.injEq : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (a b c : NumberField.RingOfIntegers K)
  (u : (NumberField.RingOfIntegers K)ˣ) (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hc : c ≠ 0)
  (coprime : IsCoprime a b) (hcdvd : hζ.toInteger - 1 ∣ c) (H : a ^ 3 + b ^ 3 = ↑u * c ^ 3)
  (a_1 b_1 c_1 : NumberField.RingOfIntegers K) (u_1 : (NumberField.RingOfIntegers K)ˣ) (ha_1 : ¬hζ.toInteger - 1 ∣ a_1)
  (hb_1 : ¬hζ.toInteger - 1 ∣ b_1) (hc_1 : c_1 ≠ 0) (coprime_1 : IsCoprime a_1 b_1) (hcdvd_1 : hζ.toInteger - 1 ∣ c_1)
  (H_1 : a_1 ^ 3 + b_1 ^ 3 = ↑u_1 * c_1 ^ 3),
  ({ a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H } =
      { a := a_1, b := b_1, c := c_1, u := u_1, ha := ha_1, hb := hb_1, hc := hc_1, coprime := coprime_1,
        hcdvd := hcdvd_1, H := H_1 }) =
    (a = a_1 ∧ b = b_1 ∧ c = c_1 ∧ u = u_1)
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPreconnected_closedEBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  IsPreconnected (Metric.closedEBall x r)
-- Mathlib.Data.Num.Lemmas
PosNum.natSize_pos : ∀ (n : PosNum), 0 < n.natSize
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_atTop_iff_eventually_exists_pos : ∀ {G : Type u_5} {G' : Type u_8} [inst : Norm G] [inst_1 : SeminormedAddCommGroup G'] {α : Type u_17}
  [inst_2 : SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'},
  f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
-- Lean.Meta.Constructions.CtorIdx
Lean.isCtorIdxCore? : Lean.Environment → Lean.Name → Option Lean.InductiveVal
-- Mathlib.NumberTheory.NumberField.DedekindZeta
NumberField.dedekindZeta_residue_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.dedekindZeta_residue K ≠ 0
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.orthogonal_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → T.rangeᗮ = T.ker
-- Mathlib.LinearAlgebra.Matrix.Unique
/-- The isomorphism between the type of all one by one matrices and the base type.  -/
Matrix.uniqueEquiv : {m : Type u_1} → {n : Type u_2} → {A : Type u_3} → [Unique m] → [Unique n] → Matrix m n A ≃ A
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
/-- Returns the ring id for the given type if there is a `CommRing` instance for it.

This function will also perform sanity-checks
(e.g., the `Add` instance for `type` must be definitionally equal to the `CommRing.toAdd` one.)

It also caches the functions representing `+`, `*`, `-`, `^`, and `intCast`.
 -/
Lean.Meta.Grind.Arith.CommRing.getCommRingId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The nerve functor is both full and faithful and thus is fully faithful.  -/
CategoryTheory.nerveFunctor.fullyfaithful : CategoryTheory.nerveFunctor.FullyFaithful
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum'_obj_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) (a : A), (F.sum' G).obj (Sum.inl a) = F.obj a
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebungFun_coeff_succ : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (n : ℕ), x.verschiebungFun.coeff n.succ = x.coeff n
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.associator.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₁₂ : Type u_4} {C₂₃ : Type u_5} {D₁ : Type u_6} {D₂ : Type u_7}
  {D₃ : Type u_8} {D₁₂ : Type u_9} {D₂₃ : Type u_10} {C : Type u_11} {D : Type u_12}
  [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_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_7, u_4} C₁₂] [inst_7 : CategoryTheory.Category.{v_8, u_5} C₂₃]
  [inst_8 : CategoryTheory.Category.{v_9, u_9} D₁₂] [inst_9 : CategoryTheory.Category.{v_10, u_10} D₂₃]
  [inst_10 : CategoryTheory.Category.{v_11, u_11} C] [inst_11 : CategoryTheory.Category.{v_12, u_12} D]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃)
  (L₁₂ : CategoryTheory.Functor C₁₂ D₁₂) (L₂₃ : CategoryTheory.Functor C₂₃ D₂₃) (L : CategoryTheory.Functor C D)
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂)
  (W₃ : CategoryTheory.MorphismProperty C₃) (W₁₂ : CategoryTheory.MorphismProperty C₁₂)
  (W₂₃ : CategoryTheory.MorphismProperty C₂₃) [inst_12 : W₁.ContainsIdentities] [inst_13 : W₂.ContainsIdentities]
  [inst_14 : W₃.ContainsIdentities] [inst_15 : L₁.IsLocalization W₁] [inst_16 : L₂.IsLocalization W₂]
  [inst_17 : L₃.IsLocalization W₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (iso iso_1 : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃),
  iso = iso_1 →
    ∀ (F₁₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ D₁₂))
      (G' : CategoryTheory.Functor D₁₂ (CategoryTheory.Functor D₃ D))
      (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂₃ D))
      (G₂₃' : CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ D₂₃)), ⋯
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_bot : ∀ {α : Type u_1} {r : α → α → Prop}, Filter.IsBounded r ⊥ ↔ Nonempty α
-- Mathlib.Topology.Algebra.Support
/-- If `f` has compact support, then `f` tends to zero at infinity.  -/
HasCompactSupport.is_zero_at_infty : ∀ {α : Type u_2} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero γ] {f : α → γ} [inst_2 : TopologicalSpace γ],
  HasCompactSupport f → Filter.Tendsto f (Filter.cocompact α) (nhds 0)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (x x_1 : S.Arrow) (r : x.Relation x_1), S.preOneHypercover.p₁ r = r.g₁
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The expression that is being rewritten.  -/
Mathlib.Tactic.ClickSuggestions.RwInfo.subExpr : Mathlib.Tactic.ClickSuggestions.RwInfo → Lean.Expr
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`.  -/
EuclideanGeometry.oangle_left_eq_arccos_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₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Antitone.mul_monotone : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] [inst_2 : Preorder α] {f g : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → Monotone g → (∀ (x : α), f x ≤ 0) → (∀ (x : α), 0 ≤ g x) → Antitone (f * g)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemCont.mk : Lean.Name → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.DoElemContKind → Lean.Elab.Do.DoElemCont
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.mk : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  {𝒜 : ιA → σA} →
                    {ℳ : ιM → σM} →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [inst_7 : GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [inst_11 : DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] →
                                          [inst_13 : SetLike.GradedSMul 𝒜 ℳ] →
                                            (toSubmodule : Submodule A M) →
                                              toSubmodule.IsHomogeneous ℳ → HomogeneousSubmodule 𝒜 ℳ
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_neg_eq_add_neg_iff : ∀ {α : Type u} [inst : AddCommMonoid α] (a c : α) (b d : AddUnits α), a + ↑(-b) = c + ↑(-d) ↔ a + ↑d = c + ↑b
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_1.eq_2 : ∀ (motive : Option String → Sort u_1) (h_1 : (post : String) → motive (some post)) (h_2 : Unit → motive none),
  (match none with
    | some post => h_1 post
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.id'_coe : ∀ {R : Type u_1} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {σ : R →+* R}
  [inst_3 : RingHomId σ], ⇑LinearMap.id' = id
-- Mathlib.NumberTheory.SmoothNumbers
/-- The set of `k`-smooth numbers `≤ N` is contained in the set of numbers of the form `m^2 * P`,
where `m ≤ √N` and `P` is a product of distinct primes `< k`.  -/
Nat.smoothNumbersUpTo_subset_image : ∀ (N k : ℕ),
  N.smoothNumbersUpTo k ⊆
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum_C_tmul_one : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (r : S), (MvPolynomial.tensorEquivSum R σ ι S) (MvPolynomial.C r ⊗ₜ[R] 1) = MvPolynomial.C r
-- Mathlib.Topology.UniformSpace.Cauchy
/-- Any shift of a Cauchy sequence is also a Cauchy sequence.  -/
cauchySeq_shift : ∀ {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} (k : ℕ), (CauchySeq fun n => u (n + k)) ↔ CauchySeq u
-- Mathlib.Topology.Connected.TotallyDisconnected
IsPreconnected.isDiscrete_iff_subsingleton : ∀ {α : Type u} [inst : TopologicalSpace α] {S : Set α}, IsPreconnected S → (IsDiscrete S ↔ S.Subsingleton)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} {k k' : α} (h : t.WF),
  t.getKey? k = some k' →
    Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k =
      Option.filter (fun x => f k' x) (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coeToMonoidHom : {α : Type u_2} → {β : Type u_3} → {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → Coe (α →+* β) (α →* β)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → DifferentiableAt ℂ g x → f x ∈ Complex.slitPlane → DifferentiableAt ℂ (fun x => f x ^ g x) x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two cyclic groups of the same cardinality are isomorphic.  -/
mulEquivOfCyclicCardEq : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : Group G] → [inst_1 : Group G'] → [hG : IsCyclic G] → [hH : IsCyclic G'] → Nat.card G = Nat.card G' → G ≃* G'
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyGED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α → α
-- Init.Data.SInt.Lemmas
Int32.toInt8_toISize : ∀ (n : Int32), n.toISize.toInt8 = n.toInt8
-- Mathlib.Analysis.Calculus.MeanValue
/-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
bounded by `C` satisfies `‖f 1 - f 0‖ ≤ C`, `HasDerivWithinAt`
version.  -/
norm_image_sub_le_of_norm_deriv_le_segment_01' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {C : ℝ},
  (∀ x ∈ Set.Icc 0 1, HasDerivWithinAt f (f' x) (Set.Icc 0 1) x) → (∀ x ∈ Set.Ico 0 1, ‖f' x‖ ≤ C) → ‖f 1 - f 0‖ ≤ C
-- Init.Data.List.Lemmas
List.partition.loop.eq_def : ∀ {α : Type u} (p : α → Bool) (a : List α) (a_1 : List α × List α),
  List.partition.loop p a a_1 =
    match a, a_1 with
    | [], (bs, cs) => (bs.reverse, cs.reverse)
    | a :: as, (bs, cs) =>
      match p a with
      | true => List.partition.loop p as (a :: bs, cs)
      | false => List.partition.loop p as (bs, a :: cs)
-- Mathlib.Probability.Distributions.Exponential
/-- Measure defined by the exponential distribution  -/
ProbabilityTheory.expMeasure : ℝ → MeasureTheory.Measure ℝ
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.eq_1 : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.FaithfullyFlat = Module.FaithfullyFlat R S
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of the inverse is the negative of the order.  -/
meromorphicOrderAt_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
DifferentiableOn.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.arctan (f x)) s
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.map.eq_1 : ∀ {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : α → α') (l : Combinatorics.Line α ι),
  Combinatorics.Line.map f l = { idxFun := fun i => Option.map f (l.idxFun i), proper := ⋯ }
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ι_totalDesc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  {c₁₂ : ComplexShape I₁₂} [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂)
  (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi)
      (CategoryTheory.CategoryStruct.comp (K.totalDesc f) h) =
    CategoryTheory.CategoryStruct.comp (f i₁ i₂ hi) h
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (φ : A ⟶ B) [CategoryTheory.IsIso φ], CategoryTheory.IsIso φ.hom₂
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.coe_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : A),
  (↑𝕜 a).toProd.1 = (ContinuousLinearMap.mul 𝕜 A) a
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
/-- Club sets are closed under suprema. If `α` is a well-order with the order topology, this
condition is equivalent to `IsClosed s`.  -/
IsClub.dirSupClosed : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, IsClub s → DirSupClosed s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, t.isEmpty = true → Std.DTreeMap.Internal.Impl.contains a t = false
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `(∅ ⟶ B) □ g` lifts against `X ⟶ Y` if and only if `g` lifts against `B ⟹ X ⟶ B ⟹ Y`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {g : K ⟶ L} {h : X ⟶ Y} (i : CategoryTheory.Limits.IsInitial A),
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk (i.to B) □ CategoryTheory.Arrow.mk g).hom h ↔
    CategoryTheory.HasLiftingProperty g ((CategoryTheory.ihom B).map h)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.Total.toListRev.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] (it it_1 : Std.IterM.Total m β), it = it_1 → it.toListRev = it_1.toListRev
-- Mathlib.Analysis.Normed.Group.Continuity
/-- If `‖y‖ → ∞`, then we can assume `y ≠ x` for any fixed `x`.  -/
eventually_ne_of_tendsto_norm_atTop' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {l : Filter α} {f : α → E},
  Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop → ∀ (x : E), ∀ᶠ (y : α) in l, f y ≠ x
-- Init.Data.SInt.Lemmas
Int8.toInt_maxValue_add_one : Int8.maxValue.toInt + 1 = 2 ^ 7
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (l : List ((a : α) × β a))
  (h : Std.Internal.List.containsKey a l = true), Std.Internal.List.getKey a l h = (Std.Internal.List.getKey? a l).get ⋯
-- Init.Data.SInt.Basic
Int8.instOfNat : {n : ℕ} → OfNat Int8 n
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.zero_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁ h₂).φH = 0
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
/-- The residue field of a local ring is the quotient of the ring by its maximal ideal.  -/
ValuativeRel.«term𝓀[_]» : Lean.ParserDescr
-- Lean.Util.Trace
Lean.instInhabitedTraceState : Inhabited Lean.TraceState
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_im : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜}, MeasureTheory.Integrable f μ → ∫ (x : X), RCLike.im (f x) ∂μ = RCLike.im (∫ (x : X), f x ∂μ)
-- Mathlib.Data.Finset.Sups
Finset.sized_compls : ∀ {α : Type u_4} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {n : ℕ},
  n ≤ Fintype.card α → (Set.Sized n ↑𝒜.compls ↔ Set.Sized (Fintype.card α - n) ↑𝒜)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_C : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S) (r : R),
  (PowerSeries.map f) (PowerSeries.C r) = PowerSeries.C (f r)
-- Mathlib.Analysis.Complex.Isometry
rotation_injective : Function.Injective ⇑rotation
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.beq.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x x_1 : List α) (h_1 : Unit → motive [] [])
  (h_2 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs))
  (h_3 : (x x_2 : List α) → motive x x_2),
  (x = [] → x_1 = [] → False) →
    (∀ (a : α) (as : List α) (b : α) (bs : List α), x = a :: as → x_1 = b :: bs → False) →
      (match x, x_1 with
        | [], [] => h_1 ()
        | a :: as, b :: bs => h_2 a as b bs
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Iso_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L')
  (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R)
  (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L')
  (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L)
  (hββ' :
    CategoryTheory.CategoryStruct.comp R.rightUnitor.hom
        (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R)
            (F.functor.associator F.inverse R).hom)) =
      CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom)
        (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse)
            (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β')))))
  (hβ'β :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom
          (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β)
            (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv
              (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) =
      CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom
        (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom)
          (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))),
  (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).functor =
    CategoryTheory.StructuredArrow.map₂ α β
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.ab5OfSize : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  [self : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.AB5OfSize.{w, w, v, u} C
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instMulAction.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {m : Monoid M} [inst : (i : ι) → MulAction M (α i)],
  Sigma.instMulAction = { toSMul := Sigma.instSMul_mathlib, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- action on 2-morphisms  -/
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂ : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) →
          {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (self.map f ⟶ self.map g)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Denominator of the formula for a fractional linear transformation  -/
UpperHalfPlane.denom : GL (Fin 2) ℝ → ℂ → ℂ