mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_extendDomain : ∀ {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x y : α} {p : β → Prop} [inst : DecidablePred p]
  {f : α ≃ Subtype p}, (g.extendDomain f).SameCycle ↑(f x) ↑(f y) ↔ g.SameCycle x y
-- Init.Data.Int.Order
Int.le_of_eq : ∀ {a b : ℤ}, a = b → a ≤ b
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization.iso.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A),
  CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a =
    CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivWithinAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') s x
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Hom.sub_aux : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f g : P.Hom P') (x y : P.Ring),
  f.toAlgHom (x * y) - g.toAlgHom (x * y) -
      (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) +
        P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈
    P'.ker ^ 2
-- Mathlib.Order.Atoms
isCoatomic_dual_iff_isAtomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α], IsCoatomic αᵒᵈ ↔ IsAtomic α
-- Mathlib.Topology.Baire.BaireMeasurable
IsOpen.baireMeasurableSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsOpen s → BaireMeasurableSet s
-- Mathlib.Data.Vector.Basic
List.Vector.head_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n.succ → α), (List.Vector.ofFn f).head = f 0
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.opLaxMonoidalPi_δ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).OplaxMonoidal] (X Y : (i : I) → D i)
  (i : I),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Functor.pi F) X Y i =
    CategoryTheory.Functor.OplaxMonoidal.δ (F i) (X i) (Y i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {fallback : α},
  l.isEmpty = false → Std.Internal.List.maxKey? l = some (Std.Internal.List.maxKeyD l fallback)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.id_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_1 : X), (CategoryTheory.CategoryStruct.id x).fst.app X_1 = CategoryTheory.CategoryStruct.id (x.fst.obj X_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ Std.ExtDHashMap.Const.modify m k f},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.modify m k f) k' h =
    if heq : (k == k') = true then f (Std.ExtDHashMap.Const.get m k ⋯) else Std.ExtDHashMap.Const.get m k' ⋯
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.natPow_zero : ∀ {a : ℕ}, a.pow 0 = 1
-- Mathlib.Data.Finset.Image
Function.Semiconj.finset_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β},
  Function.Semiconj ⇑f ⇑ga ⇑gb → Function.Semiconj (Finset.map f) (Finset.map ga) (Finset.map gb)
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- Let `X, Y` be two sequences of measurable functions such that `X n` converges in distribution
to `Z`, and `Y n - X n` converges in probability to `0`.
Then `Y n` converges in distribution to `Z`.  -/
MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'}
  {μ' : MeasureTheory.Measure Ω'} [inst : MeasureTheory.IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''}
  {μ'' : MeasureTheory.Measure Ω''} [inst_1 : MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E}
  {l : Filter ι} [inst_2 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_4 : BorelSpace E]
  {X : ι → Ω'' → E} [l.IsCountablyGenerated] (Y : ι → Ω'' → E) (Z : Ω' → E),
  MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ' →
    MeasureTheory.TendstoInMeasure μ'' (Y - X) l 0 →
      (∀ (i : ι), AEMeasurable (Y i) μ'') → MeasureTheory.TendstoInDistribution Y l Z (fun x => μ'') μ'
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry.since? : Lean.DeprecatedModuleEntry → Option String
-- Init.Tactics
/-- The discharger clause of `simp` and related tactics.
This is a tactic used to discharge the side conditions on conditional rewrite rules.
 -/
Lean.Parser.Tactic.discharger : Lean.ParserDescr
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X_1 : (TopologicalSpace.Opens ↑U)ᵒᵖ),
  (X.restrict h).presheaf.obj X_1 = X.presheaf.obj (Opposite.op (h.functor.obj (Opposite.unop X_1)))
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeightOfEPs_comp : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : V → V → R) {a b c : V}
  (p : Quiver.Path a b) (q : Quiver.Path b c),
  Quiver.Path.addWeightOfEPs w (p.comp q) = Quiver.Path.addWeightOfEPs w p + Quiver.Path.addWeightOfEPs w q
-- Mathlib.GroupTheory.OrderOfElement
/-- Elements of finite order are closed under multiplication.  -/
IsOfFinOrder.mul : ∀ {G : Type u_1} [inst : CommMonoid G] {x y : G}, IsOfFinOrder x → IsOfFinOrder y → IsOfFinOrder (x * y)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instIsOrderedCancelAddMonoid : ∀ {ι : Type u_1} (α : ι → Type u_3) [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), IsOrderedCancelAddMonoid (α i)], IsOrderedCancelAddMonoid (Π₀ (i : ι), α i)
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.EStateM.adaptExcept.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s))
  (h_2 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s)),
  (match EStateM.Result.ok a s with
    | EStateM.Result.error e s => h_1 e s
    | EStateM.Result.ok a s => h_2 a s) =
    h_2 a s
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblenWith f o` is the `o`-th function in the Veblen hierarchy starting with `f`. This is
defined so that

- `veblenWith f 0 = f`.
- `veblenWith f o` for `o ≠ 0` enumerates the common fixed points of `veblenWith f o'` over all
  `o' < o`.
 -/
Ordinal.veblenWith : (Ordinal.{u} → Ordinal.{u}) → Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
-- Init.Data.Int.Lemmas
Int.sub_sub : ∀ (a b c : ℤ), a - b - c = a - (b + c)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instNoSuffixPatternModelForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.NoSuffixPatternModel p
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instAdd : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → Add (TruncatedWittVector p n R)
-- Init.Data.String.Basic
String.Pos.get.eq_1 : ∀ {s : String} (pos : s.Pos) (h : pos ≠ s.endPos), pos.get h = pos.toSlice.get ⋯
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_cexp_neg_mul_sq_norm : ∀ {b : ℂ} {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V],
  0 < b.re → ∫ (v : V), Complex.exp (-b * ↑‖v‖ ^ 2) = (↑Real.pi / b) ^ (↑(Module.finrank ℝ V) / 2)
-- Mathlib.Combinatorics.Additive.Dissociation
/-- If every dissociated subset of `s` has size at most `d`, then `s` is actually generated by a
subset of size at most `d`.

This is a dissociation analog of the fact that a set whose linearly independent subsets all have
size at most `d` is of dimension at most `d` itself.  -/
Finset.exists_subset_mulSpan_card_le_of_forall_mulDissociated : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {d : ℕ},
  (∀ s' ⊆ s, MulDissociated ↑s' → s'.card ≤ d) → ∃ s' ⊆ s, s'.card ≤ d ∧ s ⊆ s'.mulSpan
-- Lean.Compiler.ModPkgExt
Lean.ModuleEnvExtension.instInhabited : {σ : Type} → [Inhabited σ] → Inhabited (Lean.ModuleEnvExtension σ)
-- Init.Data.Int.Gcd
Int.zero_lcm : ∀ {a : ℤ}, Int.lcm 0 a = 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_insert_le_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp (t.insert k).min! t.min!).isLE = true
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_ne_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : α), SymAlg.sym a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.of_mulOpposite : ∀ {G : Type u} [inst : Mul G], UniqueProds Gᵐᵒᵖ → UniqueProds G
-- Lean.Linter.Init
Lean.Linter.logLint : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Option Bool → Lean.Syntax → Lean.MessageData → m Unit
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.dest_mk : ∀ {F : Type u → Type u} [q : QPF F] (x : F (QPF.Fix F)), (QPF.Fix.mk x).dest = x
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.buckets_withComputedSize : ∀ {α : Type u} {β : α → Type v} {self : Array (Std.DHashMap.Internal.AssocList α β)},
  (Std.DHashMap.Internal.withComputedSize self).buckets = self
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_le_sub_one_of_pos : ∀ {x : ℝ}, 0 < x → Real.log x ≤ x - 1
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_ιMulti : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ExteriorAlgebra.liftAlternating (ExteriorAlgebra.ιMulti R) = LinearMap.id
-- Std.Data.DHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.get? : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.DHashMap α β → (a : α) → Option (β a)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_one : ∀ {α : Type u_2} [inst : One α], Finset.map MulOpposite.opEquiv.toEmbedding 1 = 1
-- Mathlib.AlgebraicGeometry.Scheme
/-- The forgetful functor from `Scheme` to `Type`.  -/
AlgebraicGeometry.Scheme.forget : CategoryTheory.Functor AlgebraicGeometry.Scheme (Type u)
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.TAnchor : Type
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Adj.toSubgraph_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.toSubgraph = G.subgraphOfAdj h
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `HasProd f a L` means that the (potentially infinite) product of the `f b` for `b : β` converges
to `a` along the SummationFilter `L`.

By default `L` is the `unconditional` one, corresponding to the limit of all finite sets towards
the entire type. So we take the product over bigger and bigger finite sets. This product operation
is invariant under permuting the terms (while products for more general summation filters usually
are not).

For the definition and many statements, `α` does not need to be a topological monoid, only a monoid
with a topology (i.e. the multiplication is not assumed to be continuous). We only add this
assumption later, for the lemmas where it is relevant.

These are defined in an identical way to infinite sums (`HasSum`). For example, we say that
the function `ℕ → ℝ` sending `n` to `1 / 2` has a product of `0`, rather than saying that it does
not converge as some authors would.  -/
HasProd : {α : Type u_1} →
  {β : Type u_2} →
    [CommMonoid α] →
      [TopologicalSpace α] → (β → α) → α → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} (iso : E ≃ₗᵢ[𝕜] F), UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (⇑iso) s x = ↑↑iso
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If `p` is prime, then `cyclotomic p R = ∑ i ∈ range p, X ^ i`.  -/
Polynomial.cyclotomic_prime : ∀ (R : Type u_1) [inst : Ring R] (p : ℕ) [hp : Fact (Nat.Prime p)],
  Polynomial.cyclotomic p R = ∑ i ∈ Finset.range p, Polynomial.X ^ i
-- Lean.Meta.IndPredBelow
/-- Given `val` which corresponds to a constructor of a below inductive,
and `paramCount` which is the number of parameters in the real inductive,
return the indices of the fields corresponding to recursive calls.
 -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.belowRecIndices : Lean.ConstructorVal → ℕ → Lean.MetaM (Array (ℕ × ℕ))
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.lt_of_lt_of_le : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α}, a < b → b ≤ c → a < c
-- Batteries.Control.Nondet.Basic
/-- Convert an optional value to a nondeterministic value.  -/
Nondet.ofOption : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Option α → Nondet m α
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.Forget₂.createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.Forget₂.createsLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c hc =>
      have this := ⋯;
      have this := ⋯;
      have this_1 := this;
      have this_2 := this_1;
      {
        liftedCone :=
          {
            pt :=
              AddCommGrpCat.of
                (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommGrpCat))).pt,
            π :=
              {
                app := fun j =>
                  AddCommGrpCat.ofHom
                    (AddMonCat.limitπAddMonoidHom
                      (F.comp
                        ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp
                          (CategoryTheory.forget₂ AddGrpCat AddMonCat)))
                      j),
                naturality := ⋯ } },
        validLift :=
          (AddGrpCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).uniqueUpToIso hc,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful
            ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))
            (AddMonCat.HasLimits.limitConeIsLimit
              (F.comp
                ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))))
            (fun s =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp
                                    ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp
                                      (CategoryTheory.forget₂ AddGrpCat AddMonCat))).comp
                                (CategoryTheory.forget AddMonCat)).sections)
                        ⟨fun j =>
                          (CategoryTheory.ConcreteCategory.hom
                              (((CategoryTheory.forget AddMonCat).mapCone
                                      (((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp
                                            (CategoryTheory.forget₂ AddGrpCat AddMonCat)).mapCone
                                        s)).π.app
                                j))
                            v,
                          ⋯⟩,
                    map_zero' := ⋯, map_add' := ⋯ } })
            ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.continuousOn_one_add_mul_inv : ∀ {z : ℂ}, 1 + z ∈ Complex.slitPlane → ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.Icc 0 1)
