mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP_bound : ∀ (r : ℝ), 0 < r → ∀ (s : ℂ), ‖s‖ < r → ∀ (l : ℂ), 2 * r ≤ ‖l‖ → ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The coinduced topology on `M` from a family of continuous linear maps into `M`, which is the
finest topology that makes it into a topological module and makes every map continuous.  -/
TopModuleCat.coinduced : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M : ModuleCat R} → {I : Type u_1} → {X : I → TopModuleCat R} → ((i : I) → (X i).toModuleCat ⟶ M) → TopModuleCat R
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.eq : Mathlib.Tactic.Translate.CastKind✝
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.Hom.id`. -/
AlgebraicGeometry.Scheme.Cover.Hom.id : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (E : CategoryTheory.PreZeroHypercover S) → E.Hom E
-- Init.Core
lt_of_eq_of_lt : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a = b → b < c → a < c
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_eq_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k fallback : α}, t.contains k = true → t.getKeyD k fallback = k
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run a tactic at each proof step. See `tryAtEachStepCore` for details.  -/
Mathlib.TacticAnalysis.tryAtEachStep : (Lean.Syntax → Lean.MVarId → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) → Mathlib.TacticAnalysis.Config
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Real.measurableSpace : MeasurableSpace ℝ
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.normedGroup : {E : Type u_1} →
  [inst : NormedGroup E] → {S : Type u_2} → [inst_1 : SetLike S E] → [SubgroupClass S E] → (s : S) → NormedGroup ↥s
-- Mathlib.Order.SuccPred.Limit
WithBot.isPredLimit_bot : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMinOrder α], Order.IsPredLimit ⊥
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.mk.sizeOf_spec : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} [inst_2 : SizeOf A] [inst_3 : SizeOf B] (toRingHom : A →+* B)
  (ideal_comp : Ideal.map toRingHom I ≤ J)
  (dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom a) = toRingHom (hI.dpow n a)),
  sizeOf { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := dpow_comp } = 1 + sizeOf toRingHom
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- Mapping a `zeroKernelFork` of `f : X ⟶ Y` along a functor `G` that preserves zero morphisms
is isomorphic to the `zeroKernelFork` of `G.map f`.  -/
CategoryTheory.Limits.mapZeroKernelFork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.Limits.HasZeroObject C] →
                  [inst_6 : CategoryTheory.Limits.HasZeroObject D] →
                    {X Y : C} →
                      (f : X ⟶ Y) →
                        (CategoryTheory.Limits.kernel.zeroKernelFork f).map G ≅
                          CategoryTheory.Limits.kernel.zeroKernelFork (G.map f)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `conflict?` is `some ..` if a contradictory constraint was derived.
This field is only set when `caseSplits` is `true`. Otherwise, we
can convert `UnsatProof` into a Lean term and close the current `grind` goal.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.conflict? : Lean.Meta.Grind.Arith.Cutsat.State → Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.id_f₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.CategoryStruct.id S).f₁ = CategoryTheory.CategoryStruct.id S.L₁
-- Mathlib.Data.Set.Basic
Set.mem_ite_empty_left : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : Set α) (x : α), (x ∈ if p then ∅ else t) ↔ ¬p ∧ x ∈ t
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_opow_mul : ∀ {b v : Ordinal.{u_1}}, 1 < b → ∀ (u : Ordinal.{u_1}), v ≠ 0 → Ordinal.log b (b ^ u * v) = u + Ordinal.log b v
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R],
  IsUnit 2 → IsUnit W.Δ → W.twoTorsionPolynomial.discr ≠ 0
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite : ∀ {k : Type u} [inst : Ring k] {J : Type} [Finite J] (Z : J → ModuleCat k) [∀ (j : J), Module.Finite k ↑(Z j)],
  Module.Finite k ↑(∐ fun j => Z j)
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_zero_eq_preimage_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Construct a bundled `AddCommMonCat` from the underlying type and typeclass.  -/
AddCommMonCat.of : (M : Type u) → [AddCommMonoid M] → AddCommMonCat
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Ico_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Ico (Fin.castLE h i) (Fin.castLE h j) = Set.Ico i j
-- Mathlib.Data.Set.Function
/-- **Alias** of the reverse direction of `Equiv.bijOn_symm`. -/
Set.BijOn.equiv_symm : ∀ {α : Type u_1} {β : Type u_2} {e : α ≃ β} {s : Set α} {t : Set β}, Set.BijOn (⇑e) s t → Set.BijOn (⇑e.symm) t s
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instNonUnitalAlgHomClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B], NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (F : CategoryTheory.Functor C C) →
        [F.Additive] → CategoryTheory.Preadditive (CategoryTheory.Endofunctor.Coalgebra F)
-- Mathlib.Order.BourbakiWitt
/-- The base point is the least element of an admissible set  -/
ChainCompletePartialOrder.IsAdmissible.base_isLeast : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {s : Set α},
  ChainCompletePartialOrder.IsAdmissible x f s → IsLeast s x
-- Mathlib.Order.RelIso.Basic
RelEmbedding.sumLiftRelInl_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : α),
  (RelEmbedding.sumLiftRelInl r s) val = Sum.inl val
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.mk.congr_simp : ∀ {n : ℕ} (length : ℕ) (partSize : Fin length → ℕ) (partSize_pos : ∀ (m : Fin length), 0 < partSize m)
  (emb emb_1 : (m : Fin length) → Fin (partSize m) → Fin n) (e_emb : emb = emb_1)
  (emb_strictMono : ∀ (m : Fin length), StrictMono (emb m))
  (parts_strictMono : StrictMono fun m => emb m ⟨partSize m - 1, ⋯⟩)
  (disjoint : Set.univ.PairwiseDisjoint fun m => Set.range (emb m)) (cover : ∀ (x : Fin n), ∃ m, x ∈ Set.range (emb m)),
  { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
      parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover } =
    { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb_1, emb_strictMono := ⋯,
      parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct_join.aux.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Sort u_2)
  (h_1 : Unit → motive none) (h_2 : (s : Stream'.WSeq α) → (S : Stream'.WSeq (Stream'.WSeq α)) → motive (some (s, S))),
  (match none with
    | none => h_1 ()
    | some (s, S) => h_2 s S) =
    h_1 ()
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity : ∀ {A B : GrpCat} (f : A ⟶ B) (x : ↑B),
  ((GrpCat.SurjectiveOfEpiAuxs.g f) x) GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
-- Init.Data.SInt.Basic
Int32.ofUInt32.sizeOf_spec : ∀ (toUInt32 : UInt32), sizeOf { toUInt32 := toUInt32 } = 1 + sizeOf toUInt32
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.monic_freeMonic : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ), (Polynomial.freeMonic R n).Monic
-- Std.Http.Data.Method
/-- HTTP/2 connection preface (not used in application code).
Source: https://www.rfc-editor.org/rfc/rfc9113#section-3.4
 -/
Std.Http.Method.pri : Std.Http.Method
-- Init.Data.SInt.Lemmas
ISize.toBitVec_sub : ∀ {a b : ISize}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.RingTheory.WittVector.MulP
WittVector.wittMulN.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittMulN p 0 = 0
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.quotientQuotientEquivQuotient.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (c d : AddCon M) (h : c ≤ d),
  c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_add' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.supp_injective_iff : ∀ {V : Type u} {G : SimpleGraph V} {a₁ a₂ : G.ConnectedComponent}, a₁ = a₂ ↔ a₁.supp = a₂.supp
-- Mathlib.Data.Sign.Defs
sign_one : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : DecidableLT α]
  [Nontrivial α], SignType.sign 1 = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.PreservesTerminal.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasTerminal D]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G],
  (CategoryTheory.Limits.PreservesTerminal.iso G).hom = CategoryTheory.Limits.terminalComparison G
-- Init.Data.List.Basic
/-- Checks whether a list is empty.

`O(1)`.

Examples:
* `[].isEmpty = true`
* `["grape"].isEmpty = false`
* `["apple", "banana"].isEmpty = false`
 -/
List.isEmpty : {α : Type u} → List α → Bool
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.instInhabited : {α : Type u_1} → [inst : MeasurableSpace α] → Inhabited (MeasureTheory.JordanDecomposition α)
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.mul : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [inst : Add α] [inst_1 : Mul β] [inst_2 : HasDistribNeg β],
  Function.Antiperiodic f c → Function.Antiperiodic g c → Function.Periodic (f * g) c
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.coe_toContinuousLinearEquiv : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F), ↑↑e.toContinuousLinearEquiv = ↑e
-- Mathlib.Data.Sigma.Order
/-- The lexicographical `≤` on a sigma type.  -/
Sigma.Lex.LE : {ι : Type u_1} → {α : ι → Type u_2} → [LT ι] → [(i : ι) → LE (α i)] → LE (Σₗ (i : ι), α i)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_smul : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), ∀ U ∈ p.basisSets, ∃ V ∈ nhds 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U
-- Aesop.Script.Main
_private.Aesop.Script.Main.0.Aesop.Script.UScript.optimize.structureStatic : Aesop.Script.UScript →
  Bool → Lean.Meta.SavedState → Lean.MVarId → Lean.MetaM (Option (Aesop.Script.SScript × Aesop.ScriptGenerated))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toArray_rcc : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m...=n).toArray.size), (m...=n).toArray[i] = m + ↑i
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalCutsat : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one G)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.commutator G) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) G))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.queryMap : Std.DHashMap Lean.Name fun x => Lean.Name × Array (Lean.MacroM (Lean.TSyntax `term))
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_one : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁), MvPolynomial.eval₂ f g 1 = 1
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsFractionRingAtPrimeFractionRing : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {P : Ideal R} [inst_2 : P.IsPrime],
  IsFractionRing (Localization.AtPrime P) (FractionRing R)
-- Mathlib.SetTheory.ZFC.Basic
/-- `omega` is the first infinite von Neumann ordinal  -/
ZFSet.omega : ZFSet.{u_1}
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`.  -/
QuadraticModuleCat.instMonoidalCategory.tensorObj : {R : Type u} → [inst : CommRing R] → [Invertible 2] → QuadraticModuleCat R → QuadraticModuleCat R → QuadraticModuleCat R
-- Init.Data.List.FinRange
_private.Init.Data.List.FinRange.0.List.ofFnM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α),
  List.ofFnM f = List.reverse <$> Fin.foldlM n (fun xs i => (fun x => x :: xs) <$> f i) []
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.card_vadd_finset_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α},
  (a +ᵥ s).card ≤ s.card
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_mul_of_coprime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a b : Associates α},
  b ≠ 0 →
    ∀ {p : Associates α},
      Irreducible p →
        (∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) →
          p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
Construct the colimiting algebra from the map `λ : TL ⟶ L` given by `lambda`. We are required to
show it satisfies the two algebra laws, which follow from the algebra laws for the image of `D` and
our `commuting` lemma.
 -/
CategoryTheory.Monad.ForgetCreatesColimits.coconePoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          {D : CategoryTheory.Functor J T.Algebra} →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) →
              CategoryTheory.Limits.IsColimit c →
                [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] →
                  [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] → T.Algebra
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and left homology data `h₁` and `h₂`
for `S₁` and `S₂` respectively, this is the induced morphism `h₁.K ⟶ h₁.K` on cycles.  -/
CategoryTheory.ShortComplex.cyclesMap' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ⟶ S₂) → (h₁ : S₁.LeftHomologyData) → (h₂ : S₂.LeftHomologyData) → h₁.K ⟶ h₂.K
-- Mathlib.Tactic.GRewrite.Core
/-- Rewrite `e` using the relation `hrel : x ~ y`, and construct an implication proof
using the `gcongr` tactic to discharge this goal.

if `forwardImp = true`, we prove that `e → eNew`; otherwise `eNew → e`.

If `symm = false`, we rewrite `e` to `eNew := e[x/y]`; otherwise `eNew := e[y/x]`.

The code aligns with `Lean.MVarId.rewrite` as much as possible.
 -/
Lean.MVarId.grewrite : Lean.MVarId →
  Lean.Expr →
    Lean.Expr →
      Array (Lean.MVarId × Array Lean.LocalDecl) →
        Bool → Bool → Mathlib.Tactic.GRewrite.Config → Lean.MetaM Mathlib.Tactic.GRewrite.GRewriteResult
-- Mathlib.Data.List.Lattice
List.bagInter.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x x_1 : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x []) (h_3 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂) (x_2 : List α),
  x = x_2 →
    x_1 = [] →
      (x_2 = [] → False) →
        (match x, x_1 with
          | [], x => h_1 x
          | x, [] => h_2 x
          | a :: l₁, l₂ => h_3 a l₁ l₂) ≍
          h_2 x_2
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isIso_iff_isIso_coyoneda_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.coyoneda.map f.op).app c)
-- Mathlib.Algebra.AddConstMap.Basic
/-- If `f` is an `AddConstMap`, then so is `(c +ᵥ f ·)`.  -/
AddConstMap.instVAddOfVAddAssocClass : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} → {b : H} → {K : Type u_3} → [inst_2 : VAdd K H] → [VAddAssocClass K H H] → VAdd K (AddConstMap G H a b)
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.edge_comp_symm : ∀ {V : Type u_1} {G : SimpleGraph V}, SimpleGraph.Dart.edge ∘ SimpleGraph.Dart.symm = SimpleGraph.Dart.edge
-- Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
/-- A function `f` has a sum in a uniform additive group `α` if and only if it has that sum in the
completion of `α`.  -/
hasSum_iff_hasSum_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : IsUniformAddGroup α]
  {L : SummationFilter β} (f : β → α) (a : α), HasSum (⇑UniformSpace.Completion.toCompl ∘ f) (↑a) L ↔ HasSum f a L
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.quasiMeasurePreserving_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}, MeasureTheory.Measure.QuasiMeasurePreserving Prod.snd (μ.prod ν) ν
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given `R`-module X and `S`-module Y, any `g : Y ⟶ (coextendScalars f).obj X`
corresponds to `(restrictScalars f).obj Y ⟶ X` by `y ↦ g y 1`
 -/
ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          {X : ModuleCat R} →
            {Y : ModuleCat S} → (Y ⟶ (ModuleCat.coextendScalars f).obj X) → ((ModuleCat.restrictScalars f).obj Y ⟶ X)
-- Lean.Server.References
Lean.Server.Ilean.mk.inj : ∀ {version : ℕ} {module : Lean.Name} {directImports : Array Lean.Lsp.ImportInfo} {references : Lean.Lsp.ModuleRefs}
  {decls : Lean.Lsp.Decls} {version_1 : ℕ} {module_1 : Lean.Name} {directImports_1 : Array Lean.Lsp.ImportInfo}
  {references_1 : Lean.Lsp.ModuleRefs} {decls_1 : Lean.Lsp.Decls},
  { version := version, module := module, directImports := directImports, references := references, decls := decls } =
      { version := version_1, module := module_1, directImports := directImports_1, references := references_1,
        decls := decls_1 } →
    version = version_1 ∧
      module = module_1 ∧ directImports = directImports_1 ∧ references = references_1 ∧ decls = decls_1
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mul.match_1.splitter : {v : Lean.Level} →
  {M : Q(Type v)} →
    (motive : Mathlib.Tactic.FieldSimp.qNF q(«$M») → Mathlib.Tactic.FieldSimp.qNF q(«$M») → Sort u_1) →
      (x x_1 : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) →
        ((l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive [] l) →
          ((l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → (l = [] → False) → motive l []) →
            ((a₁ : ℤ) →
                (x₁ : Q(«$M»)) →
                  (k₁ : ℕ) →
                    (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
                      (a₂ : ℤ) →
                        (x₂ : Q(«$M»)) →
                          (k₂ : ℕ) →
                            (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)) →
              motive x x_1
-- Mathlib.Topology.MetricSpace.Gluing
Metric.glueDist_glued_points : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty Z] (Φ : Z → X)
  (Ψ : Z → Y) (ε : ℝ) (p : Z), Metric.glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  CompactSpace ↥(ProfiniteGrp.limitConePtAux F)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.imports.sizeOf_spec : sizeOf Lean.Lsp.FoldingRangeKind.imports = 1
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
FirstOrder.Language.presburger.term_realize_eq_add_dotProduct : ∀ {α : Type u_1} {A : Set ℕ} [inst : Fintype α] (t : (FirstOrder.Language.presburger.withConstants ↑A).Term α),
  ∃ k u, ∀ (v : α → ℕ), FirstOrder.Language.Term.realize v t = k + u ⬝ᵥ v
-- Mathlib.Data.Stream.Init
Stream'.bisim_simple : ∀ {α : Type u} (s₁ s₂ : Stream' α), s₁.head = s₂.head → s₁ = s₁.tail → s₂ = s₂.tail → s₁ = s₂