mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π`. -/
CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (h.iso m).inv.hom) (h.π m) =
    CategoryTheory.Subobject.pullbackπ (h.χ m) h.Ω₀
-- Init.Data.SInt.Bitwise
Int16.not_inj : ∀ {a b : Int16}, ~~~a = ~~~b ↔ a = b
-- Init.Internal.Order.Basic
Lean.Order.flat_csup : {α : Sort u} → {b : α} → (Lean.Order.FlatOrder b → Prop) → Lean.Order.FlatOrder b
-- Init.Data.Nat.Coprime
Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul : ∀ {c d a b : ℕ}, c.Coprime d → a * b = c * d → a.gcd c * b.gcd c = c
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.mapsTo_eball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → K ≠ 0 → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) (↑K * r))
-- Mathlib.Algebra.Polynomial.Laurent
/-- This is not a simp lemma, as it is usually preferable to use the lemmas about `C` and `X`
instead.  -/
Polynomial.toLaurent_apply : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R),
  Polynomial.toLaurent p = AddMonoidAlgebra.mapDomain Nat.cast p.toFinsupp
-- Init.Grind.Norm
Lean.Grind.exists_or : ∀ {α : Sort u} {p q : α → Prop}, (∃ x, p x ∨ q x) = ((∃ x, p x) ∨ ∃ x, q x)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The type of a matrix entry  -/
Mathlib.Tactic.Determinant.ReifiedBirdDet.α : (self : Mathlib.Tactic.Determinant.ReifiedBirdDet) → Q(Type udummy._pp_uniq.3)
-- Mathlib.Data.Set.Insert
Set.ofPred_mem_list_eq_replicate : ∀ {α : Type u_1} {l : List α} {a : α}, {x | x ∈ l} = {a} ↔ ∃ n > 0, l = List.replicate n a
-- Mathlib.NumberTheory.ModularForms.Cusps
isCusp_iff_of_relIndex_ne_zero : ∀ {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)}, 𝒢' ≤ 𝒢 → 𝒢'.relIndex 𝒢 ≠ 0 → ∀ (c : OnePoint ℝ), IsCusp c 𝒢' ↔ IsCusp c 𝒢
-- Mathlib.Algebra.Group.Pi.Basic
Pi.subNegMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → SubNegMonoid (f i)] → SubNegMonoid ((i : I) → f i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((k, v) ∈ List.map (fun x => (x.fst, x.snd)) l ↔
      Std.Internal.List.getKey? k l = some k ∧ Std.Internal.List.getValue? k l = some v)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constGet?_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.Equiv m₂ → Std.DHashMap.Const.get? m₁ k = Std.DHashMap.Const.get? m₂ k
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_shiftLeft : ∀ (a : BitVec 16), ∀ b < 16, { toBitVec := a <<< b } = { toBitVec := a } <<< UInt16.ofNat b
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [IsDomain R₁] (x : R₁) {I : FractionalIdeal (nonZeroDivisors R₁) K},
  IsNoetherian R₁ ↥↑I →
    IsNoetherian R₁ ↥↑(FractionalIdeal.spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) x)⁻¹ * I)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.pairwiseDisjoint_smul_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] [IsLeftCancelSMul α β] [inst_2 : DecidableEq β] {s : Set α}
  {t : Finset β}, (s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 • p.2) (s ×ˢ ↑t)
-- Mathlib.Topology.Order.IsLUB
IsGLB.mem_upperBounds_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  AntitoneOn f s → IsGLB s a → Filter.Tendsto f (nhdsWithin a s) (nhds b) → b ∈ upperBounds (f '' s)
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- **Alias** of `MeasureTheory.measure_sdiff_null`. -/
MeasureTheory.measure_diff_null : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, μ t = 0 → μ (s \ t) = μ s
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mk : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (toSubmodule : Submodule R L) →
            (∀ {x y : L}, x ∈ toSubmodule.carrier → y ∈ toSubmodule.carrier → ⁅x, y⁆ ∈ toSubmodule.carrier) →
              LieSubalgebra R L
-- Mathlib.Topology.Algebra.MulAction
ContinuousOn.vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {s : Set Y},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (f +ᵥ g) s
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F` is initial, and `t : Cone (F ⋙ G)`,
`extendCone.obj t` is a limit cone exactly when `t` is.
 -/
CategoryTheory.Functor.Initial.isLimitExtendConeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  (t : CategoryTheory.Limits.Cone (F.comp G)) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.Initial.extendCone.obj t) ≃
                      CategoryTheory.Limits.IsLimit t
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_le_bot_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), f.range ≤ ⊥ ↔ f = 0
-- Mathlib.Order.Height
Set.chainHeight_coe_univ_lt : ∀ {α : Type u_1} (s : Set α) [inst : LT α],
  (Set.univ.chainHeight fun x1 x2 => x1 < x2) = s.chainHeight fun x1 x2 => x1 < x2
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
ContinuousLinearMap.opNorm_bound_of_ball_bound : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 < r → ∀ (c : ℝ) (f : StrongDual 𝕜 E), (∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c) → ‖f‖ ≤ c / r
-- Mathlib.Data.Num.Lemmas
Num.castNum_ldiff : ∀ (m n : Num), ↑(m.ldiff n) = (↑m).ldiff ↑n
-- Mathlib.Algebra.Order.Group.MinMax
abs_max_sub_max_le_max : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c d : α),
  |max a b - max c d| ≤ max |a - c| |b - d|
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.α_inv.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z) = 1 + sizeOf X + sizeOf Y + sizeOf Z
-- Mathlib.Order.InitialSeg
InitialSeg.toPrincipalSeg_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : InitialSeg r s)
  (hf : ¬Function.Surjective ⇑f) (x : α), (f.toPrincipalSeg hf).toRelEmbedding x = f x
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofNat' : ∀ {n : ℕ}, (Int16.ofNat n).toInt8 = Int8.ofNat n
-- Mathlib.Data.Set.Basic
/-- See also `Set.not_nonempty_iff_eq_empty`.  -/
Set.nonempty_iff_ne_empty : ∀ {α : Type u} {s : Set α}, s.Nonempty ↔ s ≠ ∅
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.iInf_mono : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {α : Type u_1} {Φ Ψ : α → l},
  (∀ (a : α), Lean.Order.PartialOrder.rel (Φ a) (Ψ a)) →
    Lean.Order.PartialOrder.rel (Lean.Order.iInf Φ) (Lean.Order.iInf Ψ)
-- Lean.CoreM
Lean.Core.CoreM.run : {α : Type} → Lean.CoreM α → Lean.Core.Context → Lean.Core.State → EIO Lean.Exception (α × Lean.Core.State)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Another map from the codomain of `f` to `Z`  -/
CategoryTheory.RegularMono.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.RegularMono f) → Y ⟶ self.Z
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with subtracting a constant.  -/
iteratedFDeriv_comp_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ) (a x : E), iteratedFDeriv 𝕜 n (fun z => f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
            {Y : C} →
              {g₁ : Y ⟶ X₁} →
                {g₂ : Y ⟶ X₂} →
                  {b : Y ⟶ S} →
                    (f : Y ⟶ h.pullback) →
                      autoParam (CategoryTheory.CategoryStruct.comp f h.p₁ = g₁)
                          CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam →
                        autoParam (CategoryTheory.CategoryStruct.comp f h.p₂ = g₂)
                            CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam →
                          autoParam (CategoryTheory.CategoryStruct.comp f h.p = b)
                              CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam →
                            h.LiftStruct g₁ g₂ b
-- Lean.DefEqAttrib
/-- There are defeq theorems that only hold at transparency `.all`, but also others that hold
(from the kernel's point of view) but where the defeq checker here will run out of cycles.

So we try the more careful first.
 -/
_private.Lean.DefEqAttrib.0.Lean.isDefEqCareful : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.ofSemiring : {α : Type u} → [inst : Lean.Grind.Semiring α] → Lean.Grind.Ring (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (f f_1 : V₀.V ⟶ V₁.V) (e_f : f = f_1)
  (h : CategoryTheory.CategoryStruct.comp V₀.str (F.map f) = CategoryTheory.CategoryStruct.comp f V₁.str),
  { f := f, h := h } = { f := f_1, h := ⋯ }
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.eq_zero_or_one_of_pow_of_not_isUnit : ∀ {R : Type u_1} [inst : Monoid R] {x : R} {n : ℕ}, Squarefree (x ^ n) → ¬IsUnit x → n = 0 ∨ n = 1
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_finite_toFinset_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Set α} (hs : s.Finite),
  ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ hs.toFinset, f i
-- Mathlib.Order.Filter.Basic
Filter.Eventually.of_forall : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∀ (x : α), p x) → ∀ᶠ (x : α) in f, p x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F F_1 : CategoryTheory.Functor J C) (e_F : F = F_1) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.limit F = CategoryTheory.Limits.limit F_1
-- Mathlib.Data.Set.Finite.Lemmas
Set.exists_upper_bound_image : ∀ {α : Type u} {β : Type v} [Nonempty α] [inst : LinearOrder β] (s : Set α) (f : α → β),
  s.Finite → ∃ a, ∀ b ∈ s, f b ≤ f a
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instLattice : {E : Type u_3} → [inst : CommGroup E] → Lattice (GroupSeminorm E)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndepOn R v s ↔
    ∀ f ∈ Finsupp.supported R R s,
      ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.isCoboundedUnder_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι}
  {u : ι → α} {a : α} [f.NeBot], Filter.Tendsto u f (nhds a) → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Mathlib.Data.Sign.Defs
sign_eq_neg_one_iff : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] {a : α}, SignType.sign a = -1 ↔ a < 0
-- Mathlib.Algebra.Group.End
Equiv.Perm.val_inv_equivUnitsEnd_apply : ∀ {α : Type u_4} (e : Equiv.Perm α) (a : α), ↑(Equiv.Perm.equivUnitsEnd e)⁻¹ a = (Equiv.symm e) a
-- Init.Data.List.Nat.TakeDrop
List.head_drop : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : List.drop i l ≠ []), (List.drop i l).head h = l[i]
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_7 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (l₁ : Lean.Level) (k₁ : ℕ) (l₂ : Lean.Level) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (∀ (l₁_1 : Lean.Level), l₁ = l₁_1.succ → False) →
    (∀ (l₂_1 : Lean.Level), l₂ = l₂_1.succ → False) →
      (∀ (l₁₁ l₁₂ l₂₁ l₂₂ : Lean.Level), l₁ = l₁₁.max l₁₂ → l₂ = l₂₁.max l₂₂ → False) →
        (∀ (l₁₁ l₁₂ l₂₁ l₂₂ : Lean.Level), l₁ = l₁₁.imax l₁₂ → l₂ = l₂₁.imax l₂₂ → False) →
          (∀ (n₁ n₂ : Lean.Name), l₁ = Lean.Level.param n₁ → l₂ = Lean.Level.param n₂ → False) →
            (∀ (n₁ n₂ : Lean.LMVarId), l₁ = Lean.Level.mvar n₁ → l₂ = Lean.Level.mvar n₂ → False) →
              (match l₁, k₁, l₂, k₂ with
                | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
                | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
                | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
                | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
                | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
                | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
                | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
                h_7 l₁ k₁ l₂ k₂
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf : ∀ {R : CommRingCat},
  CategoryTheory.IsIso
    (AlgebraicGeometry.Scheme.Modules.fromTildeΓ (SheafOfModules.unit (AlgebraicGeometry.Spec R).ringCatSheaf))
-- Mathlib.LinearAlgebra.Determinant
Pi.basisFun_det : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι],
  (Pi.basisFun R ι).det = Matrix.detRowAlternating
-- Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_compProd_iff' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η]
  [MeasurableSpace.CountableOrCountablyGenerated α β] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [∀ (a : α), NeZero (κ a)],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) ↔
    μ.AbsolutelyContinuous ν ∧ ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `flexible? stx` is `true` if `stx` is syntax for a tactic that takes a "wide" variety of
inputs and modifies them in possibly unpredictable ways.

The prototypical flexible tactic is `simp`.
The prototypical non-flexible tactic `rw`.
`simp only` is also non-flexible.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.flexible? : Lean.Syntax → Bool
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.mk : ∀ {M : Type u_2} [inst : Mul M], (Std.Commutative fun x1 x2 => x1 * x2) → IsMulCommutative M
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.eq_1 : ∀ (α : Type u) [inst : Add α], AddMagma.FreeAddSemigroup α = Quot (AddMagma.AssocRel α)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.instInhabitedResult'.default : Mathlib.Meta.NormNum.Result'
-- Init.Core
Std.Identity.toRightIdentity : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [self : Std.Identity op o], Std.RightIdentity op o
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a constant and a `C^n` function within a set at a point is `C^n`
within this set at this point.  -/
ContDiffWithinAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {R : Type u_3} [inst_5 : DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {s : Set E} {f : E → F}
  {x : E} (c : R), ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (fun y => c • f y) s x
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.M.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommMonCat),
  AddCommMonCat.FilteredColimits.M F =
    AddMonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.cancelledByEdit : Lean.Server.RequestCancellationToken → IO.CancelToken
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.toAddLeftReflectLE : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α], AddLeftReflectLE α
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The product of almost everywhere strongly measurable functions is measurable.  -/
MeasureTheory.AEStronglyMeasurable.tprod' : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousMul E] {L : SummationFilter ι}
  [L.NeBot] [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (∏'[L] (i : ι), f i) μ
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.setLIntegral_deterministic' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α}
  (hg : Measurable g),
  Measurable f →
    ∀ {s : Set β},
      MeasurableSet s →
        ∀ [inst : Decidable (g a ∈ s)],
          ∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
-- Mathlib.Data.Finset.Card
/-- Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t`
are equal.

The difference with `Finset.card_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.card_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain.  -/
Finset.card_nbij : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : α → β),
  Set.MapsTo i ↑s ↑t → Set.InjOn i ↑s → Set.SurjOn i ↑s ↑t → s.card = t.card
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sumEquivOfFintype_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] (x : AdicCompletion I (DirectSum ι fun j => M j)),
  (AdicCompletion.sumEquivOfFintype I M).symm x = (AdicCompletion.sumInv I M) x
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.length_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.range_functor : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u_1} (X : I → C),
  Set.range (CategoryTheory.Discrete.functor X).obj = Set.range X
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_sumInr : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {q' : M'} {t : Set M'},
  UniqueMDiffAt[t] q' → mfderiv[t] Sum.inr q' = ContinuousLinearMap.id 𝕜 (TangentSpace I q')
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff_linearIndepOn_finset : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v s ↔ ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
-- Mathlib.Tactic.Core
/-- Elaborate syntax for an `FVarId` in the local context of the given goal.  -/
Lean.Elab.Tactic.getFVarIdAt : Lean.MVarId → Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.FVarId
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.id_preimage : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X).base).obj U = U
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.mem_torsionBy_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R)
  (x : M), x ∈ Submodule.torsionBy R M a ↔ a • x = 0