mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.whiskerLeft_def : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R) {N₁ N₂ : SemimoduleCat R} (f : N₁ ⟶ N₂),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f = SemimoduleCat.MonoidalCategory.whiskerLeft M f
-- Init.WF
Prod.rprod : {α : Type u} → {β : Type v} → WellFoundedRelation α → WellFoundedRelation β → WellFoundedRelation (α × β)
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddGrpCat.instBraidedCategory : CategoryTheory.BraidedCategory AddGrpCat
-- Lean.Elab.Do.Basic
/-- Register the given names as that of `mut` variables if the syntax token `mut` is present.  -/
Lean.Elab.Do.declareMutVars? : {α : Type} → Option Lean.Syntax → Array Lean.Ident → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Mathlib.Algebra.Category.BoolRing
BoolRing.hasForgetToBoolAlg : CategoryTheory.HasForget₂ BoolRing BoolAlg
-- Mathlib.Order.Irreducible
InfPrime.finset_inf_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : SemilatticeInf α] {a : α} [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α},
  InfPrime a → (s.inf f ≤ a ↔ ∃ i ∈ s, f i ≤ a)
-- Init.Data.Nat.Basic
Nat.lt_one_iff : ∀ {n : ℕ}, n < 1 ↔ n = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM f init t =
    Array.foldrM (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- Prove the equality between structural isomorphisms using the naturality of `normalize`.  -/
Mathlib.Tactic.BicategoryLike.MkEqOfNaturality : (Type → Type) → Type
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.ofAddSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (N : AddSubmonoid (M × M)) (H : Equivalence fun x y => (x, y) ∈ N),
  AddCon.ofAddSubmonoid N H = { r := fun x y => (x, y) ∈ N, iseqv := H, add' := ⋯ }
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_zero : ∀ {a : UInt32}, a <<< 0 = a
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.memSobolev_fun_zero : ∀ (E : Type u_1) (F : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)],
  TemperedDistribution.MemSobolev s p 0
-- Mathlib.Order.RelSeries
LTSeries.head_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p : LTSeries α) (f : α → β)
  (hf : StrictMono f), RelSeries.head (p.map f hf) = f (RelSeries.head p)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.coeff.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} (hs : IsLocalFrameOn I F n s u) (i : ι) (x : M),
  hs.coeff i x = if hx : x ∈ u then (hs.toBasisAt hx).coord i else 0
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_eq_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.Nodup → s.ndinter t = s ∩ t
-- Mathlib.Analysis.Convex.Segment
segment_eq_Icc' : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y : 𝕜),
  segment 𝕜 x y = Set.Icc (min x y) (max x y)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.forward.match_1.splitter : (motive : String.Legacy.Iterator → ℕ → Sort u_1) →
  (x : String.Legacy.Iterator) →
    (x_1 : ℕ) →
      ((it : String.Legacy.Iterator) → motive it 0) →
        ((it : String.Legacy.Iterator) → (n : ℕ) → motive it n.succ) → motive x x_1
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R) {Z : CommRingCat}
  (h : (S.mkUnder (TensorProduct ↑R ↑S ↑A.right)).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr A.hom (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Under.Hom.right (CommRingCat.tensorProdObjIsoPushoutObj S A).inv) h) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) h
-- Init.Control.Lawful.Instances
ReaderT.run_map : ∀ {m : Type u_1 → Type u_2} {α β ρ : Type u_1} [inst : Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ),
  (f <$> x).run ctx = f <$> x.run ctx
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.linear_comp_iff_of_full_of_essSurj : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {E : Type u_4}
  [inst_8 : CategoryTheory.Category.{v_3, u_4} E] [inst_9 : CategoryTheory.Preadditive E]
  [inst_10 : CategoryTheory.Linear R E] (G : CategoryTheory.Functor D E) [F.Full] [F.EssSurj],
  CategoryTheory.Functor.Linear R (F.comp G) ↔ CategoryTheory.Functor.Linear R G
-- Batteries.Data.Char.Basic
Char.instLawfulOrd : Std.LawfulOrd Char
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.contains a = false → t.getKeyD a fallback = fallback
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Submodule.IsPrincipal.contentIdeal_generator_dvd : ∀ {R : Type u_3} [inst : CommSemiring R] {p : Polynomial R} (h_prin : Submodule.IsPrincipal p.contentIdeal),
  Polynomial.C (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₃_obj_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7}
  [inst_3 : CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [inst_4 : CategoryTheory.Category.{v_8, u_8} E']
  (X : CategoryTheory.Functor E E')
  {X_1 Y : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} (α : X_1 ⟶ Y) (X_2 : C₁)
  (X_3 : C₂) (X_4 : C₃),
  ((((CategoryTheory.Functor.postcompose₃.obj X).map α).app X_2).app X_3).app X_4 =
    X.map (((α.app X_2).app X_3).app X_4)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_eq_zero_of_degree_lt : ∀ {R : Type u} [inst : CommRing R] {k : ℕ} {P : Polynomial R}, P.degree < ↑k → (⇑Polynomial.derivative)^[k] P = 0
-- Init.Data.Nat.Bitwise.Basic
Nat.land_eq : ∀ {m n : ℕ}, m.land n = m &&& n
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node4L_lemma₁ : ∀ {a b c d : ℕ}, 3 * (b + c + 1 + d) ≤ 16 * a + 9 → b + c + 1 ≤ 3 * d → b ≤ 3 * c → b < 3 * a + 1
-- Mathlib.Data.Sign.Defs
SignType.neg_iff : ∀ {a : SignType}, a < 0 ↔ a = -1
-- Aesop.Search.Expansion.Norm
Aesop.normSimp : Lean.MVarId → Std.HashSet Lean.MVarId → Aesop.NormM (Option Aesop.NormRuleResult)
-- Mathlib.Data.Matrix.Mul
one_dotProduct_one : ∀ {n : Type u_3} {α : Type v} [inst : Fintype n] [inst_1 : NonAssocSemiring α], 1 ⬝ᵥ 1 = ↑(Fintype.card n)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_4 t ×' t.below
-- Mathlib.Data.Set.Image
Set.range_subtype_map : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (x : α), p x → q (f x)),
  Set.range (Subtype.map f h) = Subtype.val ⁻¹' f '' {x | p x}
-- Qq.Match
Qq.Impl.PatternVar.mk : Lean.Name → ℕ → Lean.Expr → Lean.Term → Qq.Impl.PatternVar
-- Init.Omega.IntList
Lean.Omega.IntList.get_nil : ∀ {i : ℕ}, Lean.Omega.IntList.get [] i = 0
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Empty `ForwardRuleMatches`.  -/
Aesop.ForwardRuleMatches.empty : Aesop.ForwardRuleMatches
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.sub : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s t : Set E},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq κ]
  (𝒞 : Module.Basis κ R N) (m : M) (n : N) (i : κ),
  ((TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) i = (𝒞.repr n) i • m
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_iff_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α}, a ∈ t ↔ (Std.ExtDTreeMap.Const.get? t a).isSome = true
-- Init.Data.Int.Order
Int.instLawfulOrderLT : Std.LawfulOrderLT ℤ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.iUnion_closedBall_nat : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), ⋃ n, Metric.closedBall x ↑n = Set.univ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.L : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Month.Ordinal
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharNeTwoNF_u : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2], W.toCharNeTwoNF.u = 1
-- Mathlib.Algebra.WithConv
WithConv.toConv.inj : ∀ {A : Sort u_1} {ofConv ofConv_1 : A}, WithConv.toConv ofConv = WithConv.toConv ofConv_1 → ofConv = ofConv_1
-- Mathlib.Tactic.SetNotationForOrder
/-- Elaborator for `x ⊂ y` notation.  -/
Mathlib.Meta.SetNotationForOrder.elabSSubsetStx' : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Category.Cat
/-- Category structure on `Cat`  -/
CategoryTheory.Cat.category : CategoryTheory.LargeCategory CategoryTheory.Cat
-- Mathlib.Analysis.Complex.Tietze
Metric.instTietzeExtensionClosedBall : ∀ (𝕜 : Type v) [inst : RCLike 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (y : E) {r : ℝ}, 0 < r → TietzeExtension ↑(Metric.closedBall y r)
-- Mathlib.Algebra.Star.Pi
Pi.instInvolutiveStarForall : {I : Type u} → {f : I → Type v} → [(i : I) → InvolutiveStar (f i)] → InvolutiveStar ((i : I) → f i)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the degree of `w` in `G` is at most the size of
`s`.  -/
SimpleGraph.isBipartiteWith_degree_le' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet w)],
  G.IsBipartiteWith ↑s ↑t → w ∈ t → G.degree w ≤ s.card
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.match_3.eq_2 : ∀ (motive : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) (p : Lean.Elab.Tactic.RCases.RCasesPatt)
  (h_1 : Unit → motive []) (h_2 : (p : Lean.Elab.Tactic.RCases.RCasesPatt) → motive [p])
  (h_3 : (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive ps),
  (match [p] with
    | [] => h_1 ()
    | [p] => h_2 p
    | ps => h_3 ps) =
    h_2 p
-- Lean.MetavarContext
Lean.DependsOn.State.mk.sizeOf_spec : ∀ (visited : Lean.ExprSet) (mctx : Lean.MetavarContext),
  sizeOf { visited := visited, mctx := mctx } = 1 + sizeOf visited + sizeOf mctx
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
/-- The rank function with values in `ℕ` relative to the well founded
ancestrality relation of a regular pairing.  -/
SSet.Subcomplex.Pairing.rank : {X : SSet} → {A : X.Subcomplex} → (P : A.Pairing) → [P.IsRegular] → ↑P.II → ℕ
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : 0 = 0 → motive 0) (h_2 : (k : ℕ) → 0 = k.succ → motive k.succ),
  (match h' : 0 with
    | 0 => h_1 h'
    | k.succ => h_2 k h') =
    h_1 ⋯
-- Mathlib.Topology.Bornology.BoundedOperation
instBoundedMulNNReal : BoundedMul NNReal
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.State.mk.injEq : ∀ (cache : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64)
  (keyToExprs : Std.HashMap UInt64 (List Lean.Expr))
  (cache_1 : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64)
  (keyToExprs_1 : Std.HashMap UInt64 (List Lean.Expr)),
  ({ cache := cache, keyToExprs := keyToExprs } = { cache := cache_1, keyToExprs := keyToExprs_1 }) =
    (cache = cache_1 ∧ keyToExprs = keyToExprs_1)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.coe_submonoidClass_iff : ∀ {k : ℕ} {M : Type u_7} {B : Type u_8} [inst : CommMonoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M]
  {N : B} {ζ : ↥N}, IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.functorialityCompPostcompose.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H'),
  CategoryTheory.Functor.functorialityCompPostcompose α =
    CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (α.app c.pt) ⋯) ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_sub : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_3} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {M₂ : Type u_4} [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_8 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_9 : RingHomInvPair σ₂₁ σ₁₂] (e : M ≃SL[σ₁₂] M₂) (x y : M), e (x - y) = e x - e y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toList init f
-- Mathlib.Data.Complex.Basic
Complex.normSq_eq_zero : ∀ {z : ℂ}, Complex.normSq z = 0 ↔ z = 0
-- Mathlib.Topology.MetricSpace.Infsep
Set.nontrivial_of_infsep_pos : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, 0 < s.infsep → s.Nontrivial
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftTMetaMTermElabM_batteries : LawfulMonadLiftT Lean.MetaM Lean.Elab.TermElabM
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- The inverse functor of the equivalence `(C ≌ D) ≌ (D ≌ C)ᵒᵖ`.  -/
CategoryTheory.Equivalence.symmEquivInverse : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (D : Type u_2) → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor (D ≌ C)ᵒᵖ (C ≌ D)
-- Mathlib.Topology.Covering.Quotient
/-- Fibers of a quotient covering map by a group G is a G-torsor.  -/
IsQuotientCoveringMap.fiberEquivGroup : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] → IsQuotientCoveringMap f G → {x : X} → ↑(f ⁻¹' {x}) → ↑(f ⁻¹' {x}) ≃ G
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.eq_1 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (motive : RingCat.Colimits.Prequotient F → Sort u_2) (j : J) (x : ↑(F.obj j))
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive RingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive RingCat.Colimits.Prequotient.one)
  (h_4 : (x : RingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : RingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match RingCat.Colimits.Prequotient.of j x with
    | RingCat.Colimits.Prequotient.of j x => h_1 j x
    | RingCat.Colimits.Prequotient.zero => h_2 ()
    | RingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_1 j x
-- Mathlib.Topology.Order.LeftRight
nhdsWithinGE_sup_nhdsWithinLE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Ici a) ⊔ nhdsWithin a (s ∩ Set.Iic a) = nhdsWithin a s
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousOn.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {z : Set β},
  LowerHemicontinuousOn (fun _x => z) s
-- Init.Data.Array.Count
Array.countP_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α}, Array.countP p (xs ++ ys) = Array.countP p xs + Array.countP p ys
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.coe_mul_zeta_apply : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {x : ℕ},
  (f * ↑ArithmeticFunction.zeta) x = ∑ i ∈ x.divisors, f i
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.strLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (k' : α) → (v' : β k') → motive (some ⟨k', v'⟩)),
  (match none with
    | none => h_1 ()
    | some ⟨k', v'⟩ => h_2 k' v') =
    h_1 ()
-- Mathlib.Combinatorics.Additive.Corner.Defs
not_isCorner_empty : ∀ {G : Type u_1} [inst : AddCommMonoid G] {x₁ y₁ x₂ y₂ : G}, ¬IsCorner ∅ x₁ y₁ x₂ y₂
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : X → Y),
  Topology.IsOpenEmbedding g → Topology.IsOpenEmbedding (g ∘ f) → Topology.IsOpenEmbedding f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_alter_le_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (t.alter k f).size ≤ t.size + 1
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- If `K : CochainComplex C ℤ`, this is the canonical truncation `≥ n` of `K`.  -/
CochainComplex.truncGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : CochainComplex C ℤ) →
        [CategoryTheory.Limits.HasZeroObject C] →
          [∀ (i : ℤ), HomologicalComplex.HasHomology K i] → ℤ → CochainComplex C ℤ
-- Mathlib.Algebra.Order.Group.Multiset
/-- `countP p`, the number of elements of a multiset satisfying `p`, promoted to an
`AddMonoidHom`.  -/
Multiset.countPAddMonoidHom : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Multiset α →+ ℕ
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.isNaN.match_1.eq_2 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (x : Float.Model.UnpackedFloat)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber) (h_2 : (x : Float.Model.UnpackedFloat) → motive x),
  (x = Float.Model.UnpackedFloat.notANumber → False) →
    (match x with
      | Float.Model.UnpackedFloat.notANumber => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instModuleRat : {M : Type u_2} → [inst : AddCommGroup M] → Module ℚ (DivisibleHull M)
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesHasSum.LSeries_eq : ∀ {f : ℕ → ℂ} {s a : ℂ}, LSeriesHasSum f s a → LSeries f s = a
-- Mathlib.Data.Finset.Image
Finset.map_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α), Finset.map f {a} = {f a}
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If an open partial homeomorphism `f` is analytic at a point `a`, with invertible derivative,
then its inverse is analytic at `f a`.  -/
OpenPartialHomeomorph.analyticAt_symm' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) {a : E} {i : E ≃L[𝕜] F},
  a ∈ f.source → AnalyticAt 𝕜 (↑f) a → fderiv 𝕜 (↑f) a = ↑i → AnalyticAt 𝕜 (↑f.symm) (↑f a)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_same₃₄ : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c : ℤ),
  IsEllipticNet.atomRel W a b c c = W c * W 0 * IsEllipticNet.atom W a b
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) {Z_1 : C}
  (h : ((ChainComplex.single₀ C).obj Z).X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ProjectiveResolution.lift f P Q).f 0)
      (CategoryTheory.CategoryStruct.comp (Q.π.f 0) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (P.π.f 0) f) h
-- Mathlib.Algebra.Module.Torsion.Basic
/-- If the `p i` are pairwise coprime, a `⨅ i, p i`-torsion module is the internal direct sum of
its `p i`-torsion submodules.  -/
Submodule.torsionBySet_isInternal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : DecidableEq ι] {S : Finset ι} {p : ι → Ideal R},
  ((↑S).Pairwise fun i j => p i ⊔ p j = ⊤) →
    Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i) → DirectSum.IsInternal fun i => Submodule.torsionBySet R M ↑(p ↑i)
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView.mk : Option Lean.DeclarationLocation → Lean.Meta.SorryLabelView