mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMonoidMorphism.toMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {H' : Type u_5} →
                [inst_4 : TopologicalSpace H'] →
                  {E' : Type u_6} →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : NormedSpace 𝕜 E'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {n : WithTop ℕ∞} →
                              {G : Type u_8} →
                                [inst_7 : TopologicalSpace G] →
                                  [inst_8 : ChartedSpace H G] →
                                    [inst_9 : Monoid G] →
                                      {G' : Type u_9} →
                                        [inst_10 : TopologicalSpace G'] →
                                          [inst_11 : ChartedSpace H' G'] →
                                            [inst_12 : Monoid G'] → ContMDiffMonoidMorphism I I' n G G' → G →* G'
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State.visited : Lean.Expr.CollectLooseBVars.State → Std.HashSet (ℕ × Lean.Expr)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.quotient_iff`.

---

The image of a quotient is torsion iff the group is torsion.  -/
IsTorsion.quotient_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] {N : Subgroup G} [inst_1 : Group H] {f : G →* H},
  Function.Surjective ⇑f → N = f.ker → IsMulTorsion ↥N → (IsMulTorsion H ↔ IsMulTorsion G)
-- Lean.Meta.Tactic.Grind.Internalize
/-- Given a term `arg` that occurs as the argument at position `i` of an `f`-application `parent?`,
we consider `arg` as a candidate for case-splitting. For every other argument `arg'` that also appears
at position `i` in an `f`-application and has the same type as `e`, we add the case-split candidate `arg = arg'`.

When performing the case split, we consider the following two cases:
- `arg = arg'`, which may introduce a new congruence between the corresponding `f`-applications.
- `¬(arg = arg')`, which may trigger extensionality theorems for the type of `arg`.

This feature enables `grind` to solve examples such as:
```lean
example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
  grind
```
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addSplitCandidatesForExt : Lean.Expr → ℕ → optParam (Option Lean.Expr) none → Lean.Meta.Grind.GoalM Unit
-- Mathlib.NumberTheory.Pell
/-- If we multiply a positive solution with the inverse of a fundamental solution,
the `x`-coordinate decreases.  -/
Pell.IsFundamental.mul_inv_x_lt_x : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
  Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → (a * a₁⁻¹).x < a.x
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastIsEmptyEmpty : Lean.Meta.FastIsEmpty Empty
-- Init.Data.List.Range
List.head_range' : ∀ {s n : ℕ} (h : List.range' s n ≠ []), (List.range' s n).head h = s
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.g_eq_id : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })} {m : ℕ} {f₁ : { len := n } ⟶ { len := m }}
  {y₁ : ↑(X.nonDegenerate m)},
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ {f₂ : { len := n } ⟶ { len := m }} {y₂ : X.obj (Opposite.op { len := m })},
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) y₂ →
        ∀ (hf₁ : CategoryTheory.SplitEpi f₁),
          SSet.unique_nonDegenerate.g✝ hf₁ f₂ = CategoryTheory.CategoryStruct.id { len := m }
-- Init.GrindInstances.ToInt
Lean.Grind.instModUInt64UintOfNatNat : Lean.Grind.ToInt.Mod UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- If `k` is algebraically closed, `K / k` is a field extension, `L / k` is an intermediate field
which is algebraic, then `L` is equal to `k`. A corollary of
`IsAlgClosed.algebraMap_surjective_of_isAlgebraic`.  -/
IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [IsAlgClosed k] [inst_3 : Algebra k K]
  (L : IntermediateField k K) [Algebra.IsAlgebraic k ↥L], L = ⊥
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_closure_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {x : G}, x ∈ s → x ∈ AddSubgroup.closure s
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.inductive_claim_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {k : ℝ} {m : ℕ},
  3 ≤ m →
    (∀ (ε : Fin 3 → ℤ),
        (∀ (i : Fin 3), |ε i| = 1) → ↑(List.map (fun i => ε i • A) (List.finRange 3)).sum.card ≤ k * ↑A.card) →
      ∀ (ε : Fin m → ℤ),
        (∀ (i : Fin m), |ε i| = 1) → ↑(List.map (fun i => ε i • A) (List.finRange m)).sum.card ≤ k ^ (m - 2) * ↑A.card
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodInverse_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') {X Y : CategoryTheory.StructuredArrow S T × CategoryTheory.StructuredArrow S' T'}
  (η : X ⟶ Y),
  (CategoryTheory.StructuredArrow.prodInverse S S' T T').map η =
    CategoryTheory.StructuredArrow.homMk
      (CategoryTheory.StructuredArrow.Hom.right η.1, CategoryTheory.StructuredArrow.Hom.right η.2) ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_a₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).a₄ = f W.a₄
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.pOpcycles_singleObjOpcyclesSelfIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).pOpcycles j)
      (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv =
    (HomologicalComplex.singleObjXSelf c j A).hom
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instMin.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instMin =
    {
      min := fun x y =>
        { toTopologicalSpace := x.toTopologicalSpace ⊓ y.toTopologicalSpace, toIsTopologicalAddGroup := ⋯ } }
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.finsetSum_coeff : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ),
  (∑ b ∈ s, f b).coeff n = ∑ b ∈ s, (f b).coeff n
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_functor_obj_right_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.WithInitial.equivComma.functor.obj F).right.map f = F.map (CategoryTheory.WithInitial.incl.map f)
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_coeff_cert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → ℤ → Bool
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_prodComm : ∀ (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R E] [inst_4 : Module R E₂],
  (LinearIsometryEquiv.prodComm R E E₂).symm = LinearIsometryEquiv.prodComm R E₂ E
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `HasDerivWithinAt.Ioi_iff_Ioo`. -/
HasDerivWithinAt.Ioi_of_Ioo : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} [inst_3 : LinearOrder 𝕜] [OrderClosedTopology 𝕜] {x y : 𝕜},
  x < y → HasDerivWithinAt f f' (Set.Ioo x y) x → HasDerivWithinAt f f' (Set.Ioi x) x
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instOrdOfYear : {leap : Bool} → Ord (Std.Time.Day.Ordinal.OfYear leap)
-- Mathlib.Data.W.Constructions
WType.Natα.zero.sizeOf_spec : sizeOf WType.Natα.zero = 1
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteMulSupport.div` -/
Function.HasFiniteMulSupport.fun_div : ∀ {α : Type u_1} {M : Type u_3} [inst : DivisionMonoid M] {f g : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun i => f i / g i
-- Mathlib.SetTheory.Lists
Lists.Equiv.decidable.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x x_1 : Lists α),
  Lists.Equiv.decidable x x_1 =
    match x, x_1 with
    | ⟨false, l₁⟩, ⟨false, l₂⟩ => decidable_of_iff' (l₁ = l₂) ⋯
    | ⟨false, l₁⟩, ⟨true, l₂⟩ => isFalse ⋯
    | ⟨true, l₁⟩, ⟨false, l₂⟩ => isFalse ⋯
    | ⟨true, l₁⟩, ⟨true, l₂⟩ => decidable_of_iff' (l₁ ⊆ l₂ ∧ l₂ ⊆ l₁) ⋯
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_eq_forIn'_toArray : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  [inst_6 : Std.LawfulDeterministicIterator α Id] {γ : Type x} {it : Std.Iter β} {init : γ}
  {f : (out : β) → out ∈ it → γ → m (ForInStep γ)},
  forIn' it init f = forIn' it.toArray init fun out h acc => f out ⋯ acc
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.mulOp_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] (f : α ≃+ β),
  AddEquiv.mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)
-- Mathlib.Topology.UniformSpace.Equicontinuity
UniformEquicontinuousOn.eq_1 : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] (F : ι → β → α) (S : Set β),
  UniformEquicontinuousOn F S =
    ∀ U ∈ uniformity α, ∀ᶠ (xy : β × β) in uniformity β ⊓ Filter.principal (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
-- Lean.Attributes
Lean.ParametricAttribute.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (attr : Lean.AttributeImpl)
  (ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α))
  (preserveOrder : Bool),
  sizeOf { attr := attr, ext := ext, preserveOrder := preserveOrder } =
    1 + sizeOf attr + sizeOf ext + sizeOf preserveOrder
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTheoremCacheKey.f : Lean.Meta.Grind.CongrTheoremCacheKey → Lean.Expr
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.isClosed_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : Subsemiring R), IsClosed ↑s.topologicalClosure
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit' : ∀ {J : Type w} [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C] {α : Type u_1} [inst_3 : PartialOrder α] (h : α <i J),
  Order.IsSuccLimit h.top → CategoryTheory.Limits.HasColimitsOfShape α C
-- Init.Data.SInt.Lemmas
Int8.mul_zero : ∀ {a : Int8}, a * 0 = 0
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.sup_def : ∀ (x x_1 : ℝ),
  Real.sup✝ x x_1 =
    match x, x_1 with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 => x1 ⊔ x2) ⋯ x y }
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.neg : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → AddGroup (β i)] [∀ (i : ι), ContinuousNeg (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f (-u)
-- Mathlib.RingTheory.Trace.Basic
det_traceForm_ne_zero : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [Algebra.IsSeparable K L] [inst_4 : Fintype ι] [inst_5 : DecidableEq ι] (b : Module.Basis ι K L),
  ((LinearMap.BilinForm.toMatrix b) (Algebra.traceForm K L)).det ≠ 0
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.WideSubcategory P} {f g : X ⟶ Y}, f = g ↔ f.hom = g.hom
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `RatFunc.numDenom` are numerator and denominator of a rational function over a field,
normalized such that the denominator is monic.  -/
RatFunc.numDenom : {K : Type u} → [inst : Field K] → RatFunc K → Polynomial K × Polynomial K
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.coe_zpow : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a : { x // 0 ≤ x })
  (n : ℤ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The group morphism from `fixingSubgroup` of a union to the iterated `fixingSubgroup`.  -/
SubMulAction.fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        {s t : Set α} → ↥(fixingSubgroup M (s ∪ t)) →* ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t))
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypeEquivSubtypePerm_symm_apply : ∀ {α : Type u_4} (p : α → Prop) [inst : DecidablePred p] (f : { f // ∀ (a : α), ¬p a → f a = a }),
  (Equiv.Perm.subtypeEquivSubtypePerm p).symm f = (↑f).subtypePerm ⋯
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.of_isEmpty : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) [IsEmpty E],
  IsCoveringMap f
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.of_support_subset_isCompact : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {K : Set α} [R1Space α],
  IsCompact K → Function.support f ⊆ K → HasCompactSupport f
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.inst : (α : Type u_1) → Quiver (Quiver.SingleObj α)
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.codisjoint_map : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f → ∀ {p q : Submodule R M}, Codisjoint p q → Codisjoint (Submodule.map f p) (Submodule.map f q)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.le_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∃ J' ∈ π₂, J ≤ J'
-- Init.Data.SInt.Lemmas
BitVec.ofInt_int8ToInt : ∀ (x : Int8), BitVec.ofInt 8 x.toInt = x.toBitVec
-- Mathlib.NumberTheory.ModularForms.Cusps
cosetToCuspOrbit_apply_mk : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [inst : 𝒢.IsArithmetic] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  cosetToCuspOrbit 𝒢 ⟦g⟧ = ⟦⟨(Matrix.SpecialLinearGroup.mapGL ℝ) g⁻¹ • OnePoint.infty, ⋯⟩⟧
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.mk : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              (toWord : Monoid.CoprodI.Word G) →
                H → (∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord.toList → g ∈ d.set i) → Monoid.PushoutI.NormalWord d
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.toLax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans F G) (a : B), η.toLax.app a = η.app a
-- Init.Data.Nat.Gcd
Nat.dvd_mul : ∀ {k m n : ℕ}, k ∣ m * n ↔ ∃ k₁ k₂, k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k
-- Mathlib.Topology.Separation.Basic
eventually_nhdsWithin_eventually_nhds_iff_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {a : X} {p : X → Prop},
  IsOpen s → ((∀ᶠ (y : X) in nhdsWithin a s, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhdsWithin a s, p x)
-- Mathlib.FieldTheory.Relrank
Subfield.inf_relfinrank_right : ∀ {E : Type v} [inst : Field E] (A B : Subfield E), (A ⊓ B).relfinrank B = A.relfinrank B
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.ConfigItem.mk.inj : ∀ {ref : Lean.Syntax} {option : Lean.Ident} {value : Lean.Syntax} {bool? : Option Bool} {origOptionName : Lean.Name}
  {optionComps prevOptionComps : List Lean.Syntax} {ref_1 : Lean.Syntax} {option_1 : Lean.Ident} {value_1 : Lean.Syntax}
  {bool?_1 : Option Bool} {origOptionName_1 : Lean.Name} {optionComps_1 prevOptionComps_1 : List Lean.Syntax},
  { ref := ref, option := option, value := value, bool? := bool?, origOptionName := origOptionName,
        optionComps := optionComps, prevOptionComps := prevOptionComps } =
      { ref := ref_1, option := option_1, value := value_1, bool? := bool?_1, origOptionName := origOptionName_1,
        optionComps := optionComps_1, prevOptionComps := prevOptionComps_1 } →
    ref = ref_1 ∧
      option = option_1 ∧
        value = value_1 ∧
          bool? = bool?_1 ∧
            origOptionName = origOptionName_1 ∧ optionComps = optionComps_1 ∧ prevOptionComps = prevOptionComps_1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceOpcyclesE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂), CategoryTheory.Mono (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.get?_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α},
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.get? k = m₂.get? k
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.lcm_dvd_iff : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {x y z : R},
  EuclideanDomain.lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z
-- Mathlib.Probability.Kernel.Composition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_measure_compProd_left`.  -/
ProbabilityTheory.rnDeriv_compProd_withDensity_rnDeriv : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α)
  (κ η : ProbabilityTheory.Kernel α β) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  ((ν.withDensity (μ.rnDeriv ν)).compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η]
    (μ.compProd κ).rnDeriv (ν.compProd η)
-- Mathlib.Data.Finset.NoncommProd
/-- Sum of a `s : Finset α` mapped with `f : α → β` with `[AddMonoid β]`,
given a proof that `+` commutes on all elements `f x` for `x ∈ s`.  -/
Finset.noncommSum : {α : Type u_3} →
  {β : Type u_4} → [inst : AddMonoid β] → (s : Finset α) → (f : α → β) → (↑s).Pairwise (Function.onFun AddCommute f) → β
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- A `2`-transitive additive action is primitive.  -/
AddAction.isPreprimitive_of_is_two_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.IsMultiplyPretransitive G α 2 → AddAction.IsPreprimitive G α
-- Lean.Meta.Tactic.Grind.Types
/-- Next local E-match theorem idx.  -/
Lean.Meta.Grind.EMatch.State.nextThmIdx : Lean.Meta.Grind.EMatch.State → ℕ
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.prod_left_snd : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, (fun x => (f' x, g' x)) =o[l] k' → g' =o[l] k'
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_solve_elim_cert.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var)
  (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var) (p₂ : Int.Internal.Linear.Poly)
  (h_1 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (h_2 : (x x_1 : Int.Internal.Linear.Poly) → motive x x_1),
  (match Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ with
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_1 a₁ x₁ p₁ a₂ x₂ p₂
    | x, x_1 => h_2 x x_1) =
    h_1 a₁ x₁ p₁ a₂ x₂ p₂
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Iio : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R},
  Nat.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.isPrincipal_add_omega : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (Ordinal.omega o)
-- Init.WF
/-- The inverse image of a well-founded relation is well-founded.
 -/
invImage : {α : Sort u_1} → {β : Sort u_2} → (α → β) → WellFoundedRelation β → WellFoundedRelation α
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- Counts the number of times that the coefficients in a polynomial change sign, with
the convention that 0 can count as either sign.  -/
Polynomial.signVariations : {R : Type u_1} → [inst : Semiring R] → [LinearOrder R] → Polynomial R → ℕ
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.ExprPtr.expr : Lean.Meta.Sym.ExprPtr → Lean.Expr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Interaction of `sum` and `•` assuming some multiplication structure.  -/
SkewMonoidAlgebra.sum_smul_index : ∀ {k : Type u_1} {G : Type u_2} {N : Type u_3} [inst : AddCommMonoid N] [inst_1 : NonUnitalNonAssocSemiring k]
  {g : SkewMonoidAlgebra k G} {b : k} {h : G → k → N},
  (∀ (i : G), h i 0 = 0) → (b • g).sum h = g.sum fun x1 x2 => h x1 (b * x2)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.instInhabited : (R : Type u_4) → [inst : Mul R] → [inst_1 : Add R] → Inhabited (R ≃+* R)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite products of meromorphic functions are meromorphic.  -/
MeromorphicOn.prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_5} {s : Finset ι} {f : ι → 𝕜 → 𝕜'},
  (∀ σ ∈ s, MeromorphicOn (f σ) U) → MeromorphicOn (∏ n ∈ s, f n) U
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.isIso_of_isLeftDerivedFunctor_of_inverts : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W]
  {F : CategoryTheory.Functor C H} (LF : CategoryTheory.Functor D H) (α : L.comp LF ⟶ F),
  W.IsInvertedBy F → ∀ [LF.IsLeftDerivedFunctor α W], CategoryTheory.IsIso α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst.eq_1 : ∀ (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConst k p =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 0 else bif k == 1 then p else Lean.Grind.CommRing.Poly.mulConst.go k p