mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.addSubgroupOf K = ⊤ ↔ K ≤ H
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.IccInclusionLeft.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] {a b c : α} [inst_2 : Fact (b ≤ c)],
  ContinuousMap.IccInclusionLeft = ContinuousMap.inclusion ⋯
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.smul_add : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (z : OreLocalization S R) (x y : OreLocalization S X),
  z • (x + y) = z • x + z • y
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.one_sub_le_m_div_m_add_one_sq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      1 - ε ^ 5 / 50 ≤
        (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) /
            (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)) ^
          2
-- Mathlib.Data.EReal.Operations
EReal.add_ne_top_iff_ne_top₂ : ∀ {x y : EReal}, x ≠ ⊥ → y ≠ ⊥ → (x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤)
-- Init.Data.String.ToSlice
String.instToSlice : String.ToSlice String
-- Lean.Parser.Syntax
Lean.Parser.Syntax.unary : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- the components cover `S`  -/
AlgebraicGeometry.Scheme.AffineCover.covers : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (self : AlgebraicGeometry.Scheme.AffineCover P S) (x : ↥S), x ∈ Set.range ⇑(self.f (self.idx x))
-- Mathlib.Order.OrderIsoNat
Nat.coe_orderEmbeddingOfSet : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s],
  ⇑(Nat.orderEmbeddingOfSet s) = Subtype.val ∘ Nat.Subtype.ofNat s
-- Mathlib.RingTheory.Etale.Descent
RingHom.Smooth.codescendsAlong_faithfullyFlat : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth) fun {R S} [CommRing R] [CommRing S] =>
  RingHom.FaithfullyFlat
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.coe_sInf : ∀ {M : Type u_1} [inst : Add M] (S : Set (AddSubsemigroup M)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.RingTheory.Congruence.Hom
RingCon.liftₐ_mk : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ RingCon.ker f.toRingHom)
  (x : M), (c.liftₐ f H) ↑x = f x
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.coe_id : ∀ (A : Type u_2) [inst : Monoid A] [inst_1 : Star A], ⇑(StarMonoidHom.id A) = id
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.mk.injEq : ∀ (expr : Lean.Expr) (xName? hName? : Option Lean.Name) (expr_1 : Lean.Expr) (xName?_1 hName?_1 : Option Lean.Name),
  ({ expr := expr, xName? := xName?, hName? := hName? } = { expr := expr_1, xName? := xName?_1, hName? := hName?_1 }) =
    (expr = expr_1 ∧ xName? = xName?_1 ∧ hName? = hName?_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅} {fallback : α}, t.getKeyD (t.maxKey he) fallback = t.maxKey he
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.instCoeSortType : CoeSort TwoP (Type u_3)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ →
      ∀ (f : α → E), MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂ν
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
_private.Mathlib.Combinatorics.SimpleGraph.Acyclic.0.SimpleGraph.Walk.exists_mem_contains_edges_of_directed : ∀ {V : Type u_1} (Hs : Set (SimpleGraph V)),
  Hs.Nonempty →
    DirectedOn (fun x1 x2 => x1 ≤ x2) Hs → ∀ {u v : V} (p : (sSup Hs).Walk u v), ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km fallback : α},
        Std.Internal.List.minKeyD l fallback = km ↔
          Std.Internal.List.containsKey km l = true ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare km k).isLE = true
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendsScalars_map_leftUnitor_inv_one_tmul : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M : ModuleCat R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom
        ((ModuleCat.extendScalars f).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv))
      (1 ⊗ₜ[R] m) =
    1 ⊗ₜ[R] (1 ⊗ₜ[R] m)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.mk.sizeOf_spec : ∀ (ref modifiers : Lean.Syntax) (fieldId : Lean.Name) (type : Lean.Term)
  (matchAlts : Lean.TSyntax `Lean.Parser.Term.matchAlts),
  sizeOf { ref := ref, modifiers := modifiers, fieldId := fieldId, type := type, matchAlts := matchAlts } =
    1 + sizeOf ref + sizeOf modifiers + sizeOf fieldId + sizeOf type + sizeOf matchAlts
-- Mathlib.RingTheory.Spectrum.Prime.TensorProduct
/-- The canonical map from `Spec(S ⊗[R] T)` to the Cartesian product `Spec S × Spec T`.  -/
PrimeSpectrum.tensorProductTo : (R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] → PrimeSpectrum (TensorProduct R S T) → PrimeSpectrum S × PrimeSpectrum T
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit.match_1.splitter : {n : ℕ} →
  (motive : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1) →
    (x : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      ((l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → (b : Bool) → motive (l, b)) → motive x
-- Mathlib.Topology.Constructions.SumProd
isOpenMap_sum : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X ⊕ Y → Z},
  IsOpenMap f ↔ (IsOpenMap fun a => f (Sum.inl a)) ∧ IsOpenMap fun b => f (Sum.inr b)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.epi_L₁_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Epi self.L₁.g
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The short complex `H^{n-1}(f₃) ⟶ Z^n(f₁, f₂) ⟶ E^n(f₁, f₂, f₃)` identifies
to the cokernel sequence of the definition of the homology of the short
complex `shortComplex` as a cokernel of `ShortComplex.toCycles`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ :
                          autoParam (n₀ + 1 = n₁)
                            CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_1) →
                        (hn₂ :
                            autoParam (n₁ + 1 = n₂)
                              CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3) →
                          X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≅
                            { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁,
                              X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles,
                              X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology,
                              f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles,
                              g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyπ, zero := ⋯ }
-- Mathlib.Analysis.Analytic.Composition
/-- Variant of `id_comp` in which the zero coefficient is given by an equality hypothesis instead
of a definitional equality. Useful for rewriting or simplifying out in some situations.  -/
FormalMultilinearSeries.id_comp' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (x : F) (v0 : Fin 0 → E),
  x = (p 0) v0 → (FormalMultilinearSeries.id 𝕜 F x).comp p = p
-- Mathlib.Tactic.CategoryTheory.ToApp
_private.Mathlib.Tactic.CategoryTheory.ToApp.0.Mathlib.Tactic.CategoryTheory.ToApp.toCatExpr.apprec.eq_def : ∀ (args : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) (B inst : Lean.Expr) (i : ℕ) (e : Lean.Expr),
  Mathlib.Tactic.CategoryTheory.ToApp.toCatExpr.apprec✝ args binderInfos B inst i e =
    if h : i < args.size then
      have arg := args[i];
      have bi := binderInfos[i]!;
      do
      let e' ← Mathlib.Tactic.CategoryTheory.ToApp.toCatExpr.apprec✝ args binderInfos B inst (i + 1) e
      if (arg != B && arg != inst) = true then Lean.Meta.mkLambdaFVars #[arg] e' false true false true bi else pure e'
    else pure e
-- Init.Data.String.Lemmas.Basic
String.Pos.nextn_endPos : ∀ {n : ℕ} {s : String}, s.endPos.nextn n = s.endPos
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ) {Z : C}
  (h : G.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯) h) =
    h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_eq_zero_iff_cos_eq : ∀ {z : ℂ}, Complex.sin z = 0 ↔ Complex.cos z = 1 ∨ Complex.cos z = -1
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?.eq_1 : ∀ {α β : Type w} {γ : Type x} {m : Type x → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] (it : Std.Iter β) (f : β → m (Option γ)),
  it.findSomeM? f =
    forIn it none fun x x_1 => do
      let __do_lift ← f x
      match __do_lift with
        | none => pure (ForInStep.yield none)
        | some fx => pure (ForInStep.done (some fx))
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Ico_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Ico ↑b ↑a = Finset.map Function.Embedding.some (Finset.Ico b a)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.whiskerRight_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B),
  (CategoryTheory.Oplax.LaxTrans.whiskerRight Γ ι).as.app a =
    CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
-- Init.Data.Int.DivMod.Lemmas
Int.instNeZeroOfNatOfNat : ∀ {n : ℕ} [NeZero n], NeZero (OfNat.ofNat n)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.isCompact_closure_image_of_bounded : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂},
  IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsBounded S → IsCompact (closure (⇑f '' S))
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le : ∀ {𝕜 : 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] {n : ℕ} (c : OrderedFinpartition n)
  (f : F [×c.length]→L[𝕜] G), ‖(OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c) f‖ ≤ ‖f‖
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.instIsOrderedRingLexOfNoZeroDivisors : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : Ring R]
  [inst_3 : AddCommMonoid Γ] [inst_4 : IsOrderedCancelAddMonoid Γ] [IsOrderedRing R] [NoZeroDivisors R],
  IsOrderedRing (Lex (HahnSeries Γ R))
-- Mathlib.RingTheory.Adjoin.Field
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
then `[E[L] : E] ≤ [L : F]`.  -/
Subalgebra.adjoin_rank_le : ∀ {F : Type u_5} (E : Type u_6) {K : Type u_7} [inst : CommSemiring F] [StrongRankCondition F] [inst_2 : CommSemiring E]
  [StrongRankCondition E] [inst_4 : Semiring K] [inst_5 : SMul F E] [inst_6 : Algebra E K] [inst_7 : Algebra F K]
  [IsScalarTower F E K] (L : Subalgebra F K) [Module.Free F ↥L], Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L
-- Mathlib.Data.Finset.NatAntidiagonal
/-- The set `antidiagonal n` is equivalent to `Fin (n+1)`, via the first projection.  -/
Finset.Nat.antidiagonalEquivFin : (n : ℕ) → ↥(Finset.HasAntidiagonal.antidiagonal n) ≃ Fin (n + 1)
-- Lean.DocString.Parser
Lean.Doc.Parser.InlineCtxt.mk.injEq : ∀ (allowNewlines : Bool) (minIndent : ℕ) (boldDepth emphDepth : Option ℕ) (inLink allowNewlines_1 : Bool)
  (minIndent_1 : ℕ) (boldDepth_1 emphDepth_1 : Option ℕ) (inLink_1 : Bool),
  ({ allowNewlines := allowNewlines, minIndent := minIndent, boldDepth := boldDepth, emphDepth := emphDepth,
        inLink := inLink } =
      { allowNewlines := allowNewlines_1, minIndent := minIndent_1, boldDepth := boldDepth_1, emphDepth := emphDepth_1,
        inLink := inLink_1 }) =
    (allowNewlines = allowNewlines_1 ∧
      minIndent = minIndent_1 ∧ boldDepth = boldDepth_1 ∧ emphDepth = emphDepth_1 ∧ inLink = inLink_1)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.comp_reflectsLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.ReflectsLimit G H],
  CategoryTheory.Limits.ReflectsLimit (F.comp G) H
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.find?_char_eq_some_iff_splits : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  s.find? c = some pos ↔ ∃ t u, pos.Splits t (String.singleton c ++ u) ∧ c ∉ t.toList
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.mk.inj : ∀ {visited : Std.HashSet Lean.Meta.Sym.ExprPtr}
  {collectedThms : Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind)}
  {thms : Array Lean.Meta.Grind.EMatchTheorem} {visited_1 : Std.HashSet Lean.Meta.Sym.ExprPtr}
  {collectedThms_1 : Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind)}
  {thms_1 : Array Lean.Meta.Grind.EMatchTheorem},
  { visited := visited, collectedThms := collectedThms, thms := thms } =
      { visited := visited_1, collectedThms := collectedThms_1, thms := thms_1 } →
    visited = visited_1 ∧ collectedThms = collectedThms_1 ∧ thms = thms_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_zsmul : ∀ (z : ℤ) (x : ℝ), ↑(z • x) = z • ↑x
-- Init.PropLemmas
not_and' : ∀ {a b : Prop}, ¬(a ∧ b) ↔ b → ¬a
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.natCast : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (n : ℕ), (↑n).IsSymmetric
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.underlyingIso_inv_top_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso (CategoryTheory.CategoryStruct.id B)).inv
      ⊤.arrow =
    CategoryTheory.CategoryStruct.id B
-- Init.Data.Fin.Lemmas
Fin.mul_def : ∀ {n : ℕ} (a b : Fin n), a * b = ⟨↑a * ↑b % n, ⋯⟩
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- If `E / L / F` and `E / L' / F` are two field extension towers, `L ≃ₐ[F] L'` is an isomorphism
compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L(S)` and `L'(S)` are
equal as intermediate fields of `E / F`.  -/
IntermediateField.restrictScalars_adjoin_of_algEquiv : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type u_3}
  {L' : Type u_4} [inst_3 : Field L] [inst_4 : Field L'] [inst_5 : Algebra F L] [inst_6 : Algebra L E]
  [inst_7 : Algebra F L'] [inst_8 : Algebra L' E] [inst_9 : IsScalarTower F L E] [inst_10 : IsScalarTower F L' E]
  (i : L ≃ₐ[F] L'),
  ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i →
    ∀ (S : Set E),
      IntermediateField.restrictScalars F (IntermediateField.adjoin L S) =
        IntermediateField.restrictScalars F (IntermediateField.adjoin L' S)
-- Std.Do.PostCond
/-- Implication of postconditions.

This is defined pointwise, as the implication of the assertions about the return value and the
implications of each of the assertions about each potential exception.

While entailment of postconditions (`PostCond.entails`) is an ordinary proposition, implication of
postconditions is itself a postcondition.
 -/
Std.Do.PostCond.imp : {α : Type u_1} → {ps : Std.Do.PostShape} → Std.Do.PostCond α ps → Std.Do.PostCond α ps → Std.Do.PostCond α ps
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of the reverse direction of `Set.Iio_eq_empty_iff`. -/
IsMin.Iio_eq : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMin a → Set.Iio a = ∅
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_iff`.

---

Definition of `IsBigOWith`. We record it in a lemma as `IsBigOWith` is irreducible.  -/
Asymptotics.IsBigOWith.bound : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, Asymptotics.IsBigOWith c l f g → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
inv_mul_lt_of_lt_mul₀ : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b c : α}, a < b * c → b⁻¹ * a < c
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a b : α},
  cmp a b = Ordering.eq → t[a]? = t[b]?
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.of : {C : Type u} → C → CategoryTheory.WithInitial C
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.trans_tendsto_nhds : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) {F' : Type u_7} [inst : Norm E] [inst_1 : Norm F]
  [inst_2 : SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : One F] [NormOneClass F],
  f =O[l] g' → ∀ {y : F'}, Filter.Tendsto g' l (nhds y) → f =O[l] fun _x => 1
-- Std.Data.ExtTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtTreeMap.getKey! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α → α
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findRevM?.eq_1 : ∀ {α : Type} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Array α),
  Array.findRevM? p as =
    Array.findSomeRevM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
-- Lean.Elab.Declaration
Lean.Elab.Command.expandMutualNamespace : Lean.Macro
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (e : α) (I : Set α),
  M.fundCircuit e I = insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instIsTorsionFree : ∀ {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [Module.IsTorsionFree S M₂], Module.IsTorsionFree S (MultilinearMap R M₁ M₂)
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- **Alias** of `IsNonarchimedean.apply_natCast_le_one`. -/
IsNonarchimedean.apply_natCast_le_one_of_isNonarchimedean : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3}
  [inst_2 : AddMonoidWithOne α] [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [OneHomClass F α R]
  {f : F}, IsNonarchimedean ⇑f → ∀ {n : ℕ}, f ↑n ≤ 1
-- Lean.LibrarySuggestions.Basic
/-- Generate library suggestions for the given metavariable, using the currently registered library suggestions engine.  -/
Lean.LibrarySuggestions.select : Lean.MVarId → optParam Lean.LibrarySuggestions.Config { } → Lean.MetaM (Array Lean.LibrarySuggestions.Suggestion)
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.merge.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Sort u_2) →
    (x x_1 : Batteries.PairingHeapImp.Heap α) →
      (Unit → motive Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil) →
        ((a₂ : α) →
            (c₂ sibling : Batteries.PairingHeapImp.Heap α) →
              motive Batteries.PairingHeapImp.Heap.nil (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling)) →
          ((a₁ : α) →
              (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
                motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling) Batteries.PairingHeapImp.Heap.nil) →
            ((a₁ : α) →
                (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
                  (a₂ : α) →
                    (c₂ sibling_1 : Batteries.PairingHeapImp.Heap α) →
                      motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
                        (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1)) →
              motive x x_1
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The product of measurable functions is measurable.  -/
Measurable.tprod' : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [inst_4 : MeasurableSpace E] [BorelSpace E]
  [MeasurableMul₂ E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E},
  (∀ (i : ι), Measurable (f i)) → Measurable (∏'[L] (i : ι), f i)