mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.sum.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (s : Finset β) (f : β → FirstOrder.Language.presburger.Term α),
  FirstOrder.Language.presburger.sum s f = (List.map f s.toList).sum
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_center_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {z : R}, z ∈ NonUnitalSubsemiring.center R ↔ ∀ (g : R), g * z = z * g
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.discreteTopology_iff : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G},
  DiscreteTopology (G ⧸ N) ↔ IsOpen ↑N
-- Mathlib.Algebra.Homology.HomologySequence
/-- Exactness of `S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j`.  -/
CategoryTheory.ShortComplex.ShortExact.homology_exact₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
      g := hS.δ i j hij, zero := ⋯ }.Exact
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.borel_eq_generateFrom_Iic_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Iic ↑a})
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Edge.mk.sizeOf_spec : ∀ (src dst : ℕ) (proof : Lean.Expr),
  sizeOf { src := src, dst := dst, proof := proof } = 1 + sizeOf src + sizeOf dst + sizeOf proof
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_eq_zero_iff_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.ndinter t = 0 ↔ Disjoint s t
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.card_pairSetSeq_le_logSizeRadius_mul : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  1 < a →
    ↑(PairReduction.pairSetSeq J a c i).card ≤
      (if (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
        a ^ (PairReduction.logSizeBallSeq J hJ a c i).radius
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving_id_apply : ∀ {E : Type u_4} {p : ENNReal} [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β]
  {μb : MeasureTheory.Measure β} (g : ↥(MeasureTheory.Lp E p μb)), (MeasureTheory.Lp.compMeasurePreserving id ⋯) g = g
-- Mathlib.Data.NNReal.Defs
NNReal.instIsStrictOrderedModule : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [inst_2 : Module ℝ M] [IsStrictOrderedModule ℝ M],
  IsStrictOrderedModule NNReal M
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.curriedBraidingNatIso_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X X_1 : C),
  ((CategoryTheory.BraidedCategory.curriedBraidingNatIso C).inv.app X).app X_1 = (β_ X X_1).inv
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- We define an auxiliary sequence

$$ a_{k, n} = x^{(k+1)n} \prod_{i=0}^{n} (1 - x^{k + i + 1}) $$

We will also use its sum

$$ A_k = \sum_{n=0}^{\infty} a_{k, n} $$  -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.powMulProdOneSubPow : {R : Type u_1} → [CommRing R] → ℕ → ℕ → R → R
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonpos_of_ae_restrict : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  f ≤ᵐ[μ.restrict s] 0 → ∫ (x : X) in s, f x ∂μ ≤ 0
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_neg_index : ∀ {α : Type u_1} {M : Type u_8} {G : Type u_12} [inst : SubtractionMonoid G] [inst_1 : CommMonoid M] {g : α →₀ G}
  {h : α → G → M}, (∀ (a : α), h a 0 = 1) → (-g).prod h = g.prod fun a b => h a (-b)
-- Init.Prelude
/-- A `UInt32` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a
surrogate code point (the range `0xd800` to `0xdfff` inclusive).
 -/
UInt32.isValidChar : UInt32 → Prop
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example (a b c d : α) : transpose !![a, b; c, d] = !![a, c; b, d] := (transposeᵣ_eq _).symm
```
 -/
Matrix.transposeᵣ_eq : ∀ {α : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) α), A.transposeᵣ = A.transpose
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_Iio : ∀ {n m : ℕ} (a : Fin n) (h : n ≤ m), Finset.image (Fin.castLE h) (Finset.Iio a) = Finset.Iio (Fin.castLE h a)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.responseError.injEq : ∀ (id : Lean.JsonRpc.RequestID) (code : Lean.JsonRpc.ErrorCode) (message : String) (data? : Option Lean.Json)
  (id_1 : Lean.JsonRpc.RequestID) (code_1 : Lean.JsonRpc.ErrorCode) (message_1 : String) (data?_1 : Option Lean.Json),
  (Lean.JsonRpc.Message.responseError id code message data? =
      Lean.JsonRpc.Message.responseError id_1 code_1 message_1 data?_1) =
    (id = id_1 ∧ code = code_1 ∧ message = message_1 ∧ data? = data?_1)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.ofHom_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Algebra R X] [inst_3 : Ring Y]
  [inst_4 : Algebra R Y] (f : X →ₐ[R] Y) (x : X), (CategoryTheory.ConcreteCategory.hom (AlgCat.ofHom f)) x = f x
-- Init.Data.SInt.Bitwise
instAssociativeInt64HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_ofList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.TreeSet.Raw.ofList l cmp).size ≤ l.length
-- Mathlib.Data.Setoid.Basic
Setoid.comap_map_of_ker_le : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid α), Setoid.ker f ≤ r → Setoid.comap f (r.map f) = r
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- Let `F` be a `Type`-valued functor. If two elements `a : F c` and `b : F d` represent the
same element of `colimit F`, then `c` and `d` are related by a `Zigzag`.  -/
CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  (c d : (j : C) × F.obj j), Relation.EqvGen F.ColimitTypeRel c d → CategoryTheory.Zigzag c.fst d.fst
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_mul_le_max : ∀ {x y : NNReal}, NNReal.sqrt (x * y) ≤ max x y
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedFinTM2 : Inhabited Turing.FinTM2
-- Init.Data.Fin.Lemmas
Fin.le_last : ∀ {n : ℕ} (i : Fin (n + 1)), i ≤ Fin.last n
-- Init.Data.Array.Lemmas
Array.flatMap_replicate : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {a : α} {f : α → Array β},
  Array.flatMap f (Array.replicate n a) = (Array.replicate n (f a)).flatten
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearEquiv_injective : ∀ {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}, Function.Injective Representation.Equiv.toLinearEquiv
-- Mathlib.Analysis.CStarAlgebra.Basic
RingHomIsometric.starRingEnd : ∀ {E : Type u_2} [inst : NormedCommRing E] [inst_1 : StarRing E] [NormedStarGroup E], RingHomIsometric (starRingEnd E)
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.univ : ∀ {α : Type u} {g : Set (Set α)}, TopologicalSpace.GenerateOpen g Set.univ
-- Init.Data.String.Termination
String.Pos.lt_iff_remainingBytes_lt : ∀ {s : String} (p q : s.Pos), p < q ↔ q.remainingBytes < p.remainingBytes
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.fst_prod : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : NonUnitalNonAssocSemiring C]
  [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C),
  (NonUnitalAlgHom.fst R B C).comp (f.prod g) = f
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- The norm of a coefficient `x_i` is less than or equal to the norm of `x`.  -/
Module.Basis.norm_repr_le_norm : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] (B : Module.Basis ι K L) {x : L} (i : ι), ‖(B.repr x) i‖ ≤ B.norm x
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.numIndices : Lean.Meta.RecursorInfo → ℕ
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.Cert.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {subject : Q(«$α»)}
  (result : Mathlib.Tactic.Determinant.CertResult rα subject) (isZero : Bool),
  sizeOf { subject := subject, result := result, isZero := isZero } = 1 + sizeOf subject + sizeOf result + sizeOf isZero
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.count_eq_match_step : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.length = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.length
        pure { down := __do_lift.down + 1 }
      | Std.IterStep.skip it' => do
        let __do_lift ← it'.length
        pure { down := __do_lift.down }
      | Std.IterStep.done => pure { down := 0 }
-- Mathlib.Data.W.Constructions
/-- The constructors for lists.
There is "one constructor `cons x` for each `x : γ`",
since we view `List γ` as
```
| nil : List γ
| cons x₀ : List γ → List γ
| cons x₁ : List γ → List γ
|   ⋮      γ many times
```
 -/
WType.Listα : Type u → Type u
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.mulLeft_mul : ∀ {X : Type u_6} [inst : Semigroup X] [inst_1 : TopologicalSpace X] [inst_2 : SeparatelyContinuousMul X] (x y : X),
  ContinuousMap.mulLeft (x * y) = (ContinuousMap.mulLeft x).comp (ContinuousMap.mulLeft y)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.zero_le : ∀ {α : Type u_1} [inst : LE α] (a : WithZero α), 0 ≤ a
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.mem_equalizer : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (φ ψ : F) (x : A),
  x ∈ NonUnitalStarAlgHom.equalizer φ ψ ↔ φ x = ψ x
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.modifyMap : Std.DHashMap Lean.Name fun x => Lean.Name
-- Mathlib.Algebra.Divisibility.Basic
/-- There are two possible conventions for divisibility, which coincide in a `CommMonoid`.
This matches the convention for ordinals.  -/
semigroupDvd : {α : Type u_1} → [Semigroup α] → Dvd α
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If `F ⋙ G` is fully faithful and `G` is faithful, then `F` is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.ofCompFaithful : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D E} → [G.Faithful] → (F.comp G).FullyFaithful → F.FullyFaithful
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.nontrivial_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], Nontrivial (TopologicalSpace.NonemptyCompacts α) ↔ Nontrivial α
-- Mathlib.Data.Set.Function
Function.RightInverse.rightInvOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.RightInverse f g → ∀ (s : Set α), Set.RightInvOn f g s
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.HashMap α Unit},
  (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → m₁.Equiv m₂
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.IsClosedUnderExtensions.prop_X₂_of_shortExact : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} [self : P.IsClosedUnderExtensions]
  {S : CategoryTheory.ShortComplex C}, S.ShortExact → P S.X₁ → P S.X₃ → P S.X₂
-- Mathlib.Algebra.Order.Kleene
kstar_le_of_mul_le_left : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, 1 ≤ b → b * a ≤ b → KStar.kstar a ≤ b
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normRule.injEq : ∀ (r r_1 : Aesop.NormRule), (Aesop.BaseRuleSetMember.normRule r = Aesop.BaseRuleSetMember.normRule r_1) = (r = r_1)
-- Init.Data.Vector.Find
Vector.findSome?_empty : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1}, Vector.findSome? f #v[] = none
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- **Alias** of the reverse direction of `ContinuousLinearMap.IsStarProjection.ext_iff`.

---

Star projection operators are equal iff their range are.  -/
ContinuousLinearMap.IsStarProjection.ext : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E] {S : E →L[𝕜] E},
  IsStarProjection S → IsStarProjection T → (↑S).range = (↑T).range → S = T
-- Mathlib.Order.Hom.PowersetCard
Set.powersetCard.mem_ofFinEmbEquiv_iff_mem_range : ∀ {n : ℕ} {I : Type u_1} [inst : LinearOrder I] (f : Fin n ↪o I) (i : I),
  i ∈ Set.powersetCard.ofFinEmbEquiv f ↔ i ∈ Set.range ⇑f
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_rfl : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), X.homOfLE ⋯ = CategoryTheory.CategoryStruct.id ↑U
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getEntry?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List ((a : α) × β a) → Sort u_3) →
      (x : List ((a : α) × β a)) →
        (Unit → motive []) → ((k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)) → motive x
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_eq_not_all_not : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {p : α → β → Bool},
  m.any p = !m.all fun a b => !p a b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ Std.DTreeMap.ofList l cmp}, (Std.DTreeMap.ofList l cmp).get k' h = cast ⋯ v
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
/-- A functor `F : C ⥤ D` is dense if any `Y : D` is a canonical colimit
relatively to `F`.  -/
CategoryTheory.Functor.IsDense : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L-function of an even Dirichlet character vanishes at strictly negative even integers.  -/
DirichletCharacter.Even.LFunction_neg_two_mul_nat_add_one : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N},
  χ.Even → ∀ (n : ℕ), DirichletCharacter.LFunction χ (-(2 * (↑n + 1))) = 0
-- Mathlib.Algebra.Order.Sub.Defs
le_tsub_of_add_le_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a + b ≤ c → b ≤ c - a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k k' : α} {f : β → β} {hc : k' ∈ t.modify k f},
  (t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_5 : ∀ (motive : Lean.Expr → Sort u_1) (a : Lean.Level)
  (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.sort a.succ with
    | Lean.Expr.const name us => h_1 name us
    | f.app x => h_2 f x
    | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
    | Lean.Expr.sort Lean.Level.zero => h_4 ()
    | Lean.Expr.sort a.succ => h_5 a
    | Lean.Expr.sort u => h_6 u
    | x => h_7 x) =
    h_5 a
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
isLinearSet_iff_exists_fg_eq_vadd : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsLinearSet s ↔ ∃ a P, P.FG ∧ s = a +ᵥ ↑P
-- Mathlib.MeasureTheory.Group.Measure
/-- We shorten this from `measure_preimage_add_left`, since left invariant is the preferred option
for measures in this formalization.  -/
MeasureTheory.measure_preimage_add : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddLeftInvariant] (g : G) (A : Set G), μ ((fun h => g + h) ⁻¹' A) = μ A
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.countable_meas_level_set_pos₀ : ∀ {α : Type u_4} {β : Type u_5} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  [inst : MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β},
  MeasureTheory.NullMeasurable g μ → {t | 0 < μ {a | g a = t}}.Countable
-- Init.Grind.Lemmas
Lean.Grind.Bool.or_eq_of_eq_false_left : ∀ {a b : Bool}, a = false → (a || b) = b
-- Mathlib.Analysis.CStarAlgebra.Basic
Prod.cstarRing : ∀ {R₁ : Type u_5} {R₂ : Type u_6} [inst : NonUnitalNormedRing R₁] [inst_1 : StarRing R₁] [CStarRing R₁]
  [inst_3 : NonUnitalNormedRing R₂] [inst_4 : StarRing R₂] [CStarRing R₂], CStarRing (R₁ × R₂)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜]
  {E : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_6}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E},
  MeasureTheory.AEStronglyMeasurable φ μ → ∀ (v : F), MeasureTheory.AEStronglyMeasurable (fun a => (φ a) v) μ
-- Mathlib.Order.Interval.Finset.Defs
IsEmpty.toLocallyFiniteOrderBot.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : IsEmpty α],
  IsEmpty.toLocallyFiniteOrderBot =
    { finsetIio := fun a => isEmptyElim a, finsetIic := fun a => isEmptyElim a, finset_mem_Iic := ⋯,
      finset_mem_Iio := ⋯ }
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K], (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p - 1
-- Mathlib.Data.TypeVec
TypeVec.lastFun_prod : ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α.Arrow β) (f' : α'.Arrow β'),
  TypeVec.lastFun (TypeVec.prod.map f f') = Prod.map (TypeVec.lastFun f) (TypeVec.lastFun f')
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.mk.injEq : ∀ (label : String) (detail? : Option String) (documentation? : Option Lean.Lsp.MarkupContent)
  (kind? : Option Lean.Lsp.CompletionItemKind) (textEdit? : Option Lean.Lsp.InsertReplaceEdit)
  (sortText? : Option String) (data? : Option Lean.Lsp.ResolvableCompletionItemData)
  (tags? : Option (Array Lean.Lsp.CompletionItemTag)) (label_1 : String) (detail?_1 : Option String)
  (documentation?_1 : Option Lean.Lsp.MarkupContent) (kind?_1 : Option Lean.Lsp.CompletionItemKind)
  (textEdit?_1 : Option Lean.Lsp.InsertReplaceEdit) (sortText?_1 : Option String)
  (data?_1 : Option Lean.Lsp.ResolvableCompletionItemData) (tags?_1 : Option (Array Lean.Lsp.CompletionItemTag)),
  ({ label := label, detail? := detail?, documentation? := documentation?, kind? := kind?, textEdit? := textEdit?,
        sortText? := sortText?, data? := data?, tags? := tags? } =
      { label := label_1, detail? := detail?_1, documentation? := documentation?_1, kind? := kind?_1,
        textEdit? := textEdit?_1, sortText? := sortText?_1, data? := data?_1, tags? := tags?_1 }) =
    (label = label_1 ∧
      detail? = detail?_1 ∧
        documentation? = documentation?_1 ∧
          kind? = kind?_1 ∧ textEdit? = textEdit?_1 ∧ sortText? = sortText?_1 ∧ data? = data?_1 ∧ tags? = tags?_1)
-- Mathlib.LinearAlgebra.Matrix.Block
/-- A lower-left subblock of the inverse of a block-triangular matrix is zero. This is a first step
towards `BlockTriangular.inv_toBlock` below.  -/
Matrix.toBlock_inverse_eq_zero : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : CommRing R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : LinearOrder α] [Invertible M],
  M.BlockTriangular b → ∀ (k : α), (M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
MeasureTheory.IsHahnDecomposition.compl : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsHahnDecomposition μ ν s → MeasureTheory.IsHahnDecomposition ν μ sᶜ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_eq_zero_iff : ∀ {θ : Real.Angle}, θ.cos = 0 ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_rco : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : LT α] [inst_4 : DecidableLT α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Rco α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Lean.Meta.Tactic.Grind.Types
/-- All constants (*not* in `appMap`) that have been internalized, *and*
`appMap`'s domain. We use this collection during theorem activation.
 -/
Lean.Meta.Grind.GoalState.indicesFound : Lean.Meta.Grind.GoalState → Lean.PHashSet Lean.HeadIndex