mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.seminormedAddCommGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {s : AddSubgroup E},
  AddSubgroup.seminormedAddCommGroup =
    { toNorm := AddSubgroup.seminormedAddGroup.toNorm, toAddCommGroup := s.toAddCommGroup,
      toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Data.Finsupp.Order
Finsupp.instPosSMulStrictMono : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : Zero β]
  [inst_3 : PartialOrder β] [inst_4 : SMulWithZero α β] [PosSMulStrictMono α β], PosSMulStrictMono α (ι →₀ β)
-- Mathlib.Order.WellFounded
/-- A relation is well-founded iff it doesn't have any infinite descending chain.

See `RelEmbedding.wellFounded_iff_isEmpty` for a version in terms of relation embeddings.  -/
wellFounded_iff_isEmpty_descending_chain : ∀ {α : Sort u_1} {r : α → α → Prop}, WellFounded r ↔ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }
-- Mathlib.Algebra.GroupWithZero.Commute
pow_inv_comm₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀) (m n : ℕ), a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
-- Init.Data.BitVec.Lemmas
BitVec.not_allOnes_lt : ∀ {w : ℕ} {x : BitVec w}, ¬BitVec.allOnes w < x
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : α → β} {a : α}, IsLocalExtr f a → IsLocalExtr (fun x => -f x) a
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.toPrepathObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
      {A : C} → HomotopicalAlgebra.PathObject A → HomotopicalAlgebra.PrepathObject A
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.fst_mul : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : Add ι] [inst_1 : GradedMonoid.GMul A] (x y : GradedMonoid A),
  (x * y).fst = x.fst + y.fst
-- Mathlib.Tactic.Coe
/-- Partially applied function coercion.  Equivalent to the η-reduction of `(⇑ ·)`  -/
Lean.Elab.Term.CoeImpl.«term(⇑)» : Lean.ParserDescr
-- Mathlib.Algebra.Star.Basic
/-- **Alias** of the reverse direction of `semiconjBy_star_star_star`. -/
SemiconjBy.star_star_star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y z : R}, SemiconjBy x y z → SemiconjBy (star x) (star z) (star y)
-- Mathlib.Algebra.Algebra.Hom.Rat
AlgEquiv.toRatAlgEquiv_toRingEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R ≃ₐ[ℚ] S), f.toRingEquiv.toRatAlgEquiv = f
-- Std.Do.PredTrans
/-- The function implementing the predicate transformer.  -/
Std.Do.PredTrans.trans : {ps : Std.Do.PostShape} → {α : Type u} → Std.Do.PredTrans ps α → Std.Do.PostCond α ps → Std.Do.Assertion ps
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_comap : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  (g : LocallyConstant Y Z), ⇑(LocallyConstant.comap f g) = ⇑g ∘ ⇑f
-- Mathlib.Data.Finset.Dedup
List.toFinset_reverse : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.reverse.toFinset = l.toFinset
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_map_eq : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β),
  (∀ (a : α), ‖f a‖₊ = ‖a‖₊) → ‖A.map f‖₊ = ‖A‖₊
-- Mathlib.Logic.Equiv.Prod
Equiv.sumPiEquivProdPi_symm_apply : ∀ {ι : Type u_10} {ι' : Type u_11} (π : ι ⊕ ι' → Type u_9)
  (g : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) (t : ι ⊕ ι'),
  (Equiv.sumPiEquivProdPi π).symm g t = Sum.rec g.1 g.2 t
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Int.instMeasurableSpace : MeasurableSpace ℤ
-- Mathlib.Algebra.Polynomial.Sequence
/-- A sequence of polynomials such that the polynomial at index `i` has degree `i`.  -/
Polynomial.Sequence : (R : Type u_1) → [Semiring R] → Type u_1
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularMono.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {Z : C} {left right : Y ⟶ Z}
  {w :
    autoParam (CategoryTheory.CategoryStruct.comp f left = CategoryTheory.CategoryStruct.comp f right)
      CategoryTheory.RegularMono.w._autoParam}
  {isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)} {Z_1 : C} {left_1 right_1 : Y ⟶ Z_1}
  {w_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f left_1 = CategoryTheory.CategoryStruct.comp f right_1)
      CategoryTheory.RegularMono.w._autoParam}
  {isLimit_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w_1)},
  { Z := Z, left := left, right := right, w := w, isLimit := isLimit } =
      { Z := Z_1, left := left_1, right := right_1, w := w_1, isLimit := isLimit_1 } →
    Z = Z_1 ∧ left ≍ left_1 ∧ right ≍ right_1 ∧ isLimit ≍ isLimit_1
-- Mathlib.Data.Nat.Cast.Commute
SemiconjBy.natCast_mul_right : ∀ {α : Type u_1} [inst : Semiring α] {a x y : α}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy a (↑n * x) (↑n * y)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substAlgHom.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a), PowerSeries.substAlgHom ha = MvPowerSeries.substAlgHom ⋯
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.adj_congr_of_sym2 : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v w x : V}, s(u, v) = s(w, x) → (H.Adj u v ↔ H.Adj w x)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.liftOfRightInverse_comp_apply : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : { g // f.ker ≤ g.ker }) (x : G₁),
  ((f.liftOfRightInverse f_neg hf) g) (f x) = ↑g x
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_apply : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y z : F),
  (((InnerProductSpace.rankOne 𝕜) x) y) z = inner 𝕜 y z • x
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.contains.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    (a_1 == a || Std.DHashMap.Internal.AssocList.contains a es)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_neg : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] (t : E), MeasureTheory.charFun μ (-t) = (starRingEnd ℂ) (MeasureTheory.charFun μ t)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddEquiv.isAddCyclic : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] (e : G ≃+ G'),
  IsAddCyclic G ↔ IsAddCyclic G'
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instLattice.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousAdd G],
  OpenAddSubgroup.instLattice =
    { toSemilatticeSup := Function.Injective.semilatticeSup OpenAddSubgroup.toAddSubgroup ⋯ ⋯ ⋯ ⋯,
      inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mapsTo_reflection_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  Set.MapsTo (⇑(P.reflection i)) (Set.range ⇑P.root) (Set.range ⇑P.root)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.currySum.eq_1 : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X) (q : ↑(GenLoop (M ⊕ N) X x)),
  GenLoop.currySum x q =
    {
      toFun := fun a =>
        ⟨((↑q).comp { toFun := Homeomorph.sumArrowHomeomorphProdArrow.invFun, continuous_toFun := ⋯ }).curry.toFun a,
          ⋯⟩,
      continuous_toFun := ⋯ }
-- Mathlib.Logic.Basic
/-- **Alias** of `Xor.or`. -/
Xor'.or : ∀ {a b : Prop}, Xor a b → a ∨ b
-- Lean.ReservedNameAction
/-- Similar to `resolveGlobalName`, but also executes reserved name actions.
 -/
Lean.realizeGlobalName : Lean.Name → Lean.CoreM (List (Lean.Name × List String))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_smul_of_nonpos : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ},
  r ≤ 0 → ∀ {a : A}, (r • a)⁻ = -r • a⁺
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.ι.congr_simp : ∀ {n : ℕ} (i j j_1 : Fin (n + 2)) (e_j : j = j_1) (hij : j ≠ i), SSet.horn.ι i j hij = SSet.horn.ι i j_1 ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The bijection between `ComposableArrows C 1` and `Arrow C`.  -/
CategoryTheory.ComposableArrows.arrowEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ComposableArrows C 1 ≃ CategoryTheory.Arrow C
-- Mathlib.Tactic.NormNum.BigOperators
/-- Determine whether the expression `n : Q(ℕ)` unifies with `0` or `Nat.succ n'`.

We do not use `norm_num` functionality because we want definitional equality,
not propositional equality, for use in dependent types.

Fails if neither of the options succeed.
 -/
Mathlib.Meta.Nat.unifyZeroOrSucc : (n : Q(ℕ)) → Lean.MetaM (Mathlib.Meta.Nat.UnifyZeroOrSuccResult n)
-- Init.Data.SInt.Lemmas
ISize.lt_asymm : ∀ {a b : ISize}, a < b → ¬b < a
-- Mathlib.Topology.Bornology.Constructions
boundedSpace_induced_iff : ∀ {α : Type u_5} {β : Type u_6} [inst : Bornology β] {f : α → β}, BoundedSpace α ↔ Bornology.IsBounded (Set.range f)
-- Mathlib.Algebra.Divisibility.Basic
DecompositionMonoid.primal : ∀ {α : Type u_1} {inst : Semigroup α} [self : DecompositionMonoid α] (a : α), IsPrimal a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.zoom_del : ∀ {α : Type u_1} {cut : α → Ordering} {path : RBTree.RBNode.Path α} {t' : RBTree.RBNode α}
  {path' : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  RBTree.RBNode.zoom cut t path = (t', path') →
    path.del (RBTree.RBNode.del cut t)
        (match t with
        | RBTree.RBNode.node c l v r => c
        | x => RBTree.RBColor.red) =
      path'.del t'.delRoot
        (match t' with
        | RBTree.RBNode.node c l v r => c
        | x => RBTree.RBColor.red)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasStrongEpiImages.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C],
  (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)) →
    CategoryTheory.Limits.HasStrongEpiImages C
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_union_mem_segment : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {f : α → E} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ →
          MeasureTheory.IntegrableOn f s μ →
            MeasureTheory.IntegrableOn f t μ →
              ⨍ (x : α) in s ∪ t, f x ∂μ ∈ segment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_onFinset : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (s : Finset α) (f : α → M)
  (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) (g : α → M → N),
  (∀ i ∈ s, g i 0 = 1) → (Finsupp.onFinset s f hf).prod g = ∏ a ∈ s, g a (f a)
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iUnion : ∀ {α : Type u_1} {ι : Sort u_3} [inst : LE α] {f : ι → Set α}, (∀ (i : ι), IsUpperSet (f i)) → IsUpperSet (⋃ i, f i)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The cone hull of a convex set is simply the union of the open halflines through that set.  -/
ConvexCone.mem_hull_of_convex : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} {x : M},
  Convex 𝕜 s → (x ∈ ConvexCone.hull 𝕜 s ↔ ∃ r, 0 < r ∧ x ∈ r • s)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R), ↑S.toNonUnitalSubsemiring = ↑S
-- Init.Data.SInt.Bitwise
Int8.toInt16_and : ∀ (a b : Int8), (a &&& b).toInt16 = a.toInt16 &&& b.toInt16
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.subtypeCasesOn'.eq_1 : @Std.Internal.subtypeCasesOn'✝ = @Subtype.casesOn
-- Mathlib.Algebra.Ring.NonZeroDivisors
mul_cancel_left_mem_nonZeroDivisorsLeft : ∀ {R : Type u_1} [inst : Ring R] {x y r : R}, r ∈ nonZeroDivisorsLeft R → (r * x = r * y ↔ x = y)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- Alternative `Valued` constructor for use when there is no preferred `UniformSpace` structure.  -/
Valued.mk' : {R : Type u} →
  [inst : Ring R] → {Γ₀ : Type v} → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Valued R Γ₀
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValueCast? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
        Std.Internal.List.getValueCast? k l₁
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Mul β] (f g : MeasureTheory.SimpleFunc α β)
  (a : α), (f * g) a = f a * g a
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- A real closed subspace `S`.  -/
StandardSubspace.toClosedSubmodule : {H : Type u_1} →
  [inst : NormedAddCommGroup H] → [inst_1 : InnerProductSpace ℂ H] → StandardSubspace H → ClosedSubmodule ℝ H
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Inductive construction of isomorphisms in `ComposableArrows C (n + 1)`: in order to
construct an isomorphism `F ≅ G`, it suffices to provide `α : F.obj' 0 ≅ G.obj' 0` and
`β : F.δ₀ ≅ G.δ₀` such that `F.map' 0 1 ≫ app' β.hom 0 = α.hom ≫ G.map' 0 1`.  -/
CategoryTheory.ComposableArrows.isoMkSucc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      {F G : CategoryTheory.ComposableArrows C (n + 1)} →
        (α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) →
          (β : F.δ₀ ≅ G.δ₀) →
            CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
                  (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) =
                CategoryTheory.CategoryStruct.comp α.hom
                  (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯) →
              (F ≅ G)
-- Mathlib.Algebra.DirectSum.LinearMap
LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [inst_3 : DecidableEq ι] {κ : ι → Type u_4} [inst_4 : (i : ι) → Fintype (κ i)]
  [inst_5 : (i : ι) → DecidableEq (κ i)] {s : Finset ι} (h : DirectSum.IsInternal fun i => N ↑i)
  (b : (i : ↥s) → Module.Basis (κ ↑i) R ↥(N ↑i)) (σ : ι → ι),
  (∀ (i : ι), σ i ≠ i) →
    ∀ {f : Module.End R M},
      (∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))) →
        (∀ i ∉ s, N i = ⊥) → ((LinearMap.toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag = 0
-- Std.Sat.CNF.Relabel
/-- Change the literal type in a `Clause` from `α` to `β` by using `r`.
 -/
Std.Sat.CNF.Clause.relabel : {α : Type u_1} → {β : Type u_2} → (α → β) → Std.Sat.CNF.Clause α → Std.Sat.CNF.Clause β
-- Batteries.Data.Array.Basic
Array.uget.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : USize) (e_i : i = i_1) (h : i.toNat < xs.size),
  xs.uget i h = xs_1.uget i_1 ⋯
-- Mathlib.Topology.Algebra.Group.Basic
/-- Inversion in a topological group as a homeomorphism.  -/
Homeomorph.inv : (G : Type u_1) → [inst : TopologicalSpace G] → [inst_1 : InvolutiveInv G] → [ContinuousInv G] → G ≃ₜ G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.forM_eq_forM_toList : ∀ {α : Type u} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM f t = (Std.DTreeMap.Internal.Impl.Const.toList t).forM fun a => f a.1 a.2
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_div_interval : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α] (s t : NonemptyInterval α),
  ↑(s / t) = ↑s / ↑t
