mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Concept
Concept.extent_ofObjects : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α),
  (Concept.ofObjects r s).extent = lowerPolar r (upperPolar r s)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.merge.match_3.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (h : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.Heap.nil h)
  (h_2 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive h Batteries.BinomialHeap.Imp.Heap.nil)
  (h_3 :
    (s₁ : Batteries.BinomialHeap.Imp.Heap α) →
      (r₁ : ℕ) →
        (a₁ : α) →
          (n₁ : Batteries.BinomialHeap.Imp.HeapNode α) →
            (t₁ : Batteries.BinomialHeap.Imp.Heap α) →
              s₁ = Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁ →
                (s₂ : Batteries.BinomialHeap.Imp.Heap α) →
                  (r₂ : ℕ) →
                    (a₂ : α) →
                      (n₂ : Batteries.BinomialHeap.Imp.HeapNode α) →
                        (t₂ : Batteries.BinomialHeap.Imp.Heap α) →
                          s₂ = Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂ →
                            motive (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁)
                              (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂)),
  (match Batteries.BinomialHeap.Imp.Heap.nil, h with
    | Batteries.BinomialHeap.Imp.Heap.nil, h => h_1 h
    | h, Batteries.BinomialHeap.Imp.Heap.nil => h_2 h
    | s₁@h:(Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁),
      s₂@h_4:(Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) => h_3 s₁ r₁ a₁ n₁ t₁ h s₂ r₂ a₂ n₂ t₂ h_4) =
    h_1 h
-- Mathlib.Topology.Bornology.BoundedOperation
/-- A typeclass saying that `(p : R × R) ↦ p.1 * p.2` maps any product of bounded sets to a bounded
set. This property automatically holds for non-unital seminormed rings, but it also holds, e.g.,
for `ℝ≥0`.  -/
BoundedMul : (R : Type u_1) → [Bornology R] → [Mul R] → Prop
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α}
  [h : HasCountableSeparatingOn α IsOpen s], MeasurableSpace.CountablySeparated ↑s
-- Mathlib.NumberTheory.Padics.RingHoms
/-- The equivalence between the residue field of the `p`-adic integers and `ℤ/pℤ`  -/
PadicInt.residueField : {p : ℕ} → [hp_prime : Fact (Nat.Prime p)] → IsLocalRing.ResidueField ℤ_[p] ≃+* ZMod p
-- Mathlib.Data.List.Rotate
List.rotate_length : ∀ {α : Type u} (l : List α), l.rotate l.length = l
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instDecidableLtOffset : {x y : Std.Time.Millisecond.Offset} → Decidable (x < y)
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_antitone : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), Antitone B.polar
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x + a) ⁻¹' Set.Iio b = Set.Iio (b - a)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x_1 : C), (CategoryTheory.Join.left x_1).id = { down := CategoryTheory.CategoryStruct.id x_1 }
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_complex : ∀ {a : ℂ}, RCLike.sqrt a = a.sqrt
-- Mathlib.Probability.Density
MeasureTheory.aemeasurable_of_pdf_ne_zero : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} (X : Ω → E), ¬MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0 → AEMeasurable X ℙ
-- Mathlib.Order.Defs.Unbundled
/-- `IsTrichotomous X lt` means that the binary relation `lt` on `X` is trichotomous, that is,
either `lt a b` or `a = b` or `lt b a` for any `a` and `b`.  -/
IsTrichotomous : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.tensorHom_def : ∀ {C : Type u} {X₁ Y₁ X₂ Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom Y₁) (g : X₂.Hom Y₂),
  CategoryTheory.FreeMonoidalCategory.HomEquiv (f.tensor g)
    ((f.whiskerRight X₂).comp (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft Y₁ g))
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.IsLocalization.for_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  ∀ W ≤ CategoryTheory.MorphismProperty.isomorphisms C, (CategoryTheory.Functor.id C).IsLocalization W
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Lean.Meta.Tactic.Grind.Main
/-- Asserts extra facts provided as `grind` parameters.
 -/
Lean.Meta.Grind.assertExtra : Lean.Meta.Grind.Params → Lean.Meta.Grind.GoalM Unit
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_of_mem_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, k ∈ m.keysArray → m.contains k = true
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.mk : Array Bool →
  Array Bool → Array Bool → Array Bool → Array Lean.Name → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instNegOffset : Neg Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.comp_id : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b),
  f.comp AddConstMap.id = f
-- Mathlib.Order.RelClasses
/-- **Alias** of `ssubset_of_subset_not_superset`.

---

Set notation form of `lt_of_le_not_ge` -/
ssubset_of_subset_not_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊆ a → a ⊂ b
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonInitializationOptions.fromJson : Lean.Json → Except String Lean.Lsp.InitializationOptions
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_mul_relrank : ∀ {E : Type v} [inst : Field E] {A B C : Subfield E}, A ≤ B → B ≤ C → A.relrank B * B.relrank C = A.relrank C
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r],
  CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃ =
    CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.instPreorder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α], MulOpposite.instPreorder = Preorder.lift MulOpposite.unop
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the zeroth row  -/
CategoryTheory.ShortComplex.SnakeInput.L₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldl_eq_foldl_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.TreeMap.Raw.foldl (fun d a x => f d a) init t = Array.foldl f init t.keysArray
-- Mathlib.Tactic.NormNum.Ineq
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLT.core.intArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LT «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b →
            have e := q(«$a» < «$b»);
            Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_max?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.max?.get ⋯ = km → (cmp k km).isLE = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constGet!_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  m₁.Equiv m₂ → Std.DHashMap.Const.get! m₁ k = Std.DHashMap.Const.get! m₂ k
-- Init.Data.Array.Lemmas
Array.foldrM_push : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {xs : Array α}
  {a : α},
  Array.foldrM f init (xs.push a) = do
    let init ← f a init
    Array.foldrM f init xs
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.injective_of_surjective_of_submodule' : ∀ {R : Type u} {inst : Semiring R} [self : OrzechProperty R] {M : Type u} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M),
  Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.Data.Bool.Basic
Bool.and_elim_right : ∀ {a b : Bool}, (a && b) = true → b = true
-- Mathlib.Data.Int.Init
_private.Mathlib.Data.Int.Init.0.Int.inductionOn'.pos.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.List
List.tendsto_prod : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulOneClass α] [ContinuousMul α] {l : List α},
  Filter.Tendsto List.prod (nhds l) (nhds l.prod)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter : Type
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the forward direction of `spectrum.inv₀_mem_iff`. -/
spectrum.of_inv₀_mem : ∀ {R : Type u} {A : Type v} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : Aˣ},
  r⁻¹ ∈ spectrum R ↑a → r ∈ spectrum R ↑a⁻¹
-- Mathlib.Order.Partition.Finpartition
/-- No element of the partition is bottom  -/
Finpartition.bot_notMem : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (self : Finpartition a), ⊥ ∉ self.parts
-- Batteries.Data.List.Basic
List.takeDTR.eq_1 : ∀ {α : Type u_1} (n : ℕ) (l : List α) (dflt : α), List.takeDTR n l dflt = List.takeDTR.go dflt n l #[]
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsFunctor_obj_carrier : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (A : Rep.{w, u, v} k G),
  ↑((Rep.coinvariantsFunctor k G).obj A) = A.ρ.Coinvariants
-- Lean.Elab.PreDefinition.WF.Fix
/-- Given an array of MVars, assign MVars with equal type and subsumed local context to each other.
Returns those MVar that did not get assigned.
 -/
Lean.Elab.WF.assignSubsumed : Array Lean.MVarId → Lean.MetaM (Array Lean.MVarId)
-- Init.Data.Dyadic.Basic
Dyadic.precision_zero : Dyadic.precision 0 = none
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withAutoBoundImplicitForbiddenPred : {α : Type} → (Lean.Name → Bool) → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Lean.Parser.Syntax
Lean.Parser.Syntax.paren.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_Iio : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} [NoMinOrder α] [DenselyOrdered α], sSup (Set.Iio a) = a
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instReprKey.repr : Lean.Meta.LazyDiscrTree.Key → ℕ → Std.Format
-- Mathlib.CategoryTheory.EpiMono
/-- `IsSplitMono f` is the assertion that `f` admits a retraction  -/
CategoryTheory.IsSplitMono : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transportIso_inv_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c), (x.transportIso α).inv.base = α.hom
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Reflexive-transitive closure of `Red.Step`  -/
FreeAddGroup.Red : {α : Type u} → List (α × Bool) → List (α × Bool) → Prop
-- Mathlib.Order.Directed
IsMax.not_isMin' : ∀ {β : Type u_2} [inst : PartialOrder β] [Nontrivial β] [IsCodirectedOrder β] {b : β}, IsMax b → ¬IsMin b
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.HasInvolutiveReverse.mk : {V : Type u_2} →
  [inst : Quiver V] →
    [toHasReverse : Quiver.HasReverse V] →
      (∀ {a b : V} (f : a ⟶ b), Quiver.reverse (Quiver.reverse f) = f) → Quiver.HasInvolutiveReverse V
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₂ = f.f₃.τ₁
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- When its possible to compare the two, the composition of two `IsStronglyCartesian.map` will also
be given by a `IsStronglyCartesian.map`. In other words, given diagrams
```
a''         a'        a --φ--> b
|           |         |        |
v           v         v        v
R'' --g'--> R' --g--> R --f--> S
```
and
```
a' --φ'--> b
|          |
v          v
R' --f'--> S
```
and
```
a'' --φ''--> b
|            |
v            v
R'' --f''--> S
```
such that `φ` and `φ'` are strongly Cartesian morphisms, and such that `f' = g ≫ f` and
`f'' = g' ≫ f'`. Then composing the induced map from `a'' ⟶ a'` with the induced map from
`a' ⟶ a` gives the induced map from `a'' ⟶ a`.  -/
CategoryTheory.Functor.IsStronglyCartesian.map_comp_map : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' R'' : 𝒮} {a' a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'}
  (H : f' = CategoryTheory.CategoryStruct.comp g f) (H' : f'' = CategoryTheory.CategoryStruct.comp g' f') (φ' : a' ⟶ b)
  (φ'' : a'' ⟶ b) [inst_3 : p.IsStronglyCartesian f' φ'] [inst_4 : p.IsHomLift f'' φ''],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' H' φ'')
      (CategoryTheory.Functor.IsStronglyCartesian.map p f φ H φ') =
    CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ''
-- Mathlib.NumberTheory.Multiplicity
Nat.two_pow_sub_pow : ∀ {x y : ℕ},
  2 ∣ x - y →
    ¬2 ∣ x →
      ∀ {n : ℕ},
        Even n →
          emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_map : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ),
  Polynomial.reflect n (Polynomial.map f p) = Polynomial.map f (Polynomial.reflect n p)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.ratfuncAdicComplRingEquiv_apply : ∀ (K : Type u_2) [inst : Field K] (x : LaurentSeries.RatFuncAdicCompl K),
  (LaurentSeries.ratfuncAdicComplRingEquiv K) x =
    LaurentSeries.ratfuncAdicComplPkg.compare (LaurentSeries.LaurentSeriesPkg K) x.toCompletion
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.isAlgebraic_iff_top : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsAlgebraic R S] [FaithfulSMul R S], Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.coe_singleton : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] (x : α), ↑{x} = {x}
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadNormalExpr.mk : {m : Type → Type} →
  [toMonadWhiskerLeft : Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft m] →
    (Mathlib.Tactic.BicategoryLike.Structural → m Mathlib.Tactic.BicategoryLike.NormalExpr) →
      (Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.NormalExpr → m Mathlib.Tactic.BicategoryLike.NormalExpr) →
        Mathlib.Tactic.BicategoryLike.MonadNormalExpr m
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- Two multiplicative characters on a monoid whose unit group is generated by `g`
are equal if and only if they agree on `g`.  -/
MulChar.eq_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_3} [inst_1 : CommMonoidWithZero R'] {g : Rˣ},
  (∀ (x : Rˣ), x ∈ Subgroup.zpowers g) → ∀ (χ₁ χ₂ : MulChar R R'), χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) =
        (Std.DTreeMap.Internal.Impl.contains k m₁ && Std.DTreeMap.Internal.Impl.contains k m₂)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f g =
    { base := CategoryTheory.Limits.pullback.fst f.base g.base,
      c :=
        {
          app := fun U =>
            CategoryTheory.CategoryStruct.comp
              (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
              (CategoryTheory.CategoryStruct.comp (g.c.app (Opposite.op (⋯.functor.obj (Opposite.unop U))))
                (Y.presheaf.map (CategoryTheory.eqToHom ⋯))),
          naturality := ⋯ } }
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instHasSheafifyAffineEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme} {A : Type u'} [inst : CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1}
  {CD : A → Type u} [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A]
  [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)],
  CategoryTheory.HasSheafify (AlgebraicGeometry.Scheme.AffineEtale.topology S) A
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.prod.inj : ∀ {fst snd : Lean.Expr.ProdTree} {lfst lsnd : Lean.Level} {fst_1 snd_1 : Lean.Expr.ProdTree}
  {lfst_1 lsnd_1 : Lean.Level},
  fst.prod snd lfst lsnd = fst_1.prod snd_1 lfst_1 lsnd_1 → fst = fst_1 ∧ snd = snd_1 ∧ lfst = lfst_1 ∧ lsnd = lsnd_1
-- Mathlib.Algebra.Order.Round
round_natCast_add : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℕ), round (↑y + x) = ↑y + round x
-- Init.Data.String.Iterator
String.Legacy.instDecidableEqIterator.decEq : (x x_1 : String.Legacy.Iterator) → Decidable (x = x_1)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
/-- **Alias** of the reverse direction of `Complex.countable_preimage_exp`. -/
Set.Countable.preimage_cexp : ∀ {s : Set ℂ}, s.Countable → (Complex.exp ⁻¹' s).Countable
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- A pair of continuous linear equivalences generates a continuous linear equivalence between
the spaces of continuous linear maps. This version is for the type alias
`CompactConvergenceCLM`.  -/
ContinuousLinearEquiv.compactConvergenceCLMCongr : {𝕜 : Type u_7} →
  {E : Type u_8} →
    {F : Type u_9} →
      {G : Type u_10} →
        {H : Type u_11} →
          [inst : AddCommGroup E] →
            [inst_1 : AddCommGroup F] →
              [inst_2 : AddCommGroup G] →
                [inst_3 : AddCommGroup H] →
                  [inst_4 : NormedField 𝕜] →
                    [inst_5 : Module 𝕜 E] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : Module 𝕜 G] →
                          [inst_8 : Module 𝕜 H] →
                            [inst_9 : TopologicalSpace E] →
                              [inst_10 : TopologicalSpace F] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : TopologicalSpace H] →
                                    [inst_13 : IsTopologicalAddGroup G] →
                                      [inst_14 : IsTopologicalAddGroup H] →
                                        [inst_15 : ContinuousConstSMul 𝕜 G] →
                                          [inst_16 : ContinuousConstSMul 𝕜 H] →
                                            (E ≃L[𝕜] F) →
                                              (H ≃L[𝕜] G) →
                                                CompactConvergenceCLM (RingHom.id 𝕜) E H ≃L[𝕜]
                                                  CompactConvergenceCLM (RingHom.id 𝕜) F G
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.forgetCreatesColimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] →
            CategoryTheory.CreatesColimitsOfShape J T.forget
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The span of two points that lie in an affine subspace is contained in that subspace.  -/
affineSpan_pair_le_of_mem_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ : P} {s : AffineSubspace k P}, p₁ ∈ s → p₂ ∈ s → line[k, p₁, p₂] ≤ s