mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)

Tactic:
· set p := minpoly K x
    have hp_sp : Splits ((minpoly K x).map (algebraMap K L)) := hn.splits x
    obtain ⟨s, hs⟩ := splits_iff_exists_multiset.mp hp_sp
    have h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1 := by
      rw [minpoly.monic (hn.isIntegral x), map_one]
    rw [leadingCoeff_map, h_lc, map_one, one_mul] at hs
    simp only [spectralNorm]
    rw [← max_norm_root_eq_spectralValue hf_pm hf_na hf1 _ _ hs]
    apply ciSup_le
    intro y
    split_ifs with h
    · obtain ⟨σ, hσ⟩ : ∃ σ : Gal(L/K), σ x = y := minpoly.exists_algEquiv_of_root'
        (Algebra.IsAlgebraic.isAlgebraic x) (aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)
      rw [← hσ]
      apply Finite.le_ciSup _ σ
    · exact iSup_nonneg fun σ ↦ apply_nonneg _ _

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f x - f y = 0

Tactic:
rw [← map_sub]

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f (x - y) = 0
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: case e_a.e_s
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
i : ι
⊢ i ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support ↔ i ∈ (zipWith nndist ⋯ f.ofLp g.ofLp).support

Tactic:
simp [← coe_nndist]

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

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree =
    (spectralMulAlgNorm K E) (-1) ^ ((mapAlg K E) (minpoly K x)).natDegree *
      (spectralMulAlgNorm K E) ((mapAlg K E) (minpoly K x)).roots.prod

pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ((mapAlg K E) (minpoly K x)).Monic

pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0

Tactic:
map_neg_eq_map,

Goal state after:
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree =
    (spectralMulAlgNorm K E) 1 ^ ((mapAlg K E) (minpoly K x)).natDegree *
      (spectralMulAlgNorm K E) ((mapAlg K E) (minpoly K x)).roots.prod

K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ((mapAlg K E) (minpoly K x)).Monic

K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0
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
x : X
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖

Tactic:
sub_add_sub_cancel',

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
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 : { P // IsLprojection X P }
Q : M
⊢ ↑Pᶜ * Q = Q - ↑P * Q

Tactic:
rw [coe_compl, sub_mul, one_mul]

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 R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑R → ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))

Tactic:
intro h₁ h₂

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑R
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))
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 R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑Q → ↑P = ↑P * ↑R → ↑P = ↑P * ↑Q * ↑R

Tactic:
intro h₁ h₂

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑P = ↑P * ↑R
⊢ ↑P = ↑P * ↑Q * ↑R
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
⊢ Disjoint E₁ (↑u).ker

Tactic:
rw [disjoint_iff_comap_eq_bot, ← LinearMap.ker_domRestrict, eqₗ,
      LinearMap.ker_comp, ker_subtype, comap_bot, LinearEquiv.ker]

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
⊢ IsClosed ↑(upperClosure s)

Tactic:
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ ↑(upperClosure s)
hx : Filter.Tendsto f Filter.atTop (nhds x)
⊢ x ∈ ↑(upperClosure s)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val✝ : Fintype ι
⊢ IsClosed ↑(lowerClosure s)

Tactic:
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ ↑(lowerClosure s)
hx : Filter.Tendsto f Filter.atTop (nhds x)
⊢ x ∈ ↑(lowerClosure s)
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n : ℕ
hn : n₀ ≤ n
⊢ u n ≤ u n₀ * ∏ i ∈ Ico n₀ n, c i + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, c i

Tactic:
by
  induction n, hn using Nat.le_induction with
  | base => simp
  | succ k hk ih =>
    have hck : 0 ≤ c k := hc k hk
    have heq : c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
        ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i := by
      rw [sum_Ico_succ_top hk, mul_sum, Ico_self, prod_empty, mul_one]
      refine congr_arg (· + b k) (sum_congr rfl fun j hj ↦ ?_)
      rw [prod_Ico_succ_top (by have := mem_Ico.mp hj; omega)]; ring
    calc u (k + 1)
      _ ≤ c k * u k + b k := hu k hk
      _ ≤ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i +
            ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k := by gcongr
      _ = u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i +
            ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i := by
          rw [← heq, ← prod_Ico_mul_eq_prod_Ico_add_one hk]; ring

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ↑L * |↑t - ↑t₀| + ↑r ≤ ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) + ↑r

Tactic:
by
      gcongr
      exact abs_sub_le_max_sub t.2.1 t.2.2 _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
by_cases h : P = 0

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P : R[X]
⊢ (fun x ↦ eval x P) ~[cobounded R] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
by_cases h : P = 0

Goal state after:
case pos
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P : R[X]
h : P = 0
⊢ (fun x ↦ eval x P) ~[cobounded R] fun x ↦ P.leadingCoeff * x ^ P.natDegree

case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P : R[X]
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[cobounded R] fun x ↦ P.leadingCoeff * x ^ P.natDegree
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr.inr
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
rcases eq_or_ne (p + q) 0 with hpq | hpq

Goal state after:
case inr.inr.inl
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
hpq : p + q = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

case inr.inr.inr
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
hpq : p + q ≠ 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
Module: Mathlib.Analysis.RCLike.BoundedContinuous

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

Tactic:
h_comp_eq

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)

Tactic:
rw [coeff_mul, IsNonarchimedean.apply_sum_eq_of_lt vna (by grind) (k := (i, j))
    (s := Finset.antidiagonal (i + j)) (Finset.mem_antidiagonal.mpr rfl) hdom]

Goal state after:
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 : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b ^ (n + 1) * ∑ i ∈ Finset.range (n + 1), ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ (n + 1) * x⌋₊

Tactic:
rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
    set y := (b : ℝ) ^ n * x
    norm_cast
    rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]

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

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z

Tactic:
refine le_trans ?_ hz; rw [sqrtTwoAddSeries_succ]; apply sqrtTwoAddSeries_monotone_left
  have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
  have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
  rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow,
    add_div_eq_mul_add_div _ _ (ne_of_gt hb'), div_le_div_iff₀ hb' (pow_pos hd' _)]
  exact mod_cast h

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: x : ℚ
x✝ : ∃ q, q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
rw [← hn, sqrt_eq, abs_mul_abs_self]

Goal state after:
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: n : ℕ
⊢ ↑↑n.sqrt = ↑n.sqrt

Tactic:
Int.cast_natCast

Goal state after:
n : ℕ
⊢ ↑n.sqrt = ↑n.sqrt
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfinitePos
hx : 0 < x
n : ℕ
⊢ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)| < |ArchimedeanOrder.val (ArchimedeanOrder.of x)|

Tactic:
simpa [abs_of_pos hx] using! h n

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-1) 1
⊢ log ((1 + x) / (1 - x)) / 2 = 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
one_div_mul_eq_div

Goal state after:
x : ℝ
hx : x ∈ Icc (-1) 1
⊢ log ((1 + x) / (1 - x)) / 2 = log ((1 + x) / (1 - x)) / 2
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inl.inr
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Tactic:
exact ⟨0, by simp [hk.ne']⟩

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

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
⊢ False

Tactic:
have j : ∀ᶠ n : ℕ in atTop, (a : ℝ) ^ (2 * n + 1) / n ! * I n (π / 2) < 1 := by
    have := (tendsto_pow_div_factorial_at_top_aux a).eventually_lt_const
      (show (0 : ℝ) < 1 / 2 by simp)
    filter_upwards [this] with n hn
    rw [lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)] at hn
    exact hn.trans_le' (mul_le_mul_of_nonneg_left (I_le _) (by positivity))

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
⊢ False
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)
⊢ (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z

Tactic:
rw [← cfc_smul_id (R := ℝ) (S := ℝ) b z, ← Algebra.algebraMap_eq_smul_one,
        ← cfc_const_add a (fun r => b • r) z]

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)
⊢ cfc (fun x ↦ a + b • x) z ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case ha
s : ℂ
hs : 0 < s.re
⊢ ↑π ^ (-s / 2) ≠ 0

Tactic:
simp [pi_ne_zero]

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

Goal state before:
pp: ⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝 0) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ

Tactic:
(by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))

Goal state after:
⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x < y ↔ b ^ y < x

Tactic:
by
  rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 < logb b x ↔ x < 1

Tactic:
← @logb_one b,

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b 1 < logb b x ↔ x < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < 0 ↔ 1 < x

Tactic:
← @logb_one b,

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < logb b 1 ↔ 1 < x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌊logb (↑b) r⌋ ≤ Int.log b r

Tactic:
← Int.zpow_le_iff_le_log hb hr,

Goal state after:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ ⌊logb (↑b) r⌋ ≤ r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℕ
⊢ ↑(Nat.log b a) ≤ ↑↑(Nat.log b a)

Tactic:
Int.cast_natCast

Goal state after:
a b : ℕ
⊢ ↑(Nat.log b a) ≤ ↑(Nat.log b a)
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ μ.toSphere s = ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)

Tactic:
by
  rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
    ((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
      (Homeomorph.measurableEmbedding _)).comap_apply,
    image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ ∀ (x : ↑(Ioi 0)), (fun x ↦ (ENNReal.ofReal (↑x ^ (dim E - 1))).toReal • f ↑x) x = (fun x ↦ ↑x ^ (dim E - 1) • f ↑x) x

Tactic:
rintro ⟨x, hx : 0 < x⟩

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
x : ℝ
hx : 0 < x
⊢ (fun x ↦ (ENNReal.ofReal (↑x ^ (dim E - 1))).toReal • f ↑x) ⟨x, hx⟩ = (fun x ↦ ↑x ^ (dim E - 1) • f ↑x) ⟨x, hx⟩
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) (Ioi 0) volume ↔
    IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
integrableOn_congr_fun _ measurableSet_Ioi

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn ?m.237 (Ioi 0) volume ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ ℝ → F

E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ EqOn (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) ?m.237 (Ioi 0)