mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Copy `Pi.addCommMonoid`, ensuring the pointwise operations hold by defeq.  -/
instAddCommMonoidFormalMultilinearSeries : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : ContinuousAdd E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : ContinuousAdd F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] → AddCommMonoid (FormalMultilinearSeries 𝕜 E F)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.top_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ⊤ ∈ P.invtRootSubmodule
-- Mathlib.Algebra.Group.Opposite
AddOpposite.unop_zsmul : ∀ {α : Type u_1} [inst : SubNegMonoid α] (x : αᵃᵒᵖ) (z : ℤ), AddOpposite.unop (z • x) = z • AddOpposite.unop x
-- Std.Sat.AIG.CNF
/-- Evaluate the CNF contained within the state.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.eval : {aig : Std.Sat.AIG ℕ} → (ℕ → Bool) → Std.Sat.AIG.toCNF.State✝ aig → Bool
-- Mathlib.Order.BoundedOrder.Basic
/-- A subtype remains a `⊥`-order if the property holds at `⊥`.  -/
Subtype.orderBot : {α : Type u} → {p : α → Prop} → [inst : LE α] → [inst_1 : OrderBot α] → p ⊥ → OrderBot { x // p x }
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Field.charP_iff_model_fieldOfChar : ∀ {p : ℕ} {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K],
  K ⊨ FirstOrder.Language.Theory.fieldOfChar p ↔ CharP K p
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)}
  [inst : Fintype ι],
  π.IsSubordinate r →
    ∀ (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J), (π.biUnionPrepartition πi).IsSubordinate r
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.adjoin_id_eq_span_one_union : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜),
  ↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) =
    ↑(Submodule.span 𝕜 ({1} ∪ ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})))
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_lt_one_iff_dvd : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]), ‖x‖ < 1 ↔ ↑p ∣ x
-- Mathlib.Tactic.LinearCombinationPrime
/-- Result of `expandLinearCombo`, either an equality proof or a value.  -/
Mathlib.Tactic.LinearCombinationPrime.Expanded : Type
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divInvMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → DivInvMonoid (f i)] → DivInvMonoid ((i : I) → f i)
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.equivNatTrans_symm_apply : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) (α : T.comp R ⟶ L.comp B),
  (CategoryTheory.TwoSquare.equivNatTrans T L R B).symm α = CategoryTheory.TwoSquare.mk T L R B α
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodAssoc_symm_apply : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : TopologicalSpace M₁] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (p₁ : M₁) (p₂ : M₂) (p₃ : M₃), (ContinuousLinearEquiv.prodAssoc R M₁ M₂ M₃).symm (p₁, p₂, p₃) = ((p₁, p₂), p₃)
-- Mathlib.LinearAlgebra.Dual.Lemmas
span_flip_eq_top_iff_linearIndependent : ∀ {ι : Type u_1} {α : Type u_2} {F : Type u_3} [Finite ι] [inst : Field F] {f : ι → α → F},
  Submodule.span F (Set.range (flip f)) = ⊤ ↔ LinearIndependent F f
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.mk.inj : ∀ {ω₁ ω₂ : ℂ} {indep : LinearIndependent ℝ ![ω₁, ω₂]} {ω₁_1 ω₂_1 : ℂ} {indep_1 : LinearIndependent ℝ ![ω₁_1, ω₂_1]},
  { ω₁ := ω₁, ω₂ := ω₂, indep := indep } = { ω₁ := ω₁_1, ω₂ := ω₂_1, indep := indep_1 } → ω₁ = ω₁_1 ∧ ω₂ = ω₂_1
