mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Prelude
/-- The substitution principle for equality. If `a = b ` and `P a` holds,
then `P b` also holds. We conventionally use the name `motive` for `P` here,
so that you can specify it explicitly using e.g.
`Eq.subst (motive := fun x => x < 5)` if it is not otherwise inferred correctly.

This theorem is the underlying mechanism behind the `rw` tactic, which is
essentially a fancy algorithm for finding good `motive` arguments to usefully
apply this theorem to replace occurrences of `a` with `b` in the goal or
hypotheses.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
Eq.subst : ∀ {α : Sort u} {motive : α → Prop} {a b : α}, a = b → motive a → motive b
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₁ → (m₁ ∪ m₂)[k]! = m₂[k]!
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.PrefixTable.step.match_1.splitter : {α : Type u_1} →
  (t : Array.PrefixTable α) →
    (motive : (k : ℕ) → k < t.size + 1 → Sort u_2) →
      (k : ℕ) →
        (hk : k < t.size + 1) →
          ((hk : 0 < t.size + 1) → motive 0 hk) → ((k : ℕ) → (hk : k + 1 < t.size + 1) → motive k.succ hk) → motive k hk
-- Mathlib.Algebra.Star.Subalgebra
/-- Forgetting that a \*-subalgebra is closed under \*.
 -/
StarSubalgebra.toSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → StarSubalgebra R A → Subalgebra R A
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- The identity linear isometry.  -/
LinearIsometry.id : {R : Type u_1} →
  {E : Type u_5} → [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → E →ₗᵢ[R] E
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State : Type
-- Mathlib.Analysis.MeanInequalities
NNReal.geom_mean_le_arith_mean3_weighted : ∀ (w₁ w₂ w₃ p₁ p₂ p₃ : NNReal), w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.polynomialModule : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module (Polynomial R) (PolynomialModule R M)
-- Std.Tactic.BVDecide.Syntax
/-- Auxiliary attribute for builtin `bv_normalize` simprocs.
 -/
Lean.Parser.bvNormalizeProcBuiltinAttr : Lean.ParserDescr
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.id : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁},
  (CategoryTheory.LocalizerMorphism.id W₁).IsLocalizedEquivalence
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `(∅ ⟶ B) □ g` lifts against `X ⟶ ⋆` if and only if `g` lifts against `(B ⟹ X) ⟶ ⋆`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {g : K ⟶ L} (i : CategoryTheory.Limits.IsInitial A)
  (t : CategoryTheory.Limits.IsTerminal Y),
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk (i.to B) □ CategoryTheory.Arrow.mk g).hom (t.from X) ↔
    CategoryTheory.HasLiftingProperty g (t.from (B ⟹ X))
-- Mathlib.Topology.MetricSpace.Pseudo.Real
Real.dist_le_of_mem_Icc : ∀ {x y x' y' : ℝ}, x ∈ Set.Icc x' y' → y ∈ Set.Icc x' y' → dist x y ≤ y' - x'
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.map_matrix_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J K : Type}
  [inst_2 : Finite J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_4 : Finite K] {f g : J → C}
  {h : K → C} (m : (k : J) → f k ⟶ g k) (n : (j : J) → (k : K) → g j ⟶ h k) {Z : C} (h_1 : ⨁ h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix n) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j) (n j k)) h_1
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_one : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : One R], QuaternionAlgebra.imK 1 = 0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.inv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence],
  F.inv =
    { obj := fun X => F.objPreimage X,
      map := fun {X Y} f =>
        F.preimage
          (CategoryTheory.CategoryStruct.comp (F.objObjPreimageIso X).hom
            (CategoryTheory.CategoryStruct.comp f (F.objObjPreimageIso Y).inv)),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] {S : Set (TopologicalSpace.Compacts α)},
  IsCompact S → IsCompact (⋃ K ∈ S, ↑K)
-- Mathlib.Data.Fintype.Basic
/-- Embed `Fin n` into `Fin (n + 1)` by appending a new `Fin.last n` to the `univ`  -/
Fin.univ_castSuccEmb : ∀ (n : ℕ), Finset.univ = Finset.cons (Fin.last n) (Finset.map Fin.castSuccEmb Finset.univ) ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset β} {a : α},
  a +ᵥ s₁ ∪ s₂ = (a +ᵥ s₁) ∪ (a +ᵥ s₂)
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `ne_zero_of_lt`. -/
LT.lt.ne_zero : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], a < b → b ≠ 0
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_5.eq_1 : ∀ (motive : Option (List Lean.MVarId) → Sort u_1) (curr' : List Lean.MVarId)
  (h_1 : (curr' : List Lean.MVarId) → motive (some curr')) (h_2 : Unit → motive none),
  (match some curr' with
    | some curr' => h_1 curr'
    | none => h_2 ()) =
    h_1 curr'
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
  (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂), (γ.add γ').φH = γ.φH + γ'.φH
-- Mathlib.RingTheory.Derivation.DifferentialRing
Differential.ext : ∀ {R : Type u_1} {inst : CommRing R} {x y : Differential R}, Differential.deriv = Differential.deriv → x = y
-- Init.Data.List.Nat.Erase
List.eraseIdx_set_lt : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α}, j < i → (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap F E)
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.Limits.HasInitial C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor X =
    CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding
        (CategoryTheory.Arrow.mk
          (CategoryTheory.Limits.initial.to (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
        X ≪≫
      CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor X
-- Aesop.RuleTac.Basic
Aesop.RuleTacOutput.mk.injEq : ∀ (applications applications_1 : Array Aesop.RuleApplication),
  ({ applications := applications } = { applications := applications_1 }) = (applications = applications_1)
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
_private.Mathlib.RingTheory.WittVector.DiscreteValuationRing.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal X)
  (c : CategoryTheory.Limits.BinaryFan X Y), Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.snd
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEvalComp.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.Structural → m Lean.Expr) →
    (Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.NormalExpr → m Lean.Expr) →
      (Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → m Lean.Expr) →
        Mathlib.Tactic.BicategoryLike.MkEvalComp m
-- Mathlib.Data.Nat.Cast.Defs
one_add_one_eq_two : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 1 + 1 = 2
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- **Alias** of `summable_of_hasFiniteSupport`. -/
summable_of_finite_support : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.HasSupport], Function.HasFiniteSupport f → Summable f L
-- Mathlib.RingTheory.AdicCompletion.Noetherian
instIsAdicCompleteMaximalIdealOfIsArtinianRing : ∀ {A : Type u_3} [inst : CommRing A] [IsArtinianRing A] [inst_2 : IsLocalRing A],
  IsAdicComplete (IsLocalRing.maximalIdeal A) A
-- Batteries.Data.String.Lemmas
/-- The stop position of a valid substring is valid.  -/
Substring.Raw.Valid.stopValid : ∀ {s : Substring.Raw}, s.Valid → String.Pos.Raw.Valid s.str s.stopPos
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- **Alias** of `fderivWithin_fun_comp_of_eq`.

---

Eta-expanded form of `fderivWithin_comp_of_eq` -/
fderivWithin_comp_of_eq' : ∀ {𝕜 : 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} (x : E) {s : Set E} {g : F → G} {t : Set F}
  {y : F},
  DifferentiableWithinAt 𝕜 g t y →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          f x = y → fderivWithin 𝕜 (fun x => g (f x)) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.lift_comp_preservesLimitIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.Cone F),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.lift F t))
      (CategoryTheory.preservesLimitIso G F).hom =
    CategoryTheory.Limits.limit.lift (F.comp G) (G.mapCone t)
-- Std.Internal.Parsec.Basic
/-- Parser that always fails with the given error message.
 -/
Std.Internal.Parsec.fail : {α ι : Type} → String → Std.Internal.Parsec ι α
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `le_neg_add_iff_add_le`. -/
le_neg_add_of_add_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a + b ≤ c → b ≤ -a + c
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- A measure is Gaussian if its map by every continuous linear form is a real Gaussian measure.  -/
ProbabilityTheory.IsGaussian : {E : Type u_1} →
  [TopologicalSpace E] →
    [inst : AddCommMonoid E] → [Module ℝ E] → {mE : MeasurableSpace E} → MeasureTheory.Measure E → Prop
-- Mathlib.Algebra.Algebra.Hom
RingHom.equivIntAlgHom_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (RingHom.equivIntAlgHom R S) f = f.toIntAlgHom
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.star_left_conjugate_le_norm_smul : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  autoParam (IsSelfAdjoint b) CStarAlgebra.star_left_conjugate_le_norm_smul._auto_1 →
    star a * b * a ≤ ‖b‖ • (star a * a)
-- Mathlib.Data.Complex.Basic
Complex.inv_I : Complex.I⁻¹ = -Complex.I
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  ¬cmp k k' = Ordering.eq → (t.alter k f).contains k' = t.contains k'
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n), (-γ).rightUnshift n hn = -γ.rightUnshift n hn
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Pointwise inequality to control `x ^ k * f` in terms of `1 / (1 + x) ^ l` if one controls both
`f` (with a bound `C₁`) and `x ^ (k + l) * f` (with a bound `C₂`). This will be used to check
integrability of `x ^ k * f x` when `f` is a Schwartz function, and to control explicitly its
integral in terms of suitable seminorms of `f`.  -/
pow_mul_le_of_le_of_pow_mul_le : ∀ {C₁ C₂ : ℝ} {k l : ℕ} {x f : ℝ},
  0 ≤ x → 0 ≤ f → f ≤ C₁ → x ^ (k + l) * f ≤ C₂ → x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)
-- Aesop.Util.UnionFind
Aesop.UnionFind.merge : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → α → α → Aesop.UnionFind α → Aesop.UnionFind α
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.ascFactorialBinary.match_1.splitter : (motive : ℕ → Sort u_1) → (k : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive k
-- Init.Data.SInt.Bitwise
UInt16.toInt16_or : ∀ (a b : UInt16), (a ||| b).toInt16 = a.toInt16 ||| b.toInt16
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.isOpen_preimage_ofUpper : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsOpen (⇑Topology.WithUpper.ofUpper ⁻¹' s) ↔ TopologicalSpace.IsOpen s
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [LawfulMonad n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ}
  {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← (f b).run
          pure (g d c))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.mapWithPostcondition f it) ⦃Q⦄
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.mk.inj : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Jacobian R} {point : WeierstrassCurve.Jacobian.PointClass R}
  {nonsingular : W'.NonsingularLift point} {point_1 : WeierstrassCurve.Jacobian.PointClass R}
  {nonsingular_1 : W'.NonsingularLift point_1},
  { point := point, nonsingular := nonsingular } = { point := point_1, nonsingular := nonsingular_1 } → point = point_1
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.eq_comp_symm : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : M₂ → α) (g : M₁ → α), f = g ∘ ⇑e₁₂.symm ↔ f ∘ ⇑e₁₂ = g
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.mk.injEq : ∀ {σ : Type} (id : ℕ) (mkInitial : IO σ) (id_1 : ℕ) (mkInitial_1 : IO σ),
  ({ id := id, mkInitial := mkInitial } = { id := id_1, mkInitial := mkInitial_1 }) =
    (id = id_1 ∧ mkInitial = mkInitial_1)
-- Lean.Structure
Lean.instInhabitedStructureInfo : Inhabited Lean.StructureInfo
-- Mathlib.Algebra.Group.Ideal
/-- The semigroup ideal generated by `s` is `s ∪ Set.univ * s`.  -/
SemigroupIdeal.mem_closure' : ∀ {M : Type u_1} [inst : Semigroup M] {s : Set M} {x : M},
  x ∈ SemigroupIdeal.closure s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x
-- Mathlib.Data.Int.Bitwise
Int.shiftRight_natCast : ∀ (m n : ℕ), ↑m >>> ↑n = ↑(m >>> n)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algHom_surjective : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Surjective ⇑(SymmetricAlgebra.algHom R M)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.Limits.HasBiproductsOfShape J C]
  (F : J → C), CategoryTheory.Limits.HasBiproduct F
-- Mathlib.Topology.Homeomorph.Lemmas
/-- The topological space `Π i, Y i` can be split as a product by separating the indices in ι
depending on whether they satisfy a predicate p or not.  -/
Homeomorph.piEquivPiSubtypeProd : {ι : Type u_7} →
  (p : ι → Prop) →
    (Y : ι → Type u_8) →
      [inst : (i : ι) → TopologicalSpace (Y i)] →
        [DecidablePred p] → ((i : ι) → Y i) ≃ₜ ((i : { x // p x }) → Y ↑i) × ((i : { x // ¬p x }) → Y ↑i)
-- Mathlib.Logic.Equiv.Fintype
/-- Extend the domain of `e : Equiv.Perm α`, mapping it through `f : α ↪ β`.
Everything outside of `Set.range f` is kept fixed. Has poor computational performance,
due to exhaustive searching in constructed inverse due to using `Function.Embedding.toEquivRange`.
When a better `α ≃ Set.range f` is known, use `Equiv.Perm.viaSetRange`.
When `[Fintype α]` is not available, a noncomputable version is available as
`Equiv.Perm.viaEmbedding`.
 -/
Equiv.Perm.viaFintypeEmbedding : {α : Type u_1} → {β : Type u_2} → [Fintype α] → [DecidableEq β] → Equiv.Perm α → (α ↪ β) → Equiv.Perm β
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.dropEndWhile_eq_self_iff_or : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice},
  s.dropEndWhile pat = s ↔
    ¬String.Slice.Pattern.Model.RevMatchesAt pat s.endPos ∨
      String.Slice.Pattern.Model.IsLongestRevMatchAt pat s.endPos s.endPos
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_mk' : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂)
  (h : Continuous f.toFun), ⇑{ toLinearMap := f, cont := h } = ⇑f
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.ofSurjective_Ring : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Type w}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] (f : P →ₐ[R] S) (h : Function.Surjective ⇑f),
  (Algebra.Extension.ofSurjective f h).Ring = P
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_restrict : ∀ {α : Type u_1} (E R : Set α), (Matroid.loopyOn E).restrict R = Matroid.loopyOn R
-- Mathlib.Algebra.Order.Sub.Basic
/-- **Alias** of the reverse direction of `tsub_eq_zero_iff_le`. -/
tsub_eq_zero_of_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a ≤ b → a - b = 0
-- Mathlib.Topology.UniformSpace.Basic
tendsto_prod_uniformity_fst : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  Filter.Tendsto (fun p => (p.1.1, p.2.1)) (uniformity (α × β)) (uniformity α)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.aleph0_pos : 0 < Cardinal.aleph0
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix.congr_simp : ∀ {α : Sort u_1} {C : α → Sort u_2} [inst : ∀ (a : α), Nonempty (C a)] (R : α → α → Prop)
  (F F_1 : (a : α) → ((a' : α) → R a' a → C a') → C a),
  F = F_1 → ∀ (a : α), WellFounded.extrinsicFix R F a = WellFounded.extrinsicFix R F_1 a
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier : ∀ {R : Type u} [inst : Ring R], (CategoryTheory.forget (ModuleCat R)).ReflectsIsomorphisms
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote'.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α),
  Lean.Grind.CommRing.Mon.denote' ctx Lean.Grind.CommRing.Mon.unit = 1
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.coe_zeta_mul_coe_moebius : ∀ {R : Type u_1} [inst : Ring R], ↑ArithmeticFunction.zeta * ↑ArithmeticFunction.moebius = 1
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_eq_toNNReal_iff' : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ ⊤ → (x.toNNReal = y.toNNReal ↔ x = y)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φK =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).K
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.Model.mono : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T T' : L.Theory}, M ⊨ T' → T ⊆ T' → M ⊨ T
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_le_artanh_iff : ∀ {x y : ℝ}, x ∈ Set.Ioo (-1) 1 → y ∈ Set.Ioo (-1) 1 → (Real.artanh x ≤ Real.artanh y ↔ x ≤ y)