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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
⊢ x ∈ K⟮y⟯

Tactic:
let z := x - y
    have := IntermediateField.adjoin.finiteDimensional yint
    have : IsUltrametricDist L := IsUltrametricDist.of_normedAlgebra K
    let y' : K⟮y⟯ := IntermediateField.AdjoinSimple.gen K y
    have zsep : IsSeparable K⟮y⟯ z :=
      Field.isSeparable_sub (IsSeparable.tower_top K⟮y⟯ xsep) (isSeparable_algebraMap y')
    -- It suffices to show that `z = x - y ∈ K⟮y⟯`.
    suffices z ∈ K⟮y⟯ by simpa [z, y'] using add_mem this y'.2
    have : z ∈ K⟮y⟯ ↔ z ∈ (⊥ : Subalgebra K⟮y⟯ L) := by simp [Algebra.mem_bot]
    rw [this]
    -- Suppose not, then there exists nontrivial Galois conjugates `z'` of `z` over `K⟮y⟯` in `L`.
    by_contra hz
    obtain ⟨z', hne, h1⟩ := (notMem_iff_exists_ne_and_isConjRoot zsep
        (minpoly_sub_algebraMap_splits y' (IsIntegral.minpoly_splits_tower_top
          xsep.isIntegral sp))).mp hz
    obtain ⟨σ, hσ⟩ := isConjRoot_iff_exists_algEquiv.mp h1
    apply_fun σ.symm at hσ
    simp only [AlgEquiv.symm_apply_apply] at hσ
    -- However, `‖z - z'‖ ≤ max ‖z‖ ‖z'‖ = ‖z‖ = ‖x - y‖ < ‖y - y'‖ = ‖z - z'‖`, where `y' = x - z`.
    -- This is a contradiction.
    have : ‖z - z'‖ < ‖z - z'‖ :=
      calc
        _ ≤ max ‖z‖ ‖z'‖ := by
          simpa [norm_neg, sub_eq_add_neg] using (IsUltrametricDist.norm_add_le_max z (- z'))
        _ ≤ ‖x - y‖ := by
          simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]
          rw [← AlgEquiv.restrictScalars_apply K,
              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]
          simp [z]
        _ < ‖x - (z' + y)‖ := by
          apply kr (z' + y)
          · apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral
            simpa [z, y'] using IsConjRoot.add_algebraMap y' h1
          · simpa [z, sub_eq_iff_eq_add] using hne
        _ = ‖z - z'‖ := by congr 1; ring
    simp [lt_self_iff_false] at this

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
⊢ iSup (spectralValueTerms P) ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1

Tactic:
refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
⊢ ‖P.coeff n‖ ≤ 1

case refine_2
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
⊢ iSup (spectralValueTerms P) ≤ 1
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
⊢ f x ≤ spectralValue p

Tactic:
by_cases hx0 : f x = 0

Goal state after:
case pos
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
⊢ f x ≤ spectralValue p

case neg
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
⊢ f x ≤ spectralValue p
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
n : ℕ
hn : n ≥ 1
⊢ C * ‖v n‖ ≤ C * b n

Tactic:
gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le

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

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ (ConcreteCategory.hom (f ≫ explicitCokernelπ f)) x = 0

Tactic:
rw [comp_explicitCokernelπ]; rfl

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ nndist f g = ((zipWith nndist ⋯ f.ofLp g.ofLp).sum fun _i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
ext
  simp only [coe_nndist, dist_def, sum, zipWith_apply, NNReal.coe_sum, NNReal.coe_rpow]
  congr 2
  ext i
  simp [← coe_nndist]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
⊢ μ (x * 1) = μ x * 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
⊢ μ x = μ x * 1
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
h1 : μ 1 = 1
hn0 : ↑n ≠ 0
⊢ (μ x ^ ↑n * 1) ^ (1 / ↑n) = μ x

Tactic:
mul_one,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
h1 : μ 1 = 1
hn0 : ↑n ≠ 0
⊢ (μ x ^ ↑n) ^ (1 / ↑n) = μ x
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
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 y : L
⊢ spectralNorm K L (x - y) = spectralNorm K L (-x + y)

Tactic:
← spectralNorm_neg,

Goal state after:
R : Type u_1
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 y : L
⊢ spectralNorm K L (-(x - y)) = spectralNorm K L (-x + y)

R : Type u_1
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 y : L
⊢ IsAlgebraic K (x - y)
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hfg : (g ∘SL f).HasLeftInverse
⊢ f.HasLeftInverse

Tactic:
by
  obtain ⟨fginv, hfginv⟩ := hfg
  refine ⟨fginv.comp g, fun y ↦ ?_⟩
  simp only [comp_apply]
  exact hfginv y

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ (inr R F G).HasLeftInverse

Tactic:
use ContinuousLinearMap.snd _ _ _

Goal state after:
case h
R : Type u_1
inst✝⁶ : Semiring R
F : Type u_4
G : Type u_6
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
⊢ LeftInverse ⇑(snd R F G) ⇑(inr R F G)
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 ⇑u ∧ IsClosed[inst✝⁴] ↑(↑u).range ↔
    IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed[QuotientModule.Quotient.topologicalSpace A] ↑(↑(A.mkQL ∘SL u)).range

Tactic:
calc  IsStrictMap u ∧ IsClosed (range u)
    _ ↔ (IsStrictMap (p ∘ u) ∧ IsClosed (range (p ∘ u))) :=
          ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid _ _ this
    _ ↔ (IsStrictMap (i ∘ Φ ∘ A.mkQ ∘ u) ∧ IsClosed (range (i ∘ Φ ∘ A.mkQ ∘ u))) := by
          simp_rw [← eq, Function.comp_assoc]
    _ ↔ (IsStrictMap (Φ ∘ A.mkQ ∘ u) ∧ IsClosed (range (Φ ∘ A.mkQ ∘ u))) := by
          rw [i_clemb.isStrictMap_iff, i_clemb.isClosed_iff_image_isClosed, ← range_comp]
    _ ↔ (IsStrictMap (A.mkQ ∘ u) ∧ IsClosed (range (A.mkQ ∘ u))) := by
          rw [Φ.isHomeomorph.isEmbedding.isStrictMap_iff,
            Φ.isHomeomorph.isClosedEmbedding.isClosed_iff_image_isClosed,
            ← range_comp]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)

Tactic:
convert! hf.apriori_edist_iterate_efixedPoint_le hx 0
  simp only [pow_zero, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x

Tactic:
apply Setoid.symm'
    apply edist_efixedPoint_lt_top'

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

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
⊢ IsFixedPt f (fixedPoint f^[n] hf)

Tactic:
set x := hf.fixedPoint f^[n]

Goal state after:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
⊢ IsFixedPt f x
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (f ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((f ∘ Neg.neg) t)) (Ici t) t

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t

Tactic:
· intro t ht
    convert!
      HasFDerivWithinAt.comp_hasDerivWithinAt t (hf' (-t) (hmt2 ht))
        (hasDerivAt_neg t).hasDerivWithinAt (hmt3 t)
    simp

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ ∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
⊢ Tendsto (fun x ↦ |eval x P|) atTop atTop

Tactic:
by
  rcases le_total 0 P.leadingCoeff with hP | hP
  · exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)
  · exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
⊢ Tendsto (fun x ↦ |eval x P / eval x Q|) atTop atTop

Tactic:
by
  by_cases! h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
  · exact tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)
  · exact tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)

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

Goal state before:
pp: z : ℂ
this : (X - C z).logMahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
rw [logMahlerMeasure_eq_log_MahlerMeasure] at this

Goal state after:
z : ℂ
this : log (X - C z).mahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
rw [logMahlerMeasure_eq_log_MahlerMeasure] at this

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
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 * ↑⌊↑b ^ n * x⌋₊ + ↑↑(Fin.ofNat b ⌊x * ↑b ^ (n + 1)⌋₊) * 1 = ↑⌊↑b ^ (n + 1) * x⌋₊

Tactic:
mul_one,

Goal state after:
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 * ↑⌊↑b ^ n * x⌋₊ + ↑↑(Fin.ofNat b ⌊x * ↑b ^ (n + 1)⌋₊) = ↑⌊↑b ^ (n + 1) * x⌋₊
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 * ↑⌊↑b ^ n * x⌋₊ + ↑↑(Fin.ofNat b ⌊x * ↑b ^ (n + 1)⌋₊) = ↑⌊↑b ^ (n + 1) * x⌋₊

Tactic:
mul_comm x,

Goal state after:
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 * ↑⌊↑b ^ n * x⌋₊ + ↑↑(Fin.ofNat b ⌊↑b ^ (n + 1) * x⌋₊) = ↑⌊↑b ^ (n + 1) * x⌋₊
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case hbc
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ∏ b ∈ x.toFinset, ‖b ^ count b x‖ ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
norm_pow

Goal state after:
case hbc
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

pp: case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2

Tactic:
· obtain ⟨u, hu, hu'⟩ := exists_between hs
    exact (coe_lt_coe.2 hu).trans_le (H.1 _ hu')

Goal state after:
case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case hbc
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ (g * h).mahlerMeasure

Tactic:
mahlerMeasure_mul

Goal state after:
case hbc
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.mk x ≠ 0 ↔ 0 < ArchimedeanClass.mk x

Tactic:
lt_iff_le_and_ne'

Goal state after:
x : ℝ*
⊢ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.mk x ≠ 0 ↔ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.mk x ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (-↑q + (↑q + x))

Tactic:
neg_add_cancel_left

Goal state after:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
simp [div_eq_mul_inv]

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

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

Tactic:
simp [div_eq_mul_inv]

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

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

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y

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

Tactic:
· simpa [agm_comm, min_comm] using this (not_le.mp h).le

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

Goal state before:
pp: ⊢ Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
by
  apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))
  · have : Tendsto log (𝓝[>] 0) atBot := Real.tendsto_log_nhdsGT_zero
    apply Tendsto.comp (f := (1 - ·)) (g := log) this
    have contF : Continuous ((1 : ℝ) - ·) := continuous_sub_left 1
    have : MapsTo ((1 : ℝ) - ·) (Iio 1) (Ioi 0) := by
      intro p hx
      simp_all only [mem_Iio, mem_Ioi, sub_pos]
    convert! ContinuousWithinAt.tendsto_nhdsWithin (x := (1 : ℝ)) contF.continuousWithinAt this
    exact Eq.symm (sub_eq_zero_of_eq rfl)
  · have h₁ : (1 : ℝ) - (2 : ℝ)⁻¹ < 1 := by norm_num
    filter_upwards [Ico_mem_nhdsLT h₁] with p hx
    gcongr
    exact hx.1

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 : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ 0 < deriv (qaryEntropy q) p

Tactic:
rw [deriv_qaryEntropy (by linarith)]

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 < log (↑q - 1) + log (1 - p) - log p

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)⁻¹
⊢ p ≠ 1
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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c : A
hc : 0 ≤ c
⊢ sqrt c * 1 * sqrt c = c

Tactic:
mul_one,

Goal state after:
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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c : A
hc : 0 ≤ c
⊢ sqrt c * sqrt c = c
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 : ℝ
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

Tactic:
rw [deriv_qaryEntropy (by linarith)]

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
⊢ log (↑q - 1) + log (1 - p) - log p < 0

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
⊢ p ≠ 1