mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w✝¹ : SeminormedAddCommGroup G
w✝ : NormedSpace 𝕜 G
h : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ projectiveSeminorm

Tactic:
;

Goal state after:
case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w✝¹ : SeminormedAddCommGroup G
w✝ : NormedSpace 𝕜 G
h : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ projectiveSeminorm
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w✝¹ : SeminormedAddCommGroup G
w✝ : NormedSpace 𝕜 G
h : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
x : ⨂[𝕜] (i : ι), E i
⊢ ((normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)) x ≤
    projectiveSeminorm x

Tactic:
;

Goal state after:
case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w✝¹ : SeminormedAddCommGroup G
w✝ : NormedSpace 𝕜 G
h : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
x : ⨂[𝕜] (i : ι), E i
⊢ ((normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)) x ≤
    projectiveSeminorm x
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
p q : ℝ≥0∞
H : Type u_6
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : NormedSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : p.HolderConjugate q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
⊢ ‖ContinuousLinearMap.postcomp (↥(lp F q)) (tsumCLM 𝕜 ι H)‖ * ‖holderL 1 B hBK‖ ≤ 1 * ↑K

Tactic:
by
    gcongr
    · exact ContinuousLinearMap.norm_postcomp_le _ |>.trans norm_tsumCLM_le
    · exact norm_holderL_le 1 B hBK

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Hom.Basic

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : Group α
inst✝ : GroupSeminormClass F α ℝ
f : F
x y z : α
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)

Tactic:
;

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : Group α
inst✝ : GroupSeminormClass F α ℝ
f : F
x y z : α
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
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.topologicalClosure
⊢ IsStrictMap ((↑A.topologicalClosure).domRestrict ⇑u) ∧
      IsClosed[inst✝⁴] (range ((↑A.topologicalClosure).domRestrict ⇑u)) ↔
    IsStrictMap ((↑A.topologicalClosure).domRestrict ⇑v) ∧
      IsClosed[inst✝⁴] (range ((↑A.topologicalClosure).domRestrict ⇑v))

Tactic:
domRestrict_eq_domRestrict_iff.mpr h_eqOn

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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
⊢ ∃ z, ¬(f (smulRight v u)) z = 0 z

Tactic:
simp_rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff,
      ContinuousLinearMap.ext_iff, not_forall, smulRight_apply, zero_apply,
      smul_eq_zero_iff_left hu]
    exact ⟨u, huv⟩

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

Goal state before:
pp: case e_6
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := ⋯
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x : V
⊢ smulRight v (A x) = A * smulRight v x

Tactic:
;

Goal state after:
case e_6
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := ⋯
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x : V
⊢ smulRight v (A x) = A * smulRight v x
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case e_6
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x x✝ : V
⊢ (smulRight v (A x)) x✝ = (A * smulRight v x) x✝

Tactic:
;

Goal state after:
case e_6
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
A : V →L[𝕜] V
x x✝ : V
⊢ (smulRight v (A x)) x✝ = (A * smulRight v x) x✝
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
⊢ ∃ U, f = U.conjContinuousAlgEquiv

Tactic:
by_cases! hV : Subsingleton V
  · by_cases! hV : Subsingleton W
    · exact ⟨{ toLinearEquiv := 0 }, ext <| Subsingleton.allEq _ _⟩
    simpa using congr(f $(Subsingleton.allEq 0 1))
  simp_rw [ContinuousAlgEquiv.ext_iff, funext_iff, conjContinuousAlgEquiv_apply, ← comp_assoc,
    eq_comp_toContinuousLinearMap_symm]
  obtain ⟨u, hu⟩ := exists_ne (0 : V)
  obtain ⟨v, huv⟩ := SeparatingDual.exists_ne_zero (R := 𝕜) hu
  obtain ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : W →L[𝕜] W) z := by
    simp_rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff,
      ContinuousLinearMap.ext_iff, not_forall, smulRight_apply, zero_apply,
      smul_eq_zero_iff_left hu]
    exact ⟨u, huv⟩
  set T := apply' _ (.id 𝕜) z ∘L f.toContinuousAlgHom.toContinuousLinearMap ∘L smulRightL 𝕜 _ _ v
  have hT x : T x = f (smulRight v x) z := rfl
  have this A x : T (A x) = f A (T x) := by
    simp only [hT, ← mul_apply_eq_comp, ← map_mul]
    congr; ext; simp
  have ⟨d, hd⟩ := SeparatingDual.exists_eq_one (R := 𝕜) hz
  have surj : Function.Surjective T := fun w ↦ ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
  have inj : Function.Injective T := fun x y hxy ↦ by
    have h_smul : smulRight v x = smulRight v y := by
      apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp [← this, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)
  set Tₗ : V ≃ₗ[𝕜] W := .ofBijective T.toLinearMap ⟨inj, surj⟩
  set T' := apply' _ (.id 𝕜) u ∘L f.symm.toContinuousAlgHom.toContinuousLinearMap ∘L
    smulRightL 𝕜 _ _ d
  set TL : V ≃L[𝕜] W := { Tₗ with
    continuous_toFun := T.continuous
    continuous_invFun := by
      change Continuous Tₗ.symm.toLinearMap
      suffices T'.toLinearMap = Tₗ.symm from this ▸ T'.continuous
      simp [LinearMap.ext_iff, ← Tₗ.injective.eq_iff, T', this, hT, hd, Tₗ] }
  exact ⟨TL, fun A ↦ (ContinuousLinearMap.ext <| this A).symm⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
h : ∀ t ∈ s, IsIntegralCurveAt γ v t
⊢ IsIntegralCurveOn γ v s

Tactic:
intros t ht
  obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)
  exact h _ (mem_of_mem_nhds hs') |>.hasDerivWithinAt

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), (adjoint ↑y.symm ∘SL adjoint x) ∘SL adjoint ↑y = ↑y ∘SL adjoint x ∘SL ↑y.symm
x : V →L[𝕜] V
⊢ ((adjoint ↑y ∘SL adjoint ↑y.symm) ∘SL adjoint x) ∘SL adjoint ↑y = adjoint x ∘SL adjoint ↑y

Tactic:
← adjoint_comp

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), (adjoint ↑y.symm ∘SL adjoint x) ∘SL adjoint ↑y = ↑y ∘SL adjoint x ∘SL ↑y.symm
x : V →L[𝕜] V
⊢ adjoint (↑y ∘SL x ∘SL ↑y.symm ∘SL ↑y) = adjoint (↑y ∘SL x)
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
this : n₀ ≤ j ∧ j < k
⊢ j + 1 ≤ k

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
this : n₀ ≤ j ∧ j < k
⊢ j + 1 ≤ k
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
⊢ c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ((∏ k ∈ Ico (j + 1) k, c k) * c k)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
⊢ c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ((∏ k ∈ Ico (j + 1) k, c k) * c k)
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ((∏ x ∈ Ico n₀ k, c x) * c k) + (c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k)

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ((∏ x ∈ Ico n₀ k, c x) * c k) + (c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k)
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : ¬K = 0
⊢ δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1) ≤ δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)

Tactic:
· have hK_pos : 0 < K := by positivity
    gcongr

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

Goal state before:
pp: case hc
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ 0 ≤ 1 - ↑K

pp: case hab
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Tactic:
;

Goal state after:
case hc
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ 0 ≤ 1 - ↑K

case hab
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n
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 : ℝ → 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 : dist (f a) (g a) ≤ δ
t✝ : ℝ
a✝ : t✝ ∈ Ico a b
⊢ dist (v t✝ (f t✝)) (v t✝ (f t✝)) ≤ 0

Tactic:
;

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ 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 : dist (f a) (g a) ≤ δ
t✝ : ℝ
a✝ : t✝ ∈ Ico a b
⊢ dist (v t✝ (f t✝)) (v t✝ (f t✝)) ≤ 0
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t = β.toFun t
⊢ { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } = β

Tactic:
;

Goal state after:
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t = β.toFun t
⊢ { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } = β
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ } =
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }

Tactic:
;

Goal state after:
case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ } =
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ toFun✝¹ = toFun✝

Tactic:
;

Goal state after:
case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ toFun✝¹ = toFun✝
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
t : ↑(Icc tmin tmax)
⊢ toFun✝¹ t = toFun✝ t

Tactic:
;

Goal state after:
case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
t : ↑(Icc tmin tmax)
⊢ toFun✝¹ t = toFun✝ t
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ })
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } =
    (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ }) β
⊢ { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } = β

Tactic:
;

Goal state after:
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ })
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } =
    (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ }) β
⊢ { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } = β