mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
h : ¬smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ smoothingFun μ x + ε

Tactic:
rw [add_le_add_iff_right]

Goal state after:
case neg
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
h : ¬smoothingFun μ x ≤ smoothingFun μ y
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b ≤ smoothingFun μ x
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: case e'_5
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable fun i ↦ 1 + f' i
x✝¹ : Finset ι
x✝ : ↑K
⊢ ∏ i ∈ x✝¹, (1 + f i ↑x✝) = (∏ b ∈ x✝¹, (fun i ↦ 1 + f' i) b) x✝

Tactic:
simp [f']

Goal state after:
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
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f : (i : ι) → E i →L[𝕜] E' i
⊢ (mapL fun i ↦ g i ∘SL f i) = mapL g ∘SL mapL f

Tactic:
apply ContinuousLinearMap.coe_injective

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
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f : (i : ι) → E i →L[𝕜] E' i
⊢ ↑(mapL fun i ↦ g i ∘SL f i) = ↑(mapL g ∘SL mapL f)
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)
F : Type u_4
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
⊢ (liftIsometry 𝕜 E' F) h ∘SL mapL f = (liftIsometry 𝕜 E F) (h.compContinuousLinearMap f)

Tactic:
apply ContinuousLinearMap.coe_injective

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)
F : Type u_4
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
⊢ ↑((liftIsometry 𝕜 E' F) h ∘SL mapL f) = ↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))
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)
⊢ (mapL fun i ↦ ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)

Tactic:
apply ContinuousLinearMap.coe_injective

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)
⊢ ↑(mapL fun i ↦ ContinuousLinearMap.id 𝕜 (E i)) = ↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))
Module: Mathlib.Analysis.Normed.Order.Hom.Ultra

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroup α
inst✝ : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean ⇑f
hd : inst = (toSeminormedAddGroup f).toDist
x y z : α
⊢ -x + z = -x + y + (-y + z)

Tactic:
rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]

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
F' : Submodule 𝕜 F := (↑u).range
h_range : IsClosed[inst✝³] ↑F'
i : ↥F' →L[𝕜] F := F'.subtypeL
i_clemb : IsClosedEmbedding ⇑i
u' : E →L[𝕜] ↥F' := u.rangeRestrict
range_u' : (↑u').range = ⊤
eq1 : u = i ∘SL u'
eq2 : u.domRestrict A = i ∘SL u'.domRestrict A
⊢ IsStrictMap ⇑u' ↔ IsStrictMap ⇑(u'.domRestrict A) ∧ IsClosed[instTopologicalSpaceSubtype] ↑(↑(u'.domRestrict A)).range

Tactic:
exact step2 u' A A_closed (u.ker_rangeRestrict ▸ h_ker) range_u'

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t

Tactic:
by
  obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx
  refine ⟨α.compProj, by rw [FunSpace.compProj_val, ← hα, FunSpace.next_apply₀], fun t ht ↦ ?_⟩
  apply hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry
    α.continuous_compProj.continuousOn (fun _ ht' ↦ α.compProj_mem_closedBall hf.mul_max_le)
    x ht |>.congr_of_mem _ ht
  intro t' ht'
  nth_rw 1 [← hα]
  rw [FunSpace.compProj_of_mem ht', FunSpace.next_apply]

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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ Ioo (t₀ - ε) (t₀ + ε),
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ EqOn f g (Ioo (t₀ - ε) (t₀ + ε))

Tactic:
apply ODE_solution_unique_of_mem_Ioo (fun _ ht ↦ (h _ ht).1)
    (Real.ball_eq_Ioo t₀ ε ▸ mem_ball_self hε)
    (fun _ ht ↦ (h _ ht).2.1) (fun _ ht ↦ (h _ ht).2.2) heq

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

Goal state before:
pp: case pos
𝕜 : 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
⊢ P.degree < Q.degree

Tactic:
simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ

Goal state after:
case pos
𝕜 : 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 = 0 ∨ Q.leadingCoeff = 0
⊢ P.degree < Q.degree
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : {x | |↑(eval x P)| ≤ |↑(eval x Q)|}.Finite
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite

Tactic:
norm_cast at key

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

Goal state before:
pp: 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
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
obtain ⟨j, hj_q, hlt_q⟩ := q.exists_min_eq_gaussNorm v hc0

Goal state after:
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
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff t) (f * g)) * t.prod fun x1 x2 ↦ c x1 ^ x2) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
hprod

Goal state after:
case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
⊢ v ((coeff t) (f * g)) * ((k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2) ≤
    gaussNorm v c f * gaussNorm v c g
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.logMahlerMeasure = log (if p ≠ 0 then rexp p.logMahlerMeasure else 0)

Tactic:
split_ifs

Goal state after:
case pos
p : ℂ[X]
h✝ : p ≠ 0
⊢ p.logMahlerMeasure = log (rexp p.logMahlerMeasure)

case neg
p : ℂ[X]
h✝ : ¬p ≠ 0
⊢ p.logMahlerMeasure = log 0
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
hprod : ((i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) = (i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f) * v ((coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
hprod

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
hprod : ((i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) = (i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f) * v ((coeff j₀) g) * ((i₀.prod fun x1 x2 ↦ c x1 ^ x2) * j₀.prod fun x1 x2 ↦ c x1 ^ x2)
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
⊢ (fun x1 x2 ↦ x1 < x2) = LiftRel fun x1 x2 ↦ x1 < x2

Tactic:
ext ⟨f⟩ ⟨g⟩
  exact coe_lt

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

Goal state before:
pp: 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⌋₊
⊢ 0 ≤ ↑b ^ n * x

Tactic:
by have := hx.left; positivity

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

Goal state before:
pp: r : ℝ
f : ℕ → ℝ
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → ∀ᶠ (x : ℕ) in ↑(hyperfilter ℕ), f x ∈ Set.Ioo i.1 i.2) ↔
    (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s

Tactic:
simp_rw [Set.mem_Ioo, eventually_and, ← ofSeq_lt_ofSeq]

Goal state after:
r : ℝ
f : ℕ → ℝ
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2) ↔
    (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
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
c1 : ↑↑D ≠ 0
⊢ False

Tactic:
have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1

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
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ x ≠ 1

Tactic:
simpa only [Nat.cast_one] using h.ne_nat 1

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

Goal state before:
pp: r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : (ofSeq g).IsSt r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)

Tactic:
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)

Goal state after:
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))

Tactic:
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
| cos (-z) + sin (-z) * I
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y (n + 1) =
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)

Tactic:
by
  rw [agmSequences, agmSequences, iterate_succ', comp_apply]

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

Goal state before:
pp: case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    -I / 2 * (((-1) ^ (2 * k + 0 + 1) + 1) * (z * I) ^ (2 * k + 0) / ↑(2 * k + 0)) +
      -I / 2 * (((-1) ^ (2 * k + ↑1 + 1) + 1) * (z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1))

Tactic:
Fin.val_one,

Goal state after:
case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    -I / 2 * (((-1) ^ (2 * k + 0 + 1) + 1) * (z * I) ^ (2 * k + 0) / ↑(2 * k + 0)) +
      -I / 2 * (((-1) ^ (2 * k + 1 + 1) + 1) * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ p < sqrt (p * q)

Tactic:
nth_rw 1 [← mul_self_sqrt p, sqrt_mul]

Goal state after:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ sqrt p * sqrt p < sqrt p * sqrt q
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe

Goal state after:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy p < log 2
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ 1

Tactic:
exact ConcaveOn.congr (concaveOn_id (convex_Ici _)) nnrpow_one_eqOn.symm

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ AEStronglyMeasurable (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo
    exact ContinuousOn.mono (continuousOn_rpowIntegrand₀₁ hp hx) Ioo_subset_Ioi_self

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2)

Tactic:
rw [Complex.Gamma_mul_Gamma_one_sub, cpow_one]
    ring_nf

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

Goal state before:
pp: p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ p.rpowIntegrand₁₂ t x

Tactic:
by
  by_cases ht' : 0 < t
  · rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht']
    refine mul_nonneg hx ?_
    exact rpowIntegrand₀₁_nonneg (by grind) (by grind) hx
  · have ht' : t = 0 := by grind
    simp [rpowIntegrand₁₂, ht', zero_rpow (by grind : p - 1 ≠ 0)]

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioi 1
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₁₂) (Ioi 0 ×ˢ s)

Tactic:
by
  unfold rpowIntegrand₁₂
  fun_prop (disch := grind)

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p = (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * ∫ (a : ℝ) in Ioi 0, x * (p - 1).rpowIntegrand₀₁ a x

Tactic:
integral_const_mul_of_integrable
      (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx)

Goal state after:
p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p =
    (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * (x * ∫ (x_1 : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ x_1 x)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ =
    deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + √π * γ

Tactic:
rw [funext Gamma_mul_Gamma_add_half]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b ^ (log b r + 1)

pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r < ↑b ^ (log b r + 1)

Tactic:
· rw [log_of_right_le_zero _ hr, zero_add, zpow_one]
    exact hr.trans_lt (zero_lt_one.trans_le <| mod_cast hb.le)

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r < ↑b ^ (log b r + 1)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ (log b r + 1)

Tactic:
log_of_one_le_right _ hr1,

Goal state after:
case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ (↑(Nat.log b ⌊r⌋₊) + 1)