mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.ReducedWord.exists_normalWord_prod_eq : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : HNNExtension.NormalWord.TransversalPair G A B)
  (w : HNNExtension.NormalWord.ReducedWord G A B),
  ∃ w',
    HNNExtension.NormalWord.ReducedWord.prod φ w'.toReducedWord = HNNExtension.NormalWord.ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ HNNExtension.toSubgroup A B (-u)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Reachable.refl : ∀ {V : Type u} [inst : Quiver V] (a : V), Quiver.Reachable a a
-- Mathlib.Logic.Relation
Relation.symmGen_swap : ∀ {α : Type u_1} (r : α → α → Prop), Relation.SymmGen (Function.swap r) = Relation.SymmGen r
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_wr : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (n d : aig.RefVec w) (wn wr : ℕ) (q r : aig.RefVec w) (qbv rbv : BitVec w),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr =
    (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wr
-- Mathlib.RingTheory.QuasiFinite.Polynomial
/-- If `P` is a prime of `R[X]/I` that is quasi finite over `R`,
then `I` is not contained in `(P ∩ R)[X]`.

For usability, we replace `I` by the kernel of a surjective map `R[X] →ₐ[R] S`.  -/
Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S),
  Function.Surjective ⇑f →
    ∀ (P : Ideal S) [inst_3 : P.IsPrime] [Algebra.QuasiFiniteAt R P],
      ¬RingHom.ker f ≤ Ideal.map Polynomial.C (Ideal.under R P)
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.J_mem : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R],
  Matrix.J l R ∈ Matrix.symplecticGroup l R
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromCommLeftNeg_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (a : ↥S.leftNeg), S.fromCommLeftNeg a = S.fromLeftNeg a
-- Init.Data.Option.Lemmas
Option.any_guard : ∀ {α : Type u_1} {q p : α → Bool} (a : α), Option.any q (Option.guard p a) = (p a && q a)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.ofUnique.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Add M] [inst_3 : Add N]
  [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N],
  ContinuousAddEquiv.ofUnique = { toAddEquiv := AddEquiv.ofUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.interior : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage (interior s) (interior t)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.toIsIrreducible : ∀ {ι : 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} [self : P.IsG2],
  P.IsIrreducible
-- Mathlib.Order.SymmDiff
bihimp_himp_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b ⇨ b = a ⊔ b
-- Init.Data.Nat.Lcm
Nat.lcm_mul_left_left : ∀ (m n : ℕ), (m * n).lcm n = m * n
-- Mathlib.Topology.UniformSpace.Cauchy
IsCompact.totallyBounded : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, IsCompact s → TotallyBounded s
-- Lean.Elab.Tactic.Monotonicity
Lean.Meta.Monotonicity.headBetaUnderLambda : Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.inf_lie : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I J : LieIdeal R L), ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆
-- Aesop.Rule.Name
Aesop.RuleName.instToJson : Lean.ToJson Aesop.RuleName
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList.eq_2 : Nat.primeFactorsList 1 = []
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.eq_of_add_eq_add_right : ∀ {a b c : Cardinal.{u_1}}, a + b = c + b → b < Cardinal.aleph0 → a = c
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.smul_const : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K β] (k : K) (b : β),
  k • MeasureTheory.SimpleFunc.const α b = MeasureTheory.SimpleFunc.const α (k • b)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.liftAux.smulₛₗ : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (r : R)
  (x : TensorProduct R M N), (TensorProduct.liftAux f') (r • x) = σ₁₂ r • (TensorProduct.liftAux f') x
-- Mathlib.Computability.StateTransition
/-- Run a state transition function `σ → Option σ` "to completion". The return value is the last
state returned before a `none` result. If the state transition function always returns `some`,
then the computation diverges, returning `Part.none`.  -/
StateTransition.eval : {σ : Type u_1} → (σ → Option σ) → σ → Part σ
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.recvReady' : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] →
        [MonadLiftT IO m] → [MonadLiftT BaseIO m] → ℕ → Std.AtomicT (Std.Bounded.State✝ α) m Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β k}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl = true},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.getKey a h₁ =
    if h₂ : compare k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubmonoid.even.eq_1 : ∀ (M : Type u_1) [inst : AddCommMonoid M],
  AddSubmonoid.even M = { toAddSubsemigroup := AddSubsemigroup.even M, zero_mem' := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Const.equiv_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : BEq β] [LawfulBEq β], m₁.WF → m₂.WF → (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.homCategory_id_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.CategoryStruct.id η).as.app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Taking the `sum` under `h` is an additive homomorphism, if `h` is an additive homomorphism.
This is a more general version of `SkewMonoidAlgebra.sum_add_index'`;
the latter has simpler hypotheses.  -/
SkewMonoidAlgebra.sum_add_index : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : DecidableEq G]
  [inst_2 : AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S},
  (∀ a ∈ f.support ∪ g.support, h a 0 = 0) →
    (∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_iInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} [inst_1 : Finite β]
  {f : β → L.BoundedFormula α n} {v : α → M} {v' : Fin n → M},
  (FirstOrder.Language.BoundedFormula.iInf f).Realize v v' ↔ ∀ (b : β), (f b).Realize v v'
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {x : E},
  IsSymmSndFDerivWithinAt 𝕜 f t x →
    t ∈ nhdsWithin x s →
      ContDiffWithinAt 𝕜 2 f t x → UniqueDiffOn 𝕜 s → UniqueDiffOn 𝕜 t → x ∈ s → IsSymmSndFDerivWithinAt 𝕜 f s x
-- Lean.Parser.Term
Lean.Parser.Term.logNamedErrorMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.PicardGroup
TensorProduct.equivOfCompatibleSMul.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_22) (S : Type u_23) (M : Type u_24) (N : Type u_25)
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : CommSemiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : SMulCommClass R A M]
  [inst_9 : CommSemiring S] [inst_10 : Module S M] [inst_11 : SMulCommClass R S M] [inst_12 : SMulCommClass A S M]
  [inst_13 : TensorProduct.CompatibleSMul R A M N] [inst_14 : TensorProduct.CompatibleSMul A R M N],
  TensorProduct.equivOfCompatibleSMul R A S M N =
    { toLinearMap := TensorProduct.mapOfCompatibleSMul R A S M N,
      invFun := ⇑(TensorProduct.mapOfCompatibleSMul A R S M N), left_inv := ⋯, right_inv := ⋯ }
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex? : ℕ → (s : String) → s.Pos → ℕ → Option (s.Pos × ℕ)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The GCD is a divisor of the second element.  -/
GCDMonoid.gcd_dvd_right : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α] (a b : α), gcd a b ∣ b
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra),
  (CategoryTheory.Monad.algebraFunctorOfMonadHomId.inv.app X).f =
    (CategoryTheory.Iso.refl
        ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).inv
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Monoid M],
  MonoidAlgebra.mapDomainRingHom R (MonoidHom.id M) = RingHom.id (MonoidAlgebra R M)
-- Std.Http.Data.URI.Encoding
/-- Converts a hexadecimal digit character to its numeric value (0-15).
Returns `none` if the character is not a valid hex digit.
 -/
Std.Http.URI.hexDigitToUInt8? : UInt8 → Option UInt8
-- Lean.Meta.Basic
/-- Appends a `'` to the namen of the given free variables.  -/
Lean.Meta.withPrimedNames : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Array Lean.Expr → n α → n α
-- Init.Data.SInt.Lemmas
Int8.toBitVec_div : ∀ {a b : Int8}, (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
-- Mathlib.Order.Concept
Concept.extent_min : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r), (c ⊓ d).extent = c.extent ∩ d.extent
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- The double dual isomorphism of a finite abelian group.  -/
AddChar.doubleDualEquiv : {α : Type u_1} → [inst : AddCommGroup α] → [Finite α] → α ≃+ AddChar (AddChar α ℂ) ℂ
-- Mathlib.Order.Interval.Finset.Nat
Finset.range_eq_Ico : ∀ (a : ℕ), Finset.range a = Finset.Ico 0 a
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Estimate for `log⁺` of a product. Special case of `Real.posLog_mul` where one of
the factors is a natural number.  -/
Real.posLog_nat_mul : ∀ {x : ℝ} {n : ℕ}, (↑n * x).posLog ≤ Real.log ↑n + x.posLog
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
/-- Converting a commutative group object in `Type u` into a group.  -/
CommGrpTypeEquivalenceCommGrp.functor : CategoryTheory.Functor (CategoryTheory.CommGrp (Type u)) CommGrpCat
-- Mathlib.FieldTheory.SeparableDegree
/-- A random bijection between `Field.Emb F E` and `Field.Emb F K` when `E` and `K` are isomorphic
as `F`-algebras.  -/
Field.embEquivOfEquiv : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) → [inst_3 : Field K] → [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → Field.Emb F E ≃ Field.Emb F K
-- Mathlib.Order.BoundedOrder.Monotone
StrictMono.minimal_preimage_bot : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] [inst_2 : OrderBot β] {f : α → β},
  StrictMono f → ∀ {a : α}, f a = ⊥ → ∀ (x : α), a ≤ x
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SimpCacheKey.variant : Lean.Elab.Tactic.Grind.SimpCacheKey → Lean.Name
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (unit : CategoryTheory.Functor.id C ⟶ F.comp G) →
              (counit : G.comp F ⟶ CategoryTheory.Functor.id D) →
                autoParam
                    (∀ (X : C),
                      CategoryTheory.CategoryStruct.comp (F.map (unit.app X)) (counit.app (F.obj X)) =
                        CategoryTheory.CategoryStruct.id (F.obj X))
                    CategoryTheory.Adjunction.left_triangle_components._autoParam →
                  autoParam
                      (∀ (Y : D),
                        CategoryTheory.CategoryStruct.comp (unit.app (G.obj Y)) (G.map (counit.app Y)) =
                          CategoryTheory.CategoryStruct.id (G.obj Y))
                      CategoryTheory.Adjunction.right_triangle_components._autoParam →
                    (F ⊣ G)
