mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε

Tactic:
max_def

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
    (if smoothingFun μ x ≤ smoothingFun μ y then smoothingFun μ y else smoothingFun μ x) + ε
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
⊢ smoothingSeminormSeq μ 0 =ᶠ[atTop] fun x ↦ 0

Tactic:
simp only [EventuallyEq, eventually_atTop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ 0 b = 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun x_1 ↦ μ x

Tactic:
simp only [EventuallyEq, eventually_atTop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = μ x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun x_1 ↦ μ x

Tactic:
simp only [EventuallyEq, eventually_atTop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = μ x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
⊢ smoothingSeminormSeq μ (x * y) =ᶠ[atTop] fun n ↦ μ x * smoothingSeminormSeq μ y n

Tactic:
simp only [EventuallyEq, eventually_atTop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ (x * y) b = μ x * smoothingSeminormSeq μ y b
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
E : Type u_2
F : Type u_4
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
hf : f.IsInvertible
⊢ f.HasRightInverse

Tactic:
by
  obtain ⟨e, rfl⟩ := hf
  exact e.hasRightInverse

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(R - R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)

Tactic:
sub_self,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖0 • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
⊢ IsIdempotentElem 0

Tactic:
rw [IsIdempotentElem, zero_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑P = ↑P + (↑P * ↑Q - ↑P * ↑Q)

Tactic:
sub_self,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : { P // IsLprojection X P }
⊢ ↑P = ↑P + 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ A - 1
⊢ A + ‖f x‖ * ‖∏ x ∈ t, (1 + f x)‖ ≤ A + ‖f x‖ * A

Tactic:
norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
x : ι
t : Finset ι
hx : x ∉ t
A : ℝ
h : Real.exp (∑ i ∈ t, ‖f i‖) = A
IH : ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ A - 1
⊢ A + ‖f x‖ * (‖∏ x ∈ t, (1 + f x) - 1‖ + ‖1‖) ≤ A + ‖f x‖ * A
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ projectiveSeminorm ∈
    upperBounds
      {p |
        ∃ G x x_1,
          p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

Tactic:
simp only [mem_upperBounds, Set.mem_ofPred_eq, forall_exists_index]

Goal state after:
case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ ∀ (x : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) (x_1 : Type (max uι u𝕜 uE)) (x_2 : SeminormedAddCommGroup x_1)
    (x_3 : NormedSpace 𝕜 x_1),
    x = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1)).comp (toDualContinuousMultilinearMap x_1) →
      x ≤ projectiveSeminorm
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
⊢ ((↑u).domRestrict E₁).ker = ⊥

Tactic:
eqₗ,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
⊢ (F₁.subtype ∘ₗ ↑↑e).ker = ⊥
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
disj : Disjoint E₁ (↑u).ker
⊢ F₁ ≤ ((↑u).domRestrict E₁).range

Tactic:
eqₗ,

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
disj : Disjoint E₁ (↑u).ker
⊢ F₁ ≤ (F₁.subtype ∘ₗ ↑↑e).range
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : z ∈ closedBall (x + const ι (3 / 4 * δ)) (δ / 4)
i : ι
⊢ y i < z i

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hz

Goal state after:
case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ y i < z i
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : z ∈ closedBall (x - const ι (3 / 4 * δ)) (δ / 4)
i : ι
⊢ z i < y i

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hz

Goal state after:
case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ gronwallBound δ K ε' (a - a)

Tactic:
sub_self,

Goal state after:
case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ gronwallBound δ K ε' 0
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt)

Tactic:
rw [← isIntegralCurveOn_univ] at *
  simpa using hγ.comp_add dt

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
ha : ‖a‖₊ = 1
this : 1 ≤ (p.cauchyBound - 1) * ↑p.natDegree
⊢ 1 ≠ p.cauchyBound

Tactic:
intro nh

Goal state after:
case inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
ha : ‖a‖₊ = 1
this : 1 ≤ (p.cauchyBound - 1) * ↑p.natDegree
nh : 1 = p.cauchyBound
⊢ False
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
this : Nonempty ↑(Icc tmin tmax)
⊢ ⨆ x_1, ‖(toContinuousMap (next hf hx α) - toContinuousMap (next hf hy α)) x_1‖ = dist x y

Tactic:
simp [add_sub_add_right_eq_sub, dist_eq_norm]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this : Tendsto (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 0)
⊢ P.degree < Q.degree

Tactic:
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨ ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax < tmin
x✝ : ℝ
ht : x✝ ∈ ∅
⊢ False

Tactic:
exact notMem_empty _ ht

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
by
  have := logMahlerMeasure_X_sub_C z
  rw [logMahlerMeasure_eq_log_MahlerMeasure] at this
  apply_fun exp at this
  rwa [posLog_eq_log_max_one (norm_nonneg z),
    exp_log (mahlerMeasure_pos_of_ne_zero <| X_sub_C_ne_zero z),
    exp_log (lt_of_lt_of_le zero_lt_one <| le_max_left 1 ‖z‖)] at this

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
n : ℕ
m : ℤ
hxr : x ^ n = ↑m
hv : ¬∃ y, x = ↑y
hnpos : 0 < n
⊢ Irrational x

Tactic:
rintro ⟨⟨N, D, P, C⟩, rfl⟩
  rw [← cast_pow] at hxr
  have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
    rw [Int.cast_ne_zero, Int.natCast_ne_zero]
    exact P
  have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
  rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr
  have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
  rw [← Int.dvd_natAbs, ← Int.natCast_pow, Int.natCast_dvd_natCast, Int.natAbs_pow,
    Nat.pow_dvd_pow_iff hnpos.ne'] at hdivn
  obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
  refine hv ⟨N, ?_⟩
  rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i ↦ 2 * ↑i) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop two_pos

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p

Tactic:
intro h
      have contAt := h.continuousAt
      cases this <;>
        simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - 1 / ↑q) 1)
this : 2 ≤ ↑q
⊢ deriv (qaryEntropy q) p < 0

Tactic:
have qinv_lt_1 : (q : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ (by linarith)

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - 1 / ↑q) 1)
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
⊢ deriv (qaryEntropy q) p < 0
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))

Tactic:
recursion

Goal state after:
θ : ℝ
n : ℕ
⊢ (2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ) * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ 0 < ↑(harmonic n) - ↑(harmonic n) - ↑(↑(n + 1))⁻¹ - (log ↑n - log ↑(n + 1))

Tactic:
sub_self,

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ 0 < 0 - ↑(↑(n + 1))⁻¹ - (log ↑n - log ↑(n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
⊢ 1 ≤ x → logb b x = |logb b x|

Tactic:
hx₁

Goal state after:
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ logb b x = |logb b x|
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
⊢ μ.InnerRegularWRT p q

Tactic:
intro A hA r hr
  obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r := by
    obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
      simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, mem_compl_iff, and_imp, imp_self,
        imp_true_iff]
  refine ⟨K, hK_subset, hK, ?_⟩
  have h_lt' : μ A - μ K < μ A - r := le_measure_sdiff.trans_lt h_lt
  exact lt_of_tsub_lt_tsub_left h_lt'

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : IsEmpty α
⊢ P ∅ᶜ < ε

Tactic:
rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : P (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : P' (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
simp only [← Set.compl_eq_univ_sdiff] at hKP hKP'

Goal state after:
case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε