mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst✝ : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
  have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0
  refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_
  refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
    (h₁.and h₃))).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
  exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
k : K
y : L
⊢ B.norm ((algebraMap K L) k * y) = B.norm ((algebraMap K L) k) * B.norm y

Tactic:
rw [norm_extends hBi, Basis.norm, Basis.norm,
    Finset.mul₀_sup' (norm_nonneg _) (fun j : ι ↦ ‖B.repr y j‖) univ univ_nonempty]
  congr with j
  rw [repr_smul', norm_mul]

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

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x : L
⊢ (Classical.choose ⋯) (σ (-x)) = (Classical.choose ⋯) (σ x)

Tactic:
by simp [map_neg σ, map_neg_eq_map]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x

Tactic:
have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop
      (𝓝 (seminormFromConst' c f x)) := by
    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)
    rintro n; use n; lia
  rw [seminormFromConst_apply_c hf1 hc hpm]
  apply tendsto_nhds_unique (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (c * x))
  have hterm : seminormFromConst_seq c f (c * x) =
      fun n ↦ f c * seminormFromConst_seq c f x (n + 1) := by
    simp only [seminormFromConst_seq_def]
    ext n
    ring_nf
    rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
  simpa [hterm] using tendsto_const_nhds.mul hlim

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
⊢ μ (x ^ (↑m1 * (n / ↑m1) + n % ↑m1)) ^ (1 / ↑n) < L + ε

Tactic:
have h2 : μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) ≤ (μ x ^ (n % m1)) ^ (1 / (n : ℝ)) := by
      by_cases hnm1 : n % m1 = 0
      · simpa [hnm1, pow_zero] using rpow_le_rpow (apply_nonneg μ _) hμ1 (one_div_cast_nonneg _)
      · exact rpow_le_rpow (apply_nonneg μ _) (map_pow_le_pow μ _ hnm1) (one_div_cast_nonneg _)

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
⊢ μ (x ^ (↑m1 * (n / ↑m1) + n % ↑m1)) ^ (1 / ↑n) < L + ε
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
use μ x
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    conv_rhs => rw [← rpow_one (μ x)]
    rw [rpow_le_rpow_left_iff hx]
    exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (cast_nonneg _)

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

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
x : K
⊢ spectralNorm K L ((algebraMap K L) x) = ‖x‖

Tactic:
rw [spectralNorm_eq_invariantExtension, invariantExtension_extends K L x]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.LpEquiv

Goal state before:
pp: case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ∞)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

pp: case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
· rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]; rfl

Goal state after:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖
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) - 1‖ + ‖1‖) ≤ A + ‖f x‖ * A

Tactic:
IH,

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‖ * (A - 1 + ‖1‖) ≤ A + ‖f x‖ * A
Module: Mathlib.Analysis.Normed.Order.UpperLower

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

Tactic:
by
  simpa only [dist_comm] using dist_mono_left_pi (y := x)

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

Goal state before:
pp: u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
have : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k := sum_nonneg <| by grind

Goal state after:
u b c : ℕ → ℝ
n₀ n₁ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n ∈ Ico n₀ n₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)
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 : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ↑K ^ (n + 1) * |↑t - ↑t₀| ^ (n + 1) / |↑n + 1| / |↑n !| * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
div_div,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ↑K ^ (n + 1) * |↑t - ↑t₀| ^ (n + 1) / (|↑n + 1| * |↑n !|) * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg
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
hlt : tmax ≤ tmin
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmax)

Tactic:
le_iff_lt_or_eq

Goal state after:
case neg
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
hlt : tmax < tmin ∨ tmax = tmin
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmax)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f✝ : ℝ → E → E
tmin tmax : ℝ
t₀✝ : ↑(Icc tmin tmax)
x₀✝ x : E
a✝ r✝ L✝ K✝ : ℝ≥0
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)

Tactic:
simp [le_of_lt hε]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f✝ : ℝ → E → E
tmin tmax : ℝ
t₀✝ : ↑(Icc tmin tmax)
x₀✝ x : E
a✝ r✝ L✝ K✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
ε : ℝ
hε : 0 < ε
a r L K : ℝ≥0
x✝ : 0 < r
t₀ : ℝ
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)

Tactic:
simp [le_of_lt hε]

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

Goal state before:
pp: α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s : Finset ι
hs : s.Nonempty
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
⊢ ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton j => simp only [Finset.mem_singleton, Finset.sum_singleton, exists_eq_left, le_refl]
  | cons j s hj _ IH =>
      simp only [Finset.sum_cons, Finset.mem_cons, exists_eq_or_imp]
      refine (le_total (g (∑ i ∈ s, f i)) (g (f j))).imp ?_ ?_ <;> intro h
      · exact (na _ _).trans (max_eq_left h).le
      · exact ⟨_, IH.choose_spec.left, (na _ _).trans <|
          ((max_eq_right h).le.trans IH.choose_spec.right)⟩

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

Goal state before:
pp: case h.right
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∀ y ∈ {x | eval (circleMap 0 1 x) p ≠ 0}, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)

Tactic:
· intro _ _
    gcongr
    rw [eval_eq_sum]
    apply norm_sum_le_of_le p.support
    simp

Goal state after:
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‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), ‖eval (circleMap 0 1 x) p‖ ∈ Ici 0

Tactic:
filter_upwards

Goal state after:
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‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ∀ (a : ℝ), ‖eval (circleMap 0 1 a) p‖ ∈ Ici 0
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this : 0 < b
⊢ x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

Tactic:
have := ofDigits_digits_sum_eq (b := b) hx n

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : 0 < b
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

Tactic:
have := ofDigits_digits_sum_eq (b := b) hx n

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

Goal state before:
pp: b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ (↑b - 1) * (↑b ^ (n + 1))⁻¹ ≤ ↑b * (↑b ^ (n + 1))⁻¹

Tactic:
gcongr
          linarith

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

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
⊢ ↑↑D ≠ 0

Tactic:
rw [Int.cast_ne_zero, Int.natCast_ne_zero]

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
⊢ D ≠ 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ((map v p).sum fun x a ↦ ‖a‖) = p.sum fun x a ↦ ‖a‖

Tactic:
rw [sum_def, sum_def, support_map_of_injective _ hv.injective]

Goal state after:
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ p.support, ‖(map v p).coeff n‖ = ∑ n ∈ p.support, ‖p.coeff n‖
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ (∏ x ∈ range n, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))) *
      ((2 * ↑n + 2) / (2 * ↑n + 1) * ((2 * ↑n + 2) / (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
IH,

Goal state after:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) *
      ((2 * ↑n + 2) / (2 * ↑n + 1) * ((2 * ↑n + 2) / (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 1) * (2 * ↑x + 2) / (2 * ↑x + 3)

Tactic:
mul_div_assoc

Goal state after:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

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

Tactic:
by
  refine tendsto_nhds_unique ?_ tendsto_agmSequences_snd_agm
  have key := @tendsto_agmSequences_snd_agm x y
  rw [← tendsto_add_atTop_iff_nat (n + 1)] at key
  convert! key using 2 with m
  simp_rw [agmSequences, Prod.mk.eta, ← iterate_add_apply, add_right_comm]

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

Goal state before:
pp: case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv (fun p ↦ p.negMulLog + (1 - p).negMulLog) p = log (1 - p) - log p

Tactic:
deriv_fun_add,

Goal state after:
case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv negMulLog p + deriv (fun p ↦ (1 - p).negMulLog) p = log (1 - p) - log p

case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))
  · have : Tendsto log (𝓝[>] 0) atBot := Real.tendsto_log_nhdsGT_zero
    apply Tendsto.comp (f := (1 - ·)) (g := log) this
    have contF : Continuous ((1 : ℝ) - ·) := continuous_sub_left 1
    have : MapsTo ((1 : ℝ) - ·) (Iio 1) (Ioi 0) := by
      intro p hx
      simp_all only [mem_Iio, mem_Ioi, sub_pos]
    convert! ContinuousWithinAt.tendsto_nhdsWithin (x := (1 : ℝ)) contF.continuousWithinAt this
    exact Eq.symm (sub_eq_zero_of_eq rfl)
  · have h₁ : (1 : ℝ) - (2 : ℝ)⁻¹ < 1 := by norm_num
    filter_upwards [Ico_mem_nhdsLT h₁] with p hx
    gcongr
    exact hx.1

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
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (a • x + b • y)⁻¹ʳ = (a • (conjSqrt x) 1 + b • (conjSqrt x) z)⁻¹ʳ

Tactic:
conjSqrt_conjSqrt_ringInverse _ _ xpos,

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
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (a • x + b • y)⁻¹ʳ = (a • (conjSqrt x) 1 + b • y)⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1)

Tactic:
mul_div_assoc

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * (1 / (t + 1))
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ log b ↑n = ↑(Nat.log b n)

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑0 = ↑(Nat.log b 0)

case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(n✝ + 1) = ↑(Nat.log b (n✝ + 1))
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : 0 < x
⊢ y * log x / log b = y * (log x / log b)

Tactic:
mul_div_assoc

Goal state after:
b x y : ℝ
hx : 0 < x
⊢ y * (log x / log b) = y * (log x / log b)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
k : ℕ
⊢ ↑k * log x / log b = ↑k * (log x / log b)

Tactic:
mul_div_assoc

Goal state after:
b x : ℝ
k : ℕ
⊢ ↑k * (log x / log b) = ↑k * (log x / log b)
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
⊢ x ∈ Ici (rexp 1) → ∀ ⦃b : ℝ⦄, b ∈ Ici (rexp 1) → x ≤ b → (fun x ↦ log x / x) b ≤ (fun x ↦ log x / x) x

Tactic:
hex

Goal state after:
x : ℝ
hex : x ∈ Ici (rexp 1)
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ici (rexp 1) → x ≤ b → (fun x ↦ log x / x) b ≤ (fun x ↦ log x / x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
⊢ x ∈ Ici (rexp a⁻¹) → ∀ ⦃b : ℝ⦄, b ∈ Ici (rexp a⁻¹) → x ≤ b → (fun x ↦ log x / x ^ a) b ≤ (fun x ↦ log x / x ^ a) x

Tactic:
hex

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ici (rexp a⁻¹) → x ≤ b → (fun x ↦ log x / x ^ a) b ≤ (fun x ↦ log x / x ^ a) x
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
    · simpa only [closure_closure, Function.comp_apply] using hK2.closure
    · exact hK3.trans_le (measure_mono subset_closure)

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

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| ≤ δ * (P K).toReal

Tactic:
rw [← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
      (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)), ← norm_eq_abs]
  exact norm_setIntegral_le_of_norm_le_const hK.measure_lt_top
    (fun x hxK => le_trans (dist_mulExpNegMulSq_le_dist hε) (hfg x hxK).le)

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

Goal state before:
pp: n : ℕ
a b c : ℂ
⊢ (a.regularizedGaussHGFunSeries b c).coeff n =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n ! * Gamma (c + ↑n))

Tactic:
simp [regularizedGaussHGFunSeries, regularizedHGFunCoeff]

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

Goal state before:
pp: case refine_1
x : ℝ
⊢ 0 < x.sigmoid ∧ x.sigmoid < 1

Tactic:
bound

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

Goal state before:
pp: x : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x✝ : ℝ
⊢ 0 ≤ x✝.sigmoid

Tactic:
bound

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

Goal state before:
pp: x : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x✝ : ℝ
⊢ x✝.sigmoid ≤ 1

Tactic:
bound

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1

Tactic:
refine ⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
  rw [← neg_neg x, ← image_neg_Ici] at h
  have := (h.comp (-x) differentiableWithinAt_id.fun_neg (mapsTo_image _ _)).fun_neg
  simpa [(· ∘ ·), differentiableWithinAt_arcsin_Ici] using this

Goal state after: