mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case smul_tprod
ι : 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
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‖
r✝ : 𝕜
f✝ : (i : ι) → E i
⊢ ↑(e ((lift f'.toMultilinearMap) (r✝ • (tprod 𝕜) f✝))) = (lift f.toMultilinearMap) (r✝ • (tprod 𝕜) f✝)

Tactic:
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'₀]

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

Goal state before:
pp: case inr.inl
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
p r : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
e : ↥(lp E p)
hp : 1 ≤ p.toReal
hpqr : p.HolderTriple ∞ r
inst✝ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
obtain rfl : r = p := ENNReal.HolderTriple.unique p ∞ r p

Goal state after:
case inr.inl
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖
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[inst✝³] ↑(↑(i ∘SL u'.domRestrict A)).range

Tactic:
toLinearMap_comp,

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
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[inst✝³] ↑(↑i ∘ₗ ↑(u'.domRestrict A)).range
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
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
by
  -- To reduce to step 3, it suffices to show that, if `u.domRestrict A` has closed range,
  -- then so does `u`.
  suffices IsClosed ((u.domRestrict A).range : Set F) → IsClosed (u.range : Set F) by
    grind only [step3]
  -- This follows from a general lemma, but we recall the proof below for completeness
  simpa using u.toLinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotient

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

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ

pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
· grw [dist_self_sub_left, ← const_def, pi_norm_const_le]
    apply le_of_eq
    simp [abs_of_nonneg, hδ.le]
    ring

Goal state after:
case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
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
⊢ ↑u ≈ ↑(p ∘SL u)

Tactic:
toLinearMap_comp,

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
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
⊢ ↑u ≈ ↑p ∘ₗ ↑u
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β : β * β = α⁻¹
⊢ (starRingEnd 𝕜) β = β

Tactic:
by simp [β]

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

Goal state before:
pp: case a
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ x ∈ Icc a b

Tactic:
· exact hx

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := ⋯
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun x ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 β)

Tactic:
h y hy |>.fixedPoint_unique (hβ.iterate m)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑(1 - C)⁻¹
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun x ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 (ContractingWith.fixedPoint (next hf hy)^[m] ⋯))
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : x ∈ {a | eval a Q ∣ eval a P} \ {x | |eval x Q| ≤ |eval x R|}
⊢ x ∈ {x | R.IsRoot x}

Tactic:
simp only [Set.mem_sdiff, Set.mem_ofPred_eq, not_le] at mx

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : eval x Q ∣ eval x P ∧ |eval x R| < |eval x Q|
⊢ x ∈ {x | R.IsRoot x}
Module: Mathlib.Analysis.Polynomial.Order

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

Tactic:
suffices 0 < (-P).eval x by apply neg_pos.mp; rwa [← eval_neg]

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
⊢ 0 < eval x (-P)
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec * ↑prec + 1 / ↑prec * ↑prec) ^ 2

Tactic:
div_mul_cancel₀,

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt + 1 / ↑prec * ↑prec) ^ 2

case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ volume ({x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) = 0

Tactic:
apply (Finite.of_sdiff _ <| finite_singleton (2 * π)).measure_zero

Goal state after:
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ (({x | x ∉ {x | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) \ {2 * π}).Finite
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) = √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 * 2 ^ (n + 1)

Tactic:
div_mul_cancel₀,

Goal state after:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) = √(2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)

case h
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
have := ofDigits_digits_sum_eq (b := b) hx n
  have h_le := Nat.floor_le (a := b ^ n * x) (by have := hx.left; positivity)
  have hb := NeZero.ne b
  rw [← this, mul_le_mul_iff_of_pos_left (by positivity)] at h_le
  exact h_le

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

Goal state before:
pp: x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
⊢ Irrational x

Tactic:
by
  rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
  · rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
    simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
      (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv
  refine irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos
  rintro ⟨y, rfl⟩
  rw [← Int.cast_pow, Int.cast_inj] at hxr
  subst m
  have : y ≠ 0 := by rintro rfl; rw [zero_pow hnpos.ne'] at hm; exact hm rfl
  rw [(Int.finiteMultiplicity_iff.2 ⟨by simp [hp.1.ne_one], this⟩).multiplicity_pow
    (Nat.prime_iff_prime_int.1 hp.1), Nat.mul_mod_right] at hv
  exact hv rfl

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m + x)
⊢ Irrational x

Tactic:
← cast_intCast

Goal state after:
x : ℝ
m : ℤ
h : Irrational (↑↑m + x)
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)

Tactic:
← cast_intCast

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)

Tactic:
← cast_intCast

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑m)

Tactic:
← cast_intCast

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational (1 / x)
⊢ Irrational (↑1 / x)

Tactic:
by rwa [cast_one]

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ arcosh x

Tactic:
apply log_nonneg

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ x + √(x ^ 2 - 1)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case zero
x y : ℝ≥0
⊢ (x.agmSequences y 0).1 ≤ (x.agmSequences y (0 + 1)).1 ∧ (x.agmSequences y (0 + 1)).2 ≤ (x.agmSequences y 0).2

Tactic:
exact le_gm_and_am_le (sqrt_mul_le_half_add ..)

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

Goal state before:
pp: x y : ℝ≥0
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
by
  obtain h | h := le_total x y
  · rw [min_eq_left h, max_eq_right h]
  · rw [min_eq_right h, max_eq_left h, agmSequences_comm]

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

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

Tactic:
case neg => grind [artanh_eq_zero_iff]

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

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

Tactic:
case neg => grind [artanh_eq_zero_iff]

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
have := ((hasSum_taylorSeries_log (z := z * I) (by simpa)).add
    (hasSum_taylorSeries_neg_log (z := z * I) (by simpa))).mul_left (-I / 2)
  simp_rw [← add_div, ← add_one_mul, hasSum_arctan_aux hz] at this
  replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
  dsimp [Function.comp_def] at this
  simp_rw [← mul_comm 2 _] at this
  refine this.prod_fiberwise fun k => ?_
  dsimp only
  convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1
  rw [Fin.sum_univ_two, Fin.val_zero, Fin.val_one, Odd.neg_one_pow (n := 2 * k + 0 + 1) (by simp),
    neg_add_cancel, zero_mul, zero_div, mul_zero, zero_add,
    show 2 * k + 1 + 1 = 2 * (k + 1) by ring, Even.neg_one_pow (n := 2 * (k + 1)) (by simp),
    ← mul_div_assoc (_ / _), ← mul_assoc, show -I / 2 * (1 + 1) = -I by ring]
  congr 1
  rw [mul_pow, pow_succ' I, pow_mul, I_sq,
    show -I * _ = -(I * I) * (-1) ^ k * z ^ (2 * k + 1) by ring, I_mul_I, neg_neg, one_mul]

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

Goal state before:
pp: p : ℝ
hp : p < 0
⊢ binEntropy p < 0

Tactic:
rw [binEntropy, log_inv, log_inv]
  suffices -p * log p < (1 - p) * log (1 - p) by linarith
  by_cases hp' : p < -1
  · have : log p < log (1 - p) := by
      rw [← log_neg_eq_log]
      exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)
    nlinarith [log_pos_of_lt_neg_one hp']
  · have : -p * log p ≤ 0 := by
      wlog h : -1 < p
      · simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]
      · nlinarith [log_neg_of_lt_zero hp h]
    nlinarith [(log_pos (by linarith) : 0 < log (1 - p))]

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
⊢ 0 < deriv (qaryEntropy q) p

Tactic:
simp only [one_div, interior_Icc, mem_Ioo] at hp

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ 0 < deriv (qaryEntropy q) p
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
⊢ I 1 θ * θ ^ 2 * θ = 4 * sin θ - 4 * θ * cos θ

Tactic:
recursion' 0,

Goal state after:
θ : ℝ
⊢ (-(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) + 2 * (↑0 + 1) * (2 * ↑0 + 1) * I 0 θ - 4 * (↑0 + 1) * ↑0 * I (0 - 1) θ) *
      θ =
    4 * sin θ - 4 * θ * cos θ
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_mul_le.trans ?_

Goal state after:
case refine_2
n : ℕ
⊢ ((monomial 2) (-4)).natDegree + (sinPoly n).natDegree ≤ n + 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - 1 / ↑q) 1)
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
⊢ deriv (qaryEntropy q) p < 0

Tactic:
simp only [one_div, interior_Icc, mem_Ioo] at hp

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ deriv (qaryEntropy q) p < 0
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - x ^ 2 ∧ 1 - x ^ 2 ≤ 1

Tactic:
constructor <;> nlinarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ p⁻¹ • cfc (fun x ↦ x ^ p - 1) a = p⁻¹ • (a ^ p - 1)

Tactic:
cfc_sub _ _ (hf := by fun_prop (disch := grind)),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ p⁻¹ • (cfc (fun x ↦ x ^ p) a - cfc (fun x ↦ 1) a) = p⁻¹ • (a ^ p - 1)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ

Tactic:
set C := |log (b / a)| with hC_def

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
⊢ ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ
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
⊢ y ∈ {a | IsStrictlyPositive a} → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
(ypos : IsStrictlyPositive y)

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 : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
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⁻¹ʳ
⊢ IsStrictlyPositive (a • 1 + b • z)

Tactic:
by_cases ha' : 0 < a <;> grind [smul_nonneg]

Goal state after: