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
inst✝ : Nontrivial F
x : F
⊢ ∃ a, (ofId ℂ F) a = x

Tactic:
obtain ⟨z, hz⟩ := exists_norm_sub_smul_one_eq_zero x

Goal state after:
F : Type u_1
inst✝⁴ : NormedRing F
inst✝³ : NormOneClass F
inst✝² : NormMulClass F
inst✝¹ : NormedAlgebra ℂ F
inst✝ : Nontrivial F
x : F
z : ℂ
hz : ‖x - (algebraMap ℂ F) z‖ = 0
⊢ ∃ a, (ofId ℂ F) a = x
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le h₁ h₂

Goal state after:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
hx : ‖(B.repr (x + y)) ixy‖ ≤ ‖(B.repr x) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)

pp: case inr
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
hy : ‖(B.repr (x + y)) ixy‖ ≤ ‖(B.repr y) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)

Tactic:
· exact le_max_of_le_left (le_trans hx (norm_repr_le_norm B ixy))

Goal state after:
case inr
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
hy : ‖(B.repr (x + y)) ixy‖ ≤ ‖(B.repr y) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ Antitone (seminormFromConst_seq c f x)

Tactic:
intro m n hmn
  simp only [seminormFromConst_seq]
  nth_rw 1 [← Nat.add_sub_of_le hmn]
  rw [pow_add, ← mul_assoc]
  have hc_pos : 0 < f c := lt_of_le_of_ne (apply_nonneg f _) hc.symm
  apply le_trans ((div_le_div_iff_of_pos_right (pow_pos hc_pos _)).mpr (map_mul_le_mul f _ _))
  cases hmn.eq_or_lt with
  | inl heq =>
    have hnm : n - m = 0 := by rw [heq, Nat.sub_self n]
    rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
    conv_rhs => rw [← mul_one (f (x * c ^ n))]
    gcongr
  | inr hlt =>
    have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt
    rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹,
      ← mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
⊢ (⨆ n, if n = 0 then ‖X.coeff n - (C r).coeff n‖ ^ (1 - ↑n)⁻¹ else 0) = ‖r‖

Tactic:
suffices (⨆ n : ℕ, ite (n = 0) ‖r‖ 0) = ‖r‖ by
    rw [← this]
    apply congr_arg
    ext n
    by_cases hn : n = 0
    · rw [if_pos hn, if_pos hn, hn, cast_zero, sub_zero, coeff_X_zero, coeff_C_zero, zero_sub,
        norm_neg, inv_one, rpow_one]
    · rw [if_neg hn, if_neg hn]

Goal state after:
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
⊢ (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: case h
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
x : E
hx : r < ‖x‖
⊢ f x ∈ (closedBall 0 ε)ᶜ

Tactic:
simp [hr x hx]

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

Goal state before:
pp: 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

Tactic:
by_contra h_ge
    have hn_lt (n : ℕ) (hn : n < p.natDegree) : ‖p.coeff n‖ < f x ^ (p.natDegree - n) := by
      have hexp : (‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ))) ^ (p.natDegree - n) =
          ‖p.coeff n‖ := by
        rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
      have h_base : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) < f x := by
        rw [spectralValue, iSup, not_le, Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
          (Set.range_nonempty (spectralValueTerms p))] at h_ge
        have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈
          Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
        exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg
      rw [← hexp, ← rpow_natCast, ← rpow_natCast]
      gcongr
      exact cast_pos.mpr (tsub_pos_of_lt hn)
    have h_deg : 0 < p.natDegree := natDegree_pos_of_monic_of_aeval_eq_zero hp hx
    have h_lt : f ((Finset.range p.natDegree).sum fun i : ℕ ↦ p.coeff i • x ^ i) <
        f (x ^ p.natDegree) := by
      have hn' (n : ℕ) (hn : n < p.natDegree) : f (p.coeff n • x ^ n) < f (x ^ p.natDegree) := by
        by_cases hn0 : n = 0
        · rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg),
            ← Nat.sub_zero p.natDegree, ← hn0]
          exact (mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)
        · have : p.natDegree = p.natDegree - n + n := by rw [Nat.sub_add_cancel (le_of_lt hn)]
          rw [map_smul_eq_mul, hf_pm _ (succ_le_iff.mp (pos_iff_ne_zero.mpr hn0)),
            hf_pm _ (succ_le_iff.mpr h_deg), this, pow_add]
          gcongr
          exact hn_lt n hn
      set g := fun i : ℕ ↦ p.coeff i • x ^ i
      obtain ⟨m, hm_in, hm⟩ : ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
          f ((Finset.range p.natDegree).sum g) ≤ f (g m) := by
        obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hf_na g
          (Finset.range p.natDegree)
        rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
        exact ⟨m, hm, h⟩
      exact lt_of_le_of_lt hm (hn' m (hm_in h_deg))
    have h0 : f 0 ≠ 0 := by
      have h_eq : f 0 = f (x ^ p.natDegree) := by
        rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree,
          one_smul, ← max_eq_left_of_lt h_lt]
        exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)
      exact h_eq ▸ ne_of_gt (lt_of_le_of_lt (apply_nonneg _ _) h_lt)
    exact h0 (map_zero _)

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
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ 1 = smoothingFun μ x ^ a

Tactic:
by rw [ha, rpow_zero]

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
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
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
h_card : p.natDegree - m = (Multiset.map g t).card
r : NNReal
hr : r ∈ Multiset.map g t
w✝ : L
hzt : w✝ ∈ t
hzr : g w✝ = r
⊢ r ≤ g y

Tactic:
exact hzr ▸ hy_max _ (hts _ hzt)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
⊢ hatg ∈ closure ↑(toCompl.comp (incl f.ker)).range

Tactic:
SeminormedAddCommGroup.mem_closure_iff

Goal state after:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
⊢ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: case one
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
exact he

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

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
g : NormedAddGroupHom (SeparationQuotient M) N
⊢ ∀ (x : M), ‖x‖ = 0 → (g.comp normedMk) x = 0

Tactic:
by
    intro x hx
    rw [← norm_mk, norm_eq_zero] at hx
    simp [hx]

Goal state after:
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
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
⊢ ⋯.rightInverse = ↑f.symm

Tactic:
by
  ext y
  exact f.injective <| by simpa using f.hasRightInverse.rightInverse_rightInverse y

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f✝ : ι → R
hf : Summable fun i ↦ ‖f✝ i‖
ε : ℝ
hε : 0 < ε
f : ℝ → ℝ := fun x ↦ Real.exp x - 1
this : Set.Iio ε ∈ 𝓝 (f 0)
⊢ {x | Real.exp x - 1 < ε} ∈ 𝓝 0

Tactic:
exact ContinuousAt.preimage_mem_nhds (by fun_prop) this

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
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

Tactic:
LinearMap.range_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✝³] ↑(map (↑i) (↑(u'.domRestrict A)).range)
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
disj : Disjoint E₁ (↑u).ker
⊢ F₁ ≤ (F₁.subtype ∘ₗ ↑↑e).range

Tactic:
LinearMap.range_comp,

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
disj : Disjoint E₁ (↑u).ker
⊢ F₁ ≤ map F₁.subtype (↑↑e).range
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: u b c : ℕ → ℝ
n₀ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n₀ ≤ n
⊢ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i) ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
by
        gcongr <;> try exact add_nonneg hun₀ <| sum_nonneg <| by grind
        simpa [exp_sum] using prod_le_prod (by grind) (by grind [add_one_le_exp])

Goal state after:
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 : dt +ᵥ t ∈ s
⊢ t + dt ∈ s

Tactic:
vadd_eq_add,

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 : dt + t ∈ s
⊢ t + dt ∈ s
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₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
t₁ t₂ : ↑(Icc tmin tmax)
⊢ ‖∫ (x : ℝ) in ↑t₂..↑t₁, f x (α.compProj x)‖ ≤ ↑L * dist ↑t₁ ↑t₂

Tactic:
Real.dist_eq

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
t₁ t₂ : ↑(Icc tmin tmax)
⊢ ‖∫ (x : ℝ) in ↑t₂..↑t₁, f x (α.compProj x)‖ ≤ ↑L * |↑t₁ - ↑t₂|
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) ↔ IsIntegralCurve γ v

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
  convert! hγ.comp_mul a⁻¹
  · ext t
    simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
  · ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ dist (f t' (((next hf hx)^[n] α).compProj t')) (f t' (((next hf hx)^[n] β).compProj t')) ≤
    ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
compProj_of_mem,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ dist (f t' (((next hf hx)^[n] α).toFun ⟨t', ?m.549⟩)) (f t' (((next hf hx)^[n] β).compProj t')) ≤
    ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ t' ∈ Icc tmin tmax
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:
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.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
n : ℕ
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
⊢ ContDiffOn ℝ (↑n) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
by_cases hlt : tmin < tmax
  · have (t) (ht : t ∈ Icc tmin tmax) :=
      hasDerivWithinAt_picard_Icc ht₀ hf.continuousOn hα hmem x₀ ht
    induction n with
    | zero =>
      simp only [Nat.cast_zero, contDiffOn_zero] at *
      exact HasDerivWithinAt.continuousOn this
    | succ n hn =>
      simp only [Nat.cast_add, Nat.cast_one] at *
      rw [contDiffOn_succ_iff_derivWithin <| uniqueDiffOn_Icc hlt]
      refine ⟨fun t ht ↦ HasDerivWithinAt.differentiableWithinAt (this t ht), by simp, ?_⟩
      apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr
      intro t ht
      exact HasDerivWithinAt.derivWithin (this t ht) <| (uniqueDiffOn_Icc hlt).uniqueDiffWithinAt ht
  · rw [(subsingleton_Icc_of_ge (not_lt.mp hlt)).eq_singleton_of_mem ht₀]
    intro t ht
    rw [eq_of_mem_singleton ht]
    exact contDiffWithinAt_singleton

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
have Final (t : σ →₀ ℕ) : v ((coeff t) (f + g)) * ∏ i ∈ t.support, c ↑i ^ t ↑i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
      (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
    specialize hv (coeff t f) (coeff t g)
    rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h
    · have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_left]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
    · have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_right]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
⊢ min ↑a ↑b = map₂ min ↑a ↑b

Tactic:
rcases le_total (a : β*) b with h | h
    · rw [min_eq_left h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (min_eq_left hi).symm
    · rw [min_eq_right h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (min_eq_right hi).symm

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

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b ^ (n + 1))⁻¹

Tactic:
simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
    rw [tsum_mul_left, tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])]
    have := sub_pos.mpr hb
    field

Goal state after: