mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given expressions `y₁ y₂ : Q($M)` with specified signs (either + or -), construct a proof that
the quotient of (± `y₁`) and (± `y₂`) (here taking the specified signs) is ± `y₁ / y₂`; return this
proof and the computed sign.  -/
Mathlib.Tactic.FieldSimp.Sign.div : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (y₁ y₂ : Q(«$M»)) →
        (g₁ g₂ : Mathlib.Tactic.FieldSimp.Sign M) →
          Lean.MetaM
            ((G : Mathlib.Tactic.FieldSimp.Sign M) ×
              have a := G.expr q(«$y₁» / «$y₂»);
              have a_1 := g₂.expr y₂;
              have a_2 := g₁.expr y₁;
              Q(«$a_2» / «$a_1» = «$a»))
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.ofRealCLM_norm : ‖Complex.ofRealCLM‖ = 1
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a<...b` by
varying the upper bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a + 1`, the statement holds for the empty range `a<...b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, if the
statement holds for `a<...b`, it also holds for the larger range `a<...(b + 1)`.

The following is an example reproving `length_toList_roo`.

```
example (a b : Nat) : (a<...b).toList.length = b - a - 1 := by
  induction a, b using Nat.induct_roo_right
  case base =>
    simp only [Nat.toList_roo_eq_nil, List.length_nil, *]; omega
  case step a b hle ih =>
    rw [Nat.toList_roo_eq_append (by omega),
      List.length_append, List.length_singleton, Nat.add_sub_cancel, ih]
    omega
``` -/
Nat.induct_roo_right : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a + 1 → motive a b) →
    (∀ (a b : ℕ), a + 1 ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℕ), motive a b
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The underlying type of a bipointed type.  -/
Bipointed.X : Bipointed → Type u
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ₄_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 2 ≠ 0 → 0 < W.preΨ₄.natDegree
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyGTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGTD k fallback = t₂.getKeyGTD k fallback
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.homAux.eq_2 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex C c} (φ : (i j : ι) → K.X i ⟶ L.X j) (i' : Option ι),
  (i' = none → False) → Homotopy.extend.homAux φ i' none = 0
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_bot : ∀ {G : Type u_2} [inst : AddGroup G], ⊥.unop = ⊥
-- Init.Data.String.Basic
String.Pos.Raw.utf8SetAux.eq_1 : ∀ (c' : Char) (x x_1 : String.Pos.Raw), String.Pos.Raw.utf8SetAux c' [] x x_1 = []
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem : ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)},
  ModularGroup.T ∈ Γ → (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- A choice of octahedron given by the octahedron axiom.  -/
CategoryTheory.Triangulated.someOctahedron : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              [CategoryTheory.IsTriangulated C] →
                {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                  {u₁₂ : X₁ ⟶ X₂} →
                    {u₂₃ : X₂ ⟶ X₃} →
                      {u₁₃ : X₁ ⟶ X₃} →
                        (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) →
                          {v₁₂ : X₂ ⟶ Z₁₂} →
                            {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                              (h₁₂ :
                                  CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                    CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                {v₂₃ : X₃ ⟶ Z₂₃} →
                                  {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                    (h₂₃ :
                                        CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                          CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                      {v₁₃ : X₃ ⟶ Z₁₃} →
                                        {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                          (h₁₃ :
                                              CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                                CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                            CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_bddBelow : ∀ {V : Type u} {G : SimpleGraph V}, BddBelow {n | G.Colorable n}
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_tdiv : ∀ {a b : ℤ},
  a.fdiv b =
    a.tdiv b - if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else 1 else if 0 ≤ b then b.sign else 1 + b.sign
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roo_eq_add : ∀ {m n i : ℕ}, i < n - (m + 1) → (m<...n).toList[i]! = m + 1 + i
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat.inj : ∀ {a b : Lean.Expr} {natStructId : ℕ} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr}
  {natStructId_1 : ℕ} {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat a b natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat a_1 b_1 natStructId_1 lhs_1 rhs_1 →
    a = a_1 ∧ b = b_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Init.Data.SInt.Bitwise
instCommutativeInt64HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Init.Grind.ToInt
Lean.Grind.ToInt.Div.mk : ∀ {α : Type u} [inst : Div α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), ↑(x / y) = ↑x / ↑y) → Lean.Grind.ToInt.Div α I
-- Mathlib.Analysis.Convex.Basic
Convex.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (s : Set E), Convex 𝕜 s = ∀ ⦃x : E⦄, x ∈ s → StarConvex 𝕜 x s
-- Mathlib.Logic.Equiv.Defs
Equiv.equivCongr_refl_left : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β ≃ γ) (e : α ≃ β), ((Equiv.refl α).equivCongr bg) e = e.trans bg
-- Mathlib.Topology.Defs.Basic
/-- A map `f : X → Y` is said to be a *closed map*,
if the image of any closed `U : Set X` is closed in `Y`.  -/
IsClosedMap : {X : Type u} → {Y : Type v} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.liftSemilatticeSup.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : SemilatticeSup α]
  (gi : GaloisCoinsertion u l),
  gi.liftSemilatticeSup =
    { toPartialOrder := inst, sup := fun a b => gi.choice (u a ⊔ u b) ⋯, le_sup_left := ⋯, le_sup_right := ⋯,
      sup_le := ⋯ }
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.contract_C : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (r : R), Polynomial.contract p (Polynomial.C r) = Polynomial.C r
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.nat_add_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℤ → M},
  HasSum f m → HasSum (fun n => f ↑n + f (-(↑n + 1))) m
-- Mathlib.Algebra.Lie.Character
LieAlgebra.lieCharacter_apply_lie' : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (χ : LieAlgebra.LieCharacter R L) (x y : L), ⁅χ x, χ y⁆ = 0
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- If `F` has odd characteristic, then `quadraticChar F` takes the value `-1`.  -/
quadraticChar_exists_neg_one : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∃ a, (quadraticChar F) a = -1