mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Choose
/-- A loop around `choose1`. The main entry point for the `choose` tactic.  -/
Mathlib.Tactic.Choose.elabChoose : Bool →
  Option Lean.Expr →
    List Mathlib.Tactic.Choose.ChooseArg →
      Mathlib.Tactic.Choose.ElimStatus → Lean.MVarId → Lean.Elab.TermElabM Lean.MVarId
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t hl =
    if Std.DTreeMap.Internal.Impl.contains k t = true then
      (true, { impl := t, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ })
    else (false, Std.DTreeMap.Internal.Impl.insert k v t ⋯)
-- Mathlib.Topology.GDelta.Basic
IsGδ.biInter_of_isOpen : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {I : Set ι},
  I.Countable → ∀ {f : ι → Set X}, (∀ i ∈ I, IsOpen (f i)) → IsGδ (⋂ i ∈ I, f i)
-- Mathlib.Logic.Equiv.Prod
/-- The function type `Bool → α` is equivalent to `α × α`.  -/
Equiv.boolArrowEquivProd : (α : Type u_9) → (Bool → α) ≃ α × α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The right fraction from `X` to `Y` given by a morphism `f : X ⟶ Y`.  -/
CategoryTheory.MorphismProperty.RightFraction.ofHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) → {X Y : C} → (X ⟶ Y) → [W.ContainsIdentities] → W.RightFraction X Y
-- Mathlib.Logic.Equiv.Prod
/-- The type of functions on a sum type `α ⊕ β` is equivalent to the type of pairs of functions
on `α` and on `β`.  -/
Equiv.sumArrowEquivProdArrow : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → (α ⊕ β → γ) ≃ (α → γ) × (β → γ)
-- Init.Data.Vector.Lemmas
Vector.append_inj_right : ∀ {α : Type u_1} {n m : ℕ} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → ys₁ = ys₂
-- Lean.Elab.Tactic.Omega.Core
/-- The ground assumptions that the algorithm starts from.  -/
Lean.Elab.Tactic.Omega.Problem.assumptions : Lean.Elab.Tactic.Omega.Problem → Array Lean.Elab.Tactic.Omega.Proof
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupCohomologyIsoOdd.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i),
  Rep.FiniteCyclicGroup.groupCohomologyIsoOdd A g hg i hi = Rep.FiniteCyclicGroup.groupCohomologyIsoOdd A g hg i hi
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.isEmpty_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_eq_zero_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E}, e x = 0 ↔ x = 0
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.instTrivialStar : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Star β]
  [inst_3 : ContinuousStar β] [TrivialStar β], TrivialStar C(α, β)
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate : Type
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.go.eq_1 : ∀ (acc : String) (s a : String.Slice) (as : List String.Slice),
  String.Slice.intercalate.go✝ acc s (a :: as) = String.Slice.intercalate.go✝ (acc ++ s ++ a) s as
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_zero_inj : ∀ {o₁ o₂ : Ordinal.{u}}, Ordinal.veblen o₁ 0 = Ordinal.veblen o₂ 0 ↔ o₁ = o₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Since `Truncated.inclusion` is fully faithful, so is left Kan extension along it.  -/
CategoryTheory.SimplicialObject.Truncated.sk.fullyFaithful : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [inst_1 :
          ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] →
        [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
              (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] →
          (CategoryTheory.SimplicialObject.Truncated.sk n).FullyFaithful
-- Mathlib.Topology.Constructible
IsRetrocompact.inter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X} [T2Space X],
  IsRetrocompact s → IsRetrocompact t → IsRetrocompact (s ∩ t)
-- Mathlib.Algebra.Group.Basic
sub_sub_sub_cancel_left : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), c - a - (c - b) = b - a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {fallback : β} {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k' fallback =
    if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
    else Std.DTreeMap.Internal.Impl.Const.getD t k' fallback
-- Mathlib.Analysis.Seminorm
Seminorm.comp_add_le : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f g : E →ₛₗ[σ₁₂] E₂),
  p.comp (f + g) ≤ p.comp f + p.comp g
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instInfSet : {V : Type u} → {G : SimpleGraph V} → InfSet G.Subgraph
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.filter.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] (f f_1 : α → Bool),
  f = f_1 → ∀ (m m_1 : Std.ExtHashSet α), m = m_1 → Std.ExtHashSet.filter f m = Std.ExtHashSet.filter f_1 m_1
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_inj : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : M),
  (TensorAlgebra.ι R) x = (TensorAlgebra.ι R) y ↔ x = y
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.op_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (h : G ⊣ F),
  h.op.unit = CategoryTheory.NatTrans.op h.counit
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.mk.sizeOf_spec : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c}
  [inst_2 : SizeOf ι] [inst_3 : SizeOf V] (f : (i : ι) → A.X i ⟶ B.X i)
  (comm' :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f j))
      HomologicalComplex.Hom.comm'._autoParam),
  sizeOf { f := f, comm' := comm' } = 1
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- Group-like elements over a domain are linearly independent.  -/
linearIndep_groupLikeVal : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup A] [inst_3 : Module R A]
  [inst_4 : Coalgebra R A] [Module.IsTorsionFree R A], LinearIndependent R GroupLike.val
-- Init.Data.UInt.Lemmas
UInt8.ofNat_finVal : ∀ (n : Fin UInt8.size), UInt8.ofNat ↑n = UInt8.ofFin n
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMinOrderElemIoc : ∀ (α : Type u_1) [inst : Preorder α] [DenselyOrdered α] {x y : α}, NoMinOrder ↑(Set.Ioc x y)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_compl : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_univ_pi : ∀ (ι : Type u_5) [inst : Fintype ι], dimH Set.univ = ↑(Fintype.card ι)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.centeredArc_mono : ∀ {r s : ℝ}, r ≤ s → Circle.centeredArc r ⊆ Circle.centeredArc s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.covariant_sequence_exact₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ {n : ℕ} (x₂ : CategoryTheory.Abelian.Ext X S.X₂ n),
      x₂.comp (CategoryTheory.Abelian.Ext.mk₀ S.g) ⋯ = 0 → ∃ x₁, x₁.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) ⋯ = x₂
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (k : K) (f : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.pop k f q, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_3 k f q v S
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → m.size = m_1.size
-- Mathlib.Data.Sum.Order
/-- `toLex` promoted to a `RelIso` between `≤` relations.  -/
Sum.Lex.toLexRelIsoLE : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LE α] → [inst_1 : LE β] → (Sum.Lex (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) ≃r fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.le_topologicalClosure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] (s : AddSubgroup G),
  s ≤ s.topologicalClosure
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The commutativity property of the subgroups  -/
MulAction.IwasawaStructure.is_comm : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] (self : MulAction.IwasawaStructure M α)
  (x : α), IsMulCommutative ↥(self.T x)
-- Std.Time.Date.Unit.Weekday
/-- Converts a `Nat` to an `Option Weekday`.
 -/
Std.Time.Weekday.ofNat? : ℕ → Option Std.Time.Weekday
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_erase_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α}, (m.erase k).get? k = none
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_of_lt_skipWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos pos' : s.Pos},
  pos ≤ pos' → ∀ (h₂ : pos' < pos.skipWhile P), P (pos'.get ⋯)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mem_bot_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {x : M}, x ∈ ⊥ ↔ IsUnit x
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.indName : Lean.Meta.SparseCasesOnKey✝ → Lean.Name
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, a ∉ m → m.getKeyD a fallback = fallback
-- Init.Prelude
/-- A (named) unary parser, like `group(p)`  -/
Lean.ParserDescr.unary : Lean.Name → Lean.ParserDescr → Lean.ParserDescr
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_symm_apply_proj : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (a : B × F),
  (↑(Bundle.Trivial.trivialization B F).symm a).proj = a.1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceIsAlphaNum : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build an isomorphism in the category `AddCommMonCat`
from an `AddEquiv` between `AddCommMonoid`s.  -/
AddEquiv.toAddCommMonCatIso : {X Y : Type u} →
  [inst : AddCommMonoid X] → [inst_1 : AddCommMonoid Y] → X ≃+ Y → (AddCommMonCat.of X ≅ AddCommMonCat.of Y)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiableAt_mul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I 1 G] {a b : G},
  (MDiffAt fun x => x * a) b
-- Mathlib.Order.RelSeries
RelSeries.insertNth_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin p.length) (a : α)
  (prev_connect : (p.toFun i.castSucc, a) ∈ r) (connect_next : (a, p.toFun i.succ) ∈ r),
  (p.insertNth i a prev_connect connect_next).length = p.length + 1
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coneOfDiagramTerminal.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX hX_1 : CategoryTheory.Limits.IsTerminal X),
  hX = hX_1 →
    ∀ (F : CategoryTheory.Functor J C) [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
      CategoryTheory.Limits.coneOfDiagramTerminal hX F = CategoryTheory.Limits.coneOfDiagramTerminal hX_1 F
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- This lemma relates `weightedTotalDegree` and `weightedTotalDegree'`.  -/
MvPolynomial.weightedTotalDegree_coe : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M) (p : MvPolynomial σ R),
  p ≠ 0 → MvPolynomial.weightedTotalDegree' w p = ↑(MvPolynomial.weightedTotalDegree w p)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instRpcEncodableStrictOrLazy : {α β : Type} →
  [Lean.Server.RpcEncodable α] → [Lean.Server.RpcEncodable β] → Lean.Server.RpcEncodable (Lean.Widget.StrictOrLazy α β)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.keys_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a}, (Std.ExtDTreeMap.map f t).keys = t.keys
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `MDifferentiableAt` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabMDifferentiableAt : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Rat.Basic
/-- Embedding of `Int` in the rational numbers.  -/
Rat.ofInt : ℤ → ℚ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K` a number field.
The images of `x` by the embeddings of `K` in `A` are exactly the roots in `A` of
the minimal polynomial of `x` over `ℚ`.  -/
NumberField.Embeddings.range_eval_eq_rootSet_minpoly : ∀ (K : Type u_1) (A : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : Field A] [inst_3 : Algebra ℚ A]
  [IsAlgClosed A] (x : K), (Set.range fun φ => φ x) = (minpoly ℚ x).rootSet A
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.levelParams : Lean.Meta.Sym.Pattern → List Lean.Name
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.mk : Lean.Lsp.SignatureHelpTriggerKind → Option String → Bool → Option Lean.Lsp.SignatureHelp → Lean.Lsp.SignatureHelpContext
-- Mathlib.Analysis.Matrix.PosDef
Matrix.PosSemidef.re_dotProduct_nonneg : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜},
  A.PosSemidef → ∀ (x : n → 𝕜), 0 ≤ RCLike.re (star x ⬝ᵥ A.mulVec x)
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsOpenImmersion f] (g : Y ⟶ Z) [inst_1 : AlgebraicGeometry.LocallyOfFiniteType g],
  AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus (CategoryTheory.CategoryStruct.comp f g) =
    (TopologicalSpace.Opens.map f.base).obj (AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus g)
-- Mathlib.GroupTheory.QuotientGroup.Finite
AddGroup.fintypeOfDomOfCoker.eq_1 : ∀ {F : Type u_1} {G : Type u_2} [inst : AddGroup F] [inst_1 : AddGroup G] [inst_2 : Fintype F] (f : F →+ G)
  [inst_3 : f.range.Normal] [inst_4 : Fintype (G ⧸ f.range)],
  AddGroup.fintypeOfDomOfCoker f = AddGroup.fintypeOfKerLeRange f (QuotientAddGroup.mk' f.range) ⋯
-- Init.Data.UInt.Lemmas
UInt32.sub_add_cancel : ∀ (a b : UInt32), a - b + b = a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k km : α} (hc : k ∈ t), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {c : RBTree.RBColor} {n : ℕ} {v v' : α} [Std.TransCmp cmp]
  {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.Ordered cmp t →
      (v' ∈ RBTree.RBNode.insert cmp t v ↔ v' ∈ t ∧ RBTree.RBNode.find? (cmp v) t ≠ some v' ∨ v' = v)
-- Mathlib.Control.Bifunctor
Bifunctor.snd_comp_fst : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁}
  (f : α₀ → α₁) (f' : β₀ → β₁), Bifunctor.snd f' ∘ Bifunctor.fst f = bimap f f'
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.gradedAddHom.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_4 : AddSubmonoidClass σ A]
  [inst_5 : AddSubmonoidClass τ B] (f : 𝒜 →+*ᵍ ℬ) (i : ι),
  f.gradedAddHom i = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_conj : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  (σ * τ * σ⁻¹).support.card = τ.support.card
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_add_one_sub_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R],
  Int.fract a ≠ 0 → ↑⌈a⌉ = a + 1 - Int.fract a
-- Mathlib.RingTheory.MvPolynomial.Groebner
MonomialOrder.reduce.congr_simp : ∀ {σ : Type u_1} (m m_1 : MonomialOrder σ) (e_m : m = m_1) {R : Type u_2} [inst : CommRing R] {b b_1 : MvPolynomial σ R}
  (e_b : b = b_1) (hb : IsUnit (m.leadingCoeff b)) (f f_1 : MvPolynomial σ R),
  f = f_1 → m.reduce hb f = m_1.reduce ⋯ f_1
-- Init.Data.Order.MinMaxOn
minOn_self : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α}, minOn f x x = x
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.sub_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂), (φ - φ').τ₁ = φ.τ₁ - φ'.τ₁
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- A vector is in `(𝕜 ∙ u)ᗮ` iff it is orthogonal to `u`.  -/
Submodule.mem_orthogonal_singleton_iff_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {u v : E}, v ∈ (𝕜 ∙ u)ᗮ ↔ inner 𝕜 u v = 0
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α), PMF.map f p = p.bind (PMF.pure ∘ f)
-- Mathlib.Topology.MetricSpace.Isometry
/-- `Equiv.funUnique` as an `IsometryEquiv`.  -/
IsometryEquiv.funUnique : (ι : Type u_2) → (α : Type u) → [inst : PseudoEMetricSpace α] → [Unique ι] → [inst_2 : Fintype ι] → (ι → α) ≃ᵢ α
-- Mathlib.RingTheory.Congruence.Star
ringConGen_star : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] {r : R → R → Prop},
  (∀ (a b : R), r a b → r (star a) (star b)) → ∀ ⦃a b : R⦄, (ringConGen r) a b → (ringConGen r) (star a) (star b)
-- Mathlib.Order.Interval.Set.Monotone
iUnion_Ioo_of_mono_of_isGLB_of_isLUB : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : LinearOrder β] {f g : α → β} {a b : β},
  Antitone f → Monotone g → IsGLB (Set.range f) a → IsLUB (Set.range g) b → ⋃ x, Set.Ioo (f x) (g x) = Set.Ioo a b
-- Init.Data.Array.Lemmas
Array.extract_empty : ∀ {α : Type u_1} {start stop : ℕ}, #[].extract start stop = #[]
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_finite : ∀ {α : Type u_1} {M : Matroid α} {D : Set α} [M.Finite], (M.delete D).Finite
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.coe_iSup_of_directed : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Type u_4}
  [Nonempty ι] {K : ι → Subalgebra R A}, Directed (fun x1 x2 => x1 ≤ x2) K → ↑(iSup K) = ⋃ i, ↑(K i)
-- Mathlib.Data.Fin.Tuple.Sort
/-- `graphEquiv₂ f` is an equivalence between `Fin n` and `graph f` that respects the order.
 -/
Tuple.graphEquiv₂ : {n : ℕ} → {α : Type u_1} → [inst : LinearOrder α] → (f : Fin n → α) → Fin n ≃o ↥(Tuple.graph f)
-- Mathlib.NumberTheory.Niven
/-- Niven's theorem, giving the possible angles for `θ` in the range `0 .. π`.  -/
niven_angle_eq : ∀ {θ : ℝ},
  (∃ r, θ = ↑r * Real.pi) →
    (∃ q, Real.cos θ = ↑q) → θ ∈ Set.Icc 0 Real.pi → θ ∈ {0, Real.pi / 3, Real.pi / 2, Real.pi * (2 / 3), Real.pi}
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.gcdCoeffs.eq_2 : ∀ (x k' : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k' v p).gcdCoeffs x = p.gcdCoeffs ↑(k'.gcd x)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_ric_eq_self : ∀ {n i fallback : ℕ}, i ≤ n → (*...=n).toArray.getD i fallback = i
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_eq_of_equiv : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.supportDim R M = Module.supportDim R N
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_id_of_epi : ∀ {x : SimplexCategory} (i : x ⟶ x) [CategoryTheory.Epi i], i = CategoryTheory.CategoryStruct.id x