mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.ext : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  {I J : HomogeneousSubmodule 𝒜 ℳ}, I.toSubmodule = J.toSubmodule → I = J
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_comp_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (a : E), fderiv 𝕜 (fun x => f (a + x)) x = fderiv 𝕜 f (a + x)
-- Init.Data.Int.DivMod.Lemmas
Int.le_mul_of_tdiv_le : ∀ {a b c : ℤ}, 0 ≤ b → b ∣ a → a.tdiv b ≤ c → a ≤ c * b
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.dsimprocArrayCore : Bool → Lean.Meta.Simp.SimprocsArray → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.linearMapOfLE_comp : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q r : ENNReal} (hpq : p ≤ q)
  (hqr : q ≤ r), lp.linearMapOfLE 𝕜 E hqr ∘ₗ lp.linearMapOfLE 𝕜 E hpq = lp.linearMapOfLE 𝕜 E ⋯
-- Mathlib.Analysis.Convex.Gauge
gauge_le_one_iff_mem_closure : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → (gauge s x ≤ 1 ↔ x ∈ closure s)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv =
    CategoryTheory.CategoryStruct.id
      (X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.inv_logb : ∀ (a b : ℝ), (Real.logb a b)⁻¹ = Real.logb b a
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- `a - b` is the unique ordinal satisfying `b + (a - b) = a` when `b ≤ a`.  -/
Ordinal.sub : Sub Ordinal.{u_4}
-- Init.Data.Order.Lemmas
Std.instMinEqOrOfIsLinearOrderOfLawfulOrderInf : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [Std.IsLinearOrder α] [Std.LawfulOrderInf α], Std.MinEqOr α
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.mem_posFittingComp : ∀ (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 : M),
  m ∈ LieModule.posFittingComp R L M ↔ m ∈ ⨆ x, LieModule.posFittingCompOf R M x
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_not : ∀ {v i : ℕ} {x : BitVec v}, (~~~x).getMsbD i = (decide (i < v) && !x.getMsbD i)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.equivOfIsEmbeddingOfRangeEq_apply_infty : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
  [inst_3 : CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ),
  (OnePoint.equivOfIsEmbeddingOfRangeEq y f hf hy) OnePoint.infty = y
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_rootD_r : ∀ {self : Batteries.UnionFind} {a b : ℕ}, self.Equiv a (self.rootD b) ↔ self.Equiv a b
-- Mathlib.Data.Finset.Sups
Finset.sups_subset_self : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s : Finset α}, s ⊻ s ⊆ s ↔ SupClosed ↑s
-- Mathlib.GroupTheory.Divisible
divisibleByIntOfCharZero : {𝕜 : Type u_1} → [inst : DivisionRing 𝕜] → [CharZero 𝕜] → DivisibleBy 𝕜 ℤ
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_coe_angle_eq_iff_eq_toReal : ∀ {z : ℂ} {θ : Real.Angle}, ↑z.arg = θ ↔ z.arg = θ.toReal
-- Init.Data.Vector.Range
Vector.range'_inj : ∀ {s n s' : ℕ}, Vector.range' s n = Vector.range' s' n ↔ n = 0 ∨ s = s'
-- Mathlib.Analysis.Normed.Field.Basic
/-- The norm attains a value exceeding 1.  -/
NontriviallyNormedField.non_trivial : ∀ {α : Type u_5} [self : NontriviallyNormedField α], ∃ x, 1 < ‖x‖
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_anti_mono_ideal : ∀ {R : Type u} [inst : CommSemiring R] {s t : Ideal R}, s ≤ t → PrimeSpectrum.zeroLocus ↑t ⊆ PrimeSpectrum.zeroLocus ↑s
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.stdSimplex.edge.congr_simp : ∀ (n : ℕ) (a a_1 : Fin (n + 1)) (e_a : a = a_1) (b b_1 : Fin (n + 1)) (e_b : b = b_1) (hab : a ≤ b),
  SSet.stdSimplex.edge n a b hab = SSet.stdSimplex.edge n a_1 b_1 ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `homothety c r` is the homothety (also known as dilation) about `c` with scale factor `r`.  -/
AffineMap.homothety : {k : Type u_2} →
  {V1 : Type u_3} →
    {P1 : Type u_4} →
      [inst : CommRing k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : AddTorsor V1 P1] → [inst_3 : Module k V1] → P1 → k → P1 →ᵃ[k] P1
-- Mathlib.Analysis.Analytic.Order
natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {n : ℕ} {z₀ : 𝕜} [CharZero 𝕜] [CompleteSpace E],
  AnalyticAt 𝕜 f z₀ → (↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuous_iff_from_nat : ∀ {Y : Type u_3} [inst : TopologicalSpace Y] (f : OnePoint ℕ → Y),
  Continuous f ↔ Filter.Tendsto (fun x => f ↑x) Filter.atTop (nhds (f OnePoint.infty))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.mk.inj : ∀ {X : Type u} {point : X} {X_1 : Type u} {point_1 : X_1},
  { X := X, point := point } = { X := X_1, point := point_1 } → X = X_1 ∧ point ≍ point_1
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- The canonical embedding (as a monoid hom) from a linearly ordered cancellative additive monoid
into `ℤ`. This is either surjective or zero.  -/
LocallyFiniteOrder.addMonoidHom : (G : Type u_2) →
  [inst : AddCommGroup G] → [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → [LocallyFiniteOrder G] → G →+ ℤ
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.sectionsMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat),
  MonCat.sectionsMonoid F = (MonCat.sectionsSubmonoid F).toMonoid
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_add_of_degree_lt_left : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R}, q.degree < p.degree → (p + q).eraseLead = p.eraseLead + q
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_eq_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ],
  μ.compProd κ = 0 ↔ ∀ᵐ (a : α) ∂μ, κ a = 0
-- Init.Data.Option.Lemmas
Option.any_eq_true : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.any p x = true ↔ ∃ y, x = some y ∧ p y = true
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instFunLike : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] → [inst_7 : Module 𝕜₂ F] → FunLike (E →SWOT[σ] F) E F
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The codomain of a morphism.  -/
Mathlib.Tactic.Monoidal.tgtExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getParamsPos : Lean.Name → Array Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM (List (Option ℕ))
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.hasSumLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasSumUniformly f g → HasSumLocallyUniformly f g
-- Init.Data.SInt.Lemmas
ISize.mul_zero : ∀ {a : ISize}, a * 0 = 0
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_restrict_apply' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → (μ.restrict s).real t = μ.real (t ∩ s)
-- Batteries.Data.String.Matcher
/-- Make KMP matcher from pattern substring  -/
String.Matcher.ofSubstring : Substring.Raw → String.Matcher
-- Mathlib.Data.Finsupp.Basic
Finsupp.extendDomain_subtypeDomain : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : α →₀ M),
  (∀ a ∈ f.support, P a) → (Finsupp.subtypeDomain P f).extendDomain = f
-- Mathlib.Probability.Kernel.Posterior
/-- The posterior is contravariant.  -/
ProbabilityTheory.posterior_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {κ : ProbabilityTheory.Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ] [inst_2 : StandardBorelSpace Ω]
  [inst_3 : Nonempty Ω] [inst_4 : StandardBorelSpace 𝓧] [inst_5 : Nonempty 𝓧] {η : ProbabilityTheory.Kernel 𝓧 𝓨}
  [inst_6 : ProbabilityTheory.IsFiniteKernel η],
  ⇑(ProbabilityTheory.posterior (η.comp κ) μ) =ᵐ[(μ.bind ⇑κ).bind ⇑η]
    ⇑((ProbabilityTheory.posterior κ μ).comp (ProbabilityTheory.posterior η (μ.bind ⇑κ)))
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instInhabitedRefreshState.default : ProofWidgets.RefreshComponent.RefreshState
-- Mathlib.MeasureTheory.Measure.Tight
/-- Inner regular finite measures on T2 spaces are tight.  -/
MeasureTheory.isTightMeasureSet_singleton_of_innerRegular : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} [inst : TopologicalSpace 𝓧] [T2Space 𝓧]
  [OpensMeasurableSpace 𝓧] [MeasureTheory.IsFiniteMeasure μ] [h : μ.InnerRegular], MeasureTheory.IsTightMeasureSet {μ}
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If an additive fundamental domain has volume 0, then
`AddQuotientMeasureEqMeasurePreimage` holds.  -/
MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s ν → ν s = 0 → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν 0
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.finset_iUnion_left_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Finset ι} {s : ι → Set X} {t : Set X},
  Metric.AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, Metric.AreSeparated (s i) t
-- Mathlib.Computability.RecursiveIn
ComputableIn.unpair : ∀ {O : Set (ℕ →. ℕ)}, ComputableIn O Nat.unpair
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  (CochainComplex.mappingConeCompTriangle f g).obj₁ = CochainComplex.mappingCone f
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_const_add_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (b : G)
  {c : G} {f : α → G} {l : Filter α}, Filter.Tendsto (fun x => b + f x) l (nhds (b + c)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_erase_of_mem : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (s : Multiset α) {x : α},
  x ∈ s → Multiset.map f (s.erase x) = (Multiset.map f s).erase (f x)
-- Mathlib.SetTheory.Cardinal.Regular
/-- Lean's foundations prove the existence of `v` inaccessibles in universe `v`.  -/
Cardinal.IsInaccessible.univ : Cardinal.univ.{u, v}.IsInaccessible
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Subalgebra.le_centralizer_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S T : Subalgebra R A), S ≤ Subalgebra.centralizer R ↑T ↔ T ≤ Subalgebra.centralizer R ↑S
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryLT? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H2π.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.H2π A =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).inv (groupCohomology.π A 2)
-- Mathlib.Tactic.Linter.EmptyLine
/-- Retrieve the `String.Range` of a `Substring`.  -/
Lean.Substring.Raw.getRange : Substring.Raw → Lean.Syntax.Range
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.contains a = true → t.getKey? a = some (t.getKey! a)
-- Mathlib.Algebra.Group.Equiv.TypeTags
OneHom.mk.congr_simp : ∀ {M : Type u_10} {N : Type u_11} [inst : One M] [inst_1 : One N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_one' : toFun 1 = 1), { toFun := toFun, map_one' := map_one' } = { toFun := toFun_1, map_one' := ⋯ }
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.starConvex : ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, Balanced ℝ s → StarConvex ℝ 0 s
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.eq = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.eq = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.eq with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_2 ⋯
-- Init.Data.SInt.Lemmas
Int64.ofInt_tmod : ∀ {a b : ℤ},
  Int64.minValue.toInt ≤ a →
    a ≤ Int64.maxValue.toInt →
      Int64.minValue.toInt ≤ b → b ≤ Int64.maxValue.toInt → Int64.ofInt (a.tmod b) = Int64.ofInt a % Int64.ofInt b
-- Mathlib.Data.Sym.Sym2
Sym2.diagElemEquiv_symm_apply_coe : ∀ {α : Type u_1} (a : α), ↑(Sym2.diagElemEquiv.symm a) = Sym2.diag a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.leftIso.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y),
  CategoryTheory.Comma.leftIso α = (CategoryTheory.Comma.fst L₁ R₁).mapIso α
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.empty.sizeOf_spec : sizeOf Aesop.Script.StepTree.empty = 1
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad : {m : Type → Type u_1} →
  {n : Type u_2 → Type u_3} → {s : String.Slice} → [inst : Monad m] → [Monad n] → Std.IteratorLoop s.RevPosIterator m n
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.rpcNeedsReconnect.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.rpcNeedsReconnect = 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isClub_iff : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsClub s ↔ DirSupClosed s ∧ IsCofinal s
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  InformationTheory.klDiv μ μ = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k fallback : α}, m₂.contains k = false → (m₁.diff m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fintypeEdgeSetSdiff : {V : Type u} →
  (G₁ G₂ : SimpleGraph V) → [DecidableEq V] → [Fintype ↑G₁.edgeSet] → [Fintype ↑G₂.edgeSet] → Fintype ↑(G₁ \ G₂).edgeSet
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.isClosed_iff_image_isClosed : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → ∀ {s : Set X}, IsClosed s ↔ IsClosed (f '' s)
-- Mathlib.Topology.MetricSpace.Defs
zero_eq_nndist : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, 0 = nndist x y ↔ x = y
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.isStrictMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F}, u.IsFredholm → Topology.IsStrictMap ⇑u
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.hom_ext₀_iff : ∀ {X : SSet} {f g : (SSet.boundary 0).toSSet ⟶ X}, f = g ↔ True
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.domRestrict_toFun : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N)
  (p : L.Substructure M) (a : ↥p), (f.domRestrict p) a = f ↑a
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.pullback_equalizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (h : W ⟶ X) [inst_2 : CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.Subobject.pullback h).obj (CategoryTheory.Limits.equalizerSubobject f g) =
    CategoryTheory.Limits.equalizerSubobject (CategoryTheory.CategoryStruct.comp h f)
      (CategoryTheory.CategoryStruct.comp h g)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateSset! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu →
    Lean.FVarId → ℕ → ℕ → Lean.FVarId → Lean.Expr → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift_id_comp_of : ∀ {G : Type u₁} [inst : CategoryTheory.Groupoid G],
  (CategoryTheory.FreeGroupoid.lift (CategoryTheory.Functor.id G)).comp (CategoryTheory.FreeGroupoid.of G) =
    CategoryTheory.Functor.id (CategoryTheory.FreeGroupoid G)
-- Init.SizeOf
Fin.mk.sizeOf_spec : ∀ {n : ℕ} (val : ℕ) (isLt : val < n), sizeOf ⟨val, isLt⟩ = 1 + sizeOf val + sizeOf isLt
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `StrongDual.extendRCLike_apply`. -/
ContinuousLinearMap.extendTo𝕜_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (fr : StrongDual ℝ F) (x : F), fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.forIn_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {b : δ} {f : α → δ → m (ForInStep δ)},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → forIn t₁ b f = forIn t₂ b f
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.Equiv_isup_of_apply : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : ↥(S i)),
  (FirstOrder.Language.DirectLimit.Equiv_iSup S)
      ((FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x))
          (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i)
        x) =
    (FirstOrder.Language.Substructure.inclusion ⋯) x
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_zero_length : ∀ {i : ℕ} (x : BitVec 0), x.getLsbD i = false
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
continuousAt_continuousAlternatingMap_bundle : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {X : Type u_8}
  [inst_21 : TopologicalSpace X] {x₀ : X} (f : X → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x),
  ContinuousAt f x₀ ↔
    ContinuousAt (fun x => (f x).proj) x₀ ∧
      ContinuousAt
        (fun x => ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        x₀
-- Batteries.Data.AssocList
Batteries.AssocList.toList.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (a : α) (b : β) (es : Batteries.AssocList α β),
  (Batteries.AssocList.cons a b es).toList = (a, b) :: es.toList
-- Mathlib.Algebra.QuaternionBasis
Quaternion.hom_ext_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  {f g : Quaternion R →ₐ[R] A},
  f = g ↔
    f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i ∧
      f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j
-- Mathlib.GroupTheory.Exponent
Nat.Prime.exists_orderOf_eq_pow_factorization_exponent : ∀ (G : Type u) [inst : Monoid G] {p : ℕ}, Nat.Prime p → ∃ g, orderOf g = p ^ (Monoid.exponent G).factorization p