mathlib-initiative/mathlib-tactics huggingface dataset:
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
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
range_eq : (↑v).range = (↑u).range
range_restr_eq : (↑(v.domRestrict B)).range = (↑(u.domRestrict A)).range
π' : ↥A →L[𝕜] ↥B := π.restrict A_mapsTo_B
⊢ IsOpenQuotientMap ⇑π'

Tactic:
let φ : (N.mkQL ⁻¹' B) ≃ₜ A := .setCongr congr(SetLike.coe $comap_B)

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
range_eq : (↑v).range = (↑u).range
range_restr_eq : (↑(v.domRestrict B)).range = (↑(u.domRestrict A)).range
π' : ↥A →L[𝕜] ↥B := π.restrict A_mapsTo_B
φ : ↑(⇑N.mkQL ⁻¹' ↑B) ≃ₜ ↥A := Homeomorph.setCongr ⋯
⊢ IsOpenQuotientMap ⇑π'
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
inst✝¹ : T2Space F
u : E →L[𝕜] F
A : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥A
A_compl : A.ClosedComplemented
S : Submodule 𝕜 F
A_compl_S : IsTopCompl A S
Φ : (F ⧸ A) ≃L[𝕜] ↥S := A.quotientEquivOfIsTopCompl S A_compl_S
i : ↥S →L[𝕜] F := S.subtypeL
i_clemb : IsClosedEmbedding ⇑i
p : F →L[𝕜] F := S.projectionL A ⋯
p_def : p = S.projectionL A ⋯
eq : ⇑i ∘ ⇑Φ ∘ ⇑A.mkQ = ⇑p
this : ↑u ≈ ↑(p ∘SL u)
⊢ IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u)) ↔
    IsStrictMap (⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[instTopologicalSpaceSubtype] (range (⇑Φ ∘ ⇑A.mkQ ∘ ⇑u))

Tactic:
by
          rw [i_clemb.isStrictMap_iff, i_clemb.isClosed_iff_image_isClosed, ← range_comp]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
⊢ IsFixedPt f (efixedPoint f hf x hx)

Tactic:
try apply efixedPoint_isFixedPt

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
⊢ IsFixedPt f (efixedPoint f hf y hy)

Tactic:
try apply efixedPoint_isFixedPt

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞

Tactic:
try apply efixedPoint_isFixedPt

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:

Tactic:
_ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]

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

Goal state before:
pp: n : ℕ
⊢ toAddCircle (X ^ n) = fourier ↑n

Tactic:
by
  ext θ; simp [toAddCircle, AddCircle.toCircle_nsmul]

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

Goal state before:
pp: n : ℕ
c : ℂ
⊢ toAddCircle ((monomial n) c) = c • fourier ↑n

Tactic:
by
  ext θ; simp [toAddCircle, AddCircle.toCircle_nsmul]

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

Goal state before:

Tactic:
‖a‖₊ = ‖a‖₊ - 1 + 1 := (tsub_add_cancel_of_le ha.le).symm
        _ = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 := by field
        _ ≤ (cauchyBound p - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1)
            / ‖a‖₊ ^ p.natDegree + 1 := by gcongr
        _ = (cauchyBound p - 1) * (‖a‖₊ ^ p.natDegree - 1) / ‖a‖₊ ^ p.natDegree + 1 := by
          congr 2
          have : ‖a‖₊ - 1 ≠ 0 := fun nh ↦ (ha.trans_le (tsub_eq_zero_iff_le.mp nh)).false
          field
        _ < (cauchyBound p - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 := by
          gcongr
          · apply lt_of_le_of_ne (by simp)
            contrapose! this
            simp only [← this, zero_mul]
            apply pow_pos
            exact zero_lt_one.trans ha
          simp [zero_lt_one.trans ha]
        _ = cauchyBound p := by simp [field, tsub_add_cancel_of_le]

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

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

Tactic:
intro _

Goal state after:
case neg.inl
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
h : tmax < tmin
x✝ : ℝ
⊢ x✝ ∈ Icc tmin tmax → ContDiffWithinAt ℝ (↑n) α (Icc tmin tmax) x✝
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg.inr
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
h : tmax = tmin
⊢ ContDiffOn ℝ (↑n) α {tmin}

Tactic:
intro _

Goal state after:
case neg.inr
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
h : tmax = tmin
x✝ : ℝ
⊢ x✝ ∈ {tmin} → ContDiffWithinAt ℝ (↑n) α {tmin} x✝
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ CircleIntegrable (fun z ↦ log ‖eval z p‖) 0 1

Tactic:
exact (analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm

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 _

Goal state after:
case h.right
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
y✝ : ℝ
⊢ y✝ ∈ {x | eval (circleMap 0 1 x) p ≠ 0} → log ‖eval (circleMap 0 1 y✝) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)
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
⊢ ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖

Tactic:
ae_restrict_iff' measurableSet_uIoc

Goal state after:
p : ℂ[X]
this✝ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x

Tactic:
simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 0 v = 0

Tactic:
by
  simp [mapMahlerMeasure]

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 1 v = 1

Tactic:
by
  simp [mapMahlerMeasure]

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

Goal state before:
pp: f : ℕ → ℝ
h : ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ Tendsto f (↑(hyperfilter ℕ)) atBot

Tactic:
tendsto_atBot

Goal state after:
f : ℕ → ℝ
h : ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in ↑(hyperfilter ℕ), f a ≤ b
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
← cast_natCast,

Goal state after:
n : ℕ
x : ℝ
⊢ Irrational (↑↑n * x) ↔ n ≠ 0 ∧ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
← cast_natCast,

Goal state after:
n : ℕ
x : ℝ
⊢ Irrational (x * ↑↑n) ↔ n ≠ 0 ∧ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
← cast_natCast,

Goal state after:
n : ℕ
x : ℝ
⊢ Irrational (x / ↑↑n) ↔ n ≠ 0 ∧ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case inl
x : ℝ*
h✝ : 0 ≤ x
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]

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

Goal state before:
pp: case inr
x : ℝ*
h✝ : x ≤ 0
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]

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

Goal state before:
pp: z : ℂ
h₂ : z ≠ -I
h₁ : 1 + z * I = 0
⊢ z = I

Tactic:
add_eq_zero_iff_neg_eq,

Goal state after:
z : ℂ
h₂ : z ≠ -I
h₁ : -1 = z * I
⊢ z = I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₂ : z ≠ -I
h₁ : 1 + z * I = 0
⊢ z = I

Tactic:
rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁

Goal state after:
z : ℂ
h₂ : z ≠ -I
h₁ : I = z
⊢ z = I
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
· exact this.trans (agmSequences_snd_antitone h)

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

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).2
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2

Tactic:
by
    obtain h | h := le_total n m
    · exact (agmSequences_fst_monotone h).trans_lt this
    · exact this.trans_le (agmSequences_snd_antitone h)

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

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ min x y ≤ x.agm y

Tactic:
rw [min_eq_left h]

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ≤ x.agm y
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ tanh (artanh x) = x

Tactic:
have := sq_sub_sq 1 x
  grind [tanh_eq_sinh_div_cosh, sinh_artanh, cosh_artanh, sqrt_ne_zero', mul_pos]

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

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

Tactic:
by simp [hk.ne']

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

Goal state before:
pp: n : ℕ
⊢ ∀ x ∈ Ioc (-1) 1, 0 ≤ (1 - x ^ 2) ^ n * cos (x * (π / 2))

Tactic:
refine fun x hx => mul_nonneg (pow_nonneg ?_ _) ?_

Goal state after:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ 0 ≤ 1 - x ^ 2

case refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ 0 ≤ cos (x * (π / 2))
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
⊢ a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z

Tactic:
CFC.rpow_eq_cfc_real zpos.nonneg

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
⊢ a • 1 + b • cfc (fun x ↦ x ^ (-1)) z = cfc (fun r ↦ a + b * r ^ (-1)) z
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
⊢ ∀ x ∈ spectrum ℝ z, id x ≠ 0 ∨ 0 ≤ -1

Tactic:
by
        #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/
        intro x h
        have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h
        grind

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

Goal state before:
pp: case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
refine mul_nonneg (by positivity) ?_

Goal state after:
case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t⁻¹ - (t + x)⁻¹
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)
⊢ Function.Injective ⇑addl

Tactic:
intro _

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)
a₁✝ : A
⊢ ∀ ⦃a₂ : A⦄, addl a₁✝ = addl a₂ → a₁✝ = a₂
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Gammaℝ 1 = 1

Tactic:
rw [Gammaℝ_def, Complex.Gamma_one_half_eq]

Goal state after:
⊢ ↑π ^ (-1 / 2) * ↑π ^ (1 / 2) = 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case refine_1.refine_2
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (fun q ↦ (q.1 + q.2)⁻¹) (Ioi 0 ×ˢ s)

Tactic:
exact ContinuousOn.inv₀ (by fun_prop) (by grind)

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ s.Gammaℂ = (s - 1 + 1).Gammaℂ

Tactic:
rw [sub_add_cancel]

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 : ℕ
hr : 1 ≤ 1
⊢ (if 1 ≤ 1 then ↑(Nat.log b ⌊1⌋₊) else -↑(Nat.clog b ⌈1⁻¹⌉₊)) = -↑(Nat.clog b ⌈1⁻¹⌉₊)

Tactic:
if_pos hr,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ ↑(Nat.log b ⌊1⌋₊) = -↑(Nat.clog b ⌈1⁻¹⌉₊)
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 : ℕ
hr : 1 ≤ 1
⊢ (if 1 ≤ 1 then ↑(Nat.clog b ⌈1⌉₊) else -↑(Nat.log b ⌊1⁻¹⌋₊)) = -↑(Nat.log b ⌊1⁻¹⌋₊)

Tactic:
if_pos hr,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ ↑(Nat.clog b ⌈1⌉₊) = -↑(Nat.log b ⌊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 : ℕ
r : R
⊢ log b r⁻¹ = -clog b r

Tactic:
by
  rw [← inv_inv r, clog_inv, neg_neg, inv_inv]

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

Goal state before:
pp: case mpr
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x

Tactic:
exact logb_rpow b_pos b_ne_one

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

Goal state before:
pp: b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ log x / log b ≤ log y / log b ↔ x ≤ y

Tactic:
div_le_div_iff_of_pos_right (log_pos hb),

Goal state after:
b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ log x ≤ log y ↔ x ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

Goal state after:
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 : ℕ
hb : 1 < b
r : R
⊢ r ≤ ↑b ^ clog b r

Tactic:
rcases le_or_gt r 0 with hr | hr
  · rw [clog_of_right_le_zero _ hr, zpow_zero]
    exact hr.trans zero_le_one
  rw [← neg_log_inv_eq_clog, zpow_neg, le_inv_comm₀ hr (zpow_pos ..)]
  · exact zpow_log_le_self hb (inv_pos.mpr hr)
  · exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)

Goal state after:
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 : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)

Tactic:
exact zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

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

Goal state before:
pp: ⊢ MonotoneOn (fun x ↦ log x * x) {x | 1 ≤ x}

Tactic:
grind [mul_log_strictMonoOn.monotoneOn, MonotoneOn.mono, show exp (-1) < 1 by norm_num]

Goal state after:
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
⊢ r ≤ ↑b ^ Int.clog b r

Tactic:
exact Int.self_le_zpow_clog hb r

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

Goal state before:
pp: n : ℕ
⊢ ↑n.log2 ≤ logb 2 ↑n

Tactic:
calc (Nat.log2 n : ℝ) = Nat.log 2 n := mod_cast Nat.log2_eq_log_two
  _ ≤ Real.logb 2 n := natLog_le_logb _ _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ

Tactic:
integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using!
        (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal

X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hc : ¬c = 0
⊢ Tendsto (Norm.norm ∘ logb b) atTop atTop

Tactic:
exact tendsto_abs_logb_atTop hb

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

Goal state before:
pp: P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x

Tactic:
induction n with
  | zero => simpa using base
  | succ n ih =>
    exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step (n + 1) (by simp) ih _)

Goal state after: