mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instSMulCommClass' : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass R S M] [inst_6 : SMul S R]
  [IsScalarTower S R M], SMulCommClass (Module.End R M) S (Module.End R M)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (t.insertMany l).getKey? k' = some k
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- The module of differentials of a morphism `f : A ⟶ B` in the category `CommRingCat`.  -/
CommRingCat.KaehlerDifferential : {A B : CommRingCat} → (A ⟶ B) → ModuleCat ↑B
-- Mathlib.Algebra.Module.SpanRank
Submodule.FG.spanRank_eq_iff : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → ∀ (n : ℕ), p.spanRank = ↑n ↔ p.spanFinrank = n
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- Determine possible ways in which a `grw` call could rewrite at the given subexpression.  -/
Mathlib.Tactic.ClickSuggestions.getGrwPos? : Lean.Expr → Lean.Expr → Lean.SubExpr.Pos → Bool → Lean.MetaM (Array Mathlib.Tactic.ClickSuggestions.GrwPos)
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprEtaStructMode : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.EtaStructMode
-- Init.Ext
/-- The flag `(iff := false)` prevents `ext` from generating an `ext_iff` lemma.
 -/
Lean.Parser.Attr.extIff : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.Class
Class.ofSet.inj : ∀ {x y : ZFSet.{u}}, ↑x = ↑y → x = y
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.of_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {m n : WithTop ℕ∞}, ContDiff 𝕜 n f → m ≤ n → ContDiff 𝕜 m f
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddMonoid Y], ⇑0 = 0
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.ofEq_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (h : f = g), (CategoryTheory.Arrow.LeftHomotopy.ofEq h).hom = 0
-- Mathlib.Data.List.Chain
List.IsChain.rel_cons : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a b : α} [Trans R R R], List.IsChain R (a :: l) → b ∈ l → R a b
-- Mathlib.Data.Sigma.Basic
PSigma.elim_val : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : Sort u_3} (f : (a : α) → β a → γ) (a : α) (b : β a),
  PSigma.elim f ⟨a, b⟩ = f a b
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Taking the image of a morphism gives a functor `Over X ⥤ MonoOver X`.
 -/
CategoryTheory.MonoOver.image : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      [CategoryTheory.Limits.HasImages C] → CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.MonoOver X)
-- Mathlib.Data.Set.Prod
/-- The fiber product $X \times_Y X$.  -/
Function.PullbackSelf : {X : Type u_1} → {Y : Sort u_2} → (X → Y) → Type u_1
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode : Type
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_right_right : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime x (y + z * x)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_eq_map' : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ⟶ g b),
  CategoryTheory.Limits.biproduct.map p = CategoryTheory.Limits.biproduct.map' p
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {b : β},
  b ∈ s → s.inf f ≤ f b
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestRevMatch_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch p pos ↔
    ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯) = true
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- A preadditive monoidal category with binary biproducts is distributive.  -/
CategoryTheory.IsMonoidalDistrib.of_MonoidalPreadditive_with_binary_coproducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.Preadditive C]
  [CategoryTheory.MonoidalPreadditive C], CategoryTheory.IsMonoidalDistrib C
-- Init.Data.Vector.Zip
Vector.of_mem_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {a : α} {b : β} {as : Vector α n} {bs : Vector β n},
  (a, b) ∈ as.zip bs → a ∈ as ∧ b ∈ bs
-- Mathlib.CategoryTheory.Localization.Quotient
/-- If `homRel : HomRel C` satisfies `homRel.FactorsThroughLocalization W` and
that the class of morphisms `W` induces a class of morphisms `W'` on the quotient category,
then the localizer morphism given by the functor `Quotient.functor HomRel : C ⥤ Quotient homRel`
induces equivalences on localized categories.  -/
HomRel.FactorsThroughLocalization.isLocalizedEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {homRel : HomRel C}
  {W : CategoryTheory.MorphismProperty C},
  homRel.FactorsThroughLocalization W →
    ∀ {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)}
      (hW : W = W'.inverseImage (CategoryTheory.Quotient.functor homRel)),
      (CategoryTheory.LocalizerMorphism.ofEq hW).IsLocalizedEquivalence
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instMonoidalCategory : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] → [CategoryTheory.MonoidalCategory V] → CategoryTheory.MonoidalCategory (Action V G)
-- Mathlib.Tactic.Ring.Common
/-- The result of evaluating an (unnormalized) expression `e` into the type family `E`
(typically one of `ExSum`, `ExProd`, `ExBase` or `BaseType`) is a (normalized) element `e'`
and a representation `E e'` for it, and a proof of `e = e'`.
 -/
Mathlib.Tactic.Ring.Common.Result : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type u_1) → Q(«$α») → Type u_1
-- Batteries.Lean.NameMapAttribute
Lean.NameMapAttributeImpl.mk.inj : ∀ {α : Type} {name : Lean.Name} {ref : autoParam Lean.Name Lean.NameMapAttributeImpl.ref._autoParam} {descr : String}
  {add : Lean.Name → Lean.Syntax → Lean.AttrM α} {name_1 : Lean.Name}
  {ref_1 : autoParam Lean.Name Lean.NameMapAttributeImpl.ref._autoParam} {descr_1 : String}
  {add_1 : Lean.Name → Lean.Syntax → Lean.AttrM α},
  { name := name, ref := ref, descr := descr, add := add } =
      { name := name_1, ref := ref_1, descr := descr_1, add := add_1 } →
    name = name_1 ∧ ref = ref_1 ∧ descr = descr_1 ∧ add = add_1
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.app.sizeOf_spec : ∀ (const : Option Lean.Name) (arity : ℕ),
  sizeOf (Mathlib.Notation3.DelabKey.app const arity) = 1 + sizeOf const + sizeOf arity
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.trans_eventuallyEq : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f : α → E}
  {g₁ g₂ : α → F}, f =o[l] g₁ → g₁ =ᶠ[l] g₂ → f =o[l] g₂
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `PseudoMetricSpace E` instance from a `SeminormedSpace.Core` on a type that
already has an existing uniform space structure. This requires a proof that the uniformity induced
by the norm is equal to the preexisting uniformity. See note [reducible non-instances].  -/
PseudoMetricSpace.ofSeminormedSpaceCoreReplaceUniformity : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            [U : UniformSpace E] → (core : SeminormedSpace.Core 𝕜 E) → uniformity E = uniformity E → PseudoMetricSpace E
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L),
  h.map h (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L) ⋯ =
    CategoryTheory.CategoryStruct.id h.cochainComplex
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- There is a morphism from any cone point to `t.pt`  -/
CategoryTheory.Limits.IsLimit.lift : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t → (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
/-- Helper function for evaluating terms that have been processed by `internalize`, but
we did not added them to constraints. See comment at `assignTerms`.
 -/
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Model.0.Lean.Meta.Grind.Arith.Linear.evalTermAt? : Lean.Expr → Lean.Meta.Grind.Arith.Linear.Struct → Std.HashMap Lean.Expr ℚ → Lean.MetaM (Option ℚ)
-- Lean.Server.CodeActions.Attr
/-- An extension which collects all the hole code actions.  -/
Lean.CodeAction.holeCodeActionExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Lean.CodeAction.HoleCodeAction)
  (Array Lean.Name × Array Lean.CodeAction.HoleCodeAction)
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.faceSingletonComplIso_inv_ι_assoc : ∀ {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) {Z : SSet} (h : (SSet.horn (n + 1) i).toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso j).inv
      (CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hij) h) =
    CategoryTheory.CategoryStruct.comp (SSet.horn.faceι i j hij) h
-- Lean.Parser.Basic
/-- `withoutPosition(p)` runs `p` without the saved position, meaning that position-checking
parsers like `colGt` will have no effect. This is usually used by bracketing constructs like
`(...)` so that the user can locally override whitespace sensitivity.

This parser has the same arity as `p` - it just forwards the results of `p`.  -/
Lean.Parser.withoutPosition : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Computability.NFA
/-- `M.acceptsFrom S` is the language of `x` such that there is an accept state
in `M.evalFrom S x`.  -/
NFA.acceptsFrom : {α : Type u} → {σ : Type v} → NFA α σ → Set σ → Language α
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The inclusion `X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⟶ tensorObj X₁ (tensorObj X₂ X₃) j`
when `i₁ + i₂ + i₃ = j`.  -/
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) →
            [inst_3 : X₂.HasTensor X₃] →
              [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] →
                (i₁ i₂ i₃ j : I) →
                  i₁ + i₂ + i₃ = j →
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁)
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₂ i₂) (X₃ i₃)) ⟶
                      CategoryTheory.GradedObject.Monoidal.tensorObj X₁
                        (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarAlgHom_comp : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  [inst_7 : Star A₁] [inst_8 : Star A₂] [inst_9 : Star A₃] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₂ : A₂ ≃⋆ₐ[R] A₃),
  e₂.toStarAlgHom.comp e₁.toStarAlgHom = (e₁.trans e₂).toStarAlgHom
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
NNReal.continuousOn_rpow_const_compl_zero : ∀ {r : ℝ}, ContinuousOn (fun z => z ^ r) {0}ᶜ
-- Init.Data.Array.Count
Array.not_mem_of_count_eq_zero : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, Array.count a xs = 0 → a ∉ xs
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_nat_mul : ∀ (x : ℂ) (n : ℕ), Complex.exp (↑n * x) = Complex.exp x ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  P 2 = 0 → (W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P 0 ^ 2 ≠ 0 ∨ P 1 ^ 2 + W'.a₁ * P 0 * P 1 - W'.a₂ * P 0 ^ 2 ≠ 0))
-- Mathlib.Computability.ContextFreeGrammar
/-- Context-free languages are defined by context-free grammars.  -/
Language.IsContextFree : {T : Type u_1} → Language T → Prop
-- Init.Data.Option.Instances
Option.decidableForallMem : {α : Type u_1} → {p : α → Prop} → [DecidablePred p] → (o : Option α) → Decidable (∀ a ∈ o, p a)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_apply_succAbove : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin n),
  i.insertNth x p (i.succAbove j) = p j
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `isPGroup_iff_exponent_dvd_pow`. -/
IsPGroup.exists_exponent_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G], IsPGroup p G → ∃ n, Monoid.exponent G ∣ p ^ n
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.atom.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)] {e : Q(«$α»)} (id : ℕ),
  sizeOf (Mathlib.Tactic.Ring.Common.ExBase.atom id) = 1 + sizeOf e + sizeOf id
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iic a).Nonempty
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.Analysis.Normed.Module.Convex
/-- **Alias** of `isConnected_setOfPred_sameRay_and_ne_zero`.

---

The set of nonzero vectors in the same ray as the nonzero vector `x` is connected.  -/
isConnected_setOf_sameRay_and_ne_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E},
  x ≠ 0 → IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.comp_hasStrictFDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E),
  HasStrictDerivAt h₂ h₂' y → HasStrictFDerivAt f f' x → y = f x → HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Mathlib.NumberTheory.GaussSum
/-- Taking complex conjugates of a Gauss sum inverts both characters.  -/
star_gaussSum_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] (χ : MulChar R ℂ) (ψ : AddChar R ℂ),
  star (gaussSum χ ψ) = gaussSum χ⁻¹ ψ⁻¹
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This relies on `default ℕ = 0`.  -/
List.headI_add_tail_sum : ∀ (L : List ℕ), L.headI + L.tail.sum = L.sum
-- Mathlib.Data.Nat.Pairing
Nat.pair_lt_pair_left : ∀ {a₁ a₂ : ℕ} (b : ℕ), a₁ < a₂ → Nat.pair a₁ b < Nat.pair a₂ b
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.isZero_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
      [inst_3 : (i : I) → CategoryTheory.Limits.HasZeroMorphisms (D i)] [∀ (i : I), (F i).PreservesZeroMorphisms]
      [CategoryTheory.Limits.HasZeroObject C] {X : C},
      CategoryTheory.Limits.IsZero X ↔ ∀ (i : I), CategoryTheory.Limits.IsZero ((F i).obj X)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- For disjoint `f1` and `f2`, and function `g`, the sum of the sums of `g`
over `f1` and `f2` equals the sum of `g` over `f1 + f2`  -/
Finsupp.sum_add_index_of_disjoint : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {f1 f2 : α →₀ M},
  Disjoint f1.support f2.support →
    ∀ {β : Type u_16} [inst_1 : AddCommMonoid β] (g : α → M → β), (f1 + f2).sum g = f1.sum g + f2.sum g
-- Init.Data.Int.Gcd
Int.gcd_mul_left_dvd_mul_gcd : ∀ (k m n : ℤ), (m * n).gcd k ∣ m.gcd k * n.gcd k
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
_private.Mathlib.FieldTheory.PurelyInseparable.Exponent.0.IsPurelyInseparable.iterateFrobeniusAux.eq_1 : ∀ (K : Type u_2) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p n : ℕ) (a : L),
  IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a =
    IsPurelyInseparable.elemReduct K a ^ p ^ (n - IsPurelyInseparable.elemExponent K a)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadWithReaderOfSubExprAnalyzeM : MonadWithReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapAddMon_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapAddMon.unitIso =
    CategoryTheory.Functor.mapAddMonIdIso.symm ≪≫
      CategoryTheory.Functor.mapAddMonNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapAddMonCompIso
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.IsMonoidal.toTensorLE : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsMonoidal], P.TensorLE P P
-- Init.Data.String.Lemmas.Slice
String.Slice.beq_eq_true_iff : ∀ {s t : String.Slice}, (s == t) = true ↔ s.copy = t.copy
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_two_pi : Circle.exp (2 * Real.pi) = 1
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux_ofComp : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : (Q.comp P).Ring),
  (Algebra.Generators.H1Cotangent.δAux R Q) ((Q.ofComp P).toAlgHom x) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((Algebra.Generators.CotangentSpace.compEquiv Q P)
          (1 ⊗ₜ[(Q.comp P).Ring] (KaehlerDifferential.D R (Q.comp P).Ring) x)).2
-- Mathlib.Algebra.Free
FreeAddSemigroup.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (FreeAddSemigroup α)
-- Init.Data.List.Lemmas
List.getElem_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {i : ℕ} {h : i < (List.map f l).length},
  (List.map f l)[i] = f l[i]
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldlM_eq_foldlM_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.TreeMap.Raw.foldlM (fun d a x => f d a) init t = Array.foldlM f init t.keysArray
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Solutions to ODEs defined by $C^n$ vector fields are also $C^n$.  -/
ODE.contDiffOn_enat_Icc_of_hasDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {tmin tmax : ℝ} {n : ℕ∞},
  ContDiffOn ℝ (↑n) (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
    (∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t) →
      Set.MapsTo α (Set.Icc tmin tmax) u → ContDiffOn ℝ (↑n) α (Set.Icc tmin tmax)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_equivMap_apply : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_6}
  [inst_3 : Field K] [inst_4 : Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) (x : ↥L),
  ↑((L.equivMap f) x) = f ↑x
-- Mathlib.Algebra.Group.Indicator
Set.indicator_self_add_compl_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f : α → M) (a : α),
  s.indicator f a + sᶜ.indicator f a = f a
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- Construct an isomorphism between two objects in a bicategorical category
out of unitors and associators.  -/
CategoryTheory.bicategoricalIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → (f g : a ⟶ b) → [CategoryTheory.BicategoricalCoherence f g] → f ≅ g
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Continuous.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F},
  Continuous g → Continuous f → Continuous fun x => g x ∘SL f x
-- Lean.Parser.Term
Lean.Parser.Term.unop.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp f h
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.bot_himp : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l} [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.himp Lean.Order.bot P = Lean.Order.top
-- Mathlib.Tactic.Ring.RingNF
/-- `ring` solves equations in *commutative* (semi)rings, allowing for variables in the
exponent. If the goal is not appropriate for `ring` (e.g. not an equality) `ring_nf` will be
suggested. See also `ring1`, which fails if the goal is not an equality.

* `ring!` will use a more aggressive reducibility setting to determine equality of atoms.

Examples:
```
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf
```
 -/
Mathlib.Tactic.RingNF.tacticRing! : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_inf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f →
    ∀ (S T : Subsemigroup M), Subsemigroup.comap f (Subsemigroup.map f S ⊓ Subsemigroup.map f T) = S ⊓ T