harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean
theorem eLpNorm_trim_ae (hm : m ≤ m0) {f : α → E} (hf : AEStronglyMeasurable[m] f (μ.trim hm)) :
    eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ eLpNorm (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ

Tactic:
exact eLpNorm_trim hm hf.stronglyMeasurable_mk

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
rw [eLpNorm_congr_ae hf.ae_eq_mk, eLpNorm_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk)]

Result:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ eLpNorm (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma exists_isDynCoverOf_of_isCompact_uniformContinuous [UniformSpace X] {T : X → X} {F : Set X}
    (F_comp : IsCompact F) (h : UniformContinuous T) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) :
    ∃ s : Finset X, IsDynCoverOf T F U n s

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
uni_ite : dynEntourage T U n ∈ 𝓤 X
open_cover : X → Set X := fun x => ball x (dynEntourage T U n)
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
obtain ⟨s, _, s_cover⟩ := IsCompact.elim_nhds_subcover F_comp open_cover
  (fun (x : X) _ ↦ ball_mem_nhds x uni_ite)

Result:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
uni_ite : dynEntourage T U n ∈ 𝓤 X
open_cover : X → Set X := fun x => ball x (dynEntourage T U n)
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, open_cover x
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Proof state:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
uni_ite : dynEntourage T U n ∈ 𝓤 X
open_cover : X → Set X := fun x => ball x (dynEntourage T U n)
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, open_cover x
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
exact ⟨s, s_cover⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
have uni_ite := dynEntourage_mem_uniformity h U_uni n

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
uni_ite : dynEntourage T U n ∈ 𝓤 X
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
uni_ite : dynEntourage T U n ∈ 𝓤 X
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
let open_cover := fun x : X ↦ ball x (dynEntourage T U n)

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
uni_ite : dynEntourage T U n ∈ 𝓤 X
open_cover : X → Set X := fun x => ball x (dynEntourage T U n)
⊢ ∃ s, IsDynCoverOf T F U n ↑s
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_monic_mul {p q : R[X]} (hp : Monic p) :
    leadingCoeff (p * q) = leadingCoeff q

Proof state:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p * 0).leadingCoeff = leadingCoeff 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
rcases eq_or_ne q 0 with (rfl | H)

Result:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p * 0).leadingCoeff = leadingCoeff 0

case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]

Result:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hp.leadingCoeff, one_mul, Ne, leadingCoeff_eq_zero]

Result:
no goals
-- Mathlib/Topology/Baire/Lemmas.lean
theorem dense_biInter_of_isOpen {S : Set α} {f : α → Set X} (ho : ∀ s ∈ S, IsOpen (f s))
    (hS : S.Countable) (hd : ∀ s ∈ S, Dense (f s)) : Dense (⋂ s ∈ S, f s)

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense (⋂₀ (f '' S))

Tactic:
refine dense_sInter_of_isOpen ?_ (hS.image _) ?_ <;> rwa [forall_mem_image]

Result:
no goals

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense (⋂ s ∈ S, f s)

Tactic:
rw [← sInter_image]

Result:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense (⋂₀ (f '' S))
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem sum_mongePointVSubFaceCentroidWeightsWithCircumcenter {n : ℕ} {i₁ i₂ : Fin (n + 3)}
    (h : i₁ ≠ i₂) : ∑ i, mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ i : PointsWithCircumcenterIndex (n + 2), mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0

Tactic:
rw [mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h]

Result:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ i : PointsWithCircumcenterIndex (n + 2),
      (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i =
    0

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ 1 - ∑ x : PointsWithCircumcenterIndex (n + 2), centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x = 0

Tactic:
rw [sum_centroidWeightsWithCircumcenter, sub_self]

Result:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ {i₁, i₂}ᶜ.Nonempty

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ {i₁, i₂}ᶜ.Nonempty

Tactic:
simp [← card_pos, card_compl, h]

Result:
no goals

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ i : PointsWithCircumcenterIndex (n + 2),
      (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i =
    0

Tactic:
simp_rw [Pi.sub_apply, sum_sub_distrib, sum_mongePointWeightsWithCircumcenter]

Result:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ 1 - ∑ x : PointsWithCircumcenterIndex (n + 2), centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x = 0
-- Mathlib/RepresentationTheory/Rep.lean
theorem unit_iso_comm (V : Rep k G) (g : G) (x : V) :
    unitIsoAddEquiv ((V.ρ g).toFun x) = ((ofModuleMonoidAlgebra.obj
      (toModuleMonoidAlgebra.obj V)).ρ g).toFun (unitIsoAddEquiv x)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : ↑V.V
⊢ unitIsoAddEquiv ((V.ρ g).toFun x) =
    ((ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)).ρ g).toFun (unitIsoAddEquiv x)

Tactic:
dsimp [unitIsoAddEquiv, ofModuleMonoidAlgebra, toModuleMonoidAlgebra]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : ↑V.V
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm ((V.ρ g) x)) =
    ((Representation.ofModule V.ρ.asModule) g)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm x))

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : ↑V.V
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm ((V.ρ g) x)) =
    ((Representation.ofModule V.ρ.asModule) g)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm (V.ρ.asModuleEquiv.symm x))

Tactic:
simp only [AddEquiv.apply_eq_iff_eq, AddEquiv.apply_symm_apply,
  Representation.asModuleEquiv_symm_map_rho, Representation.ofModule_asModule_act]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
The Krull dimension is the supremum of the elements' coheights.

If `α` is `Nonempty`, then `krullDim_eq_iSup_coheight_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
-/
lemma krullDim_eq_iSup_coheight : krullDim α = ⨆ (a : α), ↑(coheight a)

Proof state:
case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ krullDim α = ⨆ a, ↑(coheight a)

Tactic:
rw [krullDim_eq_bot, ciSup_of_empty]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⨆ a, ↑(coheight a)

Tactic:
cases isEmpty_or_nonempty α with
| inl h => rw [krullDim_eq_bot, ciSup_of_empty]
| inr h => rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ krullDim α = ⨆ a, ↑(coheight a)

Tactic:
rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_three_mul : sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
have h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2 := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3

Proof state:
x : ℂ
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
have h1 : x + 2 * x = 3 * x := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
rw [← h1, sin_add x (2 * x)]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * cos (2 * x) + cos x * sin (2 * x) = 3 * sin x - 4 * sin x ^ 3

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * cos (2 * x) + cos x * sin (2 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
simp only [cos_two_mul, sin_two_mul, cos_sq']

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + 2 * sin x * (1 - sin x ^ 2) = 3 * sin x - 4 * sin x ^ 3

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
rw [h2, cos_sq']

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + 2 * sin x * (1 - sin x ^ 2) = 3 * sin x - 4 * sin x ^ 3
-- Mathlib/CategoryTheory/Subobject/Comma.lean
theorem lift_projectSubobject [HasFiniteLimits C] [PreservesFiniteLimits T]
    {A : StructuredArrow S T} :
    ∀ (P : Subobject A) {q} (hq : q ≫ T.map (projectSubobject P).arrow = A.hom),
      liftSubobject (projectSubobject P) hq = P :=
  Subobject.ind _
    (by
      intro P f hf q hq
      fapply Subobject.mk_eq_mk_of_comm
      · fapply isoMk
        · exact Subobject.underlyingIso _
        · exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)
      · exact ext _ _ (by dsimp; simp))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (q ≫ T.map (Subobject.underlyingIso f.right).hom) ≫ T.map f.right = P.hom ≫ T.map f.right

Tactic:
simpa [← T.map_comp] using hq

Result:
no goals

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (isoMk (Subobject.underlyingIso (MonoOver.mk' f).arrow.right) ⋯).hom ≫ f =
    homMk (projectSubobject (Subobject.mk f)).arrow hq

Tactic:
exact ext _ _ (by dsimp; simp)

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem properDivisors_zero : properDivisors 0 = ∅

Proof state:
⊢ properDivisors 0 = ∅

Tactic:
ext

Result:
case h
a✝ : ℕ
⊢ a✝ ∈ properDivisors 0 ↔ a✝ ∈ ∅

Proof state:
case h
a✝ : ℕ
⊢ a✝ ∈ properDivisors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem exp_mul (x y : ℝ) : exp (x * y) = exp x ^ y

Proof state:
x y : ℝ
⊢ rexp (x * y) = rexp x ^ y

Tactic:
rw [rpow_def_of_pos (exp_pos _), log_exp]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma cotangentComplexAux_zero_iff {P : PreSubmersivePresentation R S} (x : P.ker) :
    P.cotangentComplexAux (Cotangent.mk x) = 0 ↔
      ∀ i : P.rels, (aeval P.val) (pderiv (P.map i) x.val) = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : PreSubmersivePresentation R S
x : ↥P.ker
⊢ (∀ (x_1 : P.rels), P.cotangentComplexAux (Cotangent.mk x) x_1 = 0 x_1) ↔
    ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
simp_rw [cotangentComplexAux_apply, Pi.zero_apply]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : PreSubmersivePresentation R S
x : ↥P.ker
⊢ P.cotangentComplexAux (Cotangent.mk x) = 0 ↔ ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
rw [funext_iff]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : PreSubmersivePresentation R S
x : ↥P.ker
⊢ (∀ (x_1 : P.rels), P.cotangentComplexAux (Cotangent.mk x) x_1 = 0 x_1) ↔
    ∀ (i : P.rels), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem ZMod.exponent (n : ℕ) : AddMonoid.exponent (ZMod n) = n

Proof state:
n : ℕ
⊢ AddMonoid.exponent (ZMod n) = n

Tactic:
rw [IsAddCyclic.exponent_eq_card, Nat.card_zmod]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_one_add_smoothingFn_pos : ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε n

Proof state:
case h
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + ε x

Tactic:
show 0 < 1 + 1 / log x

Result:
case h
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + 1 / log x

Proof state:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ ∀ᶠ (x : ℝ) in atTop, (fun n => 0 < 1 + ε n) x

Tactic:
filter_upwards [h₁ (by norm_num : (0 : ℝ) < 1/2), eventually_gt_atTop 1] with x _ hx'

Result:
case h
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
⊢ 0 < 1 + ε x

Proof state:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n

Tactic:
have h₁ := isLittleO_smoothingFn_one

Result:
h₁ : ε =o[atTop] fun x => 1
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n

Proof state:
case h
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + 1 / log x

Tactic:
positivity

Result:
no goals

Proof state:
h₁ : ε =o[atTop] fun x => 1
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n

Tactic:
rw [isLittleO_iff] at h₁

Result:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n

Proof state:
case h
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
⊢ 0 < 1 + ε x

Tactic:
have : 0 < log x := Real.log_pos hx'

Result:
case h
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + ε x

Proof state:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n

Tactic:
refine Eventually.natCast_atTop (p := fun n => 0 < 1 + ε n) ?_

Result:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ ∀ᶠ (x : ℝ) in atTop, (fun n => 0 < 1 + ε n) x
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem mk_le_of_comm {B A : C} {X : Subobject B} {f : A ⟶ B} [Mono f] (g : A ⟶ (X : C))
    (w : g ≫ X.arrow = f) : mk f ≤ X :=
  le_of_comm ((underlyingIso f).hom ≫ g) <| by simp [w]

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
g : A ⟶ underlying.obj X
w : g ≫ X.arrow = f
⊢ ((underlyingIso f).hom ≫ g) ≫ X.arrow = (mk f).arrow

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
@[simp] lemma find_le_iff (h : ∃ n : ℕ, p n) (n : ℕ) : Nat.find h ≤ n ↔ ∃ m ≤ n, p m

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ Nat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m

Tactic:
simp only [exists_prop, ← Nat.lt_succ_iff, find_lt_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isCircuit_copy {u u'} (p : G.Walk u u) (hu : u = u') :
    (p.copy hu hu).IsCircuit ↔ p.IsCircuit

Proof state:
V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
⊢ (p.copy hu hu).IsCircuit ↔ p.IsCircuit

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit

Proof state:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma hurwitzZetaEven_def_of_ne_or_ne {a : UnitAddCircle} {s : ℂ} (h : a ≠ 0 ∨ s ≠ 0) :
    hurwitzZetaEven a s = completedHurwitzZetaEven a s / Gammaℝ s

Proof state:
case inl
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
⊢ Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ

Tactic:
rw [Function.update_of_ne h']

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
⊢ Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ

Tactic:
rcases ne_or_eq s 0 with h' | rfl

Result:
case inl
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
⊢ Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ

case inr
a : UnitAddCircle
h : a ≠ 0 ∨ 0 ≠ 0
⊢ Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) 0 =
    completedHurwitzZetaEven a 0 / Gammaℝ 0

Proof state:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
⊢ hurwitzZetaEven a s = completedHurwitzZetaEven a s / s.Gammaℝ

Tactic:
rw [hurwitzZetaEven]

Result:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
⊢ Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ

Proof state:
case inr
a : UnitAddCircle
h : a ≠ 0 ∨ 0 ≠ 0
⊢ Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) 0 =
    completedHurwitzZetaEven a 0 / Gammaℝ 0

Tactic:
simpa [Gammaℝ] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn'_congr [Monad m] {as bs : Array α} (w : as = bs)
    {b b' : β} (hb : b = b')
    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
    forIn' as b f = forIn' bs b' g

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toList✝¹ : List α
f : (a' : α) → a' ∈ { toList := toList✝¹ } → β → m (ForInStep β)
toList✝ : List α
g : (a' : α) → a' ∈ { toList := toList✝ } → β → m (ForInStep β)
w✝ : { toList := toList✝¹ } = { toList := toList✝ }
w : toList✝¹ = toList✝
h : ∀ (a : α) (m_1 : a ∈ toList✝) (b : β), f a ⋯ b = g a ⋯ b
⊢ (forIn' toList✝¹ b fun a m b => f a ⋯ b) = forIn' toList✝ b' fun a m b => g a ⋯ b

Tactic:
exact List.forIn'_congr w hb h

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as bs : Array α
w : as = bs
b b' : β
hb : b = b'
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' as b f = forIn' bs b' g

Tactic:
cases as <;> cases bs

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toList✝¹ : List α
f : (a' : α) → a' ∈ { toList := toList✝¹ } → β → m (ForInStep β)
toList✝ : List α
g : (a' : α) → a' ∈ { toList := toList✝ } → β → m (ForInStep β)
w : { toList := toList✝¹ } = { toList := toList✝ }
h : ∀ (a : α) (m_1 : a ∈ { toList := toList✝ }) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' { toList := toList✝¹ } b f = forIn' { toList := toList✝ } b' g

Proof state:
m✝ : Type ?u.27319 → Type ?u.27243
α : Type ?u.27248
β : Type ?u.27319
inst✝ : Monad m✝
as bs : Array α
w : as = bs
b✝ b' : β
hb : b✝ = b'
f : (a' : α) → a' ∈ as → β → m✝ (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m✝ (ForInStep β)
a : α
m : a ∈ bs
b : β
⊢ a ∈ as

Tactic:
simpa [w] using m

Result:
no goals

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toList✝¹ : List α
f : (a' : α) → a' ∈ { toList := toList✝¹ } → β → m (ForInStep β)
toList✝ : List α
g : (a' : α) → a' ∈ { toList := toList✝ } → β → m (ForInStep β)
w : { toList := toList✝¹ } = { toList := toList✝ }
h : ∀ (a : α) (m_1 : a ∈ { toList := toList✝ }) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' { toList := toList✝¹ } b f = forIn' { toList := toList✝ } b' g

Tactic:
simp only [mk.injEq, mem_toArray, List.forIn'_toArray] at w h ⊢

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toList✝¹ : List α
f : (a' : α) → a' ∈ { toList := toList✝¹ } → β → m (ForInStep β)
toList✝ : List α
g : (a' : α) → a' ∈ { toList := toList✝ } → β → m (ForInStep β)
w✝ : { toList := toList✝¹ } = { toList := toList✝ }
w : toList✝¹ = toList✝
h : ∀ (a : α) (m_1 : a ∈ toList✝) (b : β), f a ⋯ b = g a ⋯ b
⊢ (forIn' toList✝¹ b fun a m b => f a ⋯ b) = forIn' toList✝ b' fun a m b => g a ⋯ b