-- Mathlib.Order.CompleteLattice.Basic
iSup_range' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : SupSet α] (g : β → α) (f : ι → β), ⨆ b, g ↑b = ⨆ i, g (f i)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_div_iff_mul_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b c : α}, a < c / b ↔ a * b < c
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.cochainComplexXIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) (n : ℤ) (k : ℕ)
  (h : -↑k = n), R.cochainComplexXIso n k h = R.cochainComplexXIso n k h
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.ord_univ : Cardinal.univ.{u, v}.ord = Ordinal.univ.{u, v}
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.coev_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : A ⟹ (CategoryTheory.MonoidalCategory.tensorLeft A).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f)) h)
-- Mathlib.Data.ENat.Basic
ENat.natCast_add : ∀ (m n : ℕ), ↑(m + n) = ↑m + ↑n
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Vector addition in an additive monoid localization.  -/
AddOreLocalization.hvadd : {R : Type u_1} →
  {M : Type u_3} →
    {X : Type u_4} →
      [inst : AddMonoid M] →
        {S : AddSubmonoid M} →
          [inst_1 : AddOreLocalization.AddOreSet S] →
            [inst_2 : AddAction M X] → [VAdd R M] → R → AddOreLocalization S X → AddOreLocalization S X
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.Quotient.symm_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (γ : Path.Homotopic.Quotient x₀ x₁),
  γ.symm.trans γ = Path.Homotopic.Quotient.refl x₁
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_coe : ∀ {M : Type u_3} [inst : CommMonoid M] (l : List M), (↑l).prod = l.prod
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap'_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData)
  (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData) {Z : C} (h : h₃.K ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ₁ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ₂ h₂ h₃) h)
-- Lean.Language.Basic
Lean.Language.SnapshotBundle.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (old? : Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α)))
  (new : IO.Promise α), sizeOf { old? := old?, new := new } = 1 + sizeOf old? + sizeOf new
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.mul_zsmul : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (n m : ℤ) (a : M), (n * m) • a = n • m • a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.filterMap_eq_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {f : (a : α) → β a → γ a} {l : Std.DHashMap.Internal.AssocList α β},
  Std.DHashMap.Internal.AssocList.filterMap (fun k v => some (f k v)) l = Std.DHashMap.Internal.AssocList.map f l
-- Mathlib.Order.Filter.Pointwise
Filter.comap_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {f : Filter α}, Filter.comap Neg.neg f = -f
-- Init.Data.UInt.Lemmas
USize.neg_mul_comm : ∀ (a b : USize), -a * b = a * -b
-- Mathlib.Data.ZMod.Basic
ZMod.cast_add : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (a b : ZMod n), (a + b).cast = a.cast + b.cast
-- Mathlib.Data.FunLike.Basic
/-- The coercion to functions must be injective.  -/
DFunLike.coe_injective : ∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β],
  Function.Injective DFunLike.coe
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeries.eq_3 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E)
  (x_1 : ℕ), (x_1 = 0 → False) → (x_1 = 1 → False) → f.fpowerSeries x x_1 = 0
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions of length three are unchanged under `2`-Freiman isomorphisms.  -/
threeAPFree_image : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s A : Set α} {t : Set β}
  {f : α → β}, IsAddFreimanIso 2 s t f → A ⊆ s → (ThreeAPFree (f '' A) ↔ ThreeAPFree A)
-- Mathlib.Computability.Ackermann
ack_le_iff_left : ∀ {m₁ m₂ n : ℕ}, ack m₁ n ≤ ack m₂ n ↔ m₁ ≤ m₂
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.invertibleEquivDetInvertible_symm_apply : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A.det], A.invertibleEquivDetInvertible.symm inst_3 = A.invertibleOfDetInvertible
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.State.mk.injEq : ∀ (found : Lean.NameSet) (vars : Array Lean.Elab.Term.PatternVar) (found_1 : Lean.NameSet)
  (vars_1 : Array Lean.Elab.Term.PatternVar),
  ({ found := found, vars := vars } = { found := found_1, vars := vars_1 }) = (found = found_1 ∧ vars = vars_1)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.SMul.aux_of : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {R' : Type u_22} [inst_5 : SMul R' M] (r : R')
  (m : M) (n : N), (TensorProduct.SMul.aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n
-- Init.Data.Int.Lemmas
Int.neg_eq_neg_one_mul : ∀ (a : ℤ), -a = -1 * a
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.inst : ∀ {R : Type u_1} [inst : CommRing R], IsIntegrallyClosedIn R R
-- Mathlib.Analysis.MeanInequalitiesPow
NNReal.rpow_add_rpow_le_add : ∀ {p : ℝ} (a b : NNReal), 1 ≤ p → (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
-- Mathlib.Algebra.Group.Defs
add_neg_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + (-a + b) = b
-- Mathlib.Data.Matrix.Mul
/-- A version of `mul_eq_one_comm` that works for square matrices with rectangular types.  -/
Matrix.mul_eq_one_comm_of_equiv : ∀ {m : Type u_10} {n : Type u_11} {R : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : MulOne R] [inst_5 : AddCommMonoid R] [IsStablyFiniteRing R] {A : Matrix m n R}
  {B : Matrix n m R} (e : m ≃ n), A * B = 1 ↔ B * A = 1
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_impl_16 : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α (Task Dynamic) → NonScalar
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {s : Set (β × γ)},
  MeasurableSet s → ((κ.prod η) a) s = ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `FunLike.coe_smul`. -/
MeasureTheory.OuterMeasure.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionGluedTo : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.IsPreimmersion I.gluedTo
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.edist_lt_of_edist_lt_div : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β},
  LipschitzOnWith K f s → ∀ {x y : α}, x ∈ s → y ∈ s → ∀ {d : ENNReal}, edist x y < d / ↑K → edist (f x) (f y) < d
-- Mathlib.Algebra.GroupWithZero.Invertible
/-- `a` is the inverse of `a⁻¹`  -/
invertibleInv : {α : Type u} → [inst : GroupWithZero α] → {a : α} → [Invertible a] → Invertible a⁻¹
-- Mathlib.Analysis.InnerProductSpace.Basic
flip_innerₗ : ∀ (F : Type u_3) [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F], (innerₗ F).flip = innerₗ F
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.qr₁'_mod : ∀ (a b ab : ℕ) (r : ℤ),
  a % 2 = 1 →
    b % 4 = 1 → b % a = ab → Mathlib.Meta.NormNum.jacobiSymNat ab a = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the second map `L → R`  -/
CategoryTheory.Limits.MultispanShape.snd : (self : CategoryTheory.Limits.MultispanShape) → self.L → self.R
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Fintype.piFinset_inv : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Inv (α i)] (s : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => (s i)⁻¹) = (Fintype.piFinset s)⁻¹
-- Lean.Meta.Tactic.Simp.Main
/-- Auxiliary `dsimproc` for not visiting proof terms.  -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.doNotVisitProofs : Lean.Meta.Simp.DSimproc
-- Mathlib.Logic.Basic
/-- One of **de Morgan's laws**: the negation of a conjunction is logically equivalent to the
disjunction of the negations.  -/
not_and_or : ∀ {a b : Prop}, ¬(a ∧ b) ↔ ¬a ∨ ¬b