-- Mathlib.Data.List.Basic
List.mem_getLast?_cons : ∀ {α : Type u} {x y : α} {l : List α}, x ∈ l.getLast? → x ∈ (y :: l).getLast?
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] (f : X →+ Y),
  AddCommGrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Init.Data.Array.Attach
Array.reverse_attach : ∀ {α : Type u_1} {xs : Array α},
  xs.attach.reverse =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.reverse.attach
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.copy_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α →ᵈ β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Data.Finset.PImage
Part.toFinset_some : ∀ {α : Type u_1} {a : α} [inst : Decidable (Part.some a).Dom], (Part.some a).toFinset = {a}
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.eq_5 : ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize✝ ByteArray.utf8DecodeChar?.FirstByte.threeMore = 4
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial.eq_1 : Nat.doubleFactorial 0 = 1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.diff_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t₁.diff t₂ = t₁ \ t₂
-- Mathlib.RingTheory.IdealFilter.Topology
instRingWithIdealFilter : {A : Type u_1} → [inst : Ring A] → (x : IdealFilter A) → Ring (WithIdealFilter x)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensorAddUnit_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.AddMon C)).X =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarRingEquiv_eq_coe : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B), e.toStarRingEquiv = ↑e
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_eq_headD_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α},
  t.minD fallback = t.toList.headD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `C` has biproducts of shape `J` if we have
a limit and a colimit, with the same cone points,
of every function `F : J → C`.  -/
CategoryTheory.Limits.HasBiproductsOfShape : Type w →
  (C : Type uC) → [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Init.Data.Order.Ord
Std.LawfulEqOrd.opposite : ∀ {α : Type u} [inst : Ord α] [Std.OrientedOrd α] [Std.LawfulEqOrd α], Std.LawfulEqOrd α
-- Init.Data.UInt.Basic
instPowUInt32Nat : Pow UInt32 ℕ
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.instReflectsIsomorphismsSheafSheafCompose : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] [F.ReflectsIsomorphisms],
  (CategoryTheory.sheafCompose J F).ReflectsIsomorphisms
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), f.comp (NonUnitalRingHom.id α) = f
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.instIsLeftAdjointFree : AddCommGrpCat.free.IsLeftAdjoint
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toList_valuesIter_eq_toList_map_snd : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β},
  m.valuesIter.toList = List.map Prod.snd m.toList
-- Mathlib.GroupTheory.Index
AddSubgroup.instFiniteIndexSumSum : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex] [K.FiniteIndex], (H.prod K).FiniteIndex
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointPullback : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (AlgebraicGeometry.Scheme.Modules.pullback f).IsLeftAdjoint
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DHashMap.Raw.Const.get! (m₁ ∪ m₂) k = Std.DHashMap.Raw.Const.get! m₂ k
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.comp_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G)
  {i j : E.I₀} (a : E.I₁ i j), (f.comp g).s₁ a = g.s₁ (f.s₁ a)
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.release : Std.Internal.UV.System.UnameInfo → String
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- If `v : ι → AbsoluteValue F ℝ` is a finite family of nontrivial, pairwise inequivalent
real absolute values on a field `F`, then the diagonal embedding
`algebraMap F ((i : ι) → WithAbs (v i))` has dense range.

This is the abstract weak approximation theorem; see
`NumberField.InfinitePlace.denseRange_algebraMap_pi` for the number-field special case.
 -/
AbsoluteValue.denseRange_algebraMap_pi : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [Finite ι] {v : ι → AbsoluteValue F ℝ},
  (∀ (i : ι), (v i).IsNontrivial) →
    (Pairwise fun i j => ¬(v i).IsEquiv (v j)) → DenseRange ⇑(algebraMap F ((i : ι) → WithAbs (v i)))