mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
⊢ ∀ (p : L[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Tactic:
intro f

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
⊢ f.Monic → Irreducible f → ∃ x, eval x f = 0
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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt : f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) < f (x ^ p.natDegree)
⊢ f (x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) =
    max (f (x ^ p.natDegree)) (f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i))

Tactic:
exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
mem_ker : g - g' ∈ f.ker
⊢ ‖f g‖ ≤ ‖f‖ * ‖hatg - ↑g‖

Tactic:
by
      simpa [map_sub, hatg_in] using f.completion.le_opNorm (hatg - g)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X✝ Y✝ : SemiNormedGrp₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
⊢ (cokernelCocone f).π ≫ cokernelLift f s = Cofork.π s

Tactic:
ext
              apply NormedAddGroupHom.lift_mk f.1.range
              rintro _ ⟨b, rfl⟩
              change (f ≫ s.π) b = 0
              simp

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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    C (Polynomial.map (algebraMap K L) (minpoly K x)).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)

Tactic:
leadingCoeff_map,

Goal state after:
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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    C ((algebraMap K L) (minpoly K x).leadingCoeff) * (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)
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
inst✝ : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L) (gx * gy)
⊢ spectralNorm K L ((algebraMap (↥K⟮x, y⟯) L) (gx * gy)) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
← spectralNorm.eq_of_normalClosure (gx * gy) hxy,

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L) (gx * gy)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
      ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (gx * gy)) ≤
    spectralNorm K L x * spectralNorm K L y
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
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n

Tactic:
set g := IntermediateField.AdjoinSimple.gen K x with hg

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

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

Tactic:
hn1

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
⊢ smoothingSeminormSeq μ (x * y) n = μ x * smoothingSeminormSeq μ y n
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
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖

Tactic:
rw [add_comm, sub_sub_cancel]
    exact h.Lnorm x

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

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

Tactic:
by
    rw [add_comm, sub_sub_cancel]
    exact h.Lnorm x

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P + Q - P * Q)

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

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

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

Tactic:
rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]

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

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x

Tactic:
have heq : e (lift f'.toMultilinearMap x) = lift f.toMultilinearMap x := by
    induction x using PiTensorProduct.induction_on with
    | smul_tprod =>
      simp only [lift_symm, map_smul, lift.tprod, ContinuousMultilinearMap.coe_coe,
      MultilinearMap.coe_mkContinuous, LinearMap.compMultilinearMap_apply, LinearMap.coe_comp,
      LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.apply_symm_apply, SetLike.val_smul,
      LinearMap.codRestrict_apply, f', f'₀]
    | add _ _ hx hy => simp only [map_add, Submodule.coe_add, hx, hy]

Goal state after:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝¹ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this✝ : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
this : 0 ≤ α • 1
⊢ (α • 1).IsPositive

Tactic:
exact (nonneg_iff_isPositive _).mp this

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : 0 < RCLike.re α
h_comp_adjoint : ↑y ∘SL adjoint ↑y = α • ContinuousLinearMap.id 𝕜 W
β : 𝕜 := ↑(RCLike.re α ^ (-(1 / 2)))
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ β ≠ 0

Tactic:
simp only [β, ne_eq, map_eq_zero]

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : 0 < RCLike.re α
h_comp_adjoint : ↑y ∘SL adjoint ↑y = α • ContinuousLinearMap.id 𝕜 W
β : 𝕜 := ↑(RCLike.re α ^ (-(1 / 2)))
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ ¬RCLike.re α ^ (-(1 / 2)) = 0
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n ↦ (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
· convert! hle n
    rw [MapsTo.iterate_restrict]
    rfl

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₁
this : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k
⊢ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i) ≤
    (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
by gcongr <;> grind

Goal state after:
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 ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasDerivWithinAt γ (v (t + dt) ((fun x ↦ γ (x + dt)) t)) s (t + dt)

Tactic:
apply hγ (t + dt)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ t + dt ∈ s
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
⊢ (Set.range fun t ↦ v ((coeff t) f) * c ^ t) =
    Set.range fun t ↦ v ((MvPowerSeries.coeff t) f) * t.prod fun x x2 ↦ c ^ x2

Tactic:
refine Set.ext (fun _ ↦ ?_)

Goal state after:
R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x✝ : ℝ
⊢ (x✝ ∈ Set.range fun t ↦ v ((coeff t) f) * c ^ t) ↔
    x✝ ∈ Set.range fun t ↦ v ((MvPowerSeries.coeff t) f) * t.prod fun x x2 ↦ c ^ x2
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 ≤ gaussNorm v c p

Tactic:
by
  rw [← gaussNorm_coe_powerSeries _ _ hc, ← coeff_coe]
  apply PowerSeries.le_gaussNorm
  simpa [PowerSeries.HasGaussNorm] using! aux_bdd v p

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

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 ≤ P.leadingCoeff
⊢ 0 < eval x P

Tactic:
replace hlc : 0 < P.leadingCoeff := by
    contrapose! hroots
    exact ⟨x, by simp [leadingCoeff_eq_zero.mp <| eq_of_le_of_ge hroots hlc], le_refl x⟩

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : 0 < P.leadingCoeff
⊢ 0 < eval x P
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ ¬p = 0 → ¬p.mahlerMeasure = 0

Tactic:
exact fun h ↦ by simp [mahlerMeasure_def_of_ne_zero h]

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⌋₊
h_le : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ ↑b ^ n * x
hb : b ≠ 0
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

Tactic:
mul_le_mul_iff_of_pos_left (by positivity)

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⌋₊
h_le : ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
hb : b ≠ 0
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
x : ℕ
x✝ : x ∈ p.support
⊢ ‖(map v p).coeff x‖ = ‖p.coeff x‖

Tactic:
by
    simp [hv.norm_map_of_map_zero (map_zero _)]

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

Goal state before:
pp: x : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x

Tactic:
pow_zero

Goal state after:
x : ℝ
h : Irrational 1
⊢ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hi : ¬x.Infinitesimal
hr : x.IsSt r
⊢ r ≠ 0

Tactic:
by rintro rfl; exact hi hr

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

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

Tactic:
rw [mul_comm]; exact infinite_mul_of_infinite_not_infinitesimal hy hx

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

Goal state before:
pp: k : ℕ
⊢ W k ≤ π / 2

Tactic:
rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]
  rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]
  apply integral_sin_pow_succ_le

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (√(x ^ 2 - 1))⁻¹ x

Tactic:
← sinh_arcosh (le_of_lt hx)

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case a
x : ℝ≥0
⊢ x.agm x ≤ max x x

Tactic:
exact agm_le_max

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

Goal state before:
pp: x y : ℝ≥0
n : ℕ
key : Tendsto (fun n_1 ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
⊢ ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1]
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1,
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2)).2 =
    ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2

Tactic:
Prod.mk.eta,

Goal state after:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun n_1 ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
⊢ ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1]
        ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y))).2 =
    ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ 0 ≤ artanh x

pp: case neg
x : ℝ
hx : 0 ≤ x
h✝ : ¬x < 1
⊢ 0 ≤ artanh x

Tactic:
case pos =>
    rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]
    exact hx

Goal state after:
case neg
x : ℝ
hx : 0 ≤ x
h✝ : ¬x < 1
⊢ 0 ≤ artanh x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: case pos
x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ artanh x ≤ 0

pp: case neg
x : ℝ
hx : x ≤ 0
h✝ : ¬-1 < x
⊢ artanh x ≤ 0

Tactic:
case pos =>
    rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]
    exact hx

Goal state after:
case neg
x : ℝ
hx : x ≤ 0
h✝ : ¬-1 < x
⊢ artanh x ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c : A
⊢ Monotone ⇑(conjSqrt c)

Tactic:
intro a b hab
  by_cases hc : 0 ≤ c
  · exact IsSelfAdjoint.conjugate_le_conjugate hab (by cfc_tac)
  · simp [conjSqrt_of_not_nonneg hc]

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

Goal state before:
pp: p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Tactic:
lhs

Goal state after:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ (∑ n ∈ p.support, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) ((monomial n) (p.coeff n))) * ↑b ^ k =
    ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Tactic:
Finset.sum_mul,

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∑ i ∈ p.support, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) ((monomial i) (p.coeff i)) * ↑b ^ k =
    ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
a₁✝ a₂✝ : A
⊢ addl a₁✝ = addl a₂✝ → a₁✝ = a₂✝

Tactic:
simp [addl]

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
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := ⋯
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (⇑addl '' Ici 0) Ring.inverse

Tactic:
refine ConvexOn.subset CStarAlgebra.convexOn_ringInverse ?_ (Convex.affine_image _ (convex_Ici _))

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ⇑addl '' Ici 0 ⊆ {a | IsStrictlyPositive a}