mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_eq_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, a ∉ m → m.getKey! a = default
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α},
  t.size ≤ (Std.DTreeMap.Const.insertManyIfNewUnit t l).size
-- Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
/-- A function `f` is summable in a uniform additive group `α` if and only if it is summable in
`Completion α` and its sum in `Completion α` lies in the range of `toCompl : α →+ Completion α`.  -/
summable_iff_summable_compl_and_tsum_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : IsUniformAddGroup α]
  {L : SummationFilter β} (f : β → α),
  Summable f L ↔
    Summable (⇑UniformSpace.Completion.toCompl ∘ f) L ∧
      ∑'[L] (i : β), UniformSpace.Completion.toCompl (f i) ∈ Set.range ⇑UniformSpace.Completion.toCompl
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.Monic.natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → (p.natDegree = 0 ↔ p = 1)
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.submoduleComap_surjective_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (q : Submodule R₂ M₂), Function.Surjective ⇑f → Function.Surjective ⇑(f.submoduleComap q)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.entryAtIdx_eq_getElem : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} (htb : t.Balanced) {i : ℕ} {h : i < t.size},
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx t htb i h = (t.toListModel[i].fst, t.toListModel[i].snd)
-- Init.Data.Nat.Gcd
Nat.pow_gcd_pow : ∀ {k n m : ℕ}, (n ^ k).gcd (m ^ k) = n.gcd m ^ k
-- Init.Data.Int.OfNat
Int.Nonneg.div : ∀ (a b : ℤ), a ≥ 0 → b ≥ 0 → a / b ≥ 0
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.div_mul_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`.  -/
ENNReal.div_mul_cancel' : ∀ {a b : ENNReal}, (a = 0 → b = 0) → (a = ⊤ → b = 0) → b / a * a = b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonColor : Lean.ToJson Lean.Lsp.Color
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed
set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e.  points
to `s`, then the expected value of `g ∘ f` is less than or equal to the value of `g` at the expected
value of `f` provided that both `f` and `g ∘ f` are integrable.  -/
ConcaveOn.le_map_integral : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  ConcaveOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ → ∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)
-- Std.Http.Data.URI.Basic
/-- The optional encoded password.
 -/
Std.Http.URI.UserInfo.password : Std.Http.URI.UserInfo → Option Std.Http.URI.EncodedUserInfo
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_le_toIcoMod_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b ≤ toIcoMod hp a b + p
-- Mathlib.Data.Fintype.Sort
/-- If `α` is a linearly ordered fintype, `s : Finset α` has cardinality `m` and its complement has
cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of `Fin m` to
elements of `s` and elements of `Fin n` to elements of `sᶜ` while preserving order on each
"half" of `Fin m ⊕ Fin n` (using `Set.orderIsoOfFin`).  -/
finSumEquivOfFinset : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → [LinearOrder α] → {m n : ℕ} → {s : Finset α} → s.card = m → sᶜ.card = n → Fin m ⊕ Fin n ≃ α
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.continuous_precomp : ∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] (f : A ⟶ B),
  Continuous fun x => CategoryTheory.CategoryStruct.comp f x
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- **Krull's principal ideal theorem** (also known as **Krullscher Hauptidealsatz**) :
In a commutative Noetherian ring `R`, any prime ideal that is minimal over a principal ideal
has height at most 1.  -/
Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R) [Submodule.IsPrincipal I],
  ∀ p ∈ I.minimalPrimes, p.height ≤ 1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.mono : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∀ {t : Set α}, t ⊆ s → BoundedVariationOn f t
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasInitialChangeDiagram : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C}
  {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C},
  CategoryTheory.Limits.HasColimit F₁ → CategoryTheory.Limits.HasColimit F₂
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.zsmulFn : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.Order.WithBot
WithBot.map₂_coe_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : WithBot β),
  WithBot.map₂ f (↑a) b = WithBot.map (fun b => f a b) b
-- Lean.Compiler.IR.Basic
Lean.IR.DeclInfo.mk.inj : ∀ {sorryDep? sorryDep?_1 : Option Lean.Name},
  { sorryDep? := sorryDep? } = { sorryDep? := sorryDep?_1 } → sorryDep? = sorryDep?_1
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] {x : CompleteLattice β},
  sSupHom.instBot = { bot := { toFun := fun x_1 => ⊥, map_sSup' := ⋯ } }
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- The restriction `End(L/K) → End(B/A)` in an AKLB setup.
Also see `galRestrict` for the `AlgEquiv` version.  -/
galRestrictHom : (A : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      (B : Type u_6) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] →
              [inst_3 : Field K] →
                [inst_4 : Field L] →
                  [inst_5 : Algebra A K] →
                    [IsFractionRing A K] →
                      [inst_7 : Algebra K L] →
                        [inst_8 : Algebra A L] →
                          [IsScalarTower A K L] →
                            [inst_10 : Algebra B L] →
                              [IsScalarTower A B L] →
                                [IsIntegralClosure B A L] → [Algebra.IsAlgebraic K L] → (L →ₐ[K] L) ≃* (B →ₐ[A] B)
-- Init.Data.Nat.Lcm
Nat.le_lcm_left : ∀ {n : ℕ} (m : ℕ), 0 < n → m ≤ m.lcm n
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instNSMul.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G], ContMDiffMap.instNSMul = { smul := fun n_1 f => ⟨n_1 • ⇑f, ⋯⟩ }
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The proposition that two elements of a quadratic map space are orthogonal.  -/
QuadraticMap.IsOrtho : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → QuadraticMap R M N → M → M → Prop
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orElim'.inj : ∀ {p₁ : Mathlib.Tactic.ITauto.Proof} {x : Lean.Name} {p₂ p₃ p₁_1 : Mathlib.Tactic.ITauto.Proof} {x_1 : Lean.Name}
  {p₂_1 p₃_1 : Mathlib.Tactic.ITauto.Proof},
  p₁.orElim' x p₂ p₃ = p₁_1.orElim' x_1 p₂_1 p₃_1 → p₁ = p₁_1 ∧ x = x_1 ∧ p₂ = p₂_1 ∧ p₃ = p₃_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.maxEntryD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntryD fallback = t₂.maxEntryD fallback
-- Mathlib.Data.Set.Restrict
Set.MapsTo.restrict_surjective_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
  Function.Surjective (Set.MapsTo.restrict f s t h) ↔ Set.SurjOn f s t
-- Mathlib.Data.List.NatAntidiagonal
List.Nat.antidiagonal_succ_succ' : ∀ {n : ℕ},
  List.Nat.antidiagonal (n + 2) =
    (0, n + 2) :: List.map (Prod.map Nat.succ Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 2, 0)]
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeq.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Fin.Bitwise
Fin.or_val_of_uInt32Size : ∀ (a b : Fin UInt32.size), ↑(a ||| b) = ↑a ||| ↑b
-- Mathlib.RingTheory.WittVector.Complete
_private.Mathlib.RingTheory.WittVector.Complete.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exact._auto_3),
  (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- Given `f : E →L[𝕜] E'`, construct the continuous sesquilinear form `fun x y ↦ ⟪x, A y⟫`, given
as a continuous linear map.  -/
ContinuousLinearMap.toSesqForm : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {E' : Type u_4} →
            [inst_3 : SeminormedAddCommGroup E'] →
              [inst_4 : InnerProductSpace 𝕜 E'] → (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.prod_fst : ∀ (ι : Type w) (self : ι × ι), (CategoryTheory.Limits.MulticospanShape.prod ι).fst self = self.1
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqUserInfo : BEq Std.Http.URI.UserInfo
-- Init.PropLemmas
and_and_and_comm : ∀ {a b c d : Prop}, (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' Y'' Z'' X'' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'}
  {f'' : Y'' ⟶ X''} {g'' : Z'' ⟶ X''} [inst_2 : CategoryTheory.ChosenPullbacksAlong g']
  [inst_3 : CategoryTheory.ChosenPullbacksAlong g''] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} {δ₁ : Y'' ⟶ Y'}
  {δ₂ : Z'' ⟶ Z'} {δ₃ : X'' ⟶ X'}
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_3)
  (comm₁' :
    autoParam (CategoryTheory.CategoryStruct.comp f'' δ₃ = CategoryTheory.CategoryStruct.comp δ₁ f')
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_5)
  (comm₂' :
    autoParam (CategoryTheory.CategoryStruct.comp g'' δ₃ = CategoryTheory.CategoryStruct.comp δ₂ g')
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_7),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.pullbackMap f' g' f'' g'' δ₁ δ₂ δ₃ comm₁' comm₂')
      (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) =
    CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f'' g'' (CategoryTheory.CategoryStruct.comp δ₁ γ₁)
      (CategoryTheory.CategoryStruct.comp δ₂ γ₂) (CategoryTheory.CategoryStruct.comp δ₃ γ₃) ⋯ ⋯
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionBase.solution_spec : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : IsAlgClosed k] (a₁ a₂ : WittVector p k),
  WittVector.RecursionBase.solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasis_gen : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0), (AdjoinRoot.powerBasis hf).gen = AdjoinRoot.root f
-- Mathlib.Order.Fin.Basic
Fin.natAddOrderEmb_apply : ∀ {m : ℕ} (n : ℕ) (i : Fin m), (Fin.natAddOrderEmb n) i = Fin.natAdd n i
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toLinearOrder_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [inst_1 : LinearOrder ι]
  (j : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L), I.toLinearOrder.snd j = I.snd ↑j
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_mul_right : ∀ {α : Type u_2} [inst : Mul α] [IsRightCancelMul α] [inst_2 : DecidableEq α] {s t : Finset α},
  t.Nonempty → s.card ≤ (s * t).card
-- Init.Data.List.Perm
List.cons_append_cons_perm : ∀ {α : Type u_1} {a b : α} {as bs : List α}, (a :: as ++ b :: bs).Perm (b :: as ++ a :: bs)
-- Init.Data.UInt.Lemmas
UInt32.lt_or_lt_of_ne : ∀ {a b : UInt32}, a ≠ b → a < b ∨ b < a
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Composition by a fixed left argument as a group homomorphism  -/
CategoryTheory.Preadditive.leftComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {P Q : C} → (R : C) → (P ⟶ Q) → (Q ⟶ R) →+ (P ⟶ R)
-- Mathlib.Topology.Bornology.Absorbs
Set.Finite.absorbs_biInter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α] {t : Set α}
  {ι : Type u_3} {I : Set ι}, I.Finite → ∀ {s : ι → Set α}, Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t
-- Mathlib.Topology.Constructible
/-- A retrocompact set is a set whose intersection with every compact open is compact.  -/
IsRetrocompact : {X : Type u_2} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indicator_indepFun_pi_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [inst_4 : Fintype S]
  [MeasureTheory.IsProbabilityMeasure P] {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ),
          ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) (fun ω s => X s ω) P
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (e : T ≅ T')
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₃ = e.hom.hom₃
-- Mathlib.Algebra.Group.End
AddAutAdditive_apply_symm_apply : ∀ (G : Type u_3) [inst : Group G] (a : Additive G ≃+ Additive G) (a_1 : G),
  (MulEquiv.symm ((AddAutAdditive G) a)) a_1 = Additive.toMul (a.symm (Additive.ofMul a_1))
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A partial isomorphism from `X` to `Y` is an isomorphism between dense open subschemes
of `X` and `Y`.  -/
AlgebraicGeometry.Scheme.PartialIso : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.symm_le_symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N}, f ≤ g → f.symm ≤ g.symm
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (δ : Type u_5) [inst : MeasurableSpace δ] (κ : ProbabilityTheory.Kernel α (β × γ)),
  (ProbabilityTheory.Kernel.prodMkLeft δ κ).fst = ProbabilityTheory.Kernel.prodMkLeft δ κ.fst
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform.subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addDysonETransform e x).1 + (Finset.addDysonETransform e x).2 ⊆ x.1 + x.2
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mk : {R : Type u} →
  [inst : NonAssocSemiring R] →
    (toSubmonoid : Submonoid R) →
      (∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier) →
        0 ∈ toSubmonoid.carrier → Subsemiring R
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.MorphismProperty D} [P.ContainsIdentities] (F : CategoryTheory.Functor C D),
  (P.inverseImage F).ContainsIdentities
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- Creates a partition from a coloring.  -/
SimpleGraph.Coloring.toPartition : {V : Type u} → {G : SimpleGraph V} → {α : Type v} → G.Coloring α → G.Partition
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.GoodProducts.eval C ∘ (Profinite.NobelingProof.GoodProducts.sum_equiv C hsC ho).toFun =
    Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l => Profinite.NobelingProof.Products.eval C ↑l
-- Mathlib.RingTheory.Congruence.Hom
/-- The **second isomorphism theorem for algebras**.  -/
RingCon.comapQuotientEquivRangeₐ : {M : Type u_1} →
  {N : Type u_2} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring M] →
          [inst_2 : Algebra R M] →
            [inst_3 : Semiring N] →
              [inst_4 : Algebra R N] →
                (c : RingCon M) →
                  (f : N →ₐ[R] M) → {d : RingCon N} → d = c.comap f → d.Quotient ≃ₐ[R] ↥((RingCon.mkₐ R c).comp f).range
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instFunLike.eq_1 : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousMonoidHom.instFunLike = { coe := fun f => (↑f.toMonoidHom).toFun, coe_injective := ⋯ }
-- Mathlib.Analysis.Normed.Field.Basic
/-- The distance is induced by the norm.  -/
NormedDivisionRing.dist_eq : ∀ {α : Type u_5} [self : NormedDivisionRing α] (x y : α), dist x y = ‖-x + y‖
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprod_mulSingle : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)} [inst_3 : DecidableEq ι] (i : ι)
  (y : N i), (MonoidHom.noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = (ϕ i) y
-- Mathlib.RingTheory.Finiteness.Basic
/-- A submodule is finite as a module iff it is finitely generated.  -/
Module.Finite.iff_fg : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, Module.Finite R ↥N ↔ N.FG
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P Q : Fin 3 → R),
  W'.addX P Q =
    -P 0 * Q 1 ^ 2 * P 2 + Q 0 * P 1 ^ 2 * Q 2 - 2 * P 0 * P 1 * Q 1 * Q 2 + 2 * Q 0 * P 1 * Q 1 * P 2 -
                            W'.a₁ * P 0 ^ 2 * Q 1 * Q 2 +
                          W'.a₁ * Q 0 ^ 2 * P 1 * P 2 +
                        W'.a₂ * P 0 ^ 2 * Q 0 * Q 2 -
                      W'.a₂ * P 0 * Q 0 ^ 2 * P 2 -
                    W'.a₃ * P 0 * P 1 * Q 2 ^ 2 +
                  W'.a₃ * Q 0 * Q 1 * P 2 ^ 2 -
                2 * W'.a₃ * P 0 * Q 1 * P 2 * Q 2 +
              2 * W'.a₃ * Q 0 * P 1 * P 2 * Q 2 +
            W'.a₄ * P 0 ^ 2 * Q 2 ^ 2 -
          W'.a₄ * Q 0 ^ 2 * P 2 ^ 2 +
        3 * W'.a₆ * P 0 * P 2 * Q 2 ^ 2 -
      3 * W'.a₆ * Q 0 * P 2 ^ 2 * Q 2
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_ne_zero_iff_nonempty : ∀ (α : Type u_3), ENat.card α ≠ 0 ↔ Nonempty α
-- Mathlib.Analysis.Complex.RealDeriv
Complex.differentiable_conj : Differentiable ℝ ⇑(starRingEnd ℂ)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.quot_liftOn_mk : ∀ {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β)
  (H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂ → f L₁ = f L₂),
  Quot.liftOn (FreeAddGroup.mk L) f H = f L
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.ExtHashMap.filter f m},
  (Std.ExtHashMap.filter f m).getKey k h' = m.getKey k ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂)[k] = m₂[k]
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Given a term `e` which we want to get to have type `expectedType`, return a term of type
`expectedType` by adding cast to `e` that unfold constants in `expectedType`.  -/
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.refoldConsts : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.instSemilatticeInf : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → SemilatticeInf (Geometry.SimplicialComplex 𝕜 E)
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanGroup.mk : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [toIsTopologicalGroup : IsTopologicalGroup G],
  (∀ U ∈ nhds 1, ∃ V, ↑V ⊆ U) → NonarchimedeanGroup G