mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.MutualInductive
/-- Promote fixed indices to parameters.

The requirement for promotion is relatively strict. Given a constructor
```
Iᵢ.ctor p₁ … pₙ f₁ … fₘ : I p₁ … pₙ f₁ … fⱼ e₁ … eₖ
```
then the first `j` indices are potentially eligible for promotion to parameters.
Additionally, the fields must be definitionally equal across all constructors to be eligible for promotion.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.fixedIndicesToParams : ℕ → List Lean.InductiveType → Array Lean.Expr → Lean.MetaM ℕ
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β)
  (t : Finset γ) (f : β → γ → α), (s.inf fun b => t.inf (f b)) = t.inf fun c => s.inf fun b => f b c
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_desc_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i : ι) {Z : C}
  (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.desc φ α hα).f i) h) =
    CategoryTheory.CategoryStruct.comp (α.f i) h
-- Lean.Parser.Basic
/-- Treat keywords as identifiers.  -/
Lean.Parser.rawIdentFn : optParam Bool true → Lean.Parser.ParserFn
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.eq_def : ∀ (k : ℕ) (s : String) (p : s.Pos) (acc : ℕ),
  Lean.parseLowerHex?✝ k s p acc =
    match k with
    | 0 => some (p, acc)
    | k.succ =>
      if h : p = s.endPos then none
      else
        match Lean.fromHex?✝ (p.get h) with
        | some d => Lean.parseLowerHex?✝ k s (p.next h) (acc <<< 4 ||| d)
        | none => none
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBy.quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  {r : R}, Module.IsTorsionBy R M r → Module.IsTorsionBy R (M ⧸ N) r
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_hasPos_removePos : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment), ¬assignment.removePosAssignment.hasPosAssignment = true
-- Init.WF
PSigma.mkSkipLeft : ∀ {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α), s b₁ b₂ → PSigma.SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
-- Lean.Elab.Term.TermElabM
/-- Enable/disable implicit lambdas feature.  -/
Lean.Elab.Term.Context.implicitLambda : Lean.Elab.Term.Context → Bool
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Diffeomorph.image_interior : ∀ {𝕜 : 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'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ (Φ : Diffeomorph I I' M N n), ⇑Φ '' ModelWithCorners.interior M = ModelWithCorners.interior N
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.PrimeSpectrum.asIdeal_top : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : IsLocalRing R], ⊤.asIdeal = IsLocalRing.maximalIdeal R
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.Raw.ofList l cmp).getKey! k = default
-- Mathlib.Order.Hom.Bounded
BotHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β],
  BotHom.instFunLike = { coe := BotHom.toFun, coe_injective := ⋯ }
-- Mathlib.RingTheory.Teichmuller
/-- Given an `I`-adically **pre**complete ring `R`, where `p ∈ I`, this is the underlying function
of the Teichmüller map. It is defined as the limit of `p^n`-th powers of arbitrary lifts in `R` of
the `n`-th component from the perfection of `R ⧸ I`.

The simp NF is `teichmuller₀` when `R` is `I`-adically complete.  -/
Perfection.teichmullerFun : {p : ℕ} →
  [Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst : CommRing R] → {I : Ideal R} → [CharP (R ⧸ I) p] → [IsPrecomplete I R] → Perfection (R ⧸ I) p → R
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mk : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_3} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_4} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] → (domain : Submodule R E) → (↥domain →ₛₗ[σ] F) → E →ₛₗ.[σ] F
-- Mathlib.ModelTheory.Topology.Types
CompleteType.instTopologicalSpaceCompleteType : {L : FirstOrder.Language} → {T : L.Theory} → {α : Type u_1} → TopologicalSpace (T.CompleteType α)
-- Mathlib.Order.Comparable
not_incompRel_iff_symmGen : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, ¬IncompRel r a b ↔ Relation.SymmGen r a b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_iff : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, m[k]? = some v ↔ ∃ (h : k ∈ m), m[k] = v
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable.  -/
MeasureTheory.measurable_update_cylinderEvents' : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {i : ι} [inst : DecidableEq ι],
  Measurable fun p => Function.update p.1 i p.2
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_snd : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun p => p.2
-- Mathlib.Data.PNat.Prime
PNat.one_gcd : ∀ {n : ℕ+}, PNat.gcd 1 n = 1
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_mul_of_nonneg' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α],
  a ≤ b → c ≤ d → 0 ≤ c → 0 ≤ b → a * c ≤ b * d
-- Mathlib.Tactic.Translate.Core
/-- Loop through the prefixes of `n` to try to find a translation.
In such a case, we inherit the `relevantArg` option from the translation.  -/
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.findPrefixTranslation?.go : Mathlib.Tactic.Translate.TranslateData →
  Lean.Environment → Lean.Name → List String → Option Mathlib.Tactic.Translate.TranslationInfo
-- Mathlib.CategoryTheory.Galois.Basic
/-- `X` is not an initial object.  -/
CategoryTheory.PreGaloisCategory.IsConnected.notInitial : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {X : C}
  [self : CategoryTheory.PreGaloisCategory.IsConnected X] (a : CategoryTheory.Limits.IsInitial X), False
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Constants are well-ordered.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.const_sorted : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {c : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis c).Sorted
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindVEquiv_apply : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (A : Rep.{max u w, u, v} k G) (f : ↥(Representation.coindV φ A.ρ)),
  (Rep.coindVEquiv φ A) f =
    Rep.ofHom
      { toLinearMap := Finsupp.linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k), isIntertwining' := ⋯ }
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_mulVec : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R] [inst_1 : Fintype n₁]
  [inst_2 : Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v : n₁ ⊕ n₂ → R),
  (A₁.fromCols A₂).mulVec v = A₁.mulVec (v ∘ Sum.inl) + A₂.mulVec (v ∘ Sum.inr)
-- Lean.Parser.Basic
Lean.Parser.errorAtSavedPosFn : String → Bool → Lean.Parser.ParserFn
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invUnitsSub.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (u : Rˣ), PowerSeries.invUnitsSub u = PowerSeries.mk fun n => 1 /ₚ u ^ (n + 1)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- An arithmetic function is a function from `ℕ` that maps 0 to 0. In the literature, they are
often instead defined as functions from `ℕ+`. Multiplication on `ArithmeticFunctions` is by
Dirichlet convolution.  -/
ArithmeticFunction : (R : Type u_1) → [Zero R] → Type (max 0 u_1)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Being `C^n` is a local property.  -/
contMDiffOn_of_locally_contMDiffOn : ∀ {𝕜 : 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'} {s : Set M}
  {n : WithTop ℕ∞}, (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u)) → ContMDiffOn I I' n f s
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.X_ofNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (n : ℕ), CochainComplex.ConnectData.X K L ↑n = L.X n
-- Mathlib.Data.Finset.NAry
Finset.sup_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
  (t : Finset β) [inst_1 : SemilatticeSup δ] [inst_2 : OrderBot δ] (g : γ → δ),
  (Finset.image₂ f s t).sup g = s.sup fun x => t.sup fun x_1 => g (f x x_1)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- `Spec` as a locally ringed space  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.termSpec_ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coe_toContinuousMap : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (f : A →ₜ+ B), f.toContinuousMap = ↑f
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.checkBadRewrite : Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Init.Data.Vector.Lemmas
Vector.find?_mk : ∀ {α : Type} {n : ℕ} {xs : Array α} (h : xs.size = n) (f : α → Bool), Vector.find? f (Vector.mk xs h) = Array.find? f xs
-- Std.Http.Data.Response
/-- HTTP response structure parameterized by body type.
 -/
Std.Http.Response : Type → Type
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- An epimorphism is surjective.  -/
LinearMap.range_eq_top_of_cancel : ∀ {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  (∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v) → f.range = ⊤
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.dvd_appr_sub_appr : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (m n : ℕ), m ≤ n → p ^ m ∣ x.appr n - x.appr m
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.reverse.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode α),
  x.reverse =
    match x with
    | RBTree.RBNode.nil => RBTree.RBNode.nil
    | RBTree.RBNode.node c l v r => RBTree.RBNode.node c r.reverse v l.reverse
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModuleFunctor_obj : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R) (M : ModuleCat R),
  (ModuleCat.localizedModuleFunctor S).obj M = M.localizedModule S
-- Lean.Elab.Binders
Lean.Elab.Term.LetConfig.mk.sizeOf_spec : ∀ (nondep usedOnly zeta postponeValue generalize : Bool) (eq? : Option Lean.Ident),
  sizeOf
      { nondep := nondep, usedOnly := usedOnly, zeta := zeta, postponeValue := postponeValue, generalize := generalize,
        eq? := eq? } =
    1 + sizeOf nondep + sizeOf usedOnly + sizeOf zeta + sizeOf postponeValue + sizeOf generalize + sizeOf eq?
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_one : ∀ {α : Type u_1} [inst : BooleanRing α], toBoolAlg 1 = ⊤
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp_indexEquiv_apply : ∀ {ι : 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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7}
  {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
  [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
  {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (a : ι),
  (g.comp f).indexEquiv a = g.indexEquiv (f.indexEquiv a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).isEmpty = ((t.erase k).isEmpty && (f (t.get? k)).isNone)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.root.eq_1 : ∀ (self : Batteries.UnionFind) (x : Fin self.size),
  self.root x =
    if h : self.arr[↑x].parent = ↑x then x
    else
      have this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩
-- Mathlib.Data.Set.Sups
Set.Nonempty.of_infs_right : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α}, (s ⊼ t).Nonempty → t.Nonempty
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.pmap.match_1.eq_2 : ∀ {α : Type u_1} {p : α → Prop} (motive : (x : Option α) → (∀ (a : α), x = some a → p a) → Sort u_2) (a : α)
  (H : ∀ (a_1 : α), some a = some a_1 → p a_1) (h_1 : (x : ∀ (a : α), none = some a → p a) → motive none x)
  (h_2 : (a : α) → (H : ∀ (a_1 : α), some a = some a_1 → p a_1) → motive (some a) H),
  (match some a, H with
    | none, x => h_1 x
    | some a, H => h_2 a H) =
    h_2 a H
-- Init.Data.UInt.Basic
instNegUInt64 : Neg UInt64
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- If `legendreSym p a = -1` and `p` divides `x^2 - a*y^2`, then `p` must divide `x` and `y`.  -/
legendreSym.prime_dvd_of_eq_neg_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ℤ},
  legendreSym p a = -1 → ∀ {x y : ℤ}, ↑p ∣ x ^ 2 - a * y ^ 2 → ↑p ∣ x ∧ ↑p ∣ y
-- Init.Data.String.Basic
String.Pos.toReplaceStart : {s : String} → (p₀ pos : s.Pos) → p₀ ≤ pos → (s.sliceFrom p₀).Pos
-- Std.Data.DTreeMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.
 -/
Std.DTreeMap.insert : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → (a : α) → β a → Std.DTreeMap α β cmp
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.eq_of_eqOn_subfield_top : ∀ {K : Type u} [inst : DivisionRing K] {L : Type v} [inst_1 : Semiring L] {f g : K →+* L}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Init.Data.Nat.Basic
Nat.succ_le_iff : ∀ {m n : ℕ}, m.succ ≤ n ↔ m < n
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_idem : ∀ {α : Type u_1} (M : Matroid α) (R : Set α), (M.restrict R).restrict R = M.restrict R
-- Mathlib.Topology.ContinuousMap.Basic
/-- `IsQuotientMap.lift` as an equivalence.  -/
Topology.IsQuotientMap.liftEquiv : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            {f : C(X, Y)} → Topology.IsQuotientMap ⇑f → { g // Function.FactorsThrough ⇑g ⇑f } ≃ C(Y, Z)
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_empty : ∀ {α : Type u_1} (s s' : Set α), ∅.ite s s' = s'
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.one_fst : ∀ {q : ℕ}, 1.1 = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arcsin_eq_arctan : ∀ {x : ℝ}, x ∈ Set.Ioo (-1) 1 → Real.arcsin x = Real.arctan (x / √(1 - x ^ 2))
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.iUnion_left_iff : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} {ι : Sort u_3} [Countable ι]
  {s : ι → Set α}, MeasureTheory.AEDisjoint μ (⋃ i, s i) t ↔ ∀ (i : ι), MeasureTheory.AEDisjoint μ (s i) t
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F : C ⥤ D` commutes with shifts, this expresses the compatibility of `F.mapTriangle`
with the equivalences `Pretriangulated.triangleOpEquivalence` on `C` and `D`.
 -/
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                F.mapTriangle.op.comp (CategoryTheory.Pretriangulated.triangleOpEquivalence D).functor ≅
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.comp F.op.mapTriangle
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.isSupportedOutside₂_iff : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (K : HomologicalComplex C c), K.IsSupportedOutside e₂ ↔ K.IsSupported e₁
-- Mathlib.RingTheory.Support
Module.nonempty_support_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (Module.support R M).Nonempty ↔ Nontrivial M
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.eq_top_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S : StarSubalgebra R A},
  S = ⊤ ↔ ∀ (x : A), x ∈ S
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_iInter_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (E : Set α),
  Metric.cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), Metric.cthickening ε E
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.comp_liftNatTrans_assoc : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ F₃ : CategoryTheory.Functor C E) (F₁' F₂' F₃' : CategoryTheory.Functor D E)
  [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
  [h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) {Z : CategoryTheory.Functor D E}
  (h : F₃' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')) h
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/K` is finite dimensional, then `L` is a complete space with respect to topology induced
by the spectral norm.  -/
spectralNorm.completeSpace : ∀ (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]
  [h_fin : FiniteDimensional K L], CompleteSpace L
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.topEquiv_symm_apply_coe : ∀ {G : Type u_1} [inst : Group G] (x : G), ↑(Subgroup.topEquiv.symm x) = x
-- Mathlib.ModelTheory.PartialEquiv
/-- The equivalence between the two subdomains.  -/
FirstOrder.Language.PartialEquiv.toEquiv : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → (self : L.PartialEquiv M N) → L.Equiv ↥self.dom ↥self.cod
-- Mathlib.Data.Countable.Defs
Function.Injective.uncountable : ∀ {α : Sort u} {β : Sort v} [Uncountable α] {f : α → β}, Function.Injective f → Uncountable β
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β),
  f.comp (FrameHom.id α) = f
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.extension_property : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] {P : Type u_6} [inst_6 : AddCommGroup P]
  [inst_7 : Module R P] (f : N →ₗ[R] M), Function.Injective ⇑f → ∀ (g : N →ₗ[R] P), ∃ h, h ∘ₗ f = g
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  {F G : CategoryTheory.Functor (A ⊕ A') B}
  (η₁ : (CategoryTheory.Sum.inl_ A A').comp F ⟶ (CategoryTheory.Sum.inl_ A A').comp G)
  (η₂ : (CategoryTheory.Sum.inr_ A A').comp F ⟶ (CategoryTheory.Sum.inr_ A A').comp G) (X : A ⊕ A'),
  (CategoryTheory.Sum.natTransOfWhiskerLeftInlInr η₁ η₂).app X =
    CategoryTheory.CategoryStruct.comp (((CategoryTheory.Sum.functorEquiv A A' B).unit.app F).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.sum' η₁ η₂).app X)
        (((CategoryTheory.Sum.functorEquiv A A' B).unitInv.app G).app X))
-- Mathlib.Tactic.Push
/-- Common entry point to the implementation of `push`.  -/
Mathlib.Tactic.Push.pushCore : Mathlib.Tactic.Push.Head →
  Mathlib.Tactic.Push.Config → Option Lean.Meta.Simp.Discharge → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.PrepareRenameParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1