-- Mathlib.CategoryTheory.Limits.Cones
/-- Postcomposing by the identity does not change the cone up to isomorphism.  -/
CategoryTheory.Limits.Cone.postcomposeId : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.id F) ≅
            CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.support_induce : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V} {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s),
  (SimpleGraph.Walk.induce s w hw).support = w.support.attachWith (Membership.mem s) hw
-- Mathlib.Algebra.Group.Center
Semigroup.mem_center_iff : ∀ {M : Type u_1} [inst : Semigroup M] {z : M}, z ∈ Set.center M ↔ ∀ (g : M), g * z = z * g
-- Aesop.RuleSet
Aesop.BaseRuleSet.merge : Aesop.BaseRuleSet → Aesop.BaseRuleSet → Aesop.BaseRuleSet
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.compl_I_eq_F : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), (↑IF.I)ᶜ = ↑IF.F
-- Init.Data.String.Basic
/-- Obtains the character at the given position in the string.  -/
String.Slice.Pos.get : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.endPos → Char
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ + f₂` at `x` is the
trailing coefficient of the function with the lowest order.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₂ x →
    meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x →
      meromorphicTrailingCoeffAt (fun z => f₁ z + f₂ z) x = meromorphicTrailingCoeffAt f₁ x
-- Std.Data.HashSet.Basic
/-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.get : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.HashSet α) → (a : α) → a ∈ m → α
-- Mathlib.Algebra.Order.Hom.Ring
/-- The identity map as an ordered ring isomorphism.  -/
OrderRingIso.refl : (α : Type u_2) → [inst : Mul α] → [inst_1 : Add α] → [inst_2 : LE α] → α ≃+*o α
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE_EToCycles : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_EToCycles._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_EToCycles._auto_3),
  CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) =
    X.cyclesMap f₁ f₂ f₁ f₂₃ (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.snd_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V],
  w ≠ u → ∀ (p : G.Walk u v) (h : w ∈ p.support), (p.takeUntil w h).snd = p.snd
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableAt.continuousAlternatingMap_apply_const : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G} [Finite ι],
  DifferentiableAt 𝕜 c x → ∀ (u : ι → F), DifferentiableAt 𝕜 (fun y => (c y) u) x
-- Mathlib.Algebra.Category.Ring.Basic
/-- The object in the category of commutative semirings associated to a type equipped with the
appropriate typeclasses.  -/
CommSemiRingCat.of : (carrier : Type u) → [commSemiring : CommSemiring carrier] → CommSemiRingCat
-- Mathlib.Topology.NhdsWithin
Topology.IsInducing.map_nhdsSet_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsInducing f → ∀ (s : Set α), Filter.map f (nhdsSet s) = nhdsSetWithin (f '' s) (Set.range f)
-- Mathlib.Algebra.GroupWithZero.Basic
ne_zero_pow : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ}, n ≠ 0 → a ^ n ≠ 0 → a ≠ 0
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle** on a closed ball: if `f : E → F` is continuous on a closed ball,
is complex differentiable on the corresponding open ball, and the norm `‖f w‖` takes its maximum
value on the open ball at its center, then the norm `‖f w‖` is constant on the closed ball.  -/
Complex.norm_eqOn_closedBall_of_isMaxOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {z : E} {r : ℝ},
  DiffContOnCl ℂ f (Metric.ball z r) →
    IsMaxOn (norm ∘ f) (Metric.ball z r) z → Set.EqOn (norm ∘ f) (Function.const E ‖f z‖) (Metric.closedBall z r)
-- Mathlib.Logic.Basic
iff_not_comm : ∀ {a b : Prop}, (a ↔ ¬b) ↔ (b ↔ ¬a)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeffAddEquiv_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (self : AddMonoidAlgebra R M),
  AddMonoidAlgebra.coeffAddEquiv self = self.coeff
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.mk.injEq : ∀ {X Y : AlgebraicGeometry.Scheme} (toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace),
  ({ toLRSHom' := toLRSHom' } = { toLRSHom' := toLRSHom'_1 }) = (toLRSHom' = toLRSHom'_1)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ioi.inj : ∀ {n n_1 : Lean.Term}, BigOperators.FinsetResult.Ioi✝ n = BigOperators.FinsetResult.Ioi✝ n_1 → n = n_1