mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_eq_left_of_det_ne_zero : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [IsDomain R]
  [inst_3 : DecidableEq n] (A : Matrix n n R) (B : Matrix m n R), A.det ≠ 0 → (B * A).rank = B.rank
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mulIndicator.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : One R] {U : Set X} (f : LocallyConstant X R)
  (hU : IsClopen U), f.mulIndicator hU = { toFun := U.mulIndicator ⇑f, isLocallyConstant := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_some_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.max? = some t.max!
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.center_prod : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {B : Type u_3} [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : Module R B] [inst_7 : IsScalarTower R B B] [inst_8 : SMulCommClass R B B],
  NonUnitalSubalgebra.center R (A × B) = (NonUnitalSubalgebra.center R A).prod (NonUnitalSubalgebra.center R B)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.norm_compLpL₂_le : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {𝕜 : Type u_6} [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E]
  {F : Type u_8} {G : Type u_9} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fact (1 ≤ p)] (B : G →L[𝕜] E →L[𝕜] F),
  ‖ContinuousLinearMap.compLpL₂ p μ B‖ ≤ ‖B‖
-- Init.Prelude
/-- `` `scientific `` is the node kind of floating point literals like `1.23e-3`.  -/
Lean.scientificLitKind : Lean.SyntaxNodeKind
-- Mathlib.Combinatorics.Colex
/-- The colexicographic order is insensitive to removing the same elements from both sets.  -/
Finset.Colex.toColex_sdiff_lt_toColex_sdiff : ∀ {α : Type u_1} [inst : PartialOrder α] {s t u : Finset α} [inst_1 : DecidableEq α],
  u ⊆ s → u ⊆ t → (toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t)
-- Mathlib.Algebra.Algebra.Defs
RingHom.smul_toAlgebra' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] (i : R →+* S)
  (h : ∀ (c : R) (x : S), i c * x = x * i c) (r : R) (s : S),
  have x := i.toAlgebra' h;
  r • s = i r * s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_one_of_isMulCocycle₁ : ∀ {G : Type u_1} {M : Type u_2} [inst : Monoid G] [inst_1 : CommGroup M] [inst_2 : MulAction G M] {f : G → M},
  groupCohomology.IsMulCocycle₁ f → f 1 = 1
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.integral_const_sub : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ) (c : ℝ),
  ∫ (x : X), (BoundedContinuousFunction.const X c - f) x ∂μ = μ.real Set.univ • c - ∫ (x : X), f x ∂μ
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.mapsTo_Ioo : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictAntiOn f (Set.Icc a b) → Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
-- Mathlib.Data.Analysis.Filter
CFilter.inf : {α : Type u_1} → {σ : Type u_2} → [inst : PartialOrder α] → CFilter α σ → σ → σ → σ
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- If `f` is a ring seminorm on `a` with `f 1 ≤ 1`, then `∀ (n : ℕ), f (a ^ n) ≤ f a ^ n`.  -/
map_pow_le_pow' : ∀ {F : Type u_2} {α : Type u_3} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ] {f : F},
  f 1 ≤ 1 → ∀ (a : α) (n : ℕ), f (a ^ n) ≤ f a ^ n
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instZeroQuotient : {S : Type u_2} → (M : Type u_3) → [inst : SMul S M] → [Zero M] → (c : SMulCon S M) → Zero (SMulCon.Quotient M c)
-- Mathlib.Logic.Equiv.Bool
Equiv.boolNot_apply : ∀ (a : Bool), Equiv.boolNot a = !a
-- Mathlib.Order.Shrink
instTopShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [Top α] → Top (Shrink.{u, u_1} α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertMany_append : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF →
    ∀ {l₁ l₂ : List (α × β)},
      Std.DHashMap.Raw.Const.insertMany m (l₁ ++ l₂) =
        Std.DHashMap.Raw.Const.insertMany (Std.DHashMap.Raw.Const.insertMany m l₁) l₂
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.State.mk : Lean.PersistentExprMap Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.State
-- Lean.Environment
Lean.Kernel.Environment.setDiagnostics : Lean.Kernel.Environment → Lean.Kernel.Diagnostics → Lean.Kernel.Environment
-- Mathlib.RingTheory.PowerSeries.CoeffMulMem
PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal : ∀ {A : Type u_1} [inst : Semiring A] {I : Ideal A} {f g : PowerSeries A} (n : ℕ),
  (∀ i ≤ n, (PowerSeries.coeff i) g ∈ I) → ∀ i ≤ n, (PowerSeries.coeff i) (f * g) ∈ I
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.recOn_of_mul : ∀ {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (x : α) (xs : FreeMonoid α) (one : motive 1)
  (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (FreeMonoid.of x * xs)),
  FreeMonoid.recOn (FreeMonoid.of x * xs) one of_mul = of_mul x xs (FreeMonoid.recOn xs one of_mul)
-- Init.Data.Option.Lemmas
Option.map_congr : ∀ {α : Type u_1} {α_1 : Type u_2} {f g : α → α_1} {x : Option α},
  (∀ (a : α), x = some a → f a = g a) → Option.map f x = Option.map g x
-- Init.Core
HEq.comm : ∀ {α β : Sort u_1} {a : α} {b : β}, a ≍ b ↔ b ≍ a
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Produces.exists_nonterminal_input_mem : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.Produces u v → ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_comap : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] (f : Ω → Ω')
  (μ : MeasureTheory.FiniteMeasure Ω'), ↑(MeasureTheory.FiniteMeasure.comap f μ) = MeasureTheory.Measure.comap f ↑μ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).tail = tl
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSubNegZeroMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : SubNegZeroMonoid Mᵃᵒᵖ], DomAddAct.instSubNegZeroMonoidOfAddOpposite = inst
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- `LinearIsometryClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries
`M → M₂`.

This is an abbreviation for `SemilinearIsometryClass F (RingHom.id R) E E₂`.
 -/
LinearIsometryClass : (𝓕 : Type u_11) →
  (R : outParam (Type u_12)) →
    (E : outParam (Type u_13)) →
      (E₂ : outParam (Type u_14)) →
        [inst : Semiring R] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R E₂] → [FunLike 𝓕 E E₂] → Prop
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**, forward direction, second alternate form.

Let $M$ be a flat module over a commutative ring $R$. Let $N$ be a finite free module over $R$,
let $f \in N$, and let $x \colon N \to M$ be a linear map such that $x(f) = 0$. Then there exist a
finite free module $R^k$ and linear maps $a \colon N \to R^k$ and
$y \colon R^k \to M$ such that $x = y \circ a$ and $a(f) = 0$.  -/
Module.Flat.exists_factorization_of_apply_eq_zero_of_free : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  {N : Type u_3} [inst_4 : AddCommGroup N] [inst_5 : Module R N] [Module.Free R N] [Module.Finite R N] {f : N}
  {x : N →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
-- Mathlib.Order.Hom.Basic
OrderIso.ofHomInv_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (g : β →o α)
  (h₁ : f.comp g = OrderHom.id) (h₂ : g.comp f = OrderHom.id) (a : α), (OrderIso.ofHomInv f g h₁ h₂) a = f a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A submagma of a magma inherits a multiplication.  -/
MulMemClass.mul : {M : Type u_1} → {A : Type u_3} → [inst : Mul M] → [inst_1 : SetLike A M] → [hA : MulMemClass A M] → (S' : A) → Mul ↥S'
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {X Y Z : F ⟶ G} (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Hom X Y)
  (Δ : CategoryTheory.Pseudofunctor.StrongTrans.Hom Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp Γ Δ).as.app a = CategoryTheory.CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.equivalence_inverse : ∀ {I : Type u₁} {J : Type u₂} (e : I ≃ J),
  (CategoryTheory.Discrete.equivalence e).inverse =
    CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e.symm)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p.coeffs = Finset.image (fun m => MvPolynomial.coeff m p) p.support
-- Mathlib.Analysis.SpecificLimits.Normed
isLittleO_pow_pow_of_abs_lt_left : ∀ {r₁ r₂ : ℝ}, |r₁| < |r₂| → (fun n => r₁ ^ n) =o[Filter.atTop] fun n => r₂ ^ n
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier.uri : Lean.Lsp.VersionedTextDocumentIdentifier → Lean.Lsp.DocumentUri
-- Mathlib.Logic.IsEmpty.Basic
Relator.BiTotal.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} (R : α → β → Prop), Relator.BiTotal R = (Relator.LeftTotal R ∧ Relator.RightTotal R)
-- Mathlib.Data.Finset.Preimage
Finset.preimage_compl : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Fintype α] [inst_3 : Fintype β]
  {f : α → β} (s : Finset β) (hf : Function.Injective f), sᶜ.preimage f ⋯ = (s.preimage f ⋯)ᶜ
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_iff : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M rs ↔
    ∀ (i : ℕ) (h : i < rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_add : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.injective_of_mono : ∀ {G H : AddCommGrpCat} (f : G ⟶ H) [CategoryTheory.Mono f], Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- If `α` has at least `n` elements, then any `n`-pretransitive action on `α`
is `m`-pretransitive for any `m ≤ n`.

This version allows `α` to be infinite and uses `ENat.card`.
For `Finite α`, use `MulAction.isMultiplyPretransitive_of_le`  -/
MulAction.isMultiplyPretransitive_of_le' : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {m n : ℕ}
  [MulAction.IsMultiplyPretransitive G α n], m ≤ n → ↑n ≤ ENat.card α → MulAction.IsMultiplyPretransitive G α m
-- Mathlib.Probability.Process.FiniteDimensionalLaws
/-- Two stochastic processes are identically distributed iff they have the same
finite-dimensional distributions.  -/
ProbabilityTheory.identDistrib_iff_forall_finset_identDistrib : ∀ {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)}
  {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable (fun ω x => X x ω) P →
    AEMeasurable (fun ω x => Y x ω) P →
      (ProbabilityTheory.IdentDistrib (fun ω x => X x ω) (fun ω x => Y x ω) P P ↔
        ∀ (I : Finset T),
          ProbabilityTheory.IdentDistrib (fun ω => I.restrict fun x => X x ω) (fun ω => I.restrict fun x => Y x ω) P P)
-- Mathlib.Order.Booleanisation
Booleanisation.lift_lt_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  Booleanisation.lift a < Booleanisation.comp b ↔ Disjoint a b
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.one_div_nonneg : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 ≤ 1 / p
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂_basisFun : ∀ {R : Type u_1} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂]
  [inst_2 : Module R N₂] [inst_3 : Fintype n] [inst_4 : Fintype m] [inst_5 : DecidableEq m] [inst_6 : DecidableEq n],
  Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLinearMap₂' R
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- Pythagorean theorem, subtracting vectors, if-and-only-if vector angle form.  -/
InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Variant of `map_source`, stated for images of subsets of `source`.  -/
OpenPartialHomeomorph.image_source_subset : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e '' e.source ⊆ e.target
-- Mathlib.FieldTheory.Perfect
/-- A ring is perfect if the Frobenius map is bijective.  -/
PerfectRing.bijective_frobenius : ∀ {R : Type u_1} {p : ℕ} {inst : Pow R ℕ} [self : PerfectRing R p], Function.Bijective fun x => x ^ p
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.instAdditiveIntShiftFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ),
  (CochainComplex.shiftFunctor C n).Additive
-- Lean.Environment
Lean.Environment.Visibility.public.sizeOf_spec : sizeOf Lean.Environment.Visibility.public = 1
-- Lean.Parser.Command
Lean.Parser.Command.openSimple.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.instIsIsoπGeneratingSections : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u),
  CategoryTheory.IsIso (SheafOfModules.free.generatingSections I).π
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instHasColimits : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G], CategoryTheory.Limits.HasColimits (Rep.{w, u, v} k G)
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.isHadamard_conjTranspose_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.conjTranspose.IsHadamard ↔ A.IsHadamard
-- Mathlib.Algebra.Order.Pi
Pi.isOrderedCancelMonoid : ∀ {I : Type u_1} {f : I → Type u_5} [inst : (i : I) → CommMonoid (f i)] [inst_1 : (i : I) → Preorder (f i)]
  [∀ (i : I), IsOrderedCancelMonoid (f i)], IsOrderedCancelMonoid ((i : I) → f i)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- The product over two finsupps agree if the functions agree and are well-behaved within the
shared support.  -/
Finsupp.prod_congr_of_eq_on_union : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] [inst_2 : DecidableEq α]
  {f1 f2 : α →₀ M} {g1 g2 : α → M → N},
  (∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)) →
    (∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1) → (∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1) → f1.prod g1 = f2.prod g2
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monic_monomial_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ),
  (MvPolynomial.monomial m) 1 = m.prod fun n e => MvPolynomial.X n ^ e
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forIn.visit.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [inst : Monad m] (f : α → σ → m (ForInStep σ)) (a : σ)
  (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.forIn.visit f (RBTree.RBNode.node c l v r) a =
    ForInStep.bindM (RBTree.RBNode.forIn.visit f l a) fun b =>
      ForInStep.bindM (f v b) fun x => RBTree.RBNode.forIn.visit f r x
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_smul : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] (c : R)
  (t : Finset ι) {w : ι → R} (z : ι → E), (t.centerMass w fun i => c • z i) = c • t.centerMass w z
-- Init.Data.Array.Basic
Array.mem_toArray : ∀ {α : Type u} {a : α} {l : List α}, a ∈ l.toArray ↔ a ∈ l
-- Mathlib.RingTheory.Ideal.Span
/-- The ideal generated by a subset of a ring  -/
Ideal.span : {α : Type u} → [inst : Semiring α] → Set α → Ideal α
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_le_atBot : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Filter.IsBounded (fun x1 x2 => x1 ≤ x2) Filter.atBot
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.reindex.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [inst : AddGroup G] (b : FreeAddGroupBasis ι G) (e : ι ≃ ι'),
  b.reindex e = { repr := b.repr.trans (FreeAddGroup.freeAddGroupCongr e) }
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- The identity on `ℕ` as an `ArithmeticFunction`.  -/
ArithmeticFunction.id : ArithmeticFunction ℕ
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.map.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F G : CategoryTheory.Sheaf J AddCommGrpCat}
  (f : F ⟶ G) (n : ℕ),
  CategoryTheory.Sheaf.H.map f n =
    (CategoryTheory.Abelian.Ext.mk₀ f).postcomp
      ((CategoryTheory.constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{w, 0} ℤ))) ⋯
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.mem_succ_succ_iff : ∀ {α : Type u} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {lo hi a : α}, (a ∈ (Std.PRange.succ lo)<...Std.PRange.succ hi) ↔ ∃ a', a = Std.PRange.succ a' ∧ a' ∈ lo<...hi
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₁ ↔ CategoryTheory.IsIso T.mor₂
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instSetLike : {M : Type u_1} → [inst : MulOneClass M] → SetLike (Submonoid M) M
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Products of equivalent measurable spaces are equivalent.  -/
MeasurableEquiv.prodCongr : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        [inst : MeasurableSpace α] →
          [inst_1 : MeasurableSpace β] →
            [inst_2 : MeasurableSpace γ] → [inst_3 : MeasurableSpace δ] → α ≃ᵐ β → γ ≃ᵐ δ → α × γ ≃ᵐ β × δ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_left_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.H = h.left.H
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.instInhabitedId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → {g : c ⟶ a} → Inhabited (CategoryTheory.Bicategory.RightLift (CategoryTheory.CategoryStruct.id a) g)
-- Lean.Util.Diff
/-- An index of the element in the left array, if applicable  -/
Lean.Diff.Histogram.Entry.leftIndex : {α : Type u} → {lsize rsize : ℕ} → Lean.Diff.Histogram.Entry α lsize rsize → Option (Fin lsize)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_apply : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x y : α),
  (f.cycleOf x) y = if f.SameCycle x y then f y else y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.hasNatPow : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Monoid β] → Pow (MeasureTheory.SimpleFunc α β) ℕ
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.hasNatScalar : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → {C D : HomologicalComplex V c} → SMul ℕ (C ⟶ D)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.fourier_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ),
  (FourierTransform.fourier f) g = f (FourierTransform.fourier g)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.Relation.w : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {i j : E.I₀} (self : E.Relation i j),
  CategoryTheory.CategoryStruct.comp self.fst (E.f i) = CategoryTheory.CategoryStruct.comp self.snd (E.f j)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_smul : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ : MeasureTheory.VectorMeasure X V} {𝕜 : Type u_3} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 V] {c : 𝕜},
  (c • μ).variation = ‖c‖₊ • μ.variation
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A class describing the property of reflecting effective epimorphic families.
 -/
CategoryTheory.Functor.ReflectsEffectiveEpiFamilies : {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 C D → Prop
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_symm : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  LinearMap.BilinForm.toMatrix'.symm = Matrix.toBilin'