harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/EGauge.lean
lemma div_le_egauge_closedBall (r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (closedBall 0 r) x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖(fun x => c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
rw [enorm_smul]

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖c‖ₑ * ‖y‖ₑ / ↑r ≤ ‖c‖ₑ

Proof state:
case intro.intro.h.bc
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖y‖ₑ ≤ ↑r

Tactic:
rwa [enorm_le_coe]

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : y ∈ closedBall 0 ↑r
⊢ ‖(fun x => c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
rw [mem_closedBall_zero_iff, ← coe_nnnorm, NNReal.coe_le_coe] at hy

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖(fun x => c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Proof state:
case intro.intro.h
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * ↑r

Tactic:
gcongr

Result:
case intro.intro.h.bc
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖y‖ₑ ≤ ↑r

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
x : E
⊢ ∀ (c : 𝕜), x ∈ c • closedBall 0 ↑r → ‖x‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
rintro c ⟨y, hy, rfl⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : y ∈ closedBall 0 ↑r
⊢ ‖(fun x => c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖c‖ₑ * ‖y‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
apply ENNReal.div_le_of_le_mul

Result:
case intro.intro.h
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * ↑r

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
x : E
⊢ ‖x‖ₑ / ↑r ≤ egauge 𝕜 (closedBall 0 ↑r) x

Tactic:
rw [le_egauge_iff]

Result:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
x : E
⊢ ∀ (c : 𝕜), x ∈ c • closedBall 0 ↑r → ‖x‖ₑ / ↑r ≤ ‖c‖ₑ
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_nonneg {n : ℕ} : 0 ≤ Λ n

Proof state:
case neg
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0

Tactic:
split_ifs

Result:
case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑n.minFac

case neg
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0

Proof state:
case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑n.minFac

Tactic:
exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))

Result:
no goals

Proof state:
n : ℕ
⊢ 0 ≤ Λ n

Tactic:
rw [vonMangoldt_apply]

Result:
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_apply_of_mem_supported {l : α →₀ R} {s : Finset α}
    (hs : l ∈ supported R R (↑s : Set α)) : linearCombination R v l = s.sum fun i => l i • v i :=
  Finset.sum_subset hs fun x _ hxg =>
    show l x • v x = 0 by rw [not_mem_support_iff.1 hxg, zero_smul]

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
l : α →₀ R
s : Finset α
hs : l ∈ supported R R ↑s
x : α
x✝ : x ∈ s
hxg : x ∉ l.support
⊢ l x • v x = 0

Tactic:
rw [not_mem_support_iff.1 hxg, zero_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Reflection.lean
/-- See also `Module.Dual.eq_of_preReflection_mapsTo'` for a variant of this lemma which
applies when `Φ` does not span.

This rather technical-looking lemma exists because it is exactly what is needed to establish various
uniqueness results for root data / systems. One might regard this lemma as lying at the boundary of
linear algebra and combinatorics since the finiteness assumption is the key. -/
lemma Dual.eq_of_preReflection_mapsTo [CharZero R] [NoZeroSMulDivisors R M]
    {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hΦ₂ : span R Φ = ⊤) {f g : Dual R M}
    (hf₁ : f x = 2) (hf₂ : MapsTo (preReflection x f) Φ Φ)
    (hg₁ : g x = 2) (hg₂ : MapsTo (preReflection x g) Φ Φ) :
    f = g

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : IsOfFinOrder u
n : ℕ
hn₀ : 0 < n
hn₁ : ↑(u ^ n) = LinearMap.id
⊢ f = g

Tactic:
simpa [hn₁, hn₀.ne', hx, sub_eq_zero] using hu n

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toOrderIso_injective : Injective (toOrderIso : _ → α ≃o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f g : α ≃*o β
h : f.toOrderIso = g.toOrderIso
⊢ ∀ (a : α), f a = g a

Tactic:
convert DFunLike.ext_iff.1 h using 0

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_add_cond_compl_eq (hms : MeasurableSet s) (μ : Measure Ω) [IsFiniteMeasure μ] :
    μ[t|s] * μ s + μ[t|sᶜ] * μ sᶜ = μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] * μ s + μ[t | sᶜ] * μ sᶜ = μ t

Tactic:
rw [cond_mul_eq_inter hms, cond_mul_eq_inter hms.compl, Set.inter_comm _ t,
  Set.inter_comm _ t]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ (t ∩ s) + μ (t ∩ sᶜ) = μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ (t ∩ s) + μ (t ∩ sᶜ) = μ t

Tactic:
exact measure_inter_add_diff t hms

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
lemma le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x)

Proof state:
x c : ℝ
hc : 0 < c
⊢ c * x ≤ rexp (c * x)

Tactic:
calc c * x
_ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
_ ≤ _ := Real.add_one_le_exp (c * x)

Result:
no goals

Proof state:
x c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * rexp (c * x)

Tactic:
rw [le_inv_mul_iff₀ hc]

Result:
x c : ℝ
hc : 0 < c
⊢ c * x ≤ rexp (c * x)
-- Mathlib/NumberTheory/Pell.lean
theorem subsingleton {a b : Solution₁ d} (ha : IsFundamental a) (hb : IsFundamental b) : a = b

Proof state:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a = b

Tactic:
refine Solution₁.ext hx ?_

Result:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a.y = b.y

Proof state:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a.y = b.y

Tactic:
have : d * a.y ^ 2 = d * b.y ^ 2 := by rw [a.prop_y, b.prop_y, hx]

Result:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
this : d * a.y ^ 2 = d * b.y ^ 2
⊢ a.y = b.y

Proof state:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
this : d * a.y ^ 2 = d * b.y ^ 2
⊢ a.y = b.y

Tactic:
exact (sq_eq_sq₀ ha.2.1.le hb.2.1.le).mp (Int.eq_of_mul_eq_mul_left ha.d_pos.ne' this)

Result:
no goals

Proof state:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ d * a.y ^ 2 = d * b.y ^ 2

Tactic:
rw [a.prop_y, b.prop_y, hx]

Result:
no goals

Proof state:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
⊢ a = b

Tactic:
have hx := le_antisymm (ha.2.2 hb.1) (hb.2.2 ha.1)

Result:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a = b
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma leftRightHomologyComparison'_eq_liftH :
    leftRightHomologyComparison' h₁ h₂ =
      h₂.liftH (h₁.descH (h₁.i ≫ h₂.p) (by simp))
        (by rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]) := rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₁.i ≫ h₂.p = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0

Tactic:
rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]

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

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a fallback : α
⊢ m.getKeyD a fallback = (m.getKey? a).getD fallback

Tactic:
simp_to_model using List.getKeyD_eq_getKey?

Result:
no goals
-- Mathlib/Algebra/Lie/EngelSubalgebra.lean
@[simp]
lemma engel_zero : engel R (0 : L) = ⊤

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ engel R 0 = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ⊤ ≤ engel R 0

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ⊤ ≤ engel R 0

Tactic:
rintro x -

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ engel R 0

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, (0 ^ n) x = 0

Tactic:
use 1

Result:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (0 ^ 1) x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ engel R 0

Tactic:
rw [mem_engel_iff, LieHom.map_zero]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, (0 ^ n) x = 0

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (0 ^ 1) x = 0

Tactic:
simp only [pow_one, LinearMap.zero_apply]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
    deriv (fun z => z ^ p * (1 + ε z))
      =ᶠ[atTop] fun z => p * z ^ (p-1) * (1 + ε z) - z ^ (p-1) / (log z ^ 2) := calc
  deriv (fun x => x ^ p * (1 + ε x))
    =ᶠ[atTop] fun x => deriv (· ^ p) x * (1 + ε x) + x ^ p * deriv (1 + ε ·) x

Proof state:
case h
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
⊢ deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x =
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
simp [hderiv, Real.deriv_rpow_const (Or.inl <| by positivity), neg_div, sub_eq_add_neg]

Result:
no goals

Proof state:
case h.hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x ^ p) x

Tactic:
exact differentiableAt_rpow_const_of_ne _ (by positivity)

Result:
no goals

Proof state:
case h.hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => 1 + ε x) x

Tactic:
exact differentiableAt_one_add_smoothingFn hx

Result:
no goals

Proof state:
case h
p x : ℝ
hx : 1 < x
⊢ deriv (fun x => x ^ p * (1 + ε x)) x = deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x

Tactic:
rw [deriv_mul]

Result:
case h.hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x ^ p) x

case h.hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => 1 + ε x) x

Proof state:
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
⊢ ?m.951607 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2

Tactic:
simp [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]

Result:
no goals

Proof state:
p : ℝ
⊢ (fun x => p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)) =ᶠ[atTop] fun x =>
    p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Result:
case h
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2

Proof state:
p x : ℝ
hx : 1 < x
⊢ x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
p x : ℝ
hx : 0 < x
⊢ 0 < ?m.953938

Tactic:
positivity

Result:
no goals

Proof state:
p : ℝ
⊢ (fun x => deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x) =ᶠ[atTop] fun x =>
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_add_smoothingFn]
  with x hx hderiv

Result:
case h
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
⊢ deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x =
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)

Proof state:
p : ℝ
⊢ (deriv fun x => x ^ p * (1 + ε x)) =ᶠ[atTop] fun x =>
    deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
p x : ℝ
hx : 1 < x
⊢ deriv (fun x => x ^ p * (1 + ε x)) x = deriv (fun x => x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x => 1 + ε x) x
-- Mathlib/Data/ENNReal/Inv.lean
theorem le_div_iff_mul_le (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞ ∨ c ≠ ∞) :
    a ≤ c / b ↔ a * b ≤ c

Proof state:
case coe.inr
a b✝ c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
rw [← ENNReal.mul_le_mul_right hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

Result:
no goals

Proof state:
case coe.inr
a b✝ c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
rw [← coe_ne_zero] at hb

Result:
case coe.inr
a b✝ c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Proof state:
case top
a b c : ℝ≥0∞
h0 : ⊤ ≠ 0 ∨ c ≠ 0
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ⊤ ↔ a * ⊤ ≤ c

Tactic:
lift c to ℝ≥0 using ht.neg_resolve_left rfl

Result:
case top.intro
a b : ℝ≥0∞
c : ℝ≥0
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a ≤ ↑c / ⊤ ↔ a * ⊤ ≤ ↑c

Proof state:
a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
induction' b with b

Result:
case top
a b c : ℝ≥0∞
h0 : ⊤ ≠ 0 ∨ c ≠ 0
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ⊤ ↔ a * ⊤ ≤ c

case coe
a b✝ c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Proof state:
case coe.inl
a b c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

Tactic:
have hc : c ≠ 0 := h0.neg_resolve_left rfl

Result:
case coe.inl
a b c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
hc : c ≠ 0
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

Proof state:
case top.intro
a b : ℝ≥0∞
c : ℝ≥0
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a ≤ ↑c / ⊤ ↔ a * ⊤ ≤ ↑c

Tactic:
rw [div_top, nonpos_iff_eq_zero]

Result:
case top.intro
a b : ℝ≥0∞
c : ℝ≥0
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a = 0 ↔ a * ⊤ ≤ ↑c

Proof state:
case coe
a b✝ c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Result:
case coe.inl
a b c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

case coe.inr
a b✝ c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Proof state:
case top.intro
a b : ℝ≥0∞
c : ℝ≥0
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a = 0 ↔ a * ⊤ ≤ ↑c

Tactic:
rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]

Result:
no goals

Proof state:
case coe.inl
a b c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
hc : c ≠ 0
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

Tactic:
simp [div_zero hc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem exists_upperSemicontinuous_le_lintegral_le (f : α → ℝ≥0) (int_f : (∫⁻ x, f x ∂μ) ≠ ∞)
    {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0, (∀ x, g x ≤ f x) ∧ UpperSemicontinuous g ∧
      (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ∫⁻ (x : α), ↑(f x) ∂μ < ∫⁻ (x : α), ↑(f x) ∂μ + ε / 2
⊢ ∃ fs, (∀ (x : α), fs x ≤ f x) ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2

Tactic:
conv_rhs at this => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), ↑(f x) ∂μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ ↑(f x)), (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) + ε / 2
⊢ ∃ fs, (∀ (x : α), fs x ≤ f x) ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), fs x ≤ f x
int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), ↑(fs x) ∂μ ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ fs x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(fs x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

Tactic:
refine ⟨g, fun x => (g_le_fs x).trans (fs_le_f x), gcont, ?_⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), fs x ≤ f x
int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), ↑(fs x) ∂μ ≠ ⊤
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ fs x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(fs x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem nhdsGT_eq_bot_iff {a : α} : 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Tactic:
by_cases ha : IsTop a

Result:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : IsTop a
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Proof state:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ b, a < b
⊢ 𝓝[>] a = ⊥ ↔ ∃ b, a ⋖ b

Tactic:
simp only [(nhdsGT_basis_of_exists_gt ha).eq_bot_iff, covBy_iff_Ioo_eq]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ ∃ b, a ⋖ b

Tactic:
rw [isTop_iff_isMax, not_isMax_iff] at ha

Result:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ b, a < b
⊢ 𝓝[>] a = ⊥ ↔ ∃ b, a ⋖ b

Proof state:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : IsTop a
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Tactic:
simp [ha, ha.isMax.Ioi_eq]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Tactic:
simp only [ha, false_or]

Result:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ ∃ b, a ⋖ b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_push {a : α} {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
    (l.push a).attachWith P H =
      (l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩

Proof state:
case mk
α : Type u_1
a : α
P : α → Prop
l : Array α
H : ∀ (x : α), x ∈ { toArray := l, size_toArray := ⋯ }.push a → P x
⊢ ({ toArray := l, size_toArray := ⋯ }.push a).attachWith P H =
    ({ toArray := l, size_toArray := ⋯ }.attachWith P ⋯).push ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.16923
n : Nat
a : α
l : Vector α n
P : α → Prop
x : α
h : x ∈ l
H : ∀ (x : α), x ∈ l ∨ x = a → P x
⊢ P x

Tactic:
exact H x (.inl h)

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l.push a → P x
⊢ (l.push a).attachWith P H = (l.attachWith P ⋯).push ⟨a, ⋯⟩

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a : α
P : α → Prop
l : Array α
H : ∀ (x : α), x ∈ { toArray := l, size_toArray := ⋯ }.push a → P x
⊢ ({ toArray := l, size_toArray := ⋯ }.push a).attachWith P H =
    ({ toArray := l, size_toArray := ⋯ }.attachWith P ⋯).push ⟨a, ⋯⟩

Proof state:
α : Type ?u.16923
n : Nat
a : α
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l.push a → P x
x : α
h : x ∈ l
⊢ P x

Tactic:
simp at H

Result:
α : Type ?u.16923
n : Nat
a : α
l : Vector α n
P : α → Prop
x : α
h : x ∈ l
H : ∀ (x : α), x ∈ l ∨ x = a → P x
⊢ P x

Proof state:
α : Type ?u.16923
n : Nat
a : α
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l.push a → P x
⊢ a ∈ l.push a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma toCLM_apply_single_apply [DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n} (a : A) :
    (toCLM M) (equiv _ |>.symm <| Pi.single j a) i = M i j * a

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq n
M : CStarMatrix m n A
i : m
j : n
a : A
⊢ (toCLM M) ((equiv (n → A)).symm (Pi.single j a)) i = M i j * a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_of_right_le_one {n : ℕ} (hn : n ≤ 1) (b : ℕ) : clog b n = 0

Proof state:
n : ℕ
hn : n ≤ 1
b : ℕ
⊢ clog b n = 0

Tactic:
rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.2.not_le hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ

Proof state:
m n : Nat
h : m + 1 ≤ n + 1
i : Fin m
⊢ castLE h i.succ = (castLE ⋯ i).succ

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get_eq_iff : List.get l n = x ↔ l.get? n.1 = some x

Proof state:
α✝ : Type u_1
l : List α✝
n : Fin l.length
x : α✝
⊢ l.get n = x ↔ l.get? ↑n = some x

Tactic:
simp

Result:
no goals