harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem biSup_measure_Iic [Preorder α] {s : Set α} (hsc : s.Countable)
    (hst : ∀ x : α, ∃ y ∈ s, x ≤ y) (hdir : DirectedOn (· ≤ ·) s) :
    ⨆ x ∈ s, μ (Iic x) = μ univ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ DirectedOn ((fun x1 x2 => x1 ⊆ x2) on Iic) s

Tactic:
exact directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)

Result:
no goals

Proof state:
case h.e_6.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ ⋃ i ∈ s, Iic i = univ

Tactic:
simp only [← bex_def] at hst

Result:
case h.e_6.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hst : ∀ (x : α), ∃ x_1, ∃ (_ : x_1 ∈ s), x ≤ x_1
⊢ ⋃ i ∈ s, Iic i = univ

Proof state:
case h.e_6.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hst : ∀ (x : α), ∃ x_1, ∃ (_ : x_1 ∈ s), x ≤ x_1
⊢ ⋃ i ∈ s, Iic i = univ

Tactic:
exact iUnion₂_eq_univ_iff.2 hst

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ ⨆ x ∈ s, μ (Iic x) = μ univ

Tactic:
rw [← measure_biUnion_eq_iSup hsc]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ μ (⋃ i ∈ s, Iic i) = μ univ

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ DirectedOn ((fun x1 x2 => x1 ⊆ x2) on Iic) s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ μ (⋃ i ∈ s, Iic i) = μ univ

Tactic:
congr

Result:
case h.e_6.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ ⋃ i ∈ s, Iic i = univ
-- Mathlib/Data/Prod/Basic.lean
theorem mk.inj_left {α β : Type*} (a : α) : Function.Injective (Prod.mk a : β → α × β)

Proof state:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂

Tactic:
simpa only [true_and, Prod.mk.inj_iff, eq_self_iff_true] using h

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
a : α
⊢ Function.Injective (mk a)

Tactic:
intro b₁ b₂ h

Result:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma lintegral_le_edist_mul (f : X →ᵇ ℝ≥0) (μ : Measure X) :
    (∫⁻ x, f x ∂μ) ≤ edist 0 f * (μ Set.univ) :=
  le_trans (lintegral_mono (fun x ↦ ENNReal.coe_le_coe.mpr (f.apply_le_nndist_zero x))) (by simp)

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ ∫⁻ (a : X), ↑(nndist 0 f) ∂μ ≤ edist 0 f * μ Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem infinite_even_deficient : {n : ℕ | Even n ∧ n.Deficient}.Infinite

Proof state:
case h.right
n : ℕ
⊢ n < 2 ^ (n + 1)

Tactic:
calc
  n ≤ 2 ^ n := Nat.le_of_lt n.lt_two_pow_self
  _ < 2 ^ (n + 1) := (Nat.pow_lt_pow_iff_right (Nat.one_lt_two)).mpr (lt_add_one n)

Result:
no goals

Proof state:
case h
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient} ∧ n < 2 ^ (n + 1)

Tactic:
constructor

Result:
case h.left
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient}

case h.right
n : ℕ
⊢ n < 2 ^ (n + 1)

Proof state:
case h.left
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient}

Tactic:
exact ⟨⟨2 ^ n, by ring⟩, prime_two.deficient_pow⟩

Result:
no goals

Proof state:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Deficient}, a < b

Tactic:
intro n

Result:
n : ℕ
⊢ ∃ b ∈ {n | Even n ∧ n.Deficient}, n < b

Proof state:
⊢ {n | Even n ∧ n.Deficient}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Result:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Deficient}, a < b

Proof state:
n : ℕ
⊢ 2 ^ (n + 1) = 2 ^ n + 2 ^ n

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ ∃ b ∈ {n | Even n ∧ n.Deficient}, n < b

Tactic:
use 2 ^ (n + 1)

Result:
case h
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient} ∧ n < 2 ^ (n + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_lt_self (a : Int) {b : Int} (h : 0 < b) : a - b < a :=
  calc  a + -b
    _ < a + 0 := Int.add_lt_add_left (Int.neg_neg_of_pos h) _
    _ = a

Proof state:
a b : Int
h : 0 < b
⊢ a + 0 = a

Tactic:
rw [Int.add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem unattach_attachWith {p : α → Prop} {o : Option α}
    {H : ∀ a ∈ o, p a} :
    (o.attachWith p H).unattach = o

Proof state:
α : Type u_1
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ (o.attachWith p H).unattach = o

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma AnalyticAt.meromorphicAt {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) :
    MeromorphicAt f x :=
  ⟨0, by simpa only [pow_zero, one_smul]⟩

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ 0 • f z) x

Tactic:
simpa only [pow_zero, one_smul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_mul_C_eq_of_mul_ne_zero (h : p.leadingCoeff * a ≠ 0) :
    (p * C a).natDegree = p.natDegree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ p.natDegree ∈ (p * C a).support

Tactic:
refine mem_support_iff.mpr ?_

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (p * C a).coeff p.natDegree ≠ 0

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (p * C a).natDegree = p.natDegree

Tactic:
refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ p.natDegree ∈ (p * C a).support

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (p * C a).coeff p.natDegree ≠ 0

Tactic:
rwa [coeff_mul_C]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem opNorm_zero_iff {V₁ V₂ : Type*} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂]
    {f : NormedAddGroupHom V₁ V₂} : ‖f‖ = 0 ↔ f = 0 :=
  Iff.intro
    (fun hn =>
      ext fun x =>
        norm_le_zero_iff.1
          (calc
            _ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
            _ = _

Proof state:
V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hf : f = 0
⊢ ‖f‖ = 0

Tactic:
rw [hf, opNorm_zero]

Result:
no goals

Proof state:
V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ ‖f‖ * ‖x‖ = 0

Tactic:
rw [hn, zero_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem principal_mul_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : Principal (· * ·) c.ord

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ Principal (fun x1 x2 => x1 * x2) c.ord

Tactic:
intro a b ha hb

Result:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 => x1 * x2) a b < c.ord

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c

Tactic:
exact mul_lt_of_lt hc ha hb

Result:
no goals

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 => x1 * x2) a b < c.ord

Tactic:
rw [lt_ord, card_mul] at *

Result:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card * b.card < c
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem balanced_iff_closedBall_smul : Balanced 𝕜 s ↔ Metric.closedBall (0 : 𝕜) 1 • s ⊆ s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
⊢ Balanced 𝕜 s ↔ Metric.closedBall 0 1 • s ⊆ s

Tactic:
simp [balanced_iff_smul_mem, smul_subset_iff]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem isSplittingField_X_pow_sub_one : IsSplittingField K L (X ^ (n : ℕ) - 1) :=
  { splits' := splits_X_pow_sub_one K L (mem_singleton n)
    adjoin_rootSet'

Proof state:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ^ ↑n = 1 → X ^ ↑n - 1 ≠ 0

Tactic:
exact fun _ => X_pow_sub_C_ne_zero n.pos (1 : L)

Result:
no goals

Proof state:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ (X ^ ↑n - 1).rootSet L ↔ x ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
simp only [Polynomial.map_pow, mem_singleton_iff, Multiset.mem_toFinset, exists_eq_left,
  mem_setOf_eq, Polynomial.map_X, Polynomial.map_one, Finset.mem_coe, Polynomial.map_sub]

Result:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ (X ^ ↑n - 1).rootSet L ↔ x ^ ↑n = 1

Proof state:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ (X ^ ↑n - 1).rootSet L = {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
refine Set.ext fun x => ?_

Result:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ (X ^ ↑n - 1).rootSet L ↔ x ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((X ^ ↑n - 1).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
congr

Result:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ (X ^ ↑n - 1).rootSet L = {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ (X ^ ↑n - 1).rootSet L ↔ x ^ ↑n = 1

Tactic:
simp only [mem_rootSet', map_sub, map_pow, aeval_one, aeval_X, sub_eq_zero, map_X,
  and_iff_right_iff_imp, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one]

Result:
case e_s
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ^ ↑n = 1 → X ^ ↑n - 1 ≠ 0

Proof state:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((X ^ ↑n - 1).rootSet L) = ⊤

Tactic:
rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]

Result:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((X ^ ↑n - 1).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_add :
    mpullbackWithin I I' f (V + V₁) s =
      mpullbackWithin I I' f V s + mpullbackWithin I I' f V₁ s

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V V₁ : (x : M') → TangentSpace I' x
x : M
⊢ mpullbackWithin I I' f (V + V₁) s x = (mpullbackWithin I I' f V s + mpullbackWithin I I' f V₁ s) x

Tactic:
simp [mpullbackWithin_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V V₁ : (x : M') → TangentSpace I' x
⊢ mpullbackWithin I I' f (V + V₁) s = mpullbackWithin I I' f V s + mpullbackWithin I I' f V₁ s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V V₁ : (x : M') → TangentSpace I' x
x : M
⊢ mpullbackWithin I I' f (V + V₁) s x = (mpullbackWithin I I' f V s + mpullbackWithin I I' f V₁ s) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_eq_foldl_reverse (l : Vector α n) (f : α → β → β) (b) :
    l.foldr f b = l.reverse.foldl (fun x y => f y x) b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β → β
b : β
⊢ foldr f b l = foldl (fun x y => f y x) b l.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean
@[simp] lemma sup_eq_zero : s.sup f = 0 ↔ ∀ i ∈ s, f i = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedAddCommMonoid α
inst✝ : CanonicallyOrderedAdd α
s : Finset ι
f : ι → α
⊢ s.sup f = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp [← bot_eq_zero']

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_self_left {x : V} (hx : x ≠ 0) : o.oangle (-x) x = π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
⊢ o.oangle (-x) x = ↑π

Tactic:
simp [oangle_neg_left, hx]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.separating_iff_T1 (hp : WithSeminorms p) :
    (∀ x, x ≠ 0 → ∃ i, p i x ≠ 0) ↔ T1Space 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
⊢ (∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0) ↔ T1Space E

Tactic:
refine ⟨WithSeminorms.T1_of_separating hp, ?_⟩

Result:
𝕜 : 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
⊢ T1Space E → ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0

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
a✝ : T1Space E
⊢ ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0

Tactic:
exact WithSeminorms.separating_of_T1 hp

Result:
no goals

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
⊢ T1Space E → ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0

Tactic:
intro

Result:
𝕜 : 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
a✝ : T1Space E
⊢ ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_factorial_mul {n p : ℕ} (hp : p.Prime) :
    emultiplicity p (p * n)! = emultiplicity p n ! + n

Proof state:
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p n ! + ↑n + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + ↑n

Tactic:
rw [add_comm, add_assoc]

Result:
no goals

Proof state:
n p : ℕ
hp : Prime p
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + ↑n

Tactic:
induction' n with n ih

Result:
case zero
p : ℕ
hp : Prime p
⊢ emultiplicity p (p * 0)! = emultiplicity p 0! + ↑0

case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + ↑(n + 1)

Proof state:
case zero
p : ℕ
hp : Prime p
⊢ emultiplicity p (p * 0)! = emultiplicity p 0! + ↑0

Tactic:
simp

Result:
no goals

Proof state:
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + ↑(n + 1)

Tactic:
simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
cast_add, cast_one, ← add_assoc]

Result:
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p n ! + ↑n + emultiplicity p (n + 1) + 1 = emultiplicity p (n + 1) + emultiplicity p n ! + ↑n + 1

Proof state:
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p n ! + ↑n + emultiplicity p (n + 1) + 1 = emultiplicity p (n + 1) + emultiplicity p n ! + ↑n + 1

Tactic:
congr 1

Result:
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p n ! + ↑n + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + ↑n
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_mul_param_iff (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f

Tactic:
simpa [mul_comm k] using superpolynomialDecay_param_mul_iff f hk

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_sub_zsmul (a b : α) (m : ℤ) : toIocDiv hp a (b - m • p) = toIocDiv hp a b - m

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem ContDiffOn.continuousOn_iteratedDerivWithin
    {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffOn 𝕜 n f s)
    (hmn : m ≤ n) (hs : UniqueDiffOn 𝕜 s) : ContinuousOn (iteratedDerivWithin m f s) s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m ≤ n
hs : UniqueDiffOn 𝕜 s
⊢ ContinuousOn (iteratedDerivWithin m f s) s

Tactic:
simpa only [iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff] using
  h.continuousOn_iteratedFDerivWithin hmn hs

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_nhds {f : Filter α} {u : α → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞) :
    Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, u x ∈ Icc (a - ε) (a + ε)

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)

Tactic:
simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem IsBigOWith.rpow (h : IsBigOWith c l f g) (hc : 0 ≤ c) (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) :
    IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r

Proof state:
case a
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Tactic:
filter_upwards [hg, h.bound] with x hgx hx

Result:
case h
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Proof state:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (c * |g x|) ^ r = c ^ r * |g x ^ r|

Tactic:
rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

Result:
no goals

Proof state:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r

Tactic:
apply IsBigOWith.of_bound

Result:
case a
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Proof state:
case h
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Tactic:
calc
  |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
  _ ≤ (c * |g x|) ^ r := rpow_le_rpow (abs_nonneg _) hx hr
  _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem restrict_dirac' (hs : MeasurableSet s) [Decidable (a ∈ s)] :
    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0

Proof state:
case pos.hs
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s

Tactic:
rw [ae_dirac_iff] <;> assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (dirac a).restrict s = if a ∈ s then dirac a else 0

Tactic:
split_ifs with has

Result:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_not_mem has]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a

Tactic:
apply restrict_eq_self_of_ae_mem

Result:
case pos.hs
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range_ne_empty_iff {n : Nat} : range n ≠ #[] ↔ n ≠ 0

Proof state:
n : Nat
⊢ range n ≠ #[] ↔ n ≠ 0

Tactic:
cases n <;> simp

Result:
no goals