mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Function
ConvexOn.subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {t : Set E}, ConvexOn 𝕜 t f → s ⊆ t → Convex 𝕜 s → ConvexOn 𝕜 s f
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- Let `M` act continuously on an R₁ topological space `X`.
Let `μ` be a finite inner regular measure on `X` which is ergodic with respect to this action.
If a null measurable set `s` is a.e. equal
to its preimages under the action of a dense set of elements of `M`,
then it is either null or conull.  -/
aeconst_of_dense_setOfPred_preimage_smul_ae : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g • x) ⁻¹' s =ᵐ[μ] s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Algebra.Colimit.Module
/-- Every element of the direct limit corresponds to some element in
some component of the directed system.  -/
Module.DirectLimit.exists_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] [Nonempty ι] [IsDirectedOrder ι] (z : Module.DirectLimit G f),
  ∃ i x, (Module.DirectLimit.of R ι G f i) x = z
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.term? : Lean.Elab.PartialFixpoint → Option Lean.Term
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.u_le_u_iff : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β] (gi : GaloisInsertion l u)
  {a b : β}, u a ≤ u b ↔ a ≤ b
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_iInf : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {ι : Sort u_1} [Nonempty ι]
  (f : R →+* S),
  Function.Injective ⇑f → ∀ (s : ι → Subsemiring R), Subsemiring.map f (iInf s) = ⨅ i, Subsemiring.map f (s i)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.desc_commutes_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp (J.ι.f 0) ((CategoryTheory.InjectiveResolution.desc f I J).f 0) =
    CategoryTheory.CategoryStruct.comp f (I.ι.f 0)
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.smul_eq : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {a : 𝕜}, Balanced 𝕜 s → ‖a‖ = 1 → a • s = s
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a left invariant measure under a left action is left invariant, assuming that
the action preserves multiplication.  -/
MeasureTheory.isMulLeftInvariant_map_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : SMul α G] [SMulCommClass α G G] [MeasurableConstSMul α G] [μ.IsMulLeftInvariant] (a : α),
  (MeasureTheory.Measure.map (fun x => a • x) μ).IsMulLeftInvariant
