mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
⊢ ∃ t ∈ Filter.map (fun s ↦ ∏ b ∈ s, (fun i ↦ 1 + f i) b) (unconditional ι).filter, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Tactic:
obtain ⟨r₁, hr₁, s₁, hs₁⟩ :=
    (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finsetProd

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
⊢ ∃ t ∈ Filter.map (fun s ↦ ∏ b ∈ s, (fun i ↦ 1 + f i) b) (unconditional ι).filter, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
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✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
m : (i : ι) → E i
⊢ ∏ i, ‖(f i) (m i)‖ ≤ (∏ i, ‖f i‖) * ∏ i, ‖m i‖

Tactic:
rw [← Finset.prod_mul_distrib]

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
m : (i : ι) → E i
⊢ ∏ i, ‖(f i) (m i)‖ ≤ ∏ x, ‖f x‖ * ‖m x‖
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsEmbedding ⇑(kerLift f)

Tactic:
isEmbedding_iff_isStrictMap_injective,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsStrictMap ⇑(kerLift f) ∧ Function.Injective ⇑(kerLift f)
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
G' : Type u_3
H' : Type u_4
inst✝⁹ : Group G'
inst✝⁸ : Group H'
inst✝⁷ : Group G
inst✝⁶ : Group H
f : G →* H
g : G' →* H'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : IsTopologicalGroup G'
inst✝ : TopologicalSpace H'
Φ : ↥(f.prodMap g).range ≃ₜ ↥f.range × ↥g.range := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑f.range ↑g.range)
⊢ IsOpenQuotientMap ⇑(f.prodMap g).rangeRestrict ↔
    IsOpenQuotientMap ⇑f.rangeRestrict ∧ IsOpenQuotientMap ⇑g.rangeRestrict

Tactic:
have eq : Φ ∘ (f.prodMap g).rangeRestrict = f.rangeRestrict.prodMap g.rangeRestrict := rfl

Goal state after:
G : Type u_1
H : Type u_2
G' : Type u_3
H' : Type u_4
inst✝⁹ : Group G'
inst✝⁸ : Group H'
inst✝⁷ : Group G
inst✝⁶ : Group H
f : G →* H
g : G' →* H'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : IsTopologicalGroup G'
inst✝ : TopologicalSpace H'
Φ : ↥(f.prodMap g).range ≃ₜ ↥f.range × ↥g.range := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑f.range ↑g.range)
eq : ⇑Φ ∘ ⇑(f.prodMap g).rangeRestrict = ⇑(f.rangeRestrict.prodMap g.rangeRestrict)
⊢ IsOpenQuotientMap ⇑(f.prodMap g).rangeRestrict ↔
    IsOpenQuotientMap ⇑f.rangeRestrict ∧ IsOpenQuotientMap ⇑g.rangeRestrict
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝¹ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this✝ : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
this : IsStrictMap ⇑(uₛ.prodMap uₐ) ↔ IsStrictMap ⇑uₐ
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A)

Tactic:
by
    rwa [u_restr_eq, u_eq, ← (isEmbedding_subtypeL _).isStrictMap_iff,
      ← Ψ.isHomeomorph.isEmbedding.isStrictMap_iff,
      ← Φ.symm.isHomeomorph.isQuotientMap.isStrictMap_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
h_ker : Disjoint (↑u).ker A
h_range : Surjective ⇑↑u
u_strict : IsStrictMap ⇑u
⊢ IsQuotientMap ⇑u

Tactic:
coe_coe

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
h_ker : Disjoint (↑u).ker A
h_range : Surjective ⇑u
u_strict : IsStrictMap ⇑u
⊢ IsQuotientMap ⇑u
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
y : ι → ℝ
⊢ MonotoneOn (fun x ↦ dist x y) (Ici y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
y : ι → ℝ
⊢ AntitoneOn (fun x ↦ dist x y) (Iic y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s) ↔ IsIntegralCurveOn γ v s

Tactic:
have heq : a⁻¹ • s = { t | t * a ∈ s } := by
    ext t
    rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]
    rfl
  refine ⟨fun hγ ↦ ?_, heq ▸ fun hγ ↦ hγ.comp_mul a⟩
  convert! hγ.comp_mul a⁻¹
  · ext t
    simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
  · ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]
  · simp only [mul_comm _ a⁻¹, ← smul_eq_mul, mem_inv_smul_set_iff₀ ha, smul_inv_smul₀ ha,
      ofPred_mem_eq]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a))

Tactic:
apply ODE_solution_unique_of_mem_Icc_right hv'
    (hf.comp continuousOn_neg hmt1) _ (fun _ ht ↦ hfs _ (hmt2 ht))
    (hg.comp continuousOn_neg hmt1) _ (fun _ ht ↦ hgs _ (hmt2 ht)) (by simp [hb])

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (f ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((f ∘ Neg.neg) t)) (Ici t) t

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t
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, (if h : True then p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i else 0) = v (p.coeff i) * c ^ i

Tactic:
obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)

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 : ℕ
hi1 : i ∈ p.support
hi2 : (p.support.sup' h_supp fun i ↦ v (p.coeff i) * c ^ i) = v (p.coeff i) * c ^ i
⊢ ∃ 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.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
have hlc' : 0 ≤ Int.negOnePow (P.comp (-X)).natDegree * (P.comp (-X)).leadingCoeff := by
    rw [show (P.comp (-X)).leadingCoeff = P.leadingCoeff * Int.negOnePow P.natDegree by simp; ring,
      show (P.comp (-X)).natDegree = P.natDegree by simp [natDegree_comp], mul_comm, mul_assoc]
    simpa [Int.cast_negOnePow_natCast, pow_right_comm]

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
θ : ℝ
hθ : 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖

Tactic:
exact exp_log hθ

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(max x y) = max ↑x ↑y

Tactic:
max_def,

Goal state after:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(max x y) = map₂ max ↑x ↑y
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
y : ℝ := ↑b ^ n * x
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊y⌋₊
⊢ b * (⌊↑b * y⌋₊ / b) + ⌊↑b * y⌋₊ % b = ⌊↑b * y⌋₊

Tactic:
Nat.div_add_mod

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
y : ℝ := ↑b ^ n * x
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊y⌋₊
⊢ ⌊↑b * y⌋₊ = ⌊↑b * y⌋₊
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

pp: case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
· obtain ⟨t, ht⟩ := exists_lt r
    exact (H ⟨t, s⟩ ⟨ht, hs⟩).2.le

Goal state after:
case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : x.Infinitesimal
hy : y.Infinitesimal
⊢ (x * y).Infinitesimal

Tactic:
by simpa only [mul_zero] using! hx.mul hy

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

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (arctan 1))
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
arctan_one

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → y < x → sqrt (x * y) < (x + y) / 2
hl : ¬y < x
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
specialize this h.symm (h.gt_or_lt.resolve_left hl)

Goal state after:
case inr
x y : ℝ≥0
h : x ≠ y
this : sqrt (y * x) < (y + x) / 2
hl : ¬y < x
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2

Tactic:
induction n generalizing x y with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ -(1 - z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
Set.neg_mem_Ioo_iff,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (1 - z * I).arg ∈ Set.Ioo (-(π / 2)) (- -(π / 2))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (sqrt (x * y), (x + y) / 2).1

Tactic:
exact (le_gm_and_am_le h).1

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

Goal state before:
pp: x y k : ℝ≥0
n : ℕ
⊢ ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2

Tactic:
induction n generalizing x y with

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

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy p < 0

Tactic:
by
  rw [← binEntropy_one_sub]; exact binEntropy_neg_of_neg (sub_neg.2 hp)

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

Goal state before:

Tactic:
_ < log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) :=
    strictConcaveOn_log_Ioi.2 (inv_pos.2 hp₀) (inv_pos.2 hp₁)
      (by simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]) hp₀ hp₁ (by simp)
  _ = log 2 := by rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

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

Goal state before:
pp: p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
by
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro h rfl
    simp at h
  wlog hp : p < 2⁻¹
  · have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
    rw [← binEntropy_one_sub]
    exact this hp.ne hp
  obtain hp₀ | hp₀ := le_or_gt p 0
  · exact (binEntropy_nonpos_of_nonpos hp₀).trans_lt <| log_pos <| by simp
  have hp₁ : 0 < 1 - p := sub_pos.2 <| hp.trans <| by norm_num
  calc
  _ < log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) :=
    strictConcaveOn_log_Ioi.2 (inv_pos.2 hp₀) (inv_pos.2 hp₁)
      (by simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]) hp₀ hp₁ (by simp)
  _ = log 2 := by rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

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

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z ↦ z ^ a₁ * cexp (↑b₁ * z)) z = (fun z ↦ z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)) z

Tactic:
simp only
        rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]

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

Goal state before:
pp: case hf
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, log (1 / 2) ≤ log (1 - x)

Tactic:
have h₁ : (0 : ℝ) < 1 / 2 := by simp
    filter_upwards [Ioc_mem_nhdsGT h₁] with p hx
    gcongr
    linarith [hx.2]

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
⊢ StrictMonoOn (qaryEntropy q) (Icc 0 (1 - 1 / ↑q))

Tactic:
intro p1 hp1 p2 hp2 p1le2

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
⊢ qaryEntropy q p1 < qaryEntropy q p2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
⊢ StrictAntiOn (qaryEntropy q) (Icc (1 - 1 / ↑q) 1)

Tactic:
intro p1 hp1 p2 hp2 p1le2

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
⊢ qaryEntropy q p2 < qaryEntropy q p1
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * (‖p‖ * ‖log x‖) ^ 2 = p * ‖log x‖ ^ 2

Tactic:
grind [Real.norm_of_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Convex ℝ {a | IsStrictlyPositive a}

Tactic:
by grind [convex_iff_forall_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ ⦃x : A⦄,
    x ∈ {a | IsStrictlyPositive a} →
      ∀ ⦃y : A⦄,
        y ∈ {a | IsStrictlyPositive a} →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
intro x (xpos : IsStrictlyPositive x) y (ypos : IsStrictlyPositive y) a b ha hb hab

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
hx_pos : 0 < x
⊢ |x| < η

Tactic:
abs_of_pos hx_pos

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
hx_pos : 0 < x
⊢ x < η