-- Mathlib.RingTheory.PowerSeries.Order
_private.Mathlib.RingTheory.PowerSeries.Order.0.PowerSeries.order_add_of_order_ne.aux : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), φ.order < ψ.order → (φ + ψ).order ≤ min φ.order ψ.order
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- For a normed space `F`, we have constructed in `PiTensorProduct.liftEquiv` the canonical
linear equivalence between `ContinuousMultilinearMap 𝕜 E F` and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`
(induced by `PiTensorProduct.lift`). Here we give the upgrade of this equivalence to
an isometric linear equivalence; in particular, it is a continuous linear equivalence.  -/
PiTensorProduct.liftIsometry : {ι : Type u_1} →
  [inst : Fintype ι] →
    (𝕜 : Type u_2) →
      (E : ι → Type u_3) →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              (F : Type u_4) →
                [inst_4 : SeminormedAddCommGroup F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (PiTensorProduct 𝕜 fun i => E i) →L[𝕜] F
-- Init.Core
/-- `return (b : β) s` means that the block exited via a `return b` early-exit command  -/
DoResultPRBC.return : {α β σ : Type u} → β → σ → DoResultPRBC α β σ
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_le_card_height : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
  A.eRank ≤ ENat.card m
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.id_comp : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G'), SimpleGraph.Hom.id.comp f = f
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `grind` at every step in proofs, reporting where it succeeds.  -/
tryAtEachStepGrind : Mathlib.TacticAnalysis.Config
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.map_resLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V' ≤ V) {Z : AlgebraicGeometry.Scheme} (h : ↑U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.homOfLE i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V' ⋯) h
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.instIsOpenImmersionFromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Mathlib.Topology.Homotopy.HSpaces
Path.delayReflRight.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (θ : ↑unitInterval) (γ : Path x y),
  Path.delayReflRight θ γ =
    { toFun := fun t => γ (unitInterval.qRight (t, θ)), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.zero_compContinuous : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace γ] (f : C(γ, α)), BoundedContinuousFunction.compContinuous 0 f = 0
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Multiplication in the colimit is independent of the chosen "maximum" in the filtered category.
In particular, this lemma allows us to "unfold" the definition of the multiplication of `x` and `y`,
using a custom object `k` and morphisms `f : x.1 ⟶ k` and `g : y.1 ⟶ k`.
 -/
MonCat.FilteredColimits.colimit_mul_mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  MonCat.FilteredColimits.M.mk F x * MonCat.FilteredColimits.M.mk F y =
    MonCat.FilteredColimits.M.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd * (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩
-- Mathlib.Order.Category.BddDistLat
BddDistLat.Iso.mk_inv : ∀ {α β : BddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat),
  (BddDistLat.Iso.mk e).inv =
    BddDistLat.ofHom
      (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.Testing.Plausible.Sampleable
Plausible.PNat.Arbitrary : Plausible.Arbitrary ℕ+
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instIsScalarTowerQuotientIdealResidueField : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I : Ideal A)
  [inst_3 : I.IsPrime], IsScalarTower R (A ⧸ I) I.ResidueField
-- Mathlib.Data.Nat.Nth
Nat.nth_of_card_le : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {n : ℕ}, hf.toFinset.card ≤ n → Nat.nth p n = 0
-- Init.Tactics
/-- `exact e` closes the main goal if its target type matches that of `e`.
 -/
Lean.Parser.Tactic.exact : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.toNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {M N : CategoryTheory.Comonad C} → CategoryTheory.ComonadHom M N → CategoryTheory.NatTrans M.toFunctor N.toFunctor
-- Mathlib.Analysis.Calculus.FDeriv.Prod
Differentiable.prodMk : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {f₂ : E → G},
  Differentiable 𝕜 f₁ → Differentiable 𝕜 f₂ → Differentiable 𝕜 fun x => (f₁ x, f₂ x)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cones` is represented by `X`, each cone `s` gives a morphism `s.pt ⟶ X`.  -/
CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {X : C} → F.cones.RepresentableBy X → (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ X
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (_x _y _z : C) (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y))
  (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)),
  CategoryTheory.Join.comp f g = { down := CategoryTheory.CategoryStruct.comp f.down g.down }
-- Mathlib.Data.Finset.Sum
Finset.toLeft_sdiff : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (u \ v).toLeft = u.toLeft \ v.toLeft
-- Lean.Language.Basic
/-- Transforms a language-specific snapshot to a homogeneous snapshot tree.  -/
Lean.Language.ToSnapshotTree.toSnapshotTreeM : {α : Type} → [self : Lean.Language.ToSnapshotTree α] → α → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_comm₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < b → 0 < c → (a / b < c ↔ a / c < b)
-- Init.Data.Nat.Lemmas
Nat.mod_two_bne_zero : ∀ {a : ℕ}, (a % 2 != 0) = (a % 2 == 1)
-- Mathlib.Order.CompleteLattice.Lemmas
disjoint_of_sSup_disjoint_of_le_of_le : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α} {c d : Set α},
  (∀ e ∈ c, e ≤ a) → (∀ e ∈ d, e ≤ b) → Disjoint a b → ⊥ ∉ c ∨ ⊥ ∉ d → Disjoint c d
-- Mathlib.Data.Ineq
/-- Given an expression `e`, parse it as a `=`, `≤` or `<`, and return this relation (as a
`Linarith.Ineq`) together with the type in which the (in)equality occurs and the two sides of the
(in)equality.

This function is more naturally in the `Option` monad, but it is convenient to put in `MetaM`
for compositionality.
 -/
Lean.Expr.ineq? : Lean.Expr → Lean.MetaM (Mathlib.Ineq × Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- The category of finitely generated algebras is essentially small.  -/
instEssentiallySmallFGAlgCat : ∀ (R : Type u) [inst : CommRing R], CategoryTheory.EssentiallySmall.{u, v, max (v + 1) u} (FGAlgCat R)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_inter : ∀ {ι : Type u_3} [Finite ι] {s₁ s₂ : Set (ι → ℕ)}, IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ ∩ s₂)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).left.right = Y.right
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_add : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), ↑↑(f + g) =ᵐ[μ] ↑↑f + ↑↑g
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mkIso.congr_simp : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f f_1 : X.obj ≅ Y.obj) (e_f : f = f_1)
  (hf :
    CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) =
      CategoryTheory.CategoryStruct.comp f.hom Y.d),
  CategoryTheory.DifferentialObject.mkIso f hf = CategoryTheory.DifferentialObject.mkIso f_1 ⋯
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.mapCoeffs_apply : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {R' : Type u_13} [inst_3 : Semiring R'] [inst_4 : Module R' M] (f : R ≃+* R')
  (h : ∀ (c : R) (x : M), f c • x = c • x) (i : ι), (b.mapCoeffs f h) i = b i
-- Mathlib.Data.Sign.Defs
SignType.self_eq_neg_iff : ∀ {a : SignType}, a = -a ↔ a = 0
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_mul_of_le_right : ∀ {α : Type u} [inst : Mul α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b c : α}, a ≤ c → a ≤ b * c
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_sum : ∀ {α : Type u_3} {β : Type u_4} (f : α ⊕ β → Ordinal.{u}) [Small.{u, u_3} α] [Small.{u, u_4} β],
  iSup f = max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart.congr_simp : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x x_1 : K),
  x = x_1 → ArchimedeanClass.stdPart x = ArchimedeanClass.stdPart x_1
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.toMeasurePreserving : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) Ergodic._auto_1},
  Ergodic f μ → MeasureTheory.MeasurePreserving f μ μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.surjOn_tan : Set.SurjOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) Set.univ
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.normSq_kahler : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), Complex.normSq ((o.kahler x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- A morphism in the `Dial C` category from `⟨U, X, α⟩` to `⟨V, Y, β⟩` is a pair
`(f : U ⟶ V, F : U ⨯ Y ⟶ X)` such that `{(u,y) | α(u, F(u, y))} ≤ {(u,y) | β(f(u), y)}`.  -/
CategoryTheory.Dial.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Dial C → CategoryTheory.Dial C → Type v
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMax'.eq_2 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α) (size : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α),
  x.splitMax' x_1 (Ordnode.node size rl rx rr) =
    match rl.splitMax' rx rr with
    | (r', xm) => (x.balanceL x_1 r', xm)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_unop_of_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [CategoryTheory.Limits.HasColimit F], CategoryTheory.Limits.HasLimit F.unop
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.isMultiplicative_one : ∀ {R : Type u_1} [inst : MonoidWithZero R], ArithmeticFunction.IsMultiplicative 1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.mk : {m : Type w → Type w'} →
  {α : Type v} →
    (Property : α → Prop) →
      (small : Std.Internal.Small (Subtype Property)) →
        m (Std.Internal.USquash (Subtype Property)) → Std.Iterators.HetT m α
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTopCoeff_add_one : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [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] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M)
  (hα : α ≠ 0), LieModule.chainTopCoeff α β + 1 = Nat.find ⋯
-- Mathlib.Algebra.Algebra.Tower
/-- `AlgEquiv.restrictScalars` as a homomorphism.  -/
AlgEquiv.restrictScalarsHom : (R : Type u) →
  {S : Type v} →
    {A : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra S A] → [inst_5 : Algebra R A] → [IsScalarTower R S A] → (A ≃ₐ[S] A) →* A ≃ₐ[R] A
-- Mathlib.Data.Sym.Sym2
Sym2.pmap_pair : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (a b : α) (h : ∀ x ∈ s(a, b), P x),
  Sym2.pmap f s(a, b) h = s(f a ⋯, f b ⋯)
-- Mathlib.Order.CompleteLattice.Basic
biInf_congr' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] {p : ι → Prop} {f g : (i : ι) → p i → α},
  (∀ (i : ι) (hi : p i), f i hi = g i hi) → ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi
-- Mathlib.GroupTheory.GroupAction.Transitive
/-- An action of a group is pretransitive iff the orbit of every given element is full  -/
MulAction.isPretransitive_iff_orbit_eq_univ : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (a : X),
  MulAction.IsPretransitive G X ↔ MulAction.orbit G a = Set.univ
-- Init.Data.Order.Lemmas
Std.le_trans : ∀ {α : Type u} [inst : LE α] [Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2] {a b c : α},
  a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Logic.Function.Iterate
/-- A recursor for the iterate of a function.  -/
Function.Iterate.rec : {α : Type u} →
  (motive : α → Sort u_1) →
    {a : α} → motive a → {f : α → α} → ((a : α) → motive a → motive (f a)) → (n : ℕ) → motive (f^[n] a)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain_comp_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n),
  (CochainComplex.mappingCocone.liftCochain φ α β h).comp
      (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCocone.fst φ)) ⋯ =
    α
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce.not : ∀ {α : Type u_1} [inst : DecidableEq α] {p : Prop} {L₁ L₂ L₃ : List (α × Bool)} {x : α} {b : Bool},
  FreeAddGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- If `α` has at least `n` elements, then an `n`-pretransitive action
is `m`-pretransitive for any `m ≤ n`.

For an infinite `α`, use `MulAction.isMultiplyPretransitive_of_le'`.  -/
MulAction.isMultiplyPretransitive_of_le : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {m n : ℕ}
  [MulAction.IsMultiplyPretransitive G α n],
  m ≤ n → n ≤ Nat.card α → ∀ [Finite α], MulAction.IsMultiplyPretransitive G α m
-- Mathlib.Order.Sublattice
Sublattice.mk_sup_mk : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} (a b : α) (ha : a ∈ L) (hb : b ∈ L),
  ⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.Const.get?.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option ((_ : α) × β) → Sort u_3) (p : (_ : α) × β) (h_1 : Unit → motive none)
  (h_2 : (p : (_ : α) × β) → motive (some p)),
  (match some p with
    | none => h_1 ()
    | some p => h_2 p) =
    h_2 p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.Raw.empty.maxKey? = none
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ioi.injEq : ∀ (n n_1 : Lean.Term), (BigOperators.FinsetResult.Ioi✝ n = BigOperators.FinsetResult.Ioi✝ n_1) = (n = n_1)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- See Note [custom simps projection].  -/
OrderMonoidIso.Simps.apply : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → (α ≃*o β) → α → β
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.bilinearCombination_apply_single : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {S : Type u_4} [inst_4 : Semiring S] [inst_5 : Module S M] [inst_6 : SMulCommClass R S M]
  (v : α → M) [inst_7 : DecidableEq α] (i : α) (r : R), ((Fintype.bilinearCombination R S) v) (Pi.single i r) = r • v i