mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₂.getKey k ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.add_iff_left : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : AddCommGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] {f g : α → G}, Measurable f → (Measurable (g + f) ↔ Measurable g)
-- Mathlib.Topology.MetricSpace.Similarity
/-- A similarity scales extended distance. Forward direction of `similar_iff_exists_edist_eq`.  -/
Similar.exists_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
-- Mathlib.Computability.Language
instFintypeSymbol : {T : Type u_4} → {N : Type u_5} → [Fintype T] → [Fintype N] → Fintype (Symbol T N)
-- Init.Data.List.Perm
List.Perm.mem_iff : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.Perm l₂ → (a ∈ l₁ ↔ a ∈ l₂)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.zero_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Zero A] (i : m) (j : n), 0 i j = 0
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.var.sizeOf_spec : ∀ (id : Lean.IR.VarId), sizeOf (Lean.IR.Arg.var id) = 1 + sizeOf id
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.map_mem : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (self : 𝒜 →+*ᵍ ℬ) {i : ι} {x : A},
  x ∈ 𝒜 i → ↑self x ∈ ℬ i
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_baseSet_at : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (self : FiberBundleCore ι B F) (x : B), x ∈ self.baseSet (self.indexAt x)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.mk : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] →
                [inst_5 : Module R E₁] →
                  [inst_6 : Module R E₂] → (toLinearMap : E₁ →ₗ[R] E₂) → Monotone toLinearMap.toFun → E₁ →ₚ[R] E₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_union_of_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF),
  (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₁ = true → Std.DTreeMap.Internal.Impl.contains a m₂ = false) →
    (m₁.union m₂ ⋯ ⋯).size = m₁.size + m₂.size
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.abstractGroundMismatches?.goCore : Lean.Expr → Lean.Expr → Lean.Meta.Grind.AbstractM✝ Lean.Expr
-- Mathlib.Data.Stream.Init
Stream'.cycle_eq : ∀ {α : Type u} (l : List α) (h : l ≠ []), Stream'.cycle l h = l ++ₛ Stream'.cycle l h
-- Mathlib.MeasureTheory.Integral.Average
/-- If the average of a function `f` along a sequence of sets `aₙ` converges to `c` (more precisely,
we require that `⨍ y in a i, ‖f y - c‖ ∂μ` tends to `0`), then the integral of `gₙ • f` also tends
to `c` if `gₙ` is supported in `aₙ`, has integral converging to one and supremum at most `K / μ aₙ`.
 -/
MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} [CompleteSpace E] {ι : Type u_4} {a : ι → Set α} {l : Filter ι} {f : α → E} {c : E}
  {g : ι → α → ℝ} (K : ℝ),
  Filter.Tendsto (fun i => ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (nhds 0) →
    (∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn f (a i) μ) →
      Filter.Tendsto (fun i => ∫ (y : α), g i y ∂μ) l (nhds 1) →
        (∀ᶠ (i : ι) in l, Function.support (g i) ⊆ a i) →
          (∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)) →
            Filter.Tendsto (fun i => ∫ (y : α), g i y • f y ∂μ) l (nhds c)
-- Mathlib.Data.Set.Function
Set.surjOn_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β}, Set.SurjOn f s {b} ↔ b ∈ f '' s
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumMap_isExpansionOn : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language}
  {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (M : Type u_1) [inst : L.Structure M] [inst_1 : L'.Structure M]
  [inst_2 : L₁.Structure M] [inst_3 : L₂.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M],
  (ϕ.sumMap ψ).IsExpansionOn M
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A class of morphisms `W` has the two-out-of-three property if whenever two out
of three maps in `f`, `g`, `f ≫ g` are in `W`, then the third map is also in `W`.  -/
CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.inv_smul_integral_comp_div_sub : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
-- Mathlib.Combinatorics.Configuration
/-- If a nondegenerate configuration has a unique line through any two points, then `|P| ≤ |L|`.  -/
Configuration.HasLines.card_le : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.HasLines P L] [inst : Fintype P]
  [inst_1 : Fintype L], Fintype.card P ≤ Fintype.card L
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Presieve.isSheafFor_ofArrows_comp_iff : ∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X : C}
  {ι : Type u_2} {Y Z : ι → C} (g : (i : ι) → Z i ⟶ X) (e : (i : ι) → Y i ≅ Z i),
  CategoryTheory.Presieve.IsSheafFor F
      (CategoryTheory.Presieve.ofArrows Y fun i => CategoryTheory.CategoryStruct.comp (e i).hom (g i)) ↔
    CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Z g)
-- Mathlib.Data.Seq.Computation
Computation.promises_congr : ∀ {α : Type u} {c₁ c₂ : Computation α}, c₁.Equiv c₂ → ∀ (a : α), c₁.Promises a ↔ c₂.Promises a
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
/-- If `data : SpectralSequenceDataCore ι c r₀` is such that
`data.HasFirstPageComputation` holds, this is an isomorphism which
allows to "compute" the objects on the `r₀`th page of the spectral sequence
obtained from a spectral object `X` indexed by `ι` using data as objects
of the form `X.H`. See also `spectralSequence_first_page_d_eq` for the relation
between the differentials of the first page of the spectral sequence and `X.δ`.  -/
CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{u_4, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    [data.HasFirstPageComputation] →
                      [inst_4 : X.HasSpectralSequence data] →
                        (pq : κ) →
                          (i₁ i₂ : ι) →
                            (hi₁ : i₁ = data.i₁ pq) →
                              (hi₂ : i₂ = data.i₂ pq) →
                                (n : ℤ) →
                                  n = data.deg pq →
                                    (((X.spectralSequence data).page r₀ ⋯).X pq ≅
                                      (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X j ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f i))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        h)
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.div : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f g : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f / g) μ
-- Mathlib.Order.Cover
Prod.swap_covBy_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β}, x.swap ⋖ y.swap ↔ x ⋖ y
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- Conditional expectation of the indicator of a set, as a function in L1. Its value for sets
which are not both measurable and of finite measure is not used: we set it to 0.  -/
MeasureTheory.condExpIndL1 : {α : Type u_1} →
  {G : Type u_4} →
    [inst : NormedAddCommGroup G] →
      [NormedSpace ℝ G] →
        {m m0 : MeasurableSpace α} →
          (hm : m ≤ m0) →
            (μ : MeasureTheory.Measure α) →
              Set α → [MeasureTheory.SigmaFinite (μ.trim hm)] → G → ↥(MeasureTheory.Lp G 1 μ)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded.  -/
csInf_eq_csInf_of_forall_exists_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s t : Set α},
  (∀ x ∈ s, ∃ y ∈ t, y ≤ x) → (∀ y ∈ t, ∃ x ∈ s, x ≤ y) → sInf s = sInf t
-- Std.Data.DTreeMap.Basic
/-- Transforms a list of keys into a tree map.  -/
Std.DTreeMap.Const.unitOfList : {α : Type u} →
  List α →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Const.unitOfList._auto_1) → Std.DTreeMap α (fun x => Unit) cmp
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero ι] [inst_2 : Semiring M],
  AddMonoidAlgebra.toDirectSum 1 = 1
-- Mathlib.Algebra.Ring.Int.Parity
Int.ediv_two_mul_two_add_one_of_odd : ∀ {n : ℤ}, Odd n → n / 2 * 2 + 1 = n
-- Mathlib.Data.Set.Basic
Set.empty_def : ∀ {α : Type u}, ∅ = {_x | False}
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The tautological cofan with point `free I : SheafOfModules R`.  -/
SheafOfModules.freeCofan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] →
            (I : Type u) → CategoryTheory.Limits.Cofan fun x => SheafOfModules.unit R
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.sectionCotangent.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  P.sectionCotangent =
    ↑P.cotangentEquiv.symm ∘ₗ
      ↑(Finsupp.linearEquivFunOnFinite S S σ) ∘ₗ Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.sPolynomial_mem_ideal : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [inst : CommRing R] {I : Ideal (MvPolynomial σ R)}
  {p q : MvPolynomial σ R}, p ∈ I → q ∈ I → m.sPolynomial p q ∈ I
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The canonical map `Proj A |_ D₊(f) ⟶ Spec (A_f)₀`.
This is an isomorphism when `f` is homogeneous of positive degree. See `basicOpenIsoSpec` below.  -/
AlgebraicGeometry.Proj.basicOpenToSpec : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                ↑(AlgebraicGeometry.Proj.basicOpen 𝒜 f) ⟶
                  AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_lt_agmSequences_snd_of_ne : ∀ {x y : NNReal}, x ≠ y → ∀ (n : ℕ), x.agm y < (x.agmSequences y n).2
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology], S.HasRightHomology
-- Std.Time.Date.Unit.Year
/-- Defines the different eras.
 -/
Std.Time.Year.Era : Type
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst.go.induct_unfolding : ∀ (k : ℤ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ), motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.num (k_1 + k))) →
    (∀ (k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (Lean.Grind.CommRing.Poly.addConst.go k p) →
          motive (Lean.Grind.CommRing.Poly.add k_1 m p)
            (Lean.Grind.CommRing.Poly.add k_1 m (Lean.Grind.CommRing.Poly.addConst.go k p))) →
      ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.addConst.go k a)
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.inverse_toFun : ∀ {M : Type u_1} [inst : Monoid M] {R : Type u_10} [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R]
  {S₁ : Type u_15} [inst_3 : Semiring S₁] [inst_4 : MulSemiringAction M S₁] (f : R →+*[M] S₁) (g : S₁ → R)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : S₁), (f.inverse g h₁ h₂) a = g a
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Gets an name based on `suggestion` that is unused in the local context.
Erases macro scopes.
If `pp.safeShadowing` is true, then the name is allowed to shadow a name in the local context
if the name does not appear in `body` or in the `avoid` set.
(The `avoid` set is assumed to be a subset of the names used by the local context.)

If `preserveName` is false, then returns the name, possibly with fresh macro scopes added.
If `suggestion` has macro scopes then the result does as well.
 -/
Lean.PrettyPrinter.Delaborator.getUnusedName : Lean.Name → Lean.Expr → optParam Bool false → optParam Lean.NameSet ∅ → Lean.PrettyPrinter.Delaborator.DelabM Lean.Name
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.prod_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray_ensureTermination : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] {it : Std.IterM m β}, it.ensureTermination.toArray = it.toArray
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
  (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  m₁ = Lean.Grind.CommRing.Mon.mult p m →
    m₂ = Lean.Grind.CommRing.Mon.unit →
      (match m₁, m₂ with
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
        | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
        | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) ≍
        h_3 p m
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_three : CartanMatrix.D 3 = !![2, -1, -1; -1, 2, 0; -1, 0, 2]
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.union!_equiv_congr_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁.union! m₂).Equiv (m₁.union! m₃)
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.toIsMulCommutative : ∀ {K : Type u_4} {L : Type u_5} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L} [self : IsAbelianGalois K L],
  IsMulCommutative Gal(L/K)
-- Mathlib.Data.EReal.Basic
EReal.toReal_eq_toReal : ∀ {x y : EReal}, x ≠ ⊤ → x ≠ ⊥ → y ≠ ⊤ → y ≠ ⊥ → (x.toReal = y.toReal ↔ x = y)
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.eq_smul_of_absolutelyContinuous : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  Ergodic f μ → MeasureTheory.MeasurePreserving f ν ν → ν.AbsolutelyContinuous μ → ∃ c, ν = c • μ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.cases.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (cases : Lean.Compiler.LCNF.Cases pu),
  sizeOf (Lean.Compiler.LCNF.Code.cases cases) = 1 + sizeOf cases
-- Mathlib.Data.Complex.Basic
Complex.re_nnqsmul : ∀ (q : ℚ≥0) (z : ℂ), (q • z).re = q • z.re
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- Given an isomorphism `α : Y ≅ Y₁` in C, the enriched composition map
`eComp V X Y Z : (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z)` factors through the `V`
object `(X ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z)` via the map defined by whiskering in the
middle with `α.hom` and `α.inv`.  -/
CategoryTheory.eHom_whisker_cancel : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C}
  (α : Y ≅ Y₁),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.hom) (Y ⟶[V] Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y₁) (CategoryTheory.eHomWhiskerRight V α.inv Z))
        (CategoryTheory.eComp V X Y₁ Z)) =
    CategoryTheory.eComp V X Y Z
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.mk.inj : ∀ {lhs rhs : Lean.Expr} {rlhs rrhs : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation}
  {ofSemiring? : Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr)}
  {lhs_1 rhs_1 : Lean.Expr} {rlhs_1 rrhs_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {d_1 : Lean.Meta.Grind.Arith.CommRing.PolyDerivation}
  {ofSemiring?_1 : Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr)},
  { lhs := lhs, rhs := rhs, rlhs := rlhs, rrhs := rrhs, d := d, ofSemiring? := ofSemiring? } =
      { lhs := lhs_1, rhs := rhs_1, rlhs := rlhs_1, rrhs := rrhs_1, d := d_1, ofSemiring? := ofSemiring?_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ rlhs = rlhs_1 ∧ rrhs = rrhs_1 ∧ d = d_1 ∧ ofSemiring? = ofSemiring?_1
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`  -/
CompletelyDistribLattice.le_himp_iff : ∀ {α : Type u} [self : CompletelyDistribLattice α] (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_prime_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)], orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Eta-expanded form of `MeasureTheory.Integrable.smul` -/
MeasureTheory.Integrable.fun_smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedAddCommGroup 𝕜] [inst_2 : SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun i => c • f i) μ
-- Mathlib.Data.Subtype
Subtype.coe_eq_of_eq_mk : ∀ {α : Sort u_1} {p : α → Prop} {a : { a // p a }} {b : α} (h : ↑a = b), a = ⟨b, ⋯⟩
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_pi_single' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (a : ι) (x : M) (s : Finset ι),
  ∑ a' ∈ s, Pi.single a x a' = if a ∈ s then x else 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (n : ℕ), (I ^ n).ideal = I.ideal ^ n
-- Mathlib.Algebra.Group.Action.TransferInstance
Equiv.mulAction.eq_1 : ∀ (M : Type u_1) {α : Type u_4} {β : Type u_5} [inst : Monoid M] (e : α ≃ β) [inst_1 : MulAction M β],
  Equiv.mulAction M e = { toSMul := Equiv.smul M e, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasSplitMultiplicativeReduction.splitMultiplicativeReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasSplitMultiplicativeReduction R W],
  (Polynomial.map (algebraMap R (IsLocalRing.ResidueField R))
      (Polynomial.C (WeierstrassCurve.integralModel R W).c₄ * Polynomial.X ^ 2 +
          Polynomial.C ((WeierstrassCurve.integralModel R W).a₁ * (WeierstrassCurve.integralModel R W).c₄) *
            Polynomial.X -
        Polynomial.C
          (54 * (WeierstrassCurve.integralModel R W).b₆ -
              3 * (WeierstrassCurve.integralModel R W).b₂ * (WeierstrassCurve.integralModel R W).b₄ +
            (WeierstrassCurve.integralModel R W).a₂ * (WeierstrassCurve.integralModel R W).c₄))).Splits
-- Mathlib.Order.Filter.IsBounded
Monotone.frequently_le_map_of_frequently_le : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Monotone f → ∀ {l : R}, (∃ᶠ (x : R) in F, x ≤ l) → ∃ᶠ (x' : S) in Filter.map f F, x' ≤ f l
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.replicate.match_1.eq_2 : ∀ {w : ℕ} (motive : ℕ → BitVec w → Sort u_1) (n : ℕ) (x : BitVec w) (h_1 : (x : BitVec w) → motive 0 x)
  (h_2 : (n : ℕ) → (x : BitVec w) → motive n.succ x),
  (match n.succ, x with
    | 0, x => h_1 x
    | n.succ, x => h_2 n x) =
    h_2 n x