mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `A` is a domain with fraction field `K` and `n : ℕ`, we define `CyclotomicRing n A K` as
the `A`-subalgebra of `CyclotomicField n K` generated by the roots of `X ^ n - 1`. If `n`
is nonzero in `A`, it has the instance `IsCyclotomicExtension {n} A (CyclotomicRing n A K)`.  -/
CyclotomicRing : ℕ → (A : Type u) → (K : Type w) → [inst : CommRing A] → [inst_1 : Field K] → [Algebra A K] → Type w
-- Lean.Meta.Tactic.LibrarySearch
/-- Tries to apply the given lemma (with symmetry modifier) to the goal,
then tries to close subsequent goals using `solveByElim`.
If `solveByElim` succeeds, `[]` is returned as the list of new subgoals,
otherwise the full list of subgoals is returned.
 -/
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.librarySearchLemma : Lean.Meta.ApplyConfig →
  (List Lean.MVarId → Lean.MetaM (List Lean.MVarId)) →
    (Lean.MVarId → Lean.MetaM Bool) → Lean.Meta.LibrarySearch.Candidate → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeMonoid.symbols_one : ∀ {α : Type u_1} [inst : DecidableEq α], FreeMonoid.symbols 1 = ∅
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput.each_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (lhs rhs : aig1.Ref)
  (h1 h2 : aig1.decls.size ≤ aig2.decls.size),
  { lhs := lhs.cast h1, rhs := rhs.cast h2 } = { lhs := lhs, rhs := rhs }.cast h2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongr_apply : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
  (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun x => M₂) M₃) (v : ι₂ → M₂),
  (MultilinearMap.domDomCongr σ m) v = m fun i => v (σ i)
-- Mathlib.Algebra.Group.Units.Opposite
Units.coe_opEquiv_symm : ∀ {M : Type u_2} [inst : Monoid M] (u : Mˣᵐᵒᵖ), ↑(Units.opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)
-- Mathlib.Topology.Homotopy.Basic
/-- Given a family of homotopies `F i` between `f₀ i : C(X i, Y i)` and `f₁ i : C(X i, Y i)`,
returns a homotopy between `ContinuousMap.piMap f₀` and `ContinuousMap.piMap f₁`.  -/
ContinuousMap.Homotopy.piMap : {ι : Type u_2} →
  {X : ι → Type u_3} →
    {Y : ι → Type u_4} →
      [inst : (i : ι) → TopologicalSpace (X i)] →
        [inst_1 : (i : ι) → TopologicalSpace (Y i)] →
          {f₀ f₁ : (i : ι) → C(X i, Y i)} →
            ((i : ι) → (f₀ i).Homotopy (f₁ i)) → (ContinuousMap.piMap f₀).Homotopy (ContinuousMap.piMap f₁)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrthogonal_of_forall_apply_same : ∀ {R : Type u_20} {M : Type u_21} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {F : Type u_22} [inst_3 : FunLike F M M] [LinearMapClass F R M M] (f : F),
  IsLeftRegular 2 → LinearMap.IsSymm B → (∀ (x : M), (B (f x)) (f x) = (B x) x) → LinearMap.IsOrthogonal B ⇑f
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.continuous_normed : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E}, Continuous (f.normed μ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α}, Std.TreeMap.Raw.unitOfList l cmp = ∅.insertManyIfNewUnit l
-- Mathlib.CategoryTheory.EssentialImage
/-- The induced functor of a faithful functor is faithful.  -/
CategoryTheory.Functor.Faithful.toEssImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Faithful], F.toEssImage.Faithful
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_respectsIso : RingHom.RespectsIso @RingHom.FiniteType
-- Mathlib.NumberTheory.GaussSum
/-- The Gauss sum of the trivial multiplicative character and a nontrivial additive character,
over a finite field, is `-1`.  -/
gaussSum_one_left : ∀ {R : Type u_1} {R' : Type u_2} [inst : Field R] [inst_1 : Fintype R] [inst_2 : CommRing R'] [IsDomain R']
  {ψ : AddChar R R'}, ψ ≠ 1 → gaussSum 1 ψ = -1
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A list with product not one must have positive length.  -/
List.length_pos_of_prod_ne_one : ∀ {M : Type u_4} [inst : Monoid M] (L : List M), L.prod ≠ 1 → 0 < L.length
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation.X`. -/
FunctionField.inftyValuation.X : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)],
  (RatFunc.inftyValuation F) RatFunc.X = WithZero.exp 1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The existence of a left adjoint of `right`.  -/
CategoryTheory.Bicategory.IsRightAdjoint : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (b ⟶ a) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.fac_lift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : F'.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp F.e (CategoryTheory.CategoryStruct.comp (hF.lift F') h) =
    CategoryTheory.CategoryStruct.comp F'.e h
-- Mathlib.Data.Nat.Pairing
/-- Pairing function for the natural numbers.  -/
Nat.pair : ℕ → ℕ → ℕ
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The restriction of a `K`-Lipschitz function is `K`-Lipschitz.  -/
LipschitzWith.restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (s : Set α), LipschitzWith K (s.domRestrict f)
-- Mathlib.Order.SuccPred.Basic
Order.pred_mono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α], Monotone Order.pred
-- Init.Grind.Norm
Lean.Grind.natCast_id : ∀ (a : ℕ), ↑a = a
-- Init.Data.Range.Polymorphic.Basic
/-- This typeclass provides support for the size function for ranges with open lower bound
\(`Roc.size`,
`Roo.size` and
`Roi.size`\).

The returned size should be equal to the number of elements returned by `toList`. This
condition is captured by the typeclass
`LawfulHasSize`.
 -/
Std.Rxo.HasSize : Type u → Type u
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularEpi_unop_iff_isRegularMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.IsRegularEpi f.unop ↔ CategoryTheory.IsRegularMono f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.edist : ∀ {α : Type u_1} {x : MeasurableSpace α} {β : Type u_5} [inst : PseudoEMetricSpace β] {f g : α → β},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => edist (f x) (g x)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spine_δ_arrow_eq : ∀ {n : ℕ} {X : SSet.Truncated (n + 2)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path (m + 1)) {i : Fin m}
  {j : Fin (m + 2)},
  j = i.succ.castSucc →
    (X.spine m ⋯
            ((CategoryTheory.ConcreteCategory.hom
                (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op))
              (sx.spineToSimplex (m + 1) ⋯ f))).arrow
        i =
      sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.one_smul_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)
      CategoryTheory.ModObj.smul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The condition that the image of the map `e.f` of an embedding of
complex shapes `e : Embedding c c'` is stable by `c'.prev`.  -/
ComplexShape.Embedding.IsTruncLE : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → Prop
-- Mathlib.Data.Num.Bitwise
/-- `a.bits n` is the vector of the `n` first bits of `a` (starting from the LSB).  -/
SNum.bits : SNum → (n : ℕ) → List.Vector Bool n
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.sourceLocalClosure K P f →
    ∀ R ∈ K.coverings X,
      ∀ {U : C} (g : U ⟶ X),
        R g → CategoryTheory.MorphismProperty.sourceLocalClosure K P (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Algebra.Order.SuccPred
Order.Iio_two : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] [NeZero 1]
  [NoMaxOrder α], Set.Iio 2 = {0, 1}
-- Mathlib.Logic.Function.Conjugate
/-- The identity function semiconjugates any function to itself.  -/
Function.Semiconj.id_left : ∀ {α : Type u_1} {ga : α → α}, Function.Semiconj id ga ga
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [T1Space E] {y : E},
  DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι]
  (ih ih_1 : (i : ι) → F₁ i → F₂ i) (e_ih : ih = ih_1)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (z z_1 : DirectLimit F₁ f₁),
  z = z_1 → DirectLimit.map f₁ f₂ ih compat z = DirectLimit.map f₁ f₂ ih_1 ⋯ z_1
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_map_le_prod : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [MulLeftMono α] (f : α → α),
  (∀ x ∈ s, f x ≤ x) → (Multiset.map f s).prod ≤ s.prod
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.leftUnitor_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor α).inv.τr = (CategoryTheory.Bicategory.rightUnitor α.r).hom
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- `zetaMul χ` takes nonnegative real values when `χ` is a quadratic character.  -/
DirichletCharacter.zetaMul_nonneg : ∀ {N : ℕ} {χ : DirichletCharacter ℂ N}, χ ^ 2 = 1 → ∀ (n : ℕ), 0 ≤ χ.zetaMul n
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_eq : ∀ (x : ℝ*), x.st = ArchimedeanClass.stdPart x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β}, Std.DHashMap.Raw.Const.get? m k = some v ↔ ∃ (h : k ∈ m), Std.DHashMap.Raw.Const.get m k h = v
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- the ring associated to a component of an affine cover  -/
AlgebraicGeometry.Scheme.AffineCover.X : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} → (self : AlgebraicGeometry.Scheme.AffineCover P S) → self.I₀ → CommRingCat
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_eq_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M} {a : α} {t : Set β} {g : β → M}
  {b : β}, (a ∈ s ↔ b ∈ t) → f a = g b → s.mulIndicator f a = t.mulIndicator g b
-- Mathlib.CategoryTheory.Equivalence
/-- Natural number powers of an auto-equivalence.  Use `(^)` instead.  -/
CategoryTheory.Equivalence.powNat : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (C ≌ C) → ℕ → (C ≌ C)
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelOpUnop_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.cokernelOpUnop f).hom =
    CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯
-- Init.Data.BitVec.Bitblast
BitVec.adc.eq_1 : ∀ {w : ℕ} (x y : BitVec w), x.adc y = BitVec.iunfoldr fun i c => BitVec.adcb (x.getLsbD ↑i) (y.getLsbD ↑i) c
-- Mathlib.Combinatorics.Nullstellensatz
MonomialOrder.lex.congr_simp : ∀ {σ : Type u_1} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ], MonomialOrder.lex = MonomialOrder.lex
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
intervals `Ioc (-N) N`·  -/
SummationFilter.symmetricIoc : (G : Type u_1) → [Neg G] → [inst : Preorder G] → [LocallyFiniteOrder G] → SummationFilter G
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
analyticAt_log : ∀ {x : ℝ}, 0 < x → AnalyticAt ℝ Real.log x
-- Lean.Meta.Tactic.Simp.LoopProtection
Lean.Meta.Simp.shouldCheckLoops : Bool → Lean.Meta.Simp.Context → Lean.CoreM Bool
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- A cocone `t` of `K : J ⥤ Under X` is a colimit if and only if the corresponding cocone
`coconeLift t` of `liftFromUnder.obj K : WithInitial K ⥤ C` is a colimit.  -/
CategoryTheory.WithInitial.isColimitEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Under X)} →
            {t : CategoryTheory.Limits.Cocone K} →
              CategoryTheory.Limits.IsColimit (CategoryTheory.WithInitial.coconeEquiv.functor.obj t) ≃
                CategoryTheory.Limits.IsColimit t
-- Mathlib.Data.Sigma.Basic
Sigma.uncurry_curry : ∀ {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : Sigma β) → γ x.fst x.snd),
  Sigma.uncurry (Sigma.curry f) = f
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Set β) (f : β → α),
  ∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.Model.split : {ρ : Type} →
  (pat : ρ) →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      [String.Slice.Pattern.Model.StrictPatternModel pat] →
        {s : String.Slice} → (firstRejected curr : s.Pos) → firstRejected ≤ curr → List s.Subslice
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceTo_slice : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos},
  (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (String.Slice.Pos.ofSlice p) ⋯
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.getGlobalSymbolPriorities : Lean.CoreM Lean.Meta.Grind.SymbolPriorities
-- Mathlib.Data.Analysis.Topology
Ctop.f : {α : Type u_1} → {σ : Type u_2} → Ctop α σ → σ → Set α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 ≤ a → 0 ≤ b → 0 ≤ a / b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.hasPushout_assoc_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄
-- Mathlib.Order.Bounds.Image
Monotone.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {a : α} {s : Set α}, a ∈ upperBounds s → f a ∈ upperBounds (f '' s)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedLeanFileProgressKind.default : Lean.Lsp.LeanFileProgressKind
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a
normal subgroup `Γ` of an additive topological group `G` with Haar measure `μ`, which is also
right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
properly normalized, satisfies `AddQuotientMeasureEqMeasurePreimage`.  -/
IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [inst_3 : IsTopologicalAddGroup G] [inst_4 : BorelSpace G] [inst_5 : PolishSpace G] {Γ : AddSubgroup G}
  [inst_6 : Γ.Normal] [inst_7 : T2Space (G ⧸ Γ)] [inst_8 : SecondCountableTopology (G ⧸ Γ)] [Countable ↥Γ]
  (ν : MeasureTheory.Measure G) [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν]
  (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν →
    ν 𝓕 ≠ ⊤ →
      MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν
        (ν (QuotientAddGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.addHaarMeasure K)
-- Init.Data.Nat.Gcd
Nat.dvd_mul_gcd_iff_dvd_mul : ∀ {k n m : ℕ}, k ∣ n * k.gcd m ↔ k ∣ n * m
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.comp_substAlgHom : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {T : Type u_6} [inst_3 : CommRing T] [inst_4 : UniformSpace T]
  [inst_5 : T2Space T] [inst_6 : CompleteSpace T] [inst_7 : IsUniformAddGroup T] [inst_8 : IsTopologicalRing T]
  [inst_9 : IsLinearTopology T T] [inst_10 : Algebra R T] {ε : MvPowerSeries τ S →ₐ[R] T} [inst_11 : UniformSpace R]
  [inst_12 : DiscreteUniformity R] [inst_13 : UniformSpace S] [DiscreteUniformity S] (ha : MvPowerSeries.HasSubst a)
  (hε : Continuous ⇑ε), ε.comp (MvPowerSeries.substAlgHom ha) = MvPowerSeries.aeval ⋯
-- Lean.Syntax
Lean.Syntax.instHashableRange : Hashable Lean.Syntax.Range
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` induces a `G`-representation on the
coinvariants of `ρ|_S`.  -/
Representation.toCoinvariants : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [S.Normal] → Representation k G (Representation.Coinvariants (MonoidHom.comp ρ S.subtype))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerCompletionWithZeroMultiplicativeIntValuation : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [inst_2 : Field K]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K]
  (v : IsDedekindDomain.HeightOneSpectrum R) [inst_6 : Algebra S K] {S₀ : Type u_4} [inst_7 : CommSemiring S₀]
  [inst_8 : Algebra S₀ S] [inst_9 : Algebra S₀ K] [IsScalarTower S₀ S K],
  IsScalarTower S₀ S (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion
-- Mathlib.Algebra.GCDMonoid.Basic
instUniqueStrongNormalizationMonoid : {α : Type u_1} → [inst : CommMonoidWithZero α] → [Subsingleton αˣ] → Unique (StrongNormalizationMonoid α)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_translate : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : FunLike F UpperHalfPlane ℂ]
  [inst_1 : SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ),
  ⇑(SlashInvariantForm.translate f g) = SlashAction.map k g ⇑f
-- Aesop.Script.SScript
Aesop.Script.SScript : Type
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.IsConnected.toIsPreconnected : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} [self : CategoryTheory.IsConnected J],
  CategoryTheory.IsPreconnected J
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A) (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X))
      ((CategoryTheory.ihom.ev B).app X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (A ⟹ X))
      ((CategoryTheory.ihom.ev A).app X)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr : ∀ (b : Bool) (e' : BitVec 1), e' = BitVec.ofBool b → e'.getLsbD 0 = b
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.equivalence_unitIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.ULift.equivalence.unitIso.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id C)
-- Mathlib.RingTheory.IntegralDomain
/-- The unit group of a finite integral domain is cyclic.

To support `ℤˣ` and other infinite monoids with finite groups of units, this requires only
`Finite Rˣ` rather than deducing it from `Finite R`.  -/
instIsCyclicUnitsOfFinite : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [Finite Rˣ], IsCyclic Rˣ
-- Mathlib.Data.Finset.Sum
Finset.toRight_insert_inl : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (insert (Sum.inl a) u).toRight = u.toRight
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsStableUnderCoproductsAnodyneExtensions : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u_2, u_2 + 1} SSet.anodyneExtensions
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_symm_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  {F : CategoryTheory.Functor C (Type (max w v₁))} (t : F.obj X) {Z : CategoryTheory.Functor C (Type (max w v₁))}
  (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.uliftCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f.op)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyonedaEquiv.symm t) h)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- Formula for geometric series.  -/
MvPowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R] [T2Space R]
  {f : MvPowerSeries σ R}, MvPowerSeries.constantCoeff f = 0 → (∑' (i : ℕ), f ^ i) * (1 - f) = 1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_congr : ∀ {α : Type u} {β : Type v} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → β}
  {f' : (a : α) → o' = some a → β},
  (∀ (a : α) (h : o' = some a), f a ⋯ = f' a h) →
    Std.Internal.List.Option.dmap✝ o f = Std.Internal.List.Option.dmap✝ o' f'