mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ M * (1 + (‖w - y‖ / M) ^ n) = (M ^ n + ‖w - y‖ ^ n) / M ^ (n - 1)

Tactic:
simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
⊢ M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)

Tactic:
simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this : Tendsto (fun x_1 ↦ ‖(algebraMap ℝ F) x_1.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ sᶜ ×ˢ Set.univ
⊢ ‖(algebraMap ℝ F) w.2‖ - M * ‖x‖ ≤ ‖(algebraMap ℝ F) w.2‖ - ‖w.1 • x‖

Tactic:
specialize hM _ (Set.mem_prod.mp hw).1

Goal state after:
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
this : Tendsto (fun x_1 ↦ ‖(algebraMap ℝ F) x_1.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hM : ‖w.1‖ ≤ M
hw : w ∈ sᶜ ×ˢ Set.univ
⊢ ‖(algebraMap ℝ F) w.2‖ - M * ‖x‖ ≤ ‖(algebraMap ℝ F) w.2‖ - ‖w.1 • x‖
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ IsBoundedUnder LE.le atTop fun n ↦ p (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
by
  have h_le : ∀ m : ℕ, p (x ^ s (ψ m)) ^ (1 / (ψ m : ℝ)) ≤ p x ^ ((s (ψ m) : ℝ) / (ψ m : ℝ)) := by
    intro m
    rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]
    grw [map_pow_le_pow' hp x]
  apply isBoundedUnder_of
  cases le_or_gt (p x) 1 with
  | inl hfx =>
    use 1, fun m ↦ le_trans (h_le m) (rpow_le_one (by positivity) hfx (by positivity))
  | inr hfx =>
    use p x
    refine fun m ↦ le_trans (h_le m) <| rpow_le_self_of_one_le hfx.le ?_
    exact div_le_one_of_le₀ (mod_cast hs_le _) (cast_nonneg _)

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : DecidableEq R✝
inst✝³ : NoZeroDivisors R✝
inst✝² : Nontrivial R✝
R : Type u_2
inst✝¹ : Ring R
inst✝ : Nontrivial R
v : AbsoluteValue R ℝ
⊢ (fun N ↦ { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ })
      ((fun v ↦
          { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
            eq_zero_of_map_eq_zero' := ⋯ })
        v) =
    v

Tactic:
by ext1 x; simp

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

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ ↑f.natDegree ≠ 0

Tactic:
simp only [ne_eq, Nat.cast_eq_zero, hfm, Monic.natDegree_eq_zero]
      intro h
      simp [h] at ha

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

Goal state before:
pp: case refine_1
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
h : seminormFromBounded' f x = 0
⊢ f x = 0

Tactic:
have hf := seminormFromBounded_ge f_nonneg f_mul x

Goal state after:
case refine_1
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
h : seminormFromBounded' f x = 0
hf : f x ≤ f 1 * seminormFromBounded' f x
⊢ f x = 0
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a (∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i)‖ ≤
    ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖

Tactic:
by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this

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)
⊢ f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) < f (x ^ p.natDegree)

Tactic:
set g := fun i : ℕ ↦ p.coeff i • x ^ i

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
⊢ f ((Finset.range p.natDegree).sum g) < f (x ^ p.natDegree)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ μ (x ^ 1) ^ (1 / ↑1) ≤ μ x

Tactic:
pow_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ μ x ^ (1 / ↑1) ≤ μ x
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
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
⊢ m < p.natDegree

Tactic:
exact hm

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
⊢ c ≤ 1

Tactic:
have hμ_lim : Tendsto (fun n : ℕ => μ x ^ (↑(s (ψ n)) * (1 / (ψ n : ℝ)))) atTop (𝓝 1) := by
        nth_rw 1 [← rpow_zero (μ x)]
        convert!
          Tendsto.rpow tendsto_const_nhds hψ_lim
            (Or.inl (ne_of_gt (lt_of_lt_of_le zero_lt_one (not_lt.mp hμx))))
        · simp only [rpow_zero, mul_one_div, Function.comp_apply]
        · rw [rpow_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
hμ_lim : Tendsto (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop (𝓝 1)
⊢ c ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
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
hx : x = 0
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

pp: case neg
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
hx : ¬x = 0
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

Tactic:
· simp [hx, zero_mul, map_zero]

Goal state after:
case neg
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
hx : ¬x = 0
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed (range ⇑f)

Tactic:
rw [← f.range_toLinearMap, ← f.coe_range,
    f.range_eq_ker_of_leftInverse (hf.leftInverse_leftInverse)]

Goal state after:
R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed ↑(↑f ∘ₗ ↑hf.leftInverse - LinearMap.id).ker
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable fun i ↦ log (f i)
⊢ Multipliable f

Tactic:
have : Summable fun i ↦ log (if 0 < f i then f i else 1) := by
    apply hf.congr_cofinite
    filter_upwards [hfn] with i hi using by simp [hi]
  have : Multipliable fun i ↦ if 0 < f i then f i else 1 := by
    refine multipliable_of_summable_log (fun i ↦ ?_) this
    split_ifs with h <;> simp [h]
  refine this.congr_cofinite₀ (fun i ↦ ?_) ?_
  · split_ifs with h <;> simp [h, ne_of_gt]
  · filter_upwards [hfn] with i hi using by simp [hi]

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑R
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))

Tactic:
← h₂,

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ P ≤ R → Q ≤ R → P ⊔ Q ≤ R

Tactic:
by
    rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul,
      sub_mul, mul_assoc]
    intro h₁ h₂
    rw [← h₂, ← h₁]

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑R * ↑Q * ↑Pᶜ) = ↑P + ↑R * ↑Q * ↑Pᶜ

Tactic:
distrib_lattice_lemma

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ ↑P + ↑R * ↑Q * ↑Pᶜ = ↑P + ↑R * ↑Q * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : 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 := ⋯ }
⊢ ∀ᶠ (i : ι) in cofinite, ∀ (x : ↑K), ‖(f' i) x‖ ≤ u i

Tactic:
filter_upwards [h] with i hi using fun x ↦ hi x x.2

Goal state after:
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 ⇑π
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
have u_eq : u = v ∘L π := rfl

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 π
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range
Module: Mathlib.Dynamics.FixedPoints.Topology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ IsFixedPt f y

Tactic:
by
  refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 ?_) hy
  simp only [iterate_succ' f]
  exact hf.tendsto.comp hy

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)
⊢ ?m.622

Tactic:
by simpa using (Subalgebra.mem_center_iff (R := 𝕜)).mpr fun _ ↦ this _

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t ↦ f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
⊢ ‖f' t - g' t‖ ≤ ↑K * ‖f t - g t‖ + (εf + εg)

Tactic:
have := (hv t ht).dist_le_mul _ (hfs t ht) _ (hgs t ht)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t ↦ f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
this✝ : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
this : dist (v t (f t)) (v t (g t)) ≤ ↑K * dist (f t) (g t)
⊢ ‖f' t - g' t‖ ≤ ↑K * ‖f t - g t‖ + (εf + εg)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.degree ≤ 0

Tactic:
simp [leadingCoeff_eq_zero.1 hP]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Tactic:
simp only [h.1, this, pow_zero, mul_one]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x ↦ c) atTop (𝓝 c)
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x✝ : ℝ
⊢ (∃ y, v ((coeff y) f) * c ^ y = x✝) → ∃ y, v ((MvPowerSeries.coeff y) f) * c ^ y PUnit.unit = x✝

pp: case mpr
R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x✝ : ℝ
⊢ (∃ y, v ((MvPowerSeries.coeff y) f) * c ^ y PUnit.unit = x✝) → ∃ y, v ((coeff y) f) * c ^ y = x✝

Tactic:
· intro h
    obtain ⟨y, hy⟩ := h
    use (Finsupp.uniqueEquiv ()).symm y
    simpa [coeff] using hy

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x✝ : ℝ
⊢ (∃ y, v ((MvPowerSeries.coeff y) f) * c ^ y PUnit.unit = x✝) → ∃ y, v ((coeff y) f) * c ^ y = x✝
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < ↑a' - ↑r'
ε' : ℝ := min ε ((↑a' - ↑r') / (↑L + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ t₀ ∈ Icc (t₀ - ε') (t₀ + ε')

Tactic:
by simp [le_of_lt hε'pos]

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

Goal state before:
pp: p : ℂ[X]
⊢ p = 0 → p.mahlerMeasure = 0

Tactic:
by simp_all [mahlerMeasure_zero]

Goal state after:
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
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
θ : ℝ
⊢ 0 < ‖eval (circleMap 0 1 θ) p‖ → rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖

Tactic:
hθ

Goal state after:
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
θ : ℝ
hθ : 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case inl
digits : ℕ → Fin 1
⊢ ofDigits digits ≤ 1

pp: case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ ofDigits digits ≤ 1

Tactic:
· simp [ofDigits, ofDigitsTerm]

Goal state after:
case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ ofDigits digits ≤ 1
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)

Tactic:
rw [summable_nat_add_iff (f := fun n ↦ ((b + 1 : ℕ) : ℝ)⁻¹ ^ n) 1]

Goal state after:
case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ n
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
    · refine hx ⟨-b / a, ?_⟩
      assumption_mod_cast
    · assumption_mod_cast

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

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ (if h : ∃ r, x.IsSt r then Classical.choose h else 0) = r

Tactic:
dif_pos h

Goal state after:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ Classical.choose h = r
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))

Tactic:
inv_div

Goal state after:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
  simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
  rfl

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ tanh (arcosh x) = √(x ^ 2 - 1) / x

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_arcosh hx, cosh_arcosh hx]

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

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| (cos z + sin z * I) / (cos z - sin z * I)

Tactic:
2

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| cos z - sin z * I
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
n✝ m n : ℕ
ih : ∀ {x y : ℝ≥0}, (x.agmSequences y n).1 ≤ (x.agmSequences y n).2
x y : ℝ≥0
⊢ (x.agmSequences y (n + 1)).1 ≤ (x.agmSequences y (n + 1)).2

Tactic:
exact ih

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

Goal state before:
pp: case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x

pp: case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
· exact Real.neg_pi_div_two_lt_arctan _

Goal state after:
case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
⊢ 0 < 1 - tanh x

Tactic:
grind [tanh_lt_one]

Goal state after: