mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ∃ T, dist (∑ b ∈ T, bound b) S < ε / 3

Tactic:
exact Eventually.exists <| hS _ (by positivity)

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x y : L
⊢ IsAlgebraic K (x - y)

Tactic:
exact Algebra.IsAlgebraic.isAlgebraic (x - y)

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁸ : NontriviallyNormedField K
L : Type v
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
hu : IsUltrametricDist K
inst✝⁵ : CompleteSpace K
x : L
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Algebra L E
inst✝¹ : IsScalarTower K L E
inst✝ : Algebra.IsAlgebraic K E
a : E
ha : a ∈ ((mapAlg K E) (minpoly K x)).roots
⊢ (spectralMulAlgNorm K E) a = (spectralMulAlgNorm K E) ((algebraMap L E) x)

Tactic:
simp only [spectralMulAlgNorm_def, spectralNorm]
  have : (aeval a) (minpoly K ((algebraMap L E) x)) = 0 := by
    simp only [mem_roots', IsRoot.def] at ha
    rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
  rw [← minpoly.eq_of_root (Algebra.IsAlgebraic.isAlgebraic ((algebraMap L E) x)) this]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
s : ℝ
⊢ s ∈ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots → r = s

Tactic:
hs

Goal state after:
K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
s : ℝ
hs : s ∈ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots
⊢ r = s
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
⊢ IsLprojection X (P + Q - P * Q)

Tactic:
convert! (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1

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
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)
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 }
⊢ ↑Q = ↑Q * ↑P + (↑Q * ↑Q - ↑Q * (↑P * ↑Q))

Tactic:
(P.prop.commute Q.prop).eq,

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 }
⊢ ↑Q = ↑Q * ↑P + (↑Q * ↑Q - ↑Q * (↑Q * ↑P))
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ ‖⨂ₜ[𝕜] (i : ι), m i‖ ≤ ∏ i, ‖m i‖

Tactic:
have hle := ciInf_le (bddBelow_projectiveSemiNormAux (⨂ₜ[𝕜] i, m i))
    ⟨FreeAddMonoid.of (1, m), by simp [mem_lifts_iff]⟩
   grw [norm_def, hle]
   simp [projectiveSeminormAux]

Goal state after:
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
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
⊢ [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u,
      ∃ E₁ F₁,
        IsClosed[inst✝⁸] ↑E₁ ∧
          IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible,
      Nonempty u.FredholmPackage].TFAE

Tactic:
by
  tfae_have 1 → 4 := IsFredholm.nonempty_fredholmPackage
  tfae_have 4 → 2 := by
    rintro ⟨dec⟩
    exact ⟨dec.quasiInverse, dec.isQuasiInverse⟩
  tfae_have 2 → 3 := by
    rintro ⟨v, huv⟩
    exact exists_restrict_isInvertible_of_isQuasiInverse huv
  tfae_have 3 → 1 := by
    rintro ⟨E₁, F₁, E₁_closed, F₁_closed, E₁_coFG, F₁_coFG, u_mapsto, u_invertible⟩
    exact .of_isInvertible_restrict E₁_closed F₁_closed u_mapsto u_invertible
  tfae_finish

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Tactic:
refine ⟨fun ⟨s, hs, h⟩ ↦ ⟨s, hs, fun t ht ↦ (h t ht).hasDerivWithinAt⟩, ?_⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s) → ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ : ℝ
⊢ ∀ ⦃b : ℝ⦄, x₁ ≤ b → gronwallBound δ K ε x₁ ≤ gronwallBound δ K ε b

Tactic:
x₂

Goal state after:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
⊢ x₁ ≤ x₂ → gronwallBound δ K ε x₁ ≤ gronwallBound δ K ε x₂
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
⊢ 0 < (P.comp (-X)).degree

Tactic:
by simp [hdeg]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
h_supp : p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
simp only [gaussNorm, h_supp]

Goal state after:
case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
h_supp : p.support.Nonempty
⊢ ∃ i, (if h : True then p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i else 0) = v (p.coeff i) * c ^ i
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case pos
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p

Tactic:
simp_all [gaussNorm, sup'_nonneg_of_ne_zero, -Finset.le_sup'_iff]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p

Tactic:
simp_all [gaussNorm, sup'_nonneg_of_ne_zero, -Finset.le_sup'_iff]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ v (p.coeff i) * c ^ i ≤ PowerSeries.gaussNorm (⇑v) c ↑p

Tactic:
← coeff_coe

Goal state after:
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ v ((PowerSeries.coeff i) ↑p) * c ^ i ≤ PowerSeries.gaussNorm (⇑v) c ↑p
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vNonneg : ∀ (a : R), v a ≥ 0
⊢ 0 ≤ ⨆ t, v ((coeff t) f) * t.prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
by_cases h : HasGaussNorm v c f

Goal state after:
case pos
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ 0 ≤ ⨆ t, v ((coeff t) f) * t.prod fun x1 x2 ↦ c x1 ^ x2

case neg
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vNonneg : ∀ (a : R), v a ≥ 0
h : ¬HasGaussNorm v c f
⊢ 0 ≤ ⨆ t, v ((coeff t) f) * t.prod fun x1 x2 ↦ c x1 ^ x2
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
this : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0
hcoeff0 : p.coeff 0 ≠ 0
⊢ gaussNorm v 0 p = v (p.coeff 0)

Tactic:
· apply le_antisymm
    · aesop (add norm (by simp [gaussNorm, Finset.sup'_le_iff]))
    · grind [p.le_gaussNorm v (le_refl 0) 0]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h✝ : i < x
⊢ v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

Tactic:
calc
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))
    _ ≤ gaussNorm v c p * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) := by
        gcongr
        exact p.le_gaussNorm v hc0 x
    _ = v (p.coeff i) * c ^ i * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) := by
        rw [hi_p]
    _ < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) := by
        gcongr 1
        grind

Goal state after:
Module: Mathlib.Analysis.RCLike.BoundedContinuous

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg : (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g
hg_apply : ∀ (a : E), x a = ↑(g a)
⊢ ∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g

Tactic:
have h_comp_eq : (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal
        (x.comp reCLM (@reCLM 𝕜 _).lipschitz) = x := by
      ext a
      simp [hg_apply]

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg : (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g
hg_apply : ∀ (a : E), x a = ↑(g a)
h_comp_eq : (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (comp ⇑reCLM ⋯ x) = x
⊢ ∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
⊢ Monotone rclikeToReal

Tactic:
intro a b

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
a b : C(X, 𝕜)
⊢ a ≤ b → a.rclikeToReal ≤ b.rclikeToReal
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2 * ↑prec ^ 2

Tactic:
rw [← mul_pow, add_mul]

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec * ↑prec + 1 / ↑prec * ↑prec) ^ 2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
simp [this, exp_multiset_sum, posLog_eq_log_max_one, exp_log]

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

Goal state before:
pp: case a.refine_1
p : ℂ[X]
i : ℕ
x✝ : i ∈ p.support
⊢ ‖p.coeff i‖ ^ 2 ≤ p.supNorm ^ 2

pp: case a.refine_2
p : ℂ[X]
⊢ p.support.card • p.supNorm ^ 2 ≤ (↑p.natDegree + 1) * p.supNorm ^ 2

Tactic:
· gcongr; exact p.le_supNorm _

Goal state after:
case a.refine_2
p : ℂ[X]
⊢ p.support.card • p.supNorm ^ 2 ≤ (↑p.natDegree + 1) * p.supNorm ^ 2
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: m : ℤ
x : ℝ
⊢ Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x

Tactic:
by
  rw [← cast_intCast, irrational_div_ratCast_iff, Int.cast_ne_zero]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
· exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

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

Goal state before:
pp: case h2
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, x ^ 2 ∈ Set.Iio 1

Tactic:
· rw [eventually_iff_exists_mem]
      use Set.Ioo (-1) 1
      exact ⟨Ioo_mem_nhdsLT <| by simp,
        fun _ _ ↦ by rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]⟩

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

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * (y ^ 2) ^ x * y = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)

Tactic:
simp_rw [mul_assoc, ← pow_mul, ← pow_succ, div_mul_eq_mul_div]

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x * y ^ (2 * x + 1) / (2 * ↑x + 1) = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z

Tactic:
conv_lhs =>
    enter [2, 1, 2]
    rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos (-z) + sin (-z) * I)) = z
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    (∫ (x : ℝ) in -1..1, f x ^ (n + 1) * (cos (x * θ) * θ)) * θ

Tactic:
f,

Goal state after:
case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * (cos (x * θ) * θ)) * θ
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 = (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ

pp: case convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
· simp_rw [u₁, v₁', f, ← intervalIntegral.integral_mul_const, sq θ, mul_assoc]

Goal state after:
case convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ √((1 + tanh x) / (1 - tanh x)) = rexp x

Tactic:
← sq_eq_sq₀ (le_of_lt <| sqrt_pos_of_pos h) (exp_nonneg x),

Goal state after:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ √((1 + tanh x) / (1 - tanh x)) ^ 2 = rexp x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
⊢ x.agm y < max x y

Tactic:
wlog h : x < y generalizing x y
  · simpa [agm_comm, max_comm] using this hn.symm (hn.gt_or_lt.resolve_right h)
  rw [max_eq_right h.le]
  apply (agm_lt_agmSequences_snd_of_ne hn 0).trans_le
  rw [agmSequences_zero]
  exact (le_gm_and_am_le h.le).2

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

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 1)) atBot

pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ (fun p ↦ log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)

Tactic:
· simp only [disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true]

Goal state after:
q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ (fun p ↦ log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

Tactic:
by
  have tendstoBot : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot := by
    have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
      = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by
      ext
      ring
    rw [this]
    apply tendsto_atBot_add_const_left
    exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot
  apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoBot) nhdsWithin_le_nhds
  · simp only [disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true]
  filter_upwards [Ioo_mem_nhdsLT (show 1 - 2⁻¹ < (1 : ℝ) by norm_num)]
  intros
  apply (deriv_qaryEntropy _ _).symm
  · simp_all only [mem_Ioo, ne_eq]
    linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]
  · simp_all only [mem_Ioo, ne_eq]
    linarith [two_inv_lt_one (α := ℝ)]

Goal state after: