mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_iff_isLittleO`. -/
HasFDerivWithinAt.of_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {x : E},
  ((fun x' => f x' - f x - f' (x' - x)) =o[nhdsWithin x s] fun x' => x' - x) → HasFDerivWithinAt f f' s x
-- Init.Data.UInt.Lemmas
UInt32.ofInt_neg : ∀ (x : ℤ), UInt32.ofInt (-x) = -UInt32.ofInt x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.subset_of_mem_openRcNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} {U : TopologicalSpace.Opens α},
  U ∈ K.openRcNhds → ↑K ⊆ ↑U
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.DaylightSavingRule.mk.injEq : ∀ (name : String) (offset : Std.Time.TimeZone.Offset) (start end_ : Option Std.Time.TimeZone.TransitionRule)
  (name_1 : String) (offset_1 : Std.Time.TimeZone.Offset) (start_1 end__1 : Option Std.Time.TimeZone.TransitionRule),
  ({ name := name, offset := offset, start := start, end_ := end_ } =
      { name := name_1, offset := offset_1, start := start_1, end_ := end__1 }) =
    (name = name_1 ∧ offset = offset_1 ∧ start = start_1 ∧ end_ = end__1)
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `‖x + y‖ < ‖x‖ + ‖y‖`.
 -/
norm_add_lt_of_not_sameRay : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ¬SameRay ℝ x y → ‖x + y‖ < ‖x‖ + ‖y‖
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddZeroClass : {α : Type u_1} → [AddZeroClass α] → AddZeroClass αᵃᵒᵖ
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
/-- The centralizer of a subset of an additive semigroup.  -/
AddSubsemigroup.centralizer : {M : Type u_1} → Set M → [inst : AddSemigroup M] → AddSubsemigroup M
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_comp₂Measurable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : MeasurableSpace γ]
  [inst_8 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_9 : BorelSpace γ]
  [inst_10 : SecondCountableTopologyEither β γ] [inst_11 : MeasurableSpace δ]
  [inst_12 : TopologicalSpace.PseudoMetrizableSpace δ] [inst_13 : OpensMeasurableSpace δ]
  [inst_14 : SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β)
  (f₂ : α →ₘ[μ] γ), ↑(MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂) =ᵐ[μ] fun a => g (↑f₁ a) (↑f₂ a)
-- Mathlib.Control.Basic
CommApplicative.mk : ∀ {m : Type u → Type v} [inst : Applicative m] [toLawfulApplicative : LawfulApplicative m],
  (∀ {α β : Type u} (a : m α) (b : m β), Prod.mk <$> a <*> b = (fun b a => (a, b)) <$> b <*> a) → CommApplicative m
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A universally effective equivalence relation is an effective equivalence relation
`p₁, p₂ : R ⟶ A` such that the corresponding morphism `π : A ⟶ B` is a universal effective
epimorphism.  -/
CategoryTheory.UniversallyEffectiveEquivalenceRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R A : C} → (R ⟶ A) → (R ⟶ A) → Type (max u_1 v_1)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The restriction of a trivialization to a subset of the base.  -/
Bundle.Trivialization.restrictPreimage' : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              Bundle.Trivialization F proj →
                (s : Set B) → [Nonempty (↑s → F → ↑(proj ⁻¹' s))] → Bundle.Trivialization F (s.restrictPreimage proj)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- If a function is `C^k` on two open sets, it is also `C^n` on their union.  -/
ContMDiffOn.union_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} {s t : Set M},
  ContMDiffOn I I' n f s → ContMDiffOn I I' n f t → IsOpen s → IsOpen t → ContMDiffOn I I' n f (s ∪ t)
-- Lean.InternalExceptionId
Lean.InternalExceptionId.mk.injEq : ∀ (idx idx_1 : ℕ), ({ idx := idx } = { idx := idx_1 }) = (idx = idx_1)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.map_id : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F],
  CategoryTheory.Limits.end_.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.end_ F)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- Auxiliary function to defining scalar multiplication on tensor product.  -/
TensorProduct.SMul.aux : {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} → [SMul R' M] → R' → FreeAddMonoid (M × N) →+ TensorProduct R M N
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.mem_coboundaries_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (α : CochainComplex.HomComplex.Cocycle K L n) (m : ℤ),
  m + 1 = n → (α ∈ CochainComplex.HomComplex.coboundaries K L n ↔ ∃ β, CochainComplex.HomComplex.δ m n β = ↑α)
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- **Alias** of `CategoryTheory.Subfunctor.toFunctor_map`. -/
CategoryTheory.Subfunctor.toFunctor_map_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) {X Y : C} (i : X ⟶ Y),
  G.toFunctor.map i = TypeCat.ofHom fun x => ⟨(CategoryTheory.ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩
-- Lean.Environment
Lean.instInhabitedModuleData : Inhabited Lean.ModuleData
-- Mathlib.Analysis.Convex.Intrinsic
IsClosed.intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P},
  IsClosed (Subtype.val ⁻¹' s) → intrinsicClosure 𝕜 s = s
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.noConfusionType : Sort v✝ → Lean.Lsp.TextDocumentSyncKind → Lean.Lsp.TextDocumentSyncKind → Sort v✝
-- Init.Tactics
/-- `get_elem_tactic_trivial` has been deprecated in favour of `get_elem_tactic_extensible`.  -/
tacticGet_elem_tactic_trivial : Lean.ParserDescr
-- Lean.Elab.DocString
Lean.Doc.DocArg.num.sizeOf_spec : ∀ (val : Lean.NumLit), sizeOf (Lean.Doc.DocArg.num val) = 1 + sizeOf val
-- Mathlib.Data.Set.Basic
Set.sep_subset_ofPred : ∀ {α : Type u} (s : Set α) (p : α → Prop), {x | x ∈ s ∧ p x} ⊆ {x | p x}
-- Mathlib.Order.Lattice
sup_le : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c
-- Mathlib.Order.Interval.Set.ProjIcc
Set.monotone_projIci : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Monotone (Set.projIci a)
-- Batteries.Data.String.Lemmas
String.foldlAux_of_valid : ∀ {α : Type u_1} (f : α → Char → α) (l m r : List Char) (a : α),
  String.Legacy.foldlAux f (String.ofList (l ++ m ++ r)) { byteIdx := String.utf8Len l + String.utf8Len m }
      { byteIdx := String.utf8Len l } a =
    List.foldl f a m
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.ofStarRingHom_apply : ∀ {F : Type u_1} {G : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : FunLike F A B]
  [inst_5 : NonUnitalRingHomClass F A B] [inst_6 : NonUnitalStarRingHomClass F A B] [inst_7 : FunLike G B A] (f : F)
  (g : G) (h₁ : ∀ (x : A), g (f x) = x) (h₂ : ∀ (x : B), f (g x) = x) (a : A),
  (StarRingEquiv.ofStarRingHom f g h₁ h₂) a = f a
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_ordCompl_of_dvd_not_dvd : ∀ {p d n : ℕ}, d ∣ n → ¬p ∣ d → d ∣ n / p ^ n.factorization p
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorRepresentatives.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], addCommutatorRepresentatives G = Set.range fun g => (Exists.choose ⋯, ⋯.choose)
-- Init.Data.SInt.Lemmas
Int16.toInt_ofIntLE : ∀ {x : ℤ} {h₁ : Int16.minValue.toInt ≤ x} {h₂ : x ≤ Int16.maxValue.toInt}, (Int16.ofIntLE x h₁ h₂).toInt = x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.vComp_naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans F G)
  (θ : CategoryTheory.Lax.StrongTrans G H) {a b : B} (f : a ⟶ b),
  ((η.vComp θ).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (θ.app b))
            (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).hom)))
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.eq_sum_localFrameCoeff_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_14 : MemTrivializationAtlas e] {b : Module.Basis ι 𝕜 F}
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x' : M} {s : (x : M) → V x} [inst_16 : Fintype ι],
  x' ∈ e.baseSet → s x' = ∑ i, (Bundle.Trivialization.localFrameCoeff I e b i x') (s x') • e.localFrame b i x'
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_eq_abs_inv_sum : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.exradius signs = |(∑ i, s.excenterWeightsUnnorm signs i)⁻¹|
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapMon_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapMon.counitIso =
    CategoryTheory.Functor.mapMonCompIso.symm ≪≫
      CategoryTheory.Functor.mapMonNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapMonIdIso
-- Init.Grind.Interactive
/-- `internalize_all` internalizes all pending hypotheses into the grind E-graph.
Only available in `sym =>` mode.  -/
Lean.Parser.Tactic.Grind.symInternalizeAll : Lean.ParserDescr
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ofCore_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) (Y : Dᵒᵖ),
  ((CategoryTheory.Profunctor.ofCore P).obj X).obj Y = P.obj X (Opposite.unop Y)
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.containsThenInsert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {a : α},
  t.WF → (t.containsThenInsert a).2.WF
-- Mathlib.Topology.CompactOpen
/-- If `g : C(Y, Z)` is injective,
then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is injective too.  -/
ContinuousMap.postcomp_injective : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Function.Injective ⇑g → Function.Injective g.comp
-- Mathlib.Topology.Order.LowerUpperTopology
/-- `ofUpper` is the identity function from the `WithUpper` of a type.  -/
Topology.WithUpper.ofUpper : {α : Type u_1} → Topology.WithUpper α ≃ α
-- Mathlib.RepresentationTheory.Intertwining
LinearEquiv.isIntertwining_symm_isIntertwining : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W},
  (∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) → ∀ (g : G), ↑e.symm ∘ₗ σ g = ρ g ∘ₗ ↑e.symm
-- Init.Data.Array.Lemmas
Array.getElem?_replace : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a b : α} {xs : Array α} {i : ℕ},
  (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ xs.take i then some a else some b else xs[i]?
-- Mathlib.Analysis.Normed.Algebra.Exponential
Commute.exp_left : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸] {x y : 𝔸},
  Commute x y → Commute (NormedSpace.exp x) y
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₁_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.a₁ = 0
-- Lean.Elab.Match
Lean.Elab.Term.mkMatcher : Lean.Meta.Match.MkMatcherInput → Lean.Elab.TermElabM Lean.Meta.Match.MatcherResult
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- The product of a Liouville number and a nonzero rational number is again a Liouville number.  -/
LiouvilleWith.mul_rat : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p x → r ≠ 0 → LiouvilleWith p (x * ↑r)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.takeEndWhile_string_eq_takeEndWhile_toSlice : ∀ {pat : String} {s : String.Slice}, s.takeEndWhile pat = s.takeEndWhile pat.toSlice
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the reverse direction of `hasDerivWithinAt_iff_isLittleO`. -/
HasDerivWithinAt.of_isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  ((fun x' => f x' - f x - (x' - x) • f') =o[nhdsWithin x s] fun x' => x' - x) → HasDerivWithinAt f f' s x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {fallback : β k}, (t.erase k).getD k fallback = fallback
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_3 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.xor with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_3 ()
-- Mathlib.Data.Finset.Insert
Finset.coe_subset_singleton : ∀ {α : Type u_1} {s : Finset α} {a : α}, ↑s ⊆ {a} ↔ s ⊆ {a}
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Icc_iff_Iic : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  a < b → (ContinuousWithinAt f (Set.Icc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.Cells.hj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} (self : c.Cells), ¬IsMax self.j
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.not_rel_self : ∀ {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] (j : ι), ¬c.Rel j j
-- Lean.Message
/-- Trace class, e.g. `Elab.step`.  -/
Lean.TraceData.cls : Lean.TraceData → Lean.Name
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStAct.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] {k : K}
  (q : Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (f : σ → Γ k),
  Turing.TM2to1.trStAct q (Turing.TM2to1.StAct.push f) =
    Turing.TM1.Stmt.write (fun a s => (a.1, Function.update a.2 k (some (f s))))
      (Turing.TM1.Stmt.move Turing.Dir.right q)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqLambdaTheorem : BEq Mathlib.Meta.FunProp.LambdaTheorem
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzOddFEPair_f₀ : ∀ (a : UnitAddCircle), (HurwitzZeta.hurwitzOddFEPair a).f₀ = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.ker_prodMap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {G' : Type u_8} {N' : Type u_9} [inst_2 : Group G']
  [inst_3 : Group N'] (f : G →* N) (g : G' →* N'), (f.prodMap g).ker = f.ker.prod g.ker
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskering_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
  ((CategoryTheory.Limits.Cone.whiskering E).map f).hom = f.hom
-- Mathlib.Data.Nat.Cast.Defs
/-- An `AddCommMonoidWithOne` is an `AddMonoidWithOne` satisfying `a + b = b + a`.  -/
AddCommMonoidWithOne : Type u_2 → Type u_2
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.lift_cons : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C)
  {X Y Z : V} (p : Quiver.Path X Y) (f : Y ⟶ Z),
  (CategoryTheory.Paths.lift φ).map (p.cons f) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.lift φ).map p) (φ.map f)
-- Init.Data.Array.Erase
Array.exists_erase_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α},
  a ∈ xs → ∃ ys zs, a ∉ ys ∧ xs = ys.push a ++ zs ∧ xs.erase a = ys ++ zs
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_xor : ∀ (a b : BitVec 64), { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.swap M N = AddMonoid.Coprod.clift (AddMonoid.Coprod.mk.comp (FreeAddMonoid.map Sum.swap)) ⋯ ⋯ ⋯ ⋯
-- Init.Data.Int.Order
Int.toNat?.eq_2 : ∀ (a : ℕ), (Int.negSucc a).toNat? = none
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.le_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (self : CategoryTheory.Triangulated.TStructure C) (n a n' : ℤ),
  a + n' = n → ∀ (X : C), self.le n X → self.le n' ((CategoryTheory.shiftFunctor C a).obj X)
-- Aesop.Rule.Name
Aesop.BuilderName.constructors : Aesop.BuilderName
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {𝔸 : Type u_5} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ∀ (d : 𝔸), iteratedDerivWithin n (fun z => f z * d) s x = iteratedDerivWithin n f s x * d
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- The span of a subset `s` is the union over all `n` of the set of linear combinations of at most
`n` terms belonging to `s`.  -/
Submodule.span_eq_iUnion_nat : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  ↑(Submodule.span R s) = ⋃ n, (fun f => ∑ i, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.monotoneOn_rpowIntegrand₁₂ : ∀ {p t : ℝ}, p ∈ Set.Ioo 1 2 → 0 < t → MonotoneOn (p.rpowIntegrand₁₂ t) (Set.Ici 0)
-- Mathlib.Data.List.Nodup
List.Nodup.map : ∀ {α : Type u} {β : Type v} {l : List α} {f : α → β}, Function.Injective f → l.Nodup → (List.map f l).Nodup
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (self : D₁.Hom D₂) (i₁ i₂ : ι)
  {Z : ↑(F.obj { as := Opposite.op (sq i₁ i₂).pullback })}
  (h : (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (self.hom i₁))
      (CategoryTheory.CategoryStruct.comp (D₂.hom i₁ i₂) h) =
    CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
      (CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (self.hom i₂)) h)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.map_posFittingComp_le : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {M₂ : Type u_5} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : LieRingModule L M₂] [inst_11 : LieModule R L M₂] (f : M →ₗ⁅R,L⁆ M₂),
  LieSubmodule.map f (LieModule.posFittingComp R L M) ≤ LieModule.posFittingComp R L M₂