mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.comp_α_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n i : ℤ) {Z : C}
  (h : (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.S✝ f n).X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.f i)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α✝ f n).f i) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.Iterators.Producers.Monadic.Empty
Std.Iterators.Types.Empty.PlausibleStep : {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.isPretransitive_quotient : ∀ (G : Type u_1) [inst : AddGroup G] (H : AddSubgroup G), AddAction.IsPretransitive G (G ⧸ H)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.normal_centralizer : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [H.Normal], (AddSubgroup.centralizer ↑H).Normal
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_tensor : ∀ (C : Type u) (X Y : CategoryTheory.FreeMonoidalCategory C)
  (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as })
          X Y).symm ≪≫
      CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n) Y ≪≫
        CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C Y { as := X.normalizeObj n.as }
-- Mathlib.Algebra.Group.Invertible.Defs
mul_left_eq_iff_eq_invOf_mul : ∀ {α : Type u} [inst : Monoid α] {a b c : α} [inst_1 : Invertible c], c * a = b ↔ a = ⅟c * b
-- Init.Data.Nat.Dvd
Nat.mod_eq_zero_of_dvd : ∀ {m n : ℕ}, m ∣ n → n % m = 0
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.get_pullback : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G.EdgeLabeling K}
  {f : G' ↪g G} (x y : V') (h : G'.Adj x y), (C.pullback (RelEmbedding.toRelHom f)).get x y h = C.get (f x) (f y) ⋯
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.isTriangulated_of_precomp_iso : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  {F : CategoryTheory.Functor C D} [inst_6 : F.CommShift ℤ] {G : CategoryTheory.Functor D E} [inst_7 : G.CommShift ℤ]
  [inst_8 : CategoryTheory.Limits.HasZeroObject C] [inst_9 : CategoryTheory.Limits.HasZeroObject D]
  [inst_10 : CategoryTheory.Limits.HasZeroObject E] [inst_11 : CategoryTheory.Preadditive C]
  [inst_12 : CategoryTheory.Preadditive D] [inst_13 : CategoryTheory.Preadditive E]
  [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_15 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_16 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [inst_17 : CategoryTheory.Pretriangulated C]
  [inst_18 : CategoryTheory.Pretriangulated D] [inst_19 : CategoryTheory.Pretriangulated E]
  {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H) [inst_20 : H.CommShift ℤ] [H.IsTriangulated] [F.IsTriangulated]
  [F.mapArrow.EssSurj] [CategoryTheory.NatTrans.CommShift e.hom ℤ], G.IsTriangulated
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Following `Trie`s based on a `Key.star`.  -/
Lean.Meta.RefinedDiscrTree.Trie.star : {α : Type} → Lean.Meta.RefinedDiscrTree.Trie α → Option Lean.Meta.RefinedDiscrTree.TrieIndex
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_mul : ∀ {a b : UInt32}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.Topology.List
List.Vector.eraseIdx.eq_1 : ∀ {α : Type u_1} {n : ℕ} (i : Fin n) (l : List α) (h : l.length = n), List.Vector.eraseIdx i ⟨l, h⟩ = ⟨l.eraseIdx ↑i, ⋯⟩
-- Init.Data.BitVec.Lemmas
BitVec.getElem_twoPow : ∀ {w i j : ℕ} (h : j < w), (BitVec.twoPow w i)[j] = decide (j = i)
-- Mathlib.GroupTheory.Congruence.Defs
Con.instLE.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Con.instLE = { le := fun c d => ∀ ⦃x y : M⦄, c x y → d x y }
-- Mathlib.RingTheory.Ideal.Operations
Submodule.moduleSubmodule : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module (Ideal R) (Submodule R M)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.trans_tendsto : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {l : Filter α},
  f'' =o[l] g'' → Filter.Tendsto g'' l (nhds 0) → Filter.Tendsto f'' l (nhds 0)
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_mono`. -/
LinearOrderedField.inducedMap_mono : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α],
  Monotone (ConditionallyCompleteLinearOrderedField.inducedMap α β)
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.isLocalizedModule_map : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) {M' : Type u_1} [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] {N' : Type u_2} [inst_8 : AddCommGroup N']
  [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] [Module.FinitePresentation R M],
  IsLocalizedModule S (IsLocalizedModule.map S f g)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis_iUnion : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {ι : Type u_2} [Nonempty ι] (X : ι → Set α),
  (∀ (i : ι), M.IsBasis I (X i)) → M.IsBasis I (⋃ i, X i)
-- Mathlib.Data.Multiset.AddSub
Multiset.sub_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), s - {a} = s.erase a
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Given an element `p` in the `M`-iterated loop space of the `N`-iterated loop space of `X`,
this induces a continuous function from `I^M × I^N` to `X`.  -/
GenLoop.uncurry : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {M : Type u_3} →
        (x : X) → ↑(GenLoop M (↑(GenLoop N X x)) GenLoop.const) → C((M → ↑unitInterval) × (N → ↑unitInterval), X)
-- Mathlib.Order.Heyting.Regular
/-- **Regularization** of `a`. The smallest regular element greater than `a`.  -/
Heyting.Regular.toRegular : {α : Type u_1} → [inst : HeytingAlgebra α] → α →o Heyting.Regular α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoShortComplexH1_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.isoShortComplexH1 A).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.homMk (groupCohomology.cochainsIso₀ A).inv (groupCohomology.cochainsIso₁ A).inv
        (groupCohomology.cochainsIso₂ A).inv ⋯ ⋯)
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 0 1 2 groupCohomology.isoShortComplexH1._proof_1
              groupCohomology.isoShortComplexH1._proof_2).inv.app
        (groupCohomology.inhomogeneousCochains A))
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList_eq_cons_leadingCoeff : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R}, P ≠ 0 → ∃ ls, P.coeffList = P.leadingCoeff :: ls
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkLitS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.Literal → m Lean.Expr
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isClosed_iff_dirSupClosedOn : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D], IsLowerSet D → (IsClosed s ↔ DirSupClosedOn D s)
-- Mathlib.Data.Nat.Totient
Nat.totient_pos : ∀ {n : ℕ}, 0 < n.totient ↔ 0 < n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, 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_3 h
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.toAffineMap_injective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂], Function.Injective AffineIsometry.toAffineMap
-- Init.Data.Int.Gcd
Int.lcm_dvd_mul : ∀ (m n : ℤ), ↑(m.lcm n) ∣ m * n
-- Mathlib.NumberTheory.Chebyshev
/-- Expresses the Chebyshev theta function `ϑ` in terms of `π` by using Abel summation.  -/
Chebyshev.theta_eq_primeCounting_mul_log_sub_integral : ∀ {x : ℝ}, 2 ≤ x → Chebyshev.theta x = ↑⌊x⌋₊.primeCounting * Real.log x - ∫ (t : ℝ) in 2..x, ↑⌊t⌋₊.primeCounting / t
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfUnion.congr_simp : ∀ {α : Type u_1} {C C_1 : Set (Set α)} (e_C : C = C_1) {J J_1 : Finset (Set α)} (e_J : J = J_1)
  (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C) (j j_1 : Set α),
  j = j_1 → hC.disjointOfUnion hJ j = ⋯.disjointOfUnion ⋯ j_1
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.instFiniteIndexGamma0 : ∀ (N : ℕ) [NeZero N], (CongruenceSubgroup.Gamma0 N).FiniteIndex
-- Std.Time.Date.Unit.Weekday
/-- Saturday.  -/
Std.Time.Weekday.saturday : Std.Time.Weekday
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instLTCastInt : {d : ℕ} → LT (ℤ√↑d)
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr : Type → Type → Type
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_sndX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {Z : C} (h : G.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddAction.isMultiplyPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {n : ℕ},
  AddAction.IsMultiplyPretransitive G α n ↔ ∀ (x y : Fin n ↪ α), ∃ g, g +ᵥ x = y
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
`f` is a monotone function.  -/
monotone_of_hasDerivAt_nonneg : ∀ {f f' : ℝ → ℝ}, (∀ (x : ℝ), HasDerivAt f (f' x) x) → 0 ≤ f' → Monotone f
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Reachable.elim : ∀ {V : Type u} [inst : Quiver V] {a b : V} {p : Prop}, Quiver.Reachable a b → (∀ (a : Quiver.Path a b), p) → p
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α},
  IsOpen U → U.Nonempty → μ U ≠ ⊤ → MeasureTheory.IsLocallyFiniteMeasure μ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.union_coloops_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep (I ∪ M.coloops) ↔ M.Indep I
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.zsmul_modEq_zsmul`. -/
AddCommGroup.ModEq.zsmul_cancel : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} {z : ℤ} [IsAddTorsionFree G],
  z ≠ 0 → z • a ≡ z • b [PMOD z • p] → a ≡ b [PMOD p]
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_def : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y ↔ x ≤ᵥ y ∧ y ≤ᵥ x
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.lift_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {Y : D}
  (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X))
  (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom)
  (X_1 : CategoryTheory.MonoOver Y), ((CategoryTheory.MonoOver.lift F h).obj X_1).obj = F.obj X_1.obj
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
/-- The even or odd submodule, defined as the supremum of the even or odd powers of
`(ι Q).range`. `evenOdd 0` is the even submodule, and `evenOdd 1` is the odd submodule.  -/
CliffordAlgebra.evenOdd : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → ZMod 2 → Submodule R (CliffordAlgebra Q)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_congr_ae : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  (∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → f x = g x) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasStrictFDerivAt_const_add_iff`. -/
HasStrictFDerivAt.const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => c + f x) f' x
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.brecOn.go : {R : Type u_1} →
  {X : Type u_2} →
    {motive : FreeAlgebra.Pre R X → Sort u} →
      (t : FreeAlgebra.Pre R X) →
        ((t : FreeAlgebra.Pre R X) → FreeAlgebra.Pre.below t → motive t) → motive t ×' FreeAlgebra.Pre.below t
-- Mathlib.MeasureTheory.Function.EssSup
MeasurableEmbedding.essSup_map_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β},
  MeasurableEmbedding f →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
        MeasurableEmbedding.essSup_map_measure._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
          MeasurableEmbedding.essSup_map_measure._auto_3 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
            MeasurableEmbedding.essSup_map_measure._auto_5 →
          autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
              MeasurableEmbedding.essSup_map_measure._auto_7 →
            essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, ((g₁ +ᵥ B) ∩ (g₂ +ᵥ B)).Nonempty → g₁ +ᵥ B = g₂ +ᵥ B
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.instDecidableEqBicone.decEq : {J : Type u_1} → [DecidableEq J] → (x x_1 : CategoryTheory.Bicone J) → Decidable (x = x_1)
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.eraseList : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → List α → List ((a : α) × β a)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree : ∀ {R : Type u_1} [inst : CommSemiring R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {n : ℕ}, Squarefree n → ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.reuse.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (var : Lean.FVarId) (i : Lean.Compiler.LCNF.CtorInfo) (updateHeader : Bool)
  (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_19) (var_1 : Lean.FVarId)
  (i_1 : Lean.Compiler.LCNF.CtorInfo) (updateHeader_1 : Bool) (args_1 : Array (Lean.Compiler.LCNF.Arg pu))
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_19),
  (Lean.Compiler.LCNF.LetValue.reuse var i updateHeader args h =
      Lean.Compiler.LCNF.LetValue.reuse var_1 i_1 updateHeader_1 args_1 h_1) =
    (var = var_1 ∧ i = i_1 ∧ updateHeader = updateHeader_1 ∧ args = args_1)
-- Init.Data.Vector.MapIdx
Vector.mem_mapFinIdx : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {b : β} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β},
  b ∈ xs.mapFinIdx f ↔ ∃ i, ∃ (h : i < n), f i xs[i] h = b
-- Aesop.Rule
Aesop.Safety.almostSafe.sizeOf_spec : sizeOf Aesop.Safety.almostSafe = 1
-- Lean.Parser.Extra
/-- The parser `str` parses a string literal, such as `"foo"` or `"\r\n"`. Strings can contain
C-style escapes like `\n`, `\"`, `\x00` or `\u2665`, as well as literal unicode characters like `∈`.
Newlines in a string are interpreted literally.

This parser has arity 1: it produces a `strLitKind` node containing an atom with the raw
literal (including the quote marks and without interpreting the escapes).
You can use `TSyntax.getString` to decode the string from the resulting syntax object.  -/
Lean.Parser.strLit : Lean.Parser.Parser
-- Init.Data.Int.Order
Int.lt_or_le : ∀ (a b : ℤ), a < b ∨ b ≤ a
-- Init.Grind.AC
Lean.Grind.AC.Expr.denote : {α : Sort u_1} → Lean.Grind.AC.Context α → Lean.Grind.AC.Expr → α
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The supremum of two subspaces is equal to the span of their union.  -/
Projectivization.Subspace.span_union : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S T : Set (Projectivization K V)),
  Projectivization.Subspace.span (S ∪ T) = Projectivization.Subspace.span S ⊔ Projectivization.Subspace.span T
-- Lean.CoreM
Lean.Core.instMonadEnvCoreM : Lean.MonadEnv Lean.CoreM
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- When a vector is in `Kᗮ`, with the inner product the
other way round.  -/
ClosedSubmodule.mem_orthogonal' : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E) (v : E), v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 v u = 0
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexRange_repr : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (x : M) (i : ι) (h : optParam (b i ∈ Set.range ⇑b) ⋯),
  (b.reindexRange.repr x) ⟨b i, h⟩ = (b.repr x) i
-- Mathlib.Data.Finsupp.Multiset
Finsupp.prod_toMultiset : ∀ {α : Type u_1} [inst : CommMonoid α] (f : α →₀ ℕ), (Finsupp.toMultiset f).prod = f.prod fun a n => a ^ n
-- Init.Data.Format.Basic
Std.Format.instBEqFlattenBehavior : BEq Std.Format.FlattenBehavior
-- Mathlib.RingTheory.Algebraic.Basic
/-- If `x` is algebraic over `K`, then `x` is algebraic over `L` when `L` is an extension of `K`  -/
IsAlgebraic.tower_top : ∀ {K : Type u_1} (L : Type u_2) {A : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Ring A]
  [inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [IsScalarTower K L A] {x : A},
  IsAlgebraic K x → IsAlgebraic L x
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.lt_veblen : ∀ (a : Ordinal.{u_1}), a < Ordinal.veblen a a
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
CommGroup.mul_comm : ∀ {G : Type u} [self : CommGroup G] (a b : G), a * b = b * a
-- Mathlib.Data.Finset.Range
Finset.Nontrivial.eq_1 : ∀ {α : Type u_1} (s : Finset α), s.Nontrivial = (↑s).Nontrivial
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `a : X → A` is continuous at `x₀`
within a set `t : Set X`, and eventually `0 ≤ a x` and has spectrum contained in `s`, then
`fun x ↦ cfc f (a x)` is continuous at `x₀` within `t`.  -/
ContinuousWithinAt.cfc_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_10 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {x₀ : X} {t : Set X},
      x₀ ∈ t →
        ContinuousWithinAt a t x₀ →
          (∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum NNReal (a x) ⊆ s) →
            (∀ᶠ (x : X) in nhdsWithin x₀ t, 0 ≤ a x) →
              autoParam (ContinuousOn f s) ContinuousWithinAt.cfc_nnreal._auto_1 →
                ContinuousWithinAt (fun x => cfc f (a x)) t x₀
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α} {h' : a ∈ m}, m.get a h' = m.getD a fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_erase!_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ¬compare k t.maxKey! = Ordering.eq → (Std.DTreeMap.Internal.Impl.erase! k t).maxKey! = t.maxKey!
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- `P.cocone` is a colimit cocone.  -/
CategoryTheory.Limits.IndObjectPresentation.coconeIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (P : CategoryTheory.Limits.IndObjectPresentation A) → CategoryTheory.Limits.IsColimit P.cocone
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with subtraction.  -/
Real.circleAverage_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f₁ c R →
    CircleIntegrable f₂ c R → Real.circleAverage (f₁ - f₂) c R = Real.circleAverage f₁ c R - Real.circleAverage f₂ c R
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.isMixed_embedding : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsRamified k w → NumberField.ComplexEmbedding.IsMixed k w.embedding