mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LHopital
HasDerivAt.lhopital_zero_right_on_Ico : ∀ {a b : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  a < b →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
        ContinuousOn f (Set.Ico a b) →
          ContinuousOn g (Set.Ico a b) →
            (∀ x ∈ Set.Ioo a b, g' x ≠ 0) →
              f a = 0 →
                g a = 0 →
                  Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l →
                    Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l
-- Init.Data.String.Lemmas.Search
String.Pos.le_find : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {s : String} (pos : s.Pos) (pattern : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pattern σ], pos ≤ pos.find pattern
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_eq_some_iff_succMany : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {n : ℕ} {a b : α},
  Std.PRange.succMany? n a = some b ↔ Std.PRange.succMany n a = b
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey?_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l) =
      Option.map (fun km => if (km == k) = true then k else km) (Std.Internal.List.maxKey? l)
-- Mathlib.Logic.Basic
xor_def : ∀ {a b : Prop}, Xor a b ↔ a ∧ ¬b ∨ b ∧ ¬a
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {fg : X ⟶ Z},
  CategoryTheory.CategoryStruct.comp f g = fg →
    ∀ [HomotopicalAlgebra.WeakEquivalence f] [HomotopicalAlgebra.WeakEquivalence fg],
      HomotopicalAlgebra.WeakEquivalence g
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_add_right_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (z * x + y) → IsCoprime x y
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_roi : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LT α] [DecidableLT α] [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.Rxi.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roi α}
  {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)⦄
-- Mathlib.Control.Functor
/-- If we consider `x : F α` to, in some sense, contain values of type `α`, then
`supp x` is the set of values of type `α` that `x` contains.  -/
Functor.supp : {F : Type u → Type v} → [Functor F] → {α : Type u} → F α → Set α
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.eq_of_succ?_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α] {a b : α},
  Std.PRange.succ? a = Std.PRange.succ? b → a = b
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.topEquivalence_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.ObjectProperty.topEquivalence C).inverse = ⊤.lift (CategoryTheory.Functor.id C) ⋯
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.natDegree_iterate_derivative : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (k : ℕ),
  ((⇑Polynomial.derivative)^[k] p).natDegree ≤ p.natDegree - k
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_pos : ∀ {p : ℝ} {x : NNReal}, 0 < x → 0 < x ^ p
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K}
  (P : CategoryTheory.Limits.IsColimit (CategoryTheory.WithInitial.coconeEquiv.functor.obj t))
  (s : CategoryTheory.Limits.Cocone K),
  ((CategoryTheory.WithInitial.isColimitEquiv P).desc s).right =
    ((CategoryTheory.Limits.IsColimit.ofLeftAdjoint CategoryTheory.WithInitial.coconeEquiv.symm.toAdjunction P).desc
        s).right
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.cfcHom_eq_cfcAux : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian), cfcHom ⋯ = hA.cfcAux
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.lift_ι_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.instQuasiCompactToImage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.QuasiCompact (AlgebraicGeometry.Scheme.Hom.toImage f)
-- Mathlib.Analysis.Normed.Group.Basic
normAddGroupNorm.eq_1 : ∀ (E : Type u_5) [inst : NormedAddGroup E],
  normAddGroupNorm E = { toAddGroupSeminorm := normAddGroupSeminorm E, eq_zero_of_map_eq_zero' := ⋯ }
-- Lean.Data.JsonRpc
/-- Danger: For performance reasons, this function makes a number of fragile assumptions about `input`.
Namely:
- `input` is the output of `(toJson (v : Message)).compress`
- `compress` yields a lexicographic ordering of JSON object keys
 -/
Lean.JsonRpc.parseMessageMetaData : String → Except String Lean.JsonRpc.MessageMetaData
-- Mathlib.Combinatorics.KatonaCircle
Numbering.IsPrefix.subset_of_card_le_card : ∀ {X : Type u_1} [inst : Fintype X] {f : Numbering X} {s t : Finset X},
  f.IsPrefix s → f.IsPrefix t → s.card ≤ t.card → s ⊆ t
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = dist y x
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The prime case of the **Erdős–Ginzburg–Ziv theorem** for `ℤ/pℤ`.

Any sequence of `2 * p - 1` elements of `ZMod p` contains a subsequence of `p` elements whose sum is
zero.  -/
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.ZMod.erdos_ginzburg_ziv_prime : ∀ {ι : Type u_1} {p : ℕ} [inst : Fact (Nat.Prime p)] {s : Finset ι} (a : ι → ZMod p),
  s.card = 2 * p - 1 → ∃ t ⊆ s, t.card = p ∧ ∑ i ∈ t, a i = 0
-- Lean.Syntax
/-- Set `SourceInfo.leading` according to the trailing stop of the preceding token.
The result is a round-tripping syntax tree IF, in the input syntax tree,
* all leading stops, atom contents, and trailing starts are correct
* trailing stops are between the trailing start and the next leading stop.

Remark: after parsing, all `SourceInfo.leading` fields are empty.
The `Syntax` argument is the output produced by the parser for `source`.
This function "fixes" the `source.leading` field.

Additionally, we try to choose "nicer" splits between leading and trailing stops
according to some heuristics so that e.g. comments are associated to the (intuitively)
correct token.

Note that the `SourceInfo.trailing` fields must be correct.
The implementation of this Function relies on this property.  -/
Lean.Syntax.updateLeading : Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
be promoted to a pseudofunctor from `LocallyDiscrete I` to `B`.
 -/
CategoryTheory.Functor.toPseudofunctor' : {I : Type u_1} →
  {B : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} I] →
      [inst_1 : CategoryTheory.Bicategory B] →
        [inst_2 : CategoryTheory.Bicategory.Strict B] →
          CategoryTheory.Functor I B → CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete I) B
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.nonUnitalAlgHom_ext'_iff : ∀ {k : Type u_1} {G : Type u_2} {A : Type u_6} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Monoid G]
  [inst_2 : Semiring k] [inst_3 : MulSemiringAction G k] [inst_4 : DistribMulAction k A]
  {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A},
  φ₁ = φ₂ ↔ φ₁.toMulHom.comp ↑(SkewMonoidAlgebra.of k G) = φ₂.toMulHom.comp ↑(SkewMonoidAlgebra.of k G)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.mk.sizeOf_spec : ∀ (knowsType knowsLevel inBottomUp parentIsApp : Bool) (subExpr : Lean.SubExpr),
  sizeOf
      { knowsType := knowsType, knowsLevel := knowsLevel, inBottomUp := inBottomUp, parentIsApp := parentIsApp,
        subExpr := subExpr } =
    1 + sizeOf knowsType + sizeOf knowsLevel + sizeOf inBottomUp + sizeOf parentIsApp + sizeOf subExpr
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.image_sdiff`. -/
Set.image_diff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s t : Set α), f '' (s \ t) = f '' s \ f '' t
-- Mathlib.Algebra.Order.Kleene
add_eq_sup : ∀ {α : Type u_1} [inst : IdemSemiring α] (a b : α), a + b = a ⊔ b
-- Std.Http.Data.URI.Basic
Std.Http.instReprURI : Repr Std.Http.URI
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_dvd : ∀ {a b : ℤ}, ↑a.natAbs ∣ b ↔ a ∣ b
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : EsakiaHom α β), (EsakiaHom.id β).comp f = f
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.divXPowOrder_one : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], PowerSeries.divXPowOrder 1 = 1
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.token.sizeOf_spec : ∀ (val : Lean.Parser.Token), sizeOf (Lean.Parser.ParserExtension.Entry.token val) = 1 + sizeOf val
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative additive group and `n : ℕ`, `h : G → ℝ` satisfy
* `G / n • G` is finite,
* for all `g x : G`, `h x ≤ a * h (g + x) + c g`,
* for all `x : G`, `h (n • x) ≥ b * h x - c₀`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

where `0 ≤ a < b` and `c₀` are real numbers, `c : G → ℝ`, then `G` is finitely generated.  -/
AddCommGroup.fg_of_descent : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} {h : G → ℝ} {a b c₀ : ℝ} {c : G → ℝ},
  0 ≤ a →
    a < b →
      (nsmulAddMonoidHom n).range.FiniteIndex →
        (∀ (g x : G), h x ≤ a * h (g + x) + c g) →
          (∀ (x : G), b * h x - c₀ ≤ h (n • x)) → ∀ [Northcott h], AddGroup.FG G
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_forall_getKey_eq_of_forall_getElem?_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') →
        (∀ (k : α), m₁[k]? = m₂[k]?) → m₁.Equiv m₂
-- Mathlib.Data.ENNReal.Action
/-- A `Module` over `ℝ≥0∞` restricts to a `Module` over `ℝ≥0`.  -/
ENNReal.instModuleNNReal : {M : Type u_1} → [inst : AddCommMonoid M] → [Module ENNReal M] → Module NNReal M
-- Mathlib.Algebra.Group.Subgroup.Order
instIsModularLatticeAddSubgroup : ∀ {C : Type u_1} [inst : AddCommGroup C], IsModularLattice (AddSubgroup C)
-- Mathlib.Algebra.Homology.ExactSequence
/-- The short complex consisting of maps `S.map' i (i + 1)` and `S.map' (i + 1) (i + 2)`
when we know that `S : ComposableArrows C n` satisfies `S.IsComplex`.  -/
CategoryTheory.ComposableArrows.sc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        (S : CategoryTheory.ComposableArrows C n) →
          S.IsComplex →
            (i : ℕ) → autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.sc._auto_1 → CategoryTheory.ShortComplex C
-- Mathlib.Algebra.Lie.Nilpotent
Equiv.lieModule_isNilpotent_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [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] [LieModule R L M] {L₂ : Type u_1}
  {M₂ : Type u_2} [inst_7 : LieRing L₂] [inst_8 : LieAlgebra R L₂] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : LieRingModule L₂ M₂] [LieModule R L₂ M₂] (f : L ≃ₗ⁅R⁆ L₂) (g : M ≃ₗ[R] M₂),
  (∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) → (LieModule.IsNilpotent L M ↔ LieModule.IsNilpotent L₂ M₂)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.containsThenInsert_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.containsThenInsert k v).1 = t.contains k
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsIntegral X] (x : ↥X),
  IsFractionRing ↑(X.presheaf.stalk x) ↑X.functionField
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.of_X : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X n ⟶ X (n + 1)) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0),
  (CochainComplex.of X d sq).X = X
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_inv_apply_1_1 : ∀ {X Y Z : Type u}
  {x :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).1.1 = x.1
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The cusps of any arithmetic subgroup are the same as those of `SL(2, ℤ)`.  -/
Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] {c : OnePoint ℝ},
  IsCusp c 𝒢 ↔ IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
-- Mathlib.SetTheory.Ordinal.Notation
ONote.scale.eq_1 : ∀ (x : ONote), x.scale ONote.zero = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig.decls.size
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.regular_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.AddMonObj A], (CategoryTheory.AddMod.regular A).X = A
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : Monoid M] [inst_3 : MulAction M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] [inst_5 : MeasurableConstSMul M α],
  DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp = Function.Injective.mulAction Subtype.val ⋯ ⋯
-- Mathlib.Tactic.WLOG
/-- `wlog h : P` adds an assumption `h : P` to the main goal, and adds a side goal that
requires showing that the case `h : ¬ P` can be reduced to the case where `P` holds
(typically by symmetry). The side goal will be at the top of the stack. In this side goal,
there will be two additional assumptions:
- `h : ¬ P`: the assumption that `P` does not hold
- `this`: which is the statement that in the old context `P` suffices to prove the goal.
  By default, the entire context is reverted to produce `this`.

* `wlog h : P with H` gives the name `H` to the statement that `P` proves the goal.
* `wlog h : P generalizing x y ...` reverts certain parts of the context before creating the new
  goal. In this way, the wlog-claim `this` can be applied to `x` and `y` in different orders
  (exploiting symmetry, which is the typical use case).
* `wlog! h : P` also calls `push Not` at the generated hypothesis `h`.
  `wlog! h : P ∧ Q` will transform `¬ (P ∧ Q)` to `P → ¬ Q`
* `wlog! +distrib h : P` also calls `push +distrib Not` at the generated hypothesis `h`.
  `wlog! +distrib h : P ∧ Q` will transform `¬ (P ∧ Q)` to `¬P ∨ ¬Q`.
 -/
Mathlib.Tactic.wlog! : Lean.ParserDescr
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_assoc' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α),
  Associated (lcm (lcm m n) k) (lcm m (lcm n k))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation : Type
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.hasNoindexAnnotation : Lean.Expr → Bool
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
_private.Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence.0.AlgebraicTopology.DoldKan.homotopyPToId.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (q : ℕ) → motive q.succ),
  (match 0 with
    | 0 => h_1 ()
    | q.succ => h_2 q) =
    h_1 ()
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms in `ComposableArrows C 3`.  -/
CategoryTheory.ComposableArrows.homMk₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 3} →
      (app₀ : f.obj' 0 _proof_297✝ ⟶ g.obj' 0 _proof_297✝) →
        (app₁ : f.obj' 1 _proof_298✝ ⟶ g.obj' 1 _proof_298✝) →
          (app₂ : f.obj' 2 _proof_299✝ ⟶ g.obj' 2 _proof_299✝) →
            (app₃ : f.obj' 3 _proof_300✝ ⟶ g.obj' 3 _proof_300✝) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp
                      (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝) app₁ =
                    CategoryTheory.CategoryStruct.comp app₀
                      (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
                  _auto_291✝ →
                autoParam
                    (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂ =
                      CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_299✝))
                    _auto_293✝ →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃ =
                        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_300✝))
                      _auto_295✝ →
                    (f ⟶ g)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CnstrRHS.mk.sizeOf_spec : ∀ (levelNames : Array Lean.Name) (numMVars : ℕ) (expr : Lean.Expr),
  sizeOf { levelNames := levelNames, numMVars := numMVars, expr := expr } =
    1 + sizeOf levelNames + sizeOf numMVars + sizeOf expr
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.has_union : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s₁ s₂ : Set α},
  d.Has s₁ → d.Has s₂ → Disjoint s₁ s₂ → d.Has (s₁ ∪ s₂)
-- Mathlib.Algebra.Category.Ring.Topology
/-- `Hom(A/I, R)` has the subspace topology of `Hom(A, R)`.
More generally, a surjection `A ⟶ B` gives rise to an embedding `Hom(B, R) ⟶ Hom(A, R)`  -/
CommRingCat.HomTopology.isEmbedding_precomp_of_surjective : ∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] (f : A ⟶ B),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsEmbedding fun x => CategoryTheory.CategoryStruct.comp f x
-- Aesop.Frontend.Extension.Init
Aesop.instEmptyCollectionDeclaredRuleSets : EmptyCollection Aesop.DeclaredRuleSets
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to construct `Mor₂` terms.  -/
Mathlib.Tactic.BicategoryLike.MkMor₂ : (Type → Type) → Type
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processAppDefault : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
CategoryTheory.Precoverage.Generates.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C},
  K ≤ J.toPrecoverage →
    (∀ (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))),
        (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) →
          CategoryTheory.Presieve.IsSheaf J F) →
      K.Generates J
-- Init.Data.Bool
Bool.and'_eq_and : ∀ (a b : Bool), a.and' b = (a && b)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.forget_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C), T.forget.Faithful
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (e : R ≃+* S), e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S
-- Mathlib.Data.Finset.Card
Finset.card_le_six : ∀ {α : Type u_1} [inst : DecidableEq α] {a b c d e f : α}, {a, b, c, d, e, f}.card ≤ 6
-- Mathlib.Algebra.Group.Commute.Units
isUnit_pow_iff : ∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {a : M}, n ≠ 0 → (IsUnit (a ^ n) ↔ IsUnit a)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.instIsAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f], AlgebraicGeometry.IsAffineHom f
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isInfinitePlace : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), NumberField.IsInfinitePlace ↑v
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.getFunIndInfoForInduct? : Lean.Name → Lean.CoreM (Option Lean.Meta.FunIndInfo)
-- Init.Core
EStateM.Result.ok.inj : ∀ {ε σ α : Type u} {a : α} {a_1 : σ} {a_2 : α} {a_3 : σ},
  EStateM.Result.ok a a_1 = EStateM.Result.ok a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The underlying continuous linear map. Use `hom` instead.  -/
TopModuleCat.Hom.hom' : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → {X Y : TopModuleCat R} → X.Hom Y → ↑X.toModuleCat →L[R] ↑Y.toModuleCat
-- Mathlib.Data.Vector3
Fin2.insertPerm.eq_1 : ∀ (n : ℕ), Fin2.fz.insertPerm Fin2.fz = Fin2.fz
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- In the model space, `chartAt` is always the identity.  -/
chartAt_self_eq : ∀ {H : Type u_5} [inst : TopologicalSpace H] {x : H}, chartAt H x = OpenPartialHomeomorph.refl H
-- Mathlib.Data.TypeVec
TypeVec.diagSub.eq_1 : ∀ (n_2 : ℕ) (α_2 : TypeVec.{u} (n_2 + 1)) (a : Fin2 n_2) (x_2 : α_2 a.fs),
  TypeVec.diagSub a.fs x_2 = TypeVec.diagSub a x_2
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebung_coeff_zero : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R),
  (WittVector.verschiebung x).coeff 0 = 0