-- Std.Data.TreeSet.DecidableEquiv
Std.TreeSet.instDecidableEquivOfTransCmpOfLawfulEqCmp : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → [Std.LawfulEqCmp cmp] → {t₁ t₂ : Std.TreeSet α cmp} → Decidable (t₁.Equiv t₂)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey! = k
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.eLpNorm_ne_top : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : TopologicalSpace ε] {f : α → ε}, MeasureTheory.MemLp f p μ → MeasureTheory.eLpNorm f p μ ≠ ⊤
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) '' Set.Iic b = Set.Ici (a - b)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G} {x : E},
  AnalyticAt 𝕜 f (u x) → AnalyticAt 𝕜 (f ∘ ⇑u) x
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [inst_1 : SizeOf M]
  (toSubstructure : L.Substructure M) (isElementary' : toSubstructure.IsElementary),
  sizeOf { toSubstructure := toSubstructure, isElementary' := isElementary' } = 1 + sizeOf toSubstructure
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
/-- The isomorphism `restrictScalars α ⋙ toPresheaf R ≅ toPresheaf R'` for any
morphism of presheaves of rings `α : R ⟶ R'`.  -/
PresheafOfModules.restrictScalarsCompToPresheaf : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (α : R ⟶ R') →
        (PresheafOfModules.restrictScalars α).comp (PresheafOfModules.toPresheaf R) ≅ PresheafOfModules.toPresheaf R'
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumCongr_refl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (Homeomorph.refl X).sumCongr (Homeomorph.refl Y) = Homeomorph.refl (X ⊕ Y)
-- Mathlib.Topology.Maps.Strict.Group
/-- An additive group homomorphism is strict if and only if its
`QuotientAddGroup.kerLift` is an embedding.  -/
AddMonoidHom.isStrictMap_iff_isEmbedding_kerLift : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H], Topology.IsStrictMap ⇑f ↔ Topology.IsEmbedding ⇑(QuotientAddGroup.kerLift f)
-- Lean.Parser.Level
Lean.Parser.levelParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
integralClosure_idem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  integralClosure (↥(integralClosure R A)) A = ⊥
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- Analogue of `congr_fun h x`,
when `h : f = g` is an equality between morphisms in a concrete category.
 -/
CategoryTheory.ConcreteCategory.congr_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  {f g : X ⟶ Y},
  f = g →
    ∀ (x : CategoryTheory.ToType X),
      (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.GroupTheory.OrderOfElement
isOfFinAddOrder_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} {n : ℕ}, IsOfFinAddOrder (n • a) ↔ IsOfFinAddOrder a ∨ n = 0
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_le_log_two : ∀ {p : ℝ}, Real.binEntropy p ≤ Real.log 2
-- Mathlib.Tactic.MoveAdd
/-- `move_oper op [a]` repeatedly moves `a` to the far right hand side in applications of `op`.
Here the constant `op` refers to a binary associative commutative operation, and `a` is any term
(potentially with underscores).

If `a` contains underscores, they are filled in by unification with the first matching occurrence.
Subterms with different values for the underscores are not matched, unless you repeat `a`.

Currently, `move_oper` supports the operators `HAdd.hAdd` (`· + ·`), `HMul.hMul` (`· * ·`),
`And` (`· ∧ ·`), `Or` (`· ∨ ·`), `Max.max` and `Min.min`. To support more operations, add them to
`Mathlib.MoveAdd.moveOperSimpCtx`.

* `move_add [...]` uses addition as the operation: it abbreviates `move_oper HAdd.add [...]`.
* `move_mul [...]` uses multiplication as the operation: it abbreviates `move_oper HMul.mul [...]`.
* `move_oper op [← a]` moves the atoms matching `a` to the far left hand side instead of the right.
* `move_oper op [a, b, ← c, ← d, ...]` moves multiple atoms simultaneously, in the order indicated
  by the arguments: `c` will appear to the left of `d` and `a` will appear to the left of `b`.
 -/
Mathlib.MoveAdd.tacticMove_add_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Ext
LeftCancelMonoid.toMonoid_injective : ∀ {M : Type u}, Function.Injective (@LeftCancelMonoid.toMonoid M)
-- Init.Data.SInt.Lemmas
Int32.toInt_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (Int32.ofInt n).toInt = n
-- Init.Data.List.Lemmas
List.ext_getElem : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.length = l₂.length → (∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]) → l₁ = l₂
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instInhabitedSplitStatus.default : Lean.Meta.Grind.SplitStatus
-- Lean.Parser.Term
Lean.Parser.Term.stateRefT.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Order.Classes
Std.LawfulOrderMin.toMinEqOr : ∀ {α : Type u} {inst : Min α} {inst_1 : LE α} [self : Std.LawfulOrderMin α], Std.MinEqOr α
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_apply : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : DecidableEq κ] {k : κ} (f : ι k →₀ M)
  (i : (k : κ) × ι k), f.embSigma i = if h : i.fst = k then f (h ▸ i.snd) else 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the third point by one strictly further away on
the same ray.  -/
Sbtw.oangle_eq_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₃' : P}, Sbtw ℝ p₂ p₃ p₃' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃'
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂)[k]! = m₂.getD k m₁[k]!
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- Strongly locally contractible spaces are locally path-connected.  -/
instLocallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [StronglyLocallyContractibleSpace X], LocallyPathConnectedSpace X
-- Init.Data.String.Lemmas.Basic
String.push_ne_empty : ∀ {s : String} {c : Char}, s.push c ≠ ""
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_mul : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (a b : R),
  a ≠ 0 → b ≠ 0 → Differential.logDeriv (a * b) = Differential.logDeriv a + Differential.logDeriv b
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.irrefl`. -/
RelEmbedding.isIrrefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Irrefl s], Std.Irrefl r
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A finite group of prime order is simple.  -/
isSimpleAddGroup_of_prime_card : ∀ {α : Type u_1} [inst : AddGroup α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.card α = p → IsSimpleAddGroup α
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_toAddSubmonoid : ∀ {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.toAddSubmonoid = AddMonoidHom.mrange f
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule.mk.sizeOf_spec : ∀ (name : String) (uri : Lean.Lsp.DocumentUri) (data? : Option Lean.Json),
  sizeOf { name := name, uri := uri, data? := data? } = 1 + sizeOf name + sizeOf uri + sizeOf data?
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_castPred : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE ⋯) (SSet.stdSimplex.faceSingletonComplIso j).inv =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).inv (SSet.stdSimplex.δ (i.castPred ⋯))
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.mem_extremePoints : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X}
  [MeasureTheory.IsProbabilityMeasure μ],
  Ergodic f μ →
    μ ∈ Set.extremePoints ENNReal {ν | MeasureTheory.MeasurePreserving f ν ν ∧ MeasureTheory.IsProbabilityMeasure ν}
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, y - x)` as a `MeasurableEquiv` with inverse `(x, y) ↦ (x, y + x)`.  -/
MeasurableEquiv.shearSubRight : (G : Type u_1) →
  [inst : MeasurableSpace G] → [inst_1 : AddGroup G] → [MeasurableAdd₂ G] → [MeasurableNeg G] → G × G ≃ᵐ G × G
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.restrict_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) (s : Set α)
  (x : ↑s), (ContinuousMap.restrict s f) x = f ↑x
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_le_iff_le : ∀ {a b : ℤ} (ha₁ : Int64.minValue.toInt ≤ a) (ha₂ : a ≤ Int64.maxValue.toInt) (hb₁ : Int64.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int64.maxValue.toInt), Int64.ofIntLE a ha₁ ha₂ ≤ Int64.ofIntLE b hb₁ hb₂ ↔ a ≤ b
-- Mathlib.Topology.EMetricSpace.Basic
/-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y` and conversely.  -/
EMetric.isUniformEmbedding_iff' : ∀ {β : Type v} {γ : Type w} [inst : EMetricSpace γ] [inst_1 : PseudoEMetricSpace β] {f : γ → β},
  IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLastI.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → motive [a])
  (h_3 : (head b : α) → motive [head, b]) (h_4 : (head head_1 : α) → (l : List α) → motive (head :: head_1 :: l)),
  (match [] with
    | [] => h_1 ()
    | [a] => h_2 a
    | [head, b] => h_3 head b
    | head :: head_1 :: l => h_4 head head_1 l) =
    h_1 ()
-- Mathlib.Analysis.InnerProductSpace.NormPow
nnnorm_fderiv_norm_rpow_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : F → E},
  Differentiable ℝ f →
    ∀ {x : F} {p : NNReal}, 1 < p → ‖fderiv ℝ (fun x => ‖f x‖ ^ ↑p) x‖₊ ≤ p * ‖f x‖₊ ^ (↑p - 1) * ‖fderiv ℝ f x‖₊
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_add_not_infiniteNeg : ∀ {x y : ℝ*}, x.InfinitePos → ¬y.InfiniteNeg → (x + y).InfinitePos
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.snd_comp_prodComm : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂],
  LinearMap.snd R M₂ M ∘ₗ ↑(LinearEquiv.prodComm R M M₂) = LinearMap.fst R M M₂
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : SizeOf G] (toAddSubgroup : AddSubgroup G)
  (isNormal' : autoParam toAddSubgroup.Normal FiniteIndexNormalAddSubgroup.isNormal'._autoParam)
  (isFiniteIndex' : autoParam toAddSubgroup.FiniteIndex FiniteIndexNormalAddSubgroup.isFiniteIndex'._autoParam),
  sizeOf { toAddSubgroup := toAddSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
    1 + sizeOf toAddSubgroup + sizeOf isNormal' + sizeOf isFiniteIndex'
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesFiniteLimits F] (J : Type)
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.RingTheory.RootsOfUnity.Lemmas
/-- If `μ` is a primitive `n`th root of unity in `R`, then `∏(1≤k<n) (1-μ^k) = n`.
(Stated with `n+1` in place of `n` to avoid the condition `n ≠ 0`.)  -/
IsPrimitiveRoot.prod_one_sub_pow_eq_order : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n : ℕ} {μ : R},
  IsPrimitiveRoot μ (n + 1) → ∏ k ∈ Finset.range n, (1 - μ ^ (k + 1)) = ↑n + 1
-- Lean.Data.AssocList
Lean.AssocList.empty : {α : Type u} → {β : Type v} → Lean.AssocList α β
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ) (x_1 : L.BoundedFormula α x)
  (x_2 : ↥x_1.freeVarFinset → β),
  x_1.restrictFreeVar x_2 =
    match x, x_1, x_2 with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => FirstOrder.Language.BoundedFormula.falsum
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f =>
      FirstOrder.Language.BoundedFormula.equal (t₁.restrictVarLeft (f ∘ Set.inclusion ⋯))
        (t₂.restrictVarLeft (f ∘ Set.inclusion ⋯))
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f =>
      FirstOrder.Language.BoundedFormula.rel R fun i => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
    | _n, φ₁.imp φ₂, f => (φ₁.restrictFreeVar (f ∘ Set.inclusion ⋯)).imp (φ₂.restrictFreeVar (f ∘ Set.inclusion ⋯))
    | _n, φ.all, f => (φ.restrictFreeVar f).all
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_val : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [NeZero n] (i : ZMod n), ↑i.val = i.cast
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- A morphism of presheaves of modules consists of a family of linear maps which
satisfy the naturality condition.  -/
PresheafOfModules.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → PresheafOfModules R → Type (max u₁ v)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.adjoinZero.eq_1 : AddMonCat.adjoinZero =
  { obj := fun S => AddMonCat.of (WithZero ↑S),
    map := fun {X Y} f => AddMonCat.ofHom (WithZero.mapAddHom (AddSemigrp.Hom.hom f)),
    map_id := AddMonCat.adjoinZero._proof_1, map_comp := @AddMonCat.adjoinZero._proof_2 }
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (f : L.BoundedFormula α (x + 1)), f.all.toPrenex = f.toPrenex.all
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t t_1 : Std.DTreeMap.Raw α (fun x => β) cmp) (e_t : t = t_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ t), Std.DTreeMap.Raw.Const.get t a h = Std.DTreeMap.Raw.Const.get t_1 a_1 ⋯
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix.  -/
Matrix.fromBlocks_mul_fromRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R]
  [inst_1 : Fintype n₁] [inst_2 : Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R) (B₁₁ : Matrix m₁ n₁ R)
  (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R),
  Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
IsSelfAdjoint.commute_cfcₙHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : p a),
  IsSelfAdjoint a → Commute a b → ∀ (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜), Commute ((cfcₙHom ha) f) b
-- Mathlib.Data.Fin.Tuple.Basic
Fin.contractNth_apply_of_gt : ∀ {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
  ↑j < ↑k → j.contractNth op g k = g k.succ
-- Lean.Elab.Tactic.Simp
/-- Create the `Simp.Context` for the `simp`, `dsimp`, and `simp_all` tactics.
If `kind != SimpKind.simp`, the `discharge` option must be `none`

TODO: generate error message if non `rfl` theorems are provided as arguments to `dsimp`.

The argument `simpTheorems` defaults to `getSimpTheorems`,
but allows overriding with an arbitrary mechanism to choose
the simp theorems besides those specified in the syntax.
Note that if the syntax includes `simp only`, the `simpTheorems` argument is ignored.
 -/
Lean.Elab.Tactic.mkSimpContext : Lean.Syntax →
  Bool →
    optParam Lean.Elab.Tactic.SimpKind Lean.Elab.Tactic.SimpKind.simp →
      optParam Bool false →
        optParam (Lean.CoreM Lean.Meta.SimpTheorems) Lean.Meta.getSimpTheorems →
          Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- If `f` and `g` are surjective morphisms of algebras, then
the kernel of `Algebra.TensorProduct.map f g` is generated by the kernels of `f` and `g`  -/
Algebra.TensorProduct.map_ker : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_6}
  {B : Type u_7} {C : Type u_8} {D : Type u_9} [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Ring C] [inst_6 : Ring D]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] [inst_10 : Algebra R D] [inst_11 : Algebra S A]
  [inst_12 : Algebra S B] [inst_13 : IsScalarTower R S A] [inst_14 : IsScalarTower R S B] (f : A →ₐ[S] B)
  (g : C →ₐ[R] D),
  Function.Surjective ⇑f →
    Function.Surjective ⇑g →
      RingHom.ker (Algebra.TensorProduct.map f g) =
        Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔
          Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
-- Init.Tactics
/-- The common arguments of `simp_all?` and `simp_all?!`.  -/
Lean.Parser.Tactic.simpAllTraceArgsRest : Lean.ParserDescr
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_uIcc_of_monotoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  ContinuousOn f (Set.uIcc a b) → MonotoneOn f (Set.uIcc a b) → f '' Set.uIcc a b = Set.uIcc (f a) (f b)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iSup_of_antitone : ∀ {Ω : Type u_1} {ι : Type u_2} {m' m₁ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : SemilatticeInf ι]
  {m : ι → MeasurableSpace Ω},
  (∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ) →
    (∀ (i : ι), m i ≤ mΩ) → m₁ ≤ mΩ → Antitone m → ProbabilityTheory.CondIndep m' (⨆ i, m i) m₁ hm' μ
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f f_1 : X ⟶ R.cocomplex.X n) (e_f : f = f_1) (m m_1 : ℕ) (e_m : m = m_1) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0), R.extMk f m hm hf = R.extMk f_1 m_1 ⋯ ⋯
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.ceil_exp_one_eq_three : ⌈Real.exp 1⌉ = 3