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

Goal state before:
pp: case inr
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‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖x - (algebraMap ℂ F) (↑‖x‖ + ↑M + 1)‖ = M
⊢ False

Tactic:
norm_sub_rev

Goal state after:
case inr
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‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖(algebraMap ℂ F) (↑‖x‖ + ↑M + 1) - x‖ = M
⊢ False
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedRing F
inst✝ : NormedAlgebra ℝ F
x : F
⊢ Continuous (φ x)

Tactic:
fun_prop

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‖ ≤ ‖w.1 • x - (algebraMap ℝ F) w.2‖

Tactic:
norm_sub_rev

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
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‖
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : f c ≠ 0
hn0 : ¬x = 0
hc0 : f c = 0
⊢ False

Tactic:
exact hc hc0

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

Goal state before:
pp: case inr
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
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
⊢ f (x * c ^ m) * f (c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m

Tactic:
have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt

Goal state after:
case inr
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
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
h1 : 1 ≤ n - m
⊢ f (x * c ^ m) * f (c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case inr
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
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
h1 : 1 ≤ n - m
⊢ f (x * c ^ m) * (f c ^ n * ((f c ^ n)⁻¹ * (f c ^ m)⁻¹)) ≤ f (x * c ^ m) / f c ^ m

Tactic:
← mul_assoc (f c ^ n),

Goal state after:
case inr
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
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
h1 : 1 ≤ n - m
⊢ f (x * c ^ m) * (f c ^ n * (f c ^ n)⁻¹ * (f c ^ m)⁻¹) ≤ f (x * c ^ m) / f c ^ m
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ ↑(s (ψ n)) / ↑(ψ n) ≤ 1

Tactic:
exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (cast_nonneg _)

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

Goal state before:
pp: V W : SemiNormedGrp
f g : V ⟶ W
⊢ ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f = ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g

Tactic:
by
    ext v
    have : v.1 ∈ (f - g).hom.ker := v.2
    simpa [-SetLike.coe_mem, NormedAddGroupHom.mem_ker, sub_eq_zero] using this

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

Goal state before:
pp: X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₁ = e₂

Tactic:
have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl

Goal state after:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = e₂
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : ‖∑ b ∈ T, bound b - S‖ < ε / 3
⊢ ‖S - ∑ b ∈ T, bound b‖ < ε / 3

Tactic:
norm_sub_rev

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : ‖S - ∑ b ∈ T, bound b‖ < ε / 3
⊢ ‖S - ∑ b ∈ T, bound b‖ < ε / 3
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 * spectralNorm K L y

Tactic:
by simp [← spectralMulAlgNorm_def, map_mul]

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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖

Tactic:
by rw [sub_smul, one_smul]

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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖

Tactic:
by
        rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]

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)
⊢ ContinuousAt f 0

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
⊢ ∀ x ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ∀ y ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), dist x y < ε

Tactic:
· intro x hx y hy
    exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : 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
⊢ u.IsFredholm

Tactic:
have h : Topology.IsStrictMap u ∧ IsClosed (u.range : Set F) := by
    rw [u.isStrictMap_isClosed_range_iff_restrict E₁ E₁_closed, eqL]
    exact ⟨F₁.isEmbedding_subtype.comp e.isHomeomorph.isEmbedding |>.isStrictMap, by simpa⟩

Goal state after:
𝕜 : 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
⊢ u.IsFredholm
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 v : E →L[𝕜] F
A : Submodule 𝕜 E
inst✝ : A.CoFG
h_eqOn : EqOn ⇑u ⇑v ↑A
⊢ Continuous[inst✝⁷, inst✝⁴] ⇑u

Tactic:
fun_prop

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
inst✝¹ : T2Space F
u v : E →L[𝕜] F
A : Submodule 𝕜 E
inst✝ : A.CoFG
h_eqOn : EqOn ⇑u ⇑v ↑A
⊢ Continuous[inst✝⁷, inst✝⁴] ⇑v

Tactic:
fun_prop

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
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 ⋯
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝⁴] ↑(↑u).range ↔
    IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed[QuotientModule.Quotient.topologicalSpace A] ↑(↑(A.mkQL ∘SL u)).range

Tactic:
have eq : i ∘ Φ ∘ A.mkQ = p := 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
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
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝⁴] ↑(↑u).range ↔
    IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed[QuotientModule.Quotient.topologicalSpace A] ↑(↑(A.mkQL ∘SL u)).range
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε ↦ δ + ε * x

Tactic:
fun_prop

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

Goal state before:
pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)

Tactic:
fun_prop

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
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
⊢ ContDiffOn ℝ n (fun t ↦ (t, α t)) s

Tactic:
fun_prop

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

Goal state before:
pp: case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (-dt +ᵥ s)
t : ℝ
⊢ γ t = ((γ ∘ fun x ↦ x + dt) ∘ fun x ↦ x + -dt) t

Tactic:
simp only [comp_apply, neg_add_cancel_right]

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

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) (-dt +ᵥ s)
t : ℝ
x✝ : E
⊢ v t x✝ = ((v ∘ fun x ↦ x + dt) ∘ fun x ↦ x + -dt) t x✝

Tactic:
simp only [comp_apply, neg_add_cancel_right]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ Continuous fun a ↦ ‖a t₀ - x₀‖

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ Continuous fun a ↦ ↑r

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ α.toFun t ∈ closedBall x₀ ↑a

Tactic:
by
  rw [mem_closedBall, dist_eq_norm]
  calc
    ‖α t - x₀‖ ≤ ‖α t - α t₀‖ + ‖α t₀ - x₀‖ := norm_sub_le_norm_sub_add_norm_sub ..
    _ ≤ L * |t.1 - t₀.1| + r := by
      apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
      rw [← dist_eq_norm]
      exact α.lipschitzWith.dist_le_mul t t₀
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) + r := by
      gcongr
      exact abs_sub_le_max_sub t.2.1 t.2.2 _
    _ ≤ a - r + r := by gcongr
    _ = a := sub_add_cancel _ _

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)
⊢ Continuous fun x ↦ ↑K ^ (n + 1) * |x - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
fun_prop

Goal state after:
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 ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
⊢ f t = g t

Tactic:
by
  have := dist_le_of_trajectories_ODE_of_mem hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
  rwa [zero_mul, dist_le_zero] at this

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

Goal state before:
pp: case neg.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax = tmin
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmax)

Tactic:
| inr h =>

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
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
by
  have H (t : σ →₀ ℕ) : 0 ≤ ∏ i ∈ t.support, c i ^ t i :=
    Finset.prod_nonneg (fun i hi ↦ pow_nonneg (hc i) (t i))
  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)
  refine Real.iSup_le ?_ ?_
  · refine fun t ↦ calc
    _ ≤ _ := Final t
    _ ≤ max (gaussNorm v c f) (gaussNorm v c g) := by
      simp only [le_sup_iff]
      rcases max_choice (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i)
        (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) with h | h
      · left
        simpa [h] using! le_gaussNorm v c f hbfd t
      · right
        simpa [h] using! le_gaussNorm v c g hbgd t
  · simp only [le_sup_iff]
    left
    exact gaussNorm_nonneg v c f vNonneg

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vna : IsNonarchimedean v
vNeg : ∀ (a : R), v a = v (-a)
hbfg : HasGaussNorm v c (f * g)
i₀ j₀ : σ →₀ ℕ
hi₀ : (v ((coeff i₀) f) * i₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c f
hj₀ : (v ((coeff j₀) g) * j₀.prod fun x1 x2 ↦ c x1 ^ x2) = gaussNorm v c g
hdom' :
  ∀ p ∈ Finset.antidiagonal (i₀ + j₀),
    p ≠ (i₀, j₀) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i₀) f) * v ((coeff j₀) g)
⊢ (v ((coeff i₀) f) * v ((coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2) =
    v ((coeff i₀) f * (coeff j₀) g) * (i₀ + j₀).prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
by rw [vMulEq]

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‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
⊢ Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
⊢ ((fun x ↦ Inv.inv ∘ x) fun x ↦ 0) =ᶠ[↑φ] fun x ↦ 0

Tactic:
by simp only [Function.comp_def, inv_zero, EventuallyEq.rfl]

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

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

Tactic:
min_eq_left h,

Goal state after:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑a = map₂ min ↑a ↑b
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
by
  have := NeZero.pos b
  have := ofDigits_digits_sum_eq (b := b) hx n
  have h_le := Nat.lt_floor_add_one (b ^ n * x)
  rw [← this] at h_le
  rw [← mul_le_mul_iff_right₀ (show 0 < (b : ℝ) ^ n by positivity),
    mul_sub, inv_pow, mul_inv_cancel₀ (by positivity)]
  linarith

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

Goal state before:
pp: b : ℕ
⊢ Continuous ofDigits

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
b✝ n b : ℕ
hb0 : 0 < ↑n + 2
hb : 1 < ↑b
⊢ ∀ (i : ℕ), Continuous fun x ↦ ↑↑(x i) * (↑b ^ (i + 1))⁻¹

Tactic:
fun_prop

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

Goal state before:
pp: b : ℕ
⊢ Continuous ofDigits

Tactic:
by
  match b with
  | 0 => fun_prop
  | 1 => fun_prop
  | n + 2 =>
    obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
    generalize n + 2 = b at hb
    rify at hb0 hb
    refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_
    · simp only [ofDigitsTerm]
      fun_prop
    · exact summable_geometric_of_lt_one (by positivity) (inv_lt_one_of_one_lt₀ hb)
    · simp only [norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg, inv_pow]
      apply ofDigitsTerm_le.trans
      calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind

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

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ (map v p).support, ‖(map v p).coeff n‖ = ∑ n ∈ p.support, ‖p.coeff n‖

Tactic:
support_map_of_injective _ hv.injective

Goal state after:
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ p.support, ‖(map v p).coeff n‖ = ∑ n ∈ p.support, ‖p.coeff n‖
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
by rwa [cast_intCast]

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

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

Tactic:
by rwa [cast_intCast]

Goal state after: