harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isClosed_iff_zeroLocus (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ s, Z = zeroLocus s

Proof state:
R : Type u
inst✝ : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem embedding_mk_eq (φ : K →+* ℂ) :
    embedding (mk φ) = φ ∨ embedding (mk φ) = ComplexEmbedding.conjugate φ

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ

Tactic:
rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivation.lean
theorem mkDerivation_X (a : A) : mkDerivation R a X = a

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ ((mkDerivation R) a) X = a

Tactic:
simp [mkDerivation_apply]

Result:
no goals
-- Mathlib/Topology/Metrizable/Uniformity.lean
theorem dist_ofPreNNDist_le (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0)
    (dist_comm : ∀ x y, d x y = d y x) (x y : X) :
    @dist X (@PseudoMetricSpace.toDist X (PseudoMetricSpace.ofPreNNDist d dist_self dist_comm)) x
        y ≤
      d x y :=
  NNReal.coe_le_coe.2 <| (ciInf_le (OrderBot.bddBelow _) []).trans_eq <| by simp

Proof state:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ (zipWith d [x] ([] ++ [y])).sum = d x y

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ fderivWithin 𝕜 f s x = fderiv 𝕜 f x

Tactic:
rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter h]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated disjoint_genEigenspace (since := "2024-10-23")]
lemma disjoint_iSup_genEigenspace [NoZeroSMulDivisors R M]
    (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) :
    Disjoint (⨆ k : ℕ, f.genEigenspace μ₁ k) (⨆ k : ℕ, f.genEigenspace μ₂ k)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
⊢ Disjoint (⨆ k, (f.genEigenspace μ₁) ↑k) (⨆ k, (f.genEigenspace μ₂) ↑k)

Tactic:
simpa only [iSup_genEigenspace_eq] using disjoint_genEigenspace f hμ ⊤ ⊤

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem pre_comm_ihom_map {W X Y Z : C} [Closed W] [Closed X] (f : W ⟶ X) (g : Y ⟶ Z) :
    (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
W X Y Z : C
inst✝¹ : Closed W
inst✝ : Closed X
f : W ⟶ X
g : Y ⟶ Z
⊢ (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.erase_get [DecidableEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) :
    l.erase (l.get i) = l.eraseIdx ↑i

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
i : Fin l.length
⊢ l.erase (l.get i) = l.eraseIdx ↑i

Tactic:
simp [erase_getElem, hl]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem expNear_zero (x r) : expNear 0 x r = r

Proof state:
x r : ℝ
⊢ expNear 0 x r = r

Tactic:
simp [expNear]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_not : ∀ (a b : Bool), (a != !b) = !(a != b)

Proof state:
⊢ ∀ (a b : Bool), (a != !b) = !a != b

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_iInter_of_finite [Finite ι] (f : ι → Set X) :
    interior (⋂ i, f i) = ⋂ i, interior (f i)

Proof state:
X : Type u
ι : Sort w
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
f : ι → Set X
⊢ interior (⋂ i, f i) = ⋂ i, interior (f i)

Tactic:
rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
@[simp] lemma preimage_inl (s : Finset (α ⊕ β)) :
    s.preimage Sum.inl Sum.inl_injective.injOn = s.toLeft

Proof state:
case h
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inl ⋯ = s.toLeft

Tactic:
ext x

Result:
case h
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft
-- Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
theorem ZeroAtFilter.add [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β]
    {l : Filter α} {f g : α → β} (hf : ZeroAtFilter l f) (hg : ZeroAtFilter l g) :
    ZeroAtFilter l (f + g)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : AddZeroClass β
inst✝ : ContinuousAdd β
l : Filter α
f g : α → β
hf : l.ZeroAtFilter f
hg : l.ZeroAtFilter g
⊢ l.ZeroAtFilter (f + g)

Tactic:
simpa using hf.add hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_append {P : α → Prop} {xs ys : Array α}
    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
      ys.attachWith P (fun a h => H a (mem_append_right xs h))

Proof state:
α : Type u_1
P : α → Prop
xs ys : Array α
H : ∀ (a : α), a ∈ xs ++ ys → P a
⊢ (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯

Tactic:
simp [attachWith, attach_append, map_pmap, pmap_append]

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem meas_lt_essInf
    (hf : IsBoundedUnder (· ≥ ·) (ae μ) f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) f) _auto✝
⊢ μ {y | f y < essInf f μ} = 0

Tactic:
simp_rw [← not_le]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) f) _auto✝
⊢ μ {y | ¬essInf f μ ≤ f y} = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) f) _auto✝
⊢ μ {y | ¬essInf f μ ≤ f y} = 0

Tactic:
exact ae_essInf_le hf

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem mem_replace {a a' : α} {b : β a} {s : Finmap β} : a' ∈ replace a b s ↔ a' ∈ s :=
  induction_on s fun s => by simp

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
s : AList β
⊢ a' ∈ replace a b ⟦s⟧ ↔ a' ∈ ⟦s⟧

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem image_rootSet [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K))
    (f : K →ₐ[R] L) : f '' p.rootSet K = p.rootSet L

Proof state:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
p : R[X]
h : Splits (algebraMap R K) p
f : K →ₐ[R] L
⊢ ⇑f '' p.rootSet K = p.rootSet L

Tactic:
classical
  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom,
    ← roots_map _ ((splits_id_iff_splits (algebraMap R K)).mpr h), map_map, f.comp_algebraMap,
    ← rootSet]

Result:
no goals

Proof state:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
p : R[X]
h : Splits (algebraMap R K) p
f : K →ₐ[R] L
⊢ ⇑f '' p.rootSet K = p.rootSet L

Tactic:
rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom,
  ← roots_map _ ((splits_id_iff_splits (algebraMap R K)).mpr h), map_map, f.comp_algebraMap,
  ← rootSet]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_subset_toFinset : hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t

Proof state:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t

Tactic:
simp only [← Finset.coe_subset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : Array α) (init : γ) :
    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
l : Array α
init : γ
⊢ foldr g init (filterMap f l) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Tactic:
simp [foldr_filterMap']

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_and_le_add_one_iff : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1

Proof state:
m n : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
@[simp]
lemma T_S_rel_smul (A : Δ m) : S • S • S • T • S • T • S • A = T⁻¹ • A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • T • S • T • S • A = T⁻¹ • A

Tactic:
simp_rw [← T_S_rel, ← smul_assoc]

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Defs.lean
theorem one_right (a : M) : SemiconjBy a 1 1

Proof state:
M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ SemiconjBy a 1 1

Tactic:
rw [SemiconjBy, mul_one, one_mul]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lemmas.lean
theorem exists_max_image [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) :
    s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
  | ⟨x, hx⟩ => by
    simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩

Proof state:
α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Tactic:
simpa only [exists_prop, Finite.mem_toFinset] using
  h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h} :
    get? m a = some (get m a h)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.val.WF
a : α
h : m.contains a = true
⊢ get? m a = some (get m a h)

Tactic:
simp_to_model using List.getValue?_eq_some_getValue

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem cons_isPath_iff {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
    (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

Tactic:
constructor <;> simp +contextual [isPath_def]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[simp]
lemma eq_nnratCast [DivisionSemiring α] [FunLike F ℚ≥0 α] [RingHomClass F ℚ≥0 α] (f : F) (q : ℚ≥0) :
    f q = q

Proof state:
F : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : FunLike F ℚ≥0 α
inst✝ : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
⊢ f q = ↑q

Tactic:
rw [← map_nnratCast f, NNRat.cast_id]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
theorem isLocallySurjective_iff_range_sheafify_eq_top' {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) :
    IsLocallySurjective J f ↔ (Subpresheaf.range f).sheafify J = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subpresheaf.sheafify J (Subpresheaf.range f) = ⊤

Tactic:
apply isLocallySurjective_iff_range_sheafify_eq_top

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_div_left : a⁻¹ / b = (b * a)⁻¹

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ a⁻¹ / b = (b * a)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem get_attach (L : List α) (i) :
    (L.attach.get i).1 = L.get ⟨i, length_attach (L := L) ▸ i.2⟩

Proof state:
α : Type u
L : List α
i : Fin L.attach.length
⊢ ↑(L.attach.get i) = L.get ⟨↑i, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem pow {x : R} (hx : IsSelfAdjoint x) (n : ℕ) : IsSelfAdjoint (x ^ n)

Proof state:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℕ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem cluster_point_of_Lindelof [LindelofSpace X] (f : Filter X) [NeBot f]
    [CountableInterFilter f] : ∃ x, ClusterPt x f

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : LindelofSpace X
f : Filter X
inst✝¹ : f.NeBot
inst✝ : CountableInterFilter f
⊢ f ≤ 𝓟 univ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : LindelofSpace X
f : Filter X
inst✝¹ : f.NeBot
inst✝ : CountableInterFilter f
⊢ ∃ x, ClusterPt x f

Tactic:
simpa using isLindelof_univ (show f ≤ 𝓟 univ by simp)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.topologicalAddGroup (hp : WithSeminorms p) : IsTopologicalAddGroup E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E

Tactic:
exact AddGroupFilterBasis.isTopologicalAddGroup _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_empty : IntegrableOn f ∅ μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
⊢ IntegrableOn f ∅ μ

Tactic:
simp [IntegrableOn, integrable_zero_measure]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem uniqueElim_preimage [Unique ι] (t : ∀ i, Set (α i)) :
    uniqueElim ⁻¹' pi univ t = t (default : ι)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
⊢ uniqueElim ⁻¹' univ.pi t = t default

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
x✝ : α default
⊢ x✝ ∈ uniqueElim ⁻¹' univ.pi t ↔ x✝ ∈ t default

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
x✝ : α default
⊢ x✝ ∈ uniqueElim ⁻¹' univ.pi t ↔ x✝ ∈ t default

Tactic:
simp [Unique.forall_iff]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem lt_rank_iff {o : Ordinal} {x : PSet} : o < rank x ↔ ∃ y ∈ x, o ≤ rank y

Proof state:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∀ ⦃y : PSet.{u_1}⦄, y ∈ x → y.rank < o) ↔ ¬∃ y ∈ x, o ≤ y.rank

Tactic:
simp

Result:
no goals

Proof state:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
rw [← not_iff_not, not_lt, rank_le_iff]

Result:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∀ ⦃y : PSet.{u_1}⦄, y ∈ x → y.rank < o) ↔ ¬∃ y ∈ x, o ≤ y.rank
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm (p : ℝ≥0∞) (hf : AEStronglyMeasurable f μ)
    (φ : α → 𝕜) : eLpNorm (φ • f) p μ ≤ eLpNorm φ ∞ μ * eLpNorm f p μ

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → E
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
x✝ : α
⊢ ‖(fun x1 x2 => x1 • x2) (φ x✝) (f x✝)‖₊ ≤ 1 * ‖φ x✝‖₊ * ‖f x✝‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : range f = ⊥ ↔ f = 0

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range f = ⊥ ↔ f = 0

Tactic:
rw [← range_le_bot_iff, le_bot_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
lemma cpow_mul_nat (x y : ℂ) (n : ℕ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x y : ℂ
n : ℕ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [mul_comm, cpow_nat_mul]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
  inter_comm, add_lt_add_iff_left]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero :
    IsNilRegular φ x ↔
    MvPolynomial.eval (b.repr x)
      ((polyCharpoly φ b).coeff (nilRank φ)) ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : Free R M
inst✝² : Module.Finite R M
b : Basis ι R L
inst✝¹ : Module.Finite R L
inst✝ : Free R L
x : L
⊢ φ.IsNilRegular x ↔ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0

Tactic:
rw [IsNilRegular, polyCharpoly_coeff_eval]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem tendsto_mul_nhds_zero_of_disjoint_cocompact {l : Filter (M × M)}
    (hl : Disjoint l (cocompact (M × M))) (h'l : l ≤ (𝓝 0).coprod (𝓝 0)) :
    Tendsto (fun x : M × M ↦ x.1 * x.2) l (𝓝 0)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
h'l : l ≤ (𝓝 0).coprod (𝓝 0)
⊢ Tendsto (fun x => x.1 * x.2) l (𝓝 0)

Tactic:
simpa [inf_eq_right.mpr h'l] using tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact hl

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Spanning.exists_isBase_subset (hS : M.Spanning S) : ∃ B, M.IsBase B ∧ B ⊆ S

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
rwa [spanning_iff_exists_isBase_subset] at hS

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem continuum_lt_lift {c : Cardinal.{u}} : 𝔠 < lift.{v} c ↔ 𝔠 < c

Proof state:
c : Cardinal.{u}
⊢ 𝔠 < lift.{v, u} c ↔ 𝔠 < c

Tactic:
rw [← lift_continuum.{v, u}, lift_lt]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
/-- The product of two arithmetic functions defines the same function as the Dirichlet convolution
of the functions defined by them. -/
lemma ArithmeticFunction.coe_mul {R : Type*} [Semiring R] (f g : ArithmeticFunction R) :
    f ⍟ g = ⇑(f * g)

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction R
⊢ ⇑f ⍟ ⇑g = ⇑(f * g)

Tactic:
simp [convolution]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem continuum_power_aleph0 : 𝔠 ^ ℵ₀ = 𝔠

Proof state:
⊢ 𝔠 ^ ℵ₀ = 𝔠

Tactic:
rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/PersistentHashMap.lean
theorem size_set {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
                           : (ks.set i k).size = (vs.set j v).size

Proof state:
α : Type u_1
β : Type u_2
ks : Array α
vs : Array β
h : ks.size = vs.size
i : Fin ks.size
j : Fin vs.size
k : α
v : β
⊢ (ks.set (↑i) k ⋯).size = (vs.set (↑j) v ⋯).size

Tactic:
simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem snoc_add (f : MultilinearMap R M M₂)
    (m : ∀ i : Fin n, M (castSucc i)) (x y : M (last n)) :
    f (snoc m (x + y)) = f (snoc m x) + f (snoc m y)

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ f (snoc m (x + y)) = f (snoc m x) + f (snoc m y)

Tactic:
simp_rw [← update_snoc_last x m (x + y), f.map_update_add, update_snoc_last]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem latticeBasis_apply (i : ChooseBasisIndex ℤ (𝓞 K)) :
    latticeBasis K i = (mixedEmbedding K) (integralBasis K i)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K) i = (mixedEmbedding K) ((integralBasis K) i)

Tactic:
simp only [latticeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
  canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem length_iota (n : Nat) : length (iota n) = n

Proof state:
n : Nat
⊢ (iota n).length = n

Tactic:
simp [iota_eq_reverse_range']

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
lemma IsNilpotent.isVirtuallyNilpotent (hG : IsNilpotent G) : IsVirtuallyNilpotent G :=
  ⟨⊤, by simpa, inferInstance⟩

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ IsNilpotent ↥⊤

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem succ_mul_binomial [DecidableEq α] (h : a ≠ b) :
    (f a + f b).succ * multinomial {a, b} f =
      (f a).succ * multinomial {a, b} (Function.update f a (f a).succ)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * multinomial {a, b} f = (f a).succ * multinomial {a, b} (Function.update f a (f a).succ)

Tactic:
rw [binomial_eq_choose h, binomial_eq_choose h, mul_comm (f a).succ, Function.update_self,
  Function.update_of_ne h.symm]

Result:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ

Tactic:
rw [succ_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.of_lo_eq_false (u v k : Nat) : ((u + k ≤ v) = False) → v ≤ u + (k-1)

Proof state:
u v k : Nat
⊢ v < u + k → v ≤ u + (k - 1)

Tactic:
omega

Result:
no goals

Proof state:
u v k : Nat
⊢ (u + k ≤ v) = False → v ≤ u + (k - 1)

Tactic:
simp

Result:
u v k : Nat
⊢ v < u + k → v ≤ u + (k - 1)
-- Mathlib/Data/Nat/Init.lean
/-- `n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`. -/
lemma not_dvd_iff_between_consec_multiples (n : ℕ) {a : ℕ} (ha : 0 < a) :
    (∃ k : ℕ, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n

Proof state:
n a : ℕ
ha : 0 < a
⊢ (∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n

Tactic:
refine
  ⟨fun ⟨k, hk1, hk2⟩ => not_dvd_of_between_consec_multiples hk1 hk2, fun han =>
    ⟨n / a, ⟨Nat.lt_of_le_of_ne (mul_div_le n a) ?_, lt_mul_div_succ _ ha⟩⟩⟩

Result:
n a : ℕ
ha : 0 < a
han : ¬a ∣ n
⊢ ¬a * (n / a) = n
-- Mathlib/Analysis/Normed/Group/Basic.lean
lemma enorm_of_nonneg (hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r

Proof state:
r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
simp [enorm, nnnorm_of_nonneg hr, ENNReal.ofReal, toNNReal, hr]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem smul_mk'_one (x : R) (m : M) : x • mk' S 1 m = mk' S x m

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
m : ↥M
⊢ x • mk' S 1 m = mk' S x m

Tactic:
rw [smul_mk', mul_one]

Result:
no goals