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

Goal state before:
pp: case h.refine_2.inr.inl
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h✝ : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree = f.natDegree
n : ℕ
h : n = f.natDegree
⊢ ‖(map (algebraMap K L) (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i)).coeff n - f.coeff n‖ < ε

pp: case h.refine_2.inr.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h✝ : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree = f.natDegree
n : ℕ
h : f.natDegree < n
⊢ ‖(map (algebraMap K L) (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i)).coeff n - f.coeff n‖ < ε

Tactic:
· simp [h, hf, hε]

Goal state after:
case h.refine_2.inr.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h✝ : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree = f.natDegree
n : ℕ
h : f.natDegree < n
⊢ ‖(map (algebraMap K L) (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i)).coeff n - f.coeff n‖ < ε
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
hna : IsNonarchimedean f
⊢ IsNonarchimedean (seminormFromBounded' f)

Tactic:
by
  refine fun x y ↦ ciSup_le (fun z ↦ ?_)
  rw [le_max_iff]
  suffices hf : f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z by
    rcases hf with hfx | hfy
    · exact Or.inl <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z hfx
    · exact Or.inr <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z hfy
  by_cases hz : f z = 0
  · simp only [hz, div_zero, le_refl, or_self_iff]
  · rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz),
      div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul, ← le_max_iff]
    exact hna _ _

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ f x ≤ ⨆ y, f x * (f y / f y)

Tactic:
by_cases! f_ne_zero : f ≠ 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
⊢ f x ≤ ⨆ y, f x * (f y / f y)

case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
⊢ f x ≤ ⨆ y, f x * (f y / f y)
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ (fun y ↦ f (x * y) / f y) y ≤ f x

Tactic:
· rw [← mul_one (f x), ← div_self hy0, ← mul_div_assoc,
          div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy0), mul_div_assoc, div_self hy0, mul_one]
        exact hx y

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

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
⊢ nβ (f x) ≤ nα x

Tactic:
apply ge_of_tendsto hlim

Goal state after:
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
⊢ ∀ᶠ (c : ℕ) in atTop, nβ (f x) ≤ C ^ (1 / ↑c) * nα x
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nβ (f (x ^ n)) ≤ C * nα x ^ n

Tactic:
apply le_trans (hC (x ^ n))

Goal state after:
case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ C * nα (x ^ n) ≤ C * nα x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : n < P.natDegree
⊢ ↑n ≤ ↑P.natDegree

Tactic:
Nat.cast_le

Goal state after:
case pos
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : n < P.natDegree
⊢ n ≤ P.natDegree
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
⊢ (map (algebraMap L f.SplittingField) f).degree ≠ 0

Tactic:
by simpa using degree_ne_of_natDegree_ne fnatdeg0

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ (map (algebraMap L f.SplittingField) f).degree ≠ 0

Tactic:
by simpa using degree_ne_of_natDegree_ne fnatdeg0

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
hn' : ∀ n < p.natDegree, f (p.coeff n • x ^ n) < f (x ^ p.natDegree)
g : ℕ → L := fun i ↦ p.coeff i • x ^ i
⊢ ∃ m, ∃ (_ : 0 < p.natDegree → m < p.natDegree), f ((Finset.range p.natDegree).sum g) ≤ f (g m)

Tactic:
obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hf_na g
          (Finset.range p.natDegree)

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
hn' : ∀ n < p.natDegree, f (p.coeff n • x ^ n) < f (x ^ p.natDegree)
g : ℕ → L := fun i ↦ p.coeff i • x ^ i
m : ℕ
hm : (Finset.range p.natDegree).Nonempty → m ∈ Finset.range p.natDegree
h : f ((Finset.range p.natDegree).sum g) ≤ f (g m)
⊢ ∃ m, ∃ (_ : 0 < p.natDegree → m < p.natDegree), f ((Finset.range p.natDegree).sum g) ≤ f (g m)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
⊢ ‖p.coeff m‖ ^ (1 / (↑p.natDegree - ↑m) * (↑p.natDegree - ↑m)) ≤ (⨆ x, if x ∈ s then f x else 0) ^ (↑p.natDegree - ↑m)

Tactic:
one_div_mul_cancel (ne_of_gt h),

Goal state after:
case pos
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
⊢ ‖p.coeff m‖ ^ 1 ≤ (⨆ x, if x ∈ s then f x else 0) ^ (↑p.natDegree - ↑m)
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_2
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
x✝ : X.carrier
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case refine_2
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
x✝ : X.carrier
⊢ ↑(Hom.hom f) x✝ = ↑(Hom.hom default) x✝

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: ι : Type u_1
f : ι → ℂ
hf : Summable fun i ↦ log (f i)
⊢ Multipliable f

Tactic:
by_cases! hfn : ∃ n, f n = 0
  · exact multipliable_of_exists_eq_zero hfn
  · exact ⟨_, hasProd_of_hasSum_log hfn hf.hasSum⟩

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

Goal state before:
pp: ι : Type u_1
v : ι → ℝ
hv : Multipliable v
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
obtain ⟨r₁, hr₁⟩ := exists_gt (max 0 <| ∏' i, v i)
  rw [max_lt_iff] at hr₁
  have := hv.hasProd.eventually_le_const hr₁.2
  rw [unconditional, eventually_atTop] at this
  exact ⟨r₁, hr₁.1, this⟩

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 : { P // IsLprojection X P }
⊢ P ⊓ Q ≤ P

Tactic:
rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
      P.prop.proj.eq]

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

Goal state before:
pp: case right
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hu : Summable fun n ↦ ‖f n‖
i : ι
⊢ ‖1 + f i‖ - 1 ≤ ‖f i‖

Tactic:
· simpa [add_comm] using norm_add_le (f i) 1

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

Goal state before:
pp: case e'_6
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable fun i ↦ 1 + f' i
⊢ (fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val = ⇑(∏' (b : ι), (1 + f' b))

Tactic:
exact funext fun k ↦ ContinuousMap.tprod_apply hM k

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ⨅ i, projectiveSeminormAux ↑i * ‖f‖

Tactic:
refine le_ciInf fun ⟨p, hp⟩ ↦ ?_

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x✝ : ↑x.lifts
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ projectiveSeminormAux ↑⟨p, hp⟩ * ‖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
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑(uₛ.prodMap uₐ) ↔ IsStrictMap ⇑uₐ

Tactic:
simp_rw [← coe_coe, ContinuousLinearMap.coe_prodMap, LinearMap.isStrictMap_prodMap_iff, coe_coe,
    uₛ.isStrictMap_of_finiteDimensional, true_and]

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

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
⊢ y ∈ interior s

Tactic:
by
  cases nonempty_fintype ι
  obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h
  obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε
  rw [dist_pi_lt_iff hε] at hxz
  have hyz : ∀ i, y i < z i := by
    refine fun i =>
      (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)
    rw [← Real.norm_eq_abs, ← dist_eq_norm]
    exact (hxz _).le
  obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz
  refine mem_interior.2 ⟨ball y δ, ?_, isOpen_ball, mem_ball_self hδ⟩
  rintro w hw
  refine hs (fun i => ?_) hz
  simp_rw [ball_pi _ hδ, Real.ball_eq_Ioo] at hw
  exact ((hw _ <| mem_univ _).2.trans <| hyz _).le

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

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

Tactic:
← one_def,

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

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

Tactic:
have := hsc.completeSpace_coe

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasFDerivWithinAt γ (ContinuousLinearMap.toSpanSingleton ℝ (v (t + dt) ((fun x ↦ γ (x + dt)) t))) (dt +ᵥ -dt +ᵥ s)
    (t + dt)

Tactic:
← hasDerivWithinAt_iff_hasFDerivWithinAt,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasDerivWithinAt γ (v (t + dt) ((fun x ↦ γ (x + dt)) t)) (dt +ᵥ -dt +ᵥ s) (t + dt)
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
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ uIcc ↑t₀ ↑t ⊆ Icc tmin tmax

Tactic:
exact uIcc_subset_Icc t₀.2 t.2

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

Goal state before:
pp: case inl
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : 0 ≤ b
⊢ ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 = 0

pp: case inr
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : b < 0
⊢ ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 = 0

Tactic:
· lift b to ℕ using h
      simpa using hb

Goal state after:
case inr
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : b < 0
⊢ ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 = 0
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) ≤ ⨆ i, v (p.coeff i) * c ^ i

Tactic:
· obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p
      simp only [gaussNorm, support_nonempty.mpr hp, ↓reduceDIte] at hi
      rw [hi]
      exact le_ciSup (aux_bdd v p) i

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

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
cases P.natDegree.even_or_odd

Goal state after:
case inl
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h✝ : Even P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

case inr
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h✝ : Odd P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case hbc
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∃ v ∈ ae (volume.restrict (Icc 0 (2 * π))), ∀ y ∈ v, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)

Tactic:
use {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}

Goal state after:
case h
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ {x | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (volume.restrict (Icc 0 (2 * π))) ∧
    ∀ 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: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
f g : A[X]
⊢ (f * g).mapMahlerMeasure v = f.mapMahlerMeasure v * g.mapMahlerMeasure v

Tactic:
by
  simp [mapMahlerMeasure, mahlerMeasure_mul]

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

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False

Tactic:
rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this

Goal state after:
case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False

case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
⊢ 1 < p.natDegree

Tactic:
by_contra rid
  rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
  clear rid
  have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
  rcases em (a = 0) with (rfl | ha)
  · obtain rfl : b = 0 := by simpa
    simp at p_nonzero
  · rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
    · refine hx ⟨-b / a, ?_⟩
      assumption_mod_cast
    · assumption_mod_cast

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

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ (ofSeq f).InfinitePos

Tactic:
infinitePos_iff

Goal state after:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ 0 < ofSeq f ∧ ArchimedeanClass.mk (ofSeq f) < 0