mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Init.Data.Array.MinMax
Array.min?_empty : ∀ {α : Type u_1} [inst : Min α], #[].min? = none
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, k ∈ t.alter k f ↔ (f (t.get? k)).isSome = true
-- Batteries.Recycling.RBTree.Basic
/-- An `RBMap` is a self-balancing binary search tree, used to store a key-value map.
The `cmp` function is the comparator that will be used for performing searches;
it should satisfy the requirements of `TransCmp` for it to have sensible behavior.
 -/
RBTree.RBMap : (α : Type u) → Type v → (α → α → Ordering) → Type (max u v)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.eraseLeft.congr_simp : ∀ {n : ℕ} (c c_1 : OrderedFinpartition (n + 1)) (e_c : c = c_1) (hc : Set.range (c.emb 0) = {0}),
  c.eraseLeft hc = c_1.eraseLeft ⋯
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_finset_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_4} {s : Finset ι} {f : ι → TopologicalSpace.Compacts α},
  ↑(s.sup f) = s.sup fun i => ↑(f i)
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- `Real.exp (f x)` is bounded away from zero and infinity along a filter `l` if and only if
`|f x|` is bounded from above along this filter.  -/
Real.isTheta_exp_comp_one : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  ((fun x => Real.exp (f x)) =Θ[l] fun x => 1) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |f x|
-- Mathlib.Tactic.Simps.Basic
/-- Configuration options for `@[simps]`  -/
Simps.Config : Type
-- Mathlib.Probability.Process.Filtration
/-- A `Filtration` on a measurable space `Ω` with σ-algebra `m` is a monotone
sequence of sub-σ-algebras of `m`.  -/
MeasureTheory.Filtration : {Ω : Type u_1} → (ι : Type u_2) → [Preorder ι] → MeasurableSpace Ω → Type (max u_1 u_2)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (t.erase k).maxKey he = t.maxKey ⋯ ↔ ¬cmp k (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.normalizer_le_normalizer_sup_of_normalizer_le_left : ∀ {G : Type u_2} [inst : AddGroup G] {H K : AddSubgroup G},
  AddSubgroup.normalizer ↑H ≤ AddSubgroup.normalizer ↑K → AddSubgroup.normalizer ↑H ≤ AddSubgroup.normalizer ↑(H ⊔ K)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_perm : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [inst_5 : Fintype ι]
  [inst_6 : DecidableEq ι] (σ : Equiv.Perm ι), AlternatingMap.domDomCongr σ g = Equiv.Perm.sign σ • g
-- Init.Control.Lawful.Basic
seqLeft_eq_bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α) (y : m β),
  x <* y = do
    let a ← x
    let _ ← y
    pure a
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.map_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (X : B),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.subLeft_symm_apply : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a : α)
  (a_1 : αᵒᵈ), (RelIso.symm (OrderIso.subLeft a)) a_1 = -OrderDual.ofDual a_1 + a
-- Mathlib.Algebra.Group.TypeTags.Basic
instUniqueMultiplicative : {α : Type u} → [Unique α] → Unique (Multiplicative α)
-- Mathlib.Analysis.RCLike.Basic
RCLike.neg_iff : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, z < 0 ↔ RCLike.re z < 0 ∧ RCLike.im z = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_subset_sub_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t
-- Mathlib.Algebra.RingQuot
/-- If two (semi)rings are equivalent and their quotients by a relation `rel` are defined,
then their quotients are also equivalent.

(Special case of `algEquivQuotAlgEquiv` when `S = ℕ`, which in turn is a special
case of the third isomorphism theorem.)  -/
RingQuot.equivQuotEquiv : {A : Type uA} →
  [inst : Semiring A] →
    {B : Type u₄} →
      [inst_1 : Semiring B] →
        (f : A ≃+* B) → (rel : A → A → Prop) → RingQuot rel ≃+* RingQuot (Function.onFun rel ⇑f.symm)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates
limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsLimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesColimit K.leftOp F] → CategoryTheory.CreatesLimit K F.op
-- Mathlib.Data.Matrix.Basic
AddSubmonoid.coe_matrix : ∀ {m : Type u_2} {n : Type u_3} {A : Type u_14} [inst : AddMonoid A] (S : AddSubmonoid A), ↑S.matrix = (↑S).matrix
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.inclusionInDoubleDual_norm_eq : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], ‖NormedSpace.inclusionInDoubleDual 𝕜 E‖ = ‖ContinuousLinearMap.id 𝕜 (StrongDual 𝕜 E)‖
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.rangeKerLift.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H),
  QuotientAddGroup.rangeKerLift φ = QuotientAddGroup.lift φ.ker φ.rangeRestrict ⋯
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- A category "has enough injectives" if every object has an injective presentation,
i.e. if for every object `X` there is an injective object `J` and a monomorphism `X ↪ J`.  -/
CategoryTheory.EnoughInjectives : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_div : ∀ {x y : ℝ}, 0 ≤ x → (x / y).toNNReal = x.toNNReal / y.toNNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_inv_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.zero = iX.inv
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.add_self_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s → ∀ {a : α}, a ∈ s → MonotoneOn (variationOnFromTo f s a + f) s
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.all₂.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (h_1 : Unit → motive [] []) (h_2 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_3 : (x : List α) → (x_2 : List β) → motive x x_2),
  (x = [] → x_1 = [] → False) →
    (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
      (match x, x_1 with
        | [], [] => h_1 ()
        | a :: as, b :: bs => h_2 a as b bs
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The canonical map `Y ⊞ Z ⟶ pushout f g`  -/
CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.Limits.HasPushouts C] →
        {X Y Z : C} → (f : X ⟶ Y) → (g : X ⟶ Z) → Y ⊞ Z ⟶ CategoryTheory.Limits.pushout f g
-- Mathlib.Analysis.Calculus.VectorField
ContDiffWithinAt.lieBracketWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {m n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n V s x →
    ContDiffWithinAt 𝕜 n W s x →
      UniqueDiffOn 𝕜 s → m + 1 ≤ n → x ∈ s → ContDiffWithinAt 𝕜 m (VectorField.lieBracketWithin 𝕜 V W s) s x
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.insert_of_symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  s.Pairwise r → (∀ b ∈ s, a ≠ b → r a b) → (insert a s).Pairwise r
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Eta-expanded form of `MeromorphicOn.divisor_sphere_comp_sub_const_eq_divisor_sphere`

---

Divisors are invariant under translation, special case where the set is a sphere.  -/
MeromorphicOn.divisor_sphere_fun_comp_sub_const_eq_divisor_sphere : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {R : ℝ} {f : 𝕜 → E},
  (MeromorphicOn.divisor (fun x => f (x - c)) (Metric.sphere c R)) (z + c) =
    (MeromorphicOn.divisor f (Metric.sphere 0 R)) z
-- Mathlib.Data.Multiset.Fintype
Multiset.coeEquiv_apply_coe : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (x : m.ToType), ↑(m.coeEquiv x) = m.coeEmbedding x
-- Mathlib.CategoryTheory.Monad.Algebra
/-- If `f` and `g` are two equal morphisms of monads, then the functors of algebras induced by them
are isomorphic.
We define it like this as opposed to using `eqToIso` so that the components are nicer to prove
lemmas about.
 -/
CategoryTheory.Monad.algebraFunctorOfMonadHomEq : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T₁ T₂ : CategoryTheory.Monad C} →
      {f g : T₁ ⟶ T₂} →
        f = g → (CategoryTheory.Monad.algebraFunctorOfMonadHom f ≅ CategoryTheory.Monad.algebraFunctorOfMonadHom g)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H2Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 2)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H2Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.π h)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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 : SubNegMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} {x : M} (c : G),
  ContMDiffAt I' I n f x → ContMDiffAt I' I n (fun x => f x - c) x
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.zero_mul : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), 0 * a = 0
-- Mathlib.Data.Quot
Quotient.instDecidableLiftOn'OfDecidablePred : {α : Sort u_1} →
  {s₁ : Setoid α} →
    (q : Quotient s₁) →
      (f : α → Prop) → (h : ∀ (a b : α), s₁ a b → f a = f b) → [DecidablePred f] → Decidable (q.liftOn' f h)
-- Mathlib.Topology.Bases
/-- If `α` is a separable topological space with a partial order, then there exists a countable
dense set `s : Set α` that contains those of both bottom and top elements of `α` that actually
exist. For a dense set containing neither bot nor top elements, see
`exists_countable_dense_no_bot_top`.  -/
exists_countable_dense_bot_top : ∀ (α : Type u_1) [inst : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [inst_2 : PartialOrder α],
  ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s
-- Mathlib.Data.Nat.Choose.Factorization
/-- The `n`th central binomial coefficient is the product of its prime factors, which are
at most `2n`.  -/
Nat.prod_pow_factorization_centralBinom : ∀ (n : ℕ), ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom
-- Mathlib.Control.Functor
/-- `AddConst α` is a synonym for constant functor `Const α`, mapping
every type to `α`. When `α` has an additive monoid structure,
`AddConst α` has an `Applicative` instance. (If `α` has a
multiplicative monoid structure, see `Functor.Const`.)  -/
Functor.AddConst : Type u_1 → Type u_2 → Type u_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.one_le_mul_inv`. -/
Units.le_of_one_le_mul_inv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a : M} (u : Mˣ), 1 ≤ a * ↑u⁻¹ → ↑u ≤ a
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.trans_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ)
  (ψ : σ.Equiv τ) (v : V), (φ.trans ψ) v = ψ (φ v)
-- Init.Data.Order.MinMaxOn
le_apply_minOn_iff : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α}
  {b : β}, b ≤ f (minOn f x y) ↔ b ≤ f x ∧ b ≤ f y
-- Mathlib.Algebra.DirectSum.Ring
/-- A family of `AddMonoidHom`s preserving `DirectSum.One.one` and `DirectSum.Mul.mul`
describes a `RingHom`s on `⨁ i, A i`. This is a stronger version of `DirectSum.toMonoid`.

Of particular interest is the case when `A i` are bundled subobjects, `f` is the family of
coercions such as `AddSubmonoid.subtype (A i)`, and the `[GSemiring A]` structure originates from
`DirectSum.gsemiring.ofAddSubmonoids`, in which case the proofs about `GOne` and `GMul`
can be discharged by `rfl`.  -/
DirectSum.toSemiring : {ι : Type u_1} →
  [inst : DecidableEq ι] →
    {A : ι → Type u_2} →
      {R : Type u_3} →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : DirectSum.GSemiring A] →
              [inst_4 : Semiring R] →
                (f : (i : ι) → A i →+ R) →
                  (f 0) GradedMonoid.GOne.one = 1 →
                    (∀ {i j : ι} (ai : A i) (aj : A j),
                        (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) →
                      (DirectSum ι fun i => A i) →+* R
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_right_hom : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ f₂' : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom)
  (iso : f₂ ≅ f₂'), (sq₁₂.ι_iso_of_iso_right sq₁₂' iso).hom = sq₁₂.mapArrowRight sq₁₂' iso.hom
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α},
  Finset.image (fun x => a • x) s = a • s
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- Construct a `Mor₁` expression from a Lean expression.  -/
Mathlib.Tactic.Bicategory.mor₁OfExpr : Lean.Expr → Mathlib.Tactic.Bicategory.BicategoryM Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Tactic.CategoryTheory.Coherence.Basic
Mathlib.Tactic.BicategoryLike.mk_eq_of_cons : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {f₁ f₂ f₃ f₄ : C} (α α' : f₁ ⟶ f₂) (η η' : f₂ ⟶ f₃)
  (ηs ηs' : f₃ ⟶ f₄),
  α = α' →
    η = η' →
      ηs = ηs' →
        CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ηs) =
          CategoryTheory.CategoryStruct.comp α' (CategoryTheory.CategoryStruct.comp η' ηs')
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_left_injective : ∀ {α : Type u_1} [inst : CommMonoid α] [IsCancelMul α] {s : Submonoid α} (b : ↥s),
  Function.Injective fun a => Localization.mk a b
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Triangulated.Octahedron.map_m₃ : ∀ {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 ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Limits.HasZeroObject D] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : CategoryTheory.Preadditive D] [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃}
  {u₁₃ : X₁ ⟶ X₃} {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D)
  [inst_12 : F.CommShift ℤ] [inst_13 : F.IsTriangulated], (h.map F).m₃ = F.map h.m₃
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.lift_algebraMap_apply : ∀ (K : Type u_1) [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K]
  [inst_3 : Algebra.IsAlgebraic k K] (φ : k →+* ℂ) (x : k),
  (NumberField.ComplexEmbedding.lift K φ) ((algebraMap k K) x) = φ x
-- Init.Data.SInt.Lemmas
Int32.div_self : ∀ {a : Int32}, a / a = if a = 0 then 0 else 1
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.map_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
  (MvPolynomial.map f) ((MvPolynomial.bind₁ g) φ) =
    (MvPolynomial.bind₁ fun i => (MvPolynomial.map f) (g i)) ((MvPolynomial.map f) φ)
-- Lean.Parser.Syntax
Lean.Parser.Command.namedName : Lean.Parser.Parser
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshRef.mk.injEq : ∀ (ref ref_1 : IO.Ref ProofWidgets.RefreshComponent.RefreshState), ({ ref := ref } = { ref := ref_1 }) = (ref = ref_1)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddMonoidHom.toLocalizationMap.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] (f : M →+ N)
  (H1 : ∀ (y : ↥S), IsAddUnit (f ↑y)) (H2 : ∀ (z : N), ∃ x, z + f ↑x.2 = f x.1)
  (H3 : ∀ (x y : M), f x = f y → ∃ c, ↑c + x = ↑c + y),
  f.toLocalizationMap H1 H2 H3 = { toFun := (↑f).toFun, map_add' := ⋯, isLocalizationMap := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α] {k : α}, t.contains k = true → t.getKey! k = k
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- There is a morphism from `⊤ : MonoOver A` to the pullback of a monomorphism along itself;
as the category is thin this is an isomorphism.  -/
CategoryTheory.MonoOver.topLEPullbackSelf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {A B : C} →
        (f : A ⟶ B) →
          [inst_2 : CategoryTheory.Mono f] → ⊤ ⟶ (CategoryTheory.MonoOver.pullback f).obj (CategoryTheory.MonoOver.mk f)
-- Mathlib.Data.Sym.Basic
/-- `a ↦ {a}` as an equivalence between `α` and `Sym α 1`.  -/
Sym.oneEquiv : {α : Type u_1} → α ≃ Sym α 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.Limits.cokernel.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_2 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.Limits.cokernel f = CategoryTheory.Limits.cokernel f_1
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.r h) = h
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIic : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → (a : α) → Fintype ↑(Set.Iic a)
-- Lean.Meta.Tactic.Backtrack
/-- If `suspend g`, then we do not consider alternatives for `g`,
but return `g` as a new subgoal. (defaults to `false`)  -/
Lean.Meta.Tactic.Backtrack.BacktrackConfig.suspend : Lean.Meta.Tactic.Backtrack.BacktrackConfig → Lean.MVarId → Lean.MetaM Bool
-- Batteries.Data.Nat.Lemmas
Nat.recDiagAux_zero_left : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_left : (n : ℕ) → motive 0 n) (zero_right : (m : ℕ) → motive m 0)
  (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1)) (n : ℕ),
  Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.ofRightExact_map_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : CategoryTheory.Limits.HasZeroObject D]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ᵣ D} (α : F ⟶ G),
  ((CategoryTheory.AdditiveFunctor.ofRightExact C D).map α).hom = α.hom
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_unitIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithInitial C)ᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).unitIso.hom.app X =
    (match Opposite.unop X with
      | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x))
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).hom
-- Mathlib.NumberTheory.Multiplicity
/-- **Lifting the exponent lemma** for `p = 2`  -/
Int.two_pow_sub_pow : ∀ {x y : ℤ} {n : ℕ},
  2 ∣ x - y →
    ¬2 ∣ x →
      Even n →
        emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑n