mathlib-initiative/mathlib-tactics huggingface dataset:
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
u_fred : u.IsFredholm
dom₁ : Submodule 𝕜 E
codom₀ : Submodule 𝕜 F
h_dom : IsTopCompl (↑u).ker dom₁
h_codom : IsTopCompl (↑u).range codom₀
⊢ Set.EqOn ⇑u
    ⇑({ X₀ := codom₀, X₁ := (↑u).range, isTopCompl := h_codom, finite_X₀ := ⋯ }.X₁.subtypeL ∘SL
        ↑(((↑u).ker.quotientEquivOfIsTopCompl dom₁ h_dom).symm.trans (ContinuousLinearEquiv.quotKerEquivRange ⋯)) ∘SL
          { X₀ := (↑u).ker, X₁ := dom₁, isTopCompl := ⋯, finite_X₀ := ⋯ }.proj)
    ↑dom₁

Tactic:
·

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
u_fred : u.IsFredholm
dom₁ : Submodule 𝕜 E
codom₀ : Submodule 𝕜 F
h_dom : IsTopCompl (↑u).ker dom₁
h_codom : IsTopCompl (↑u).range codom₀
⊢ Set.EqOn ⇑u
    ⇑({ X₀ := codom₀, X₁ := (↑u).range, isTopCompl := h_codom, finite_X₀ := ⋯ }.X₁.subtypeL ∘SL
        ↑(((↑u).ker.quotientEquivOfIsTopCompl dom₁ h_dom).symm.trans (ContinuousLinearEquiv.quotKerEquivRange ⋯)) ∘SL
          { X₀ := (↑u).ker, X₁ := dom₁, isTopCompl := ⋯, finite_X₀ := ⋯ }.proj)
    ↑dom₁
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
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
tfae_1_to_4 : u.IsFredholm → Nonempty u.FredholmPackage
tfae_4_to_2 : Nonempty u.FredholmPackage → ∃ v, (↑v).IsQuasiInverse ↑u
tfae_2_to_3 :
  (∃ v, (↑v).IsQuasiInverse ↑u) →
    ∃ E₁ F₁,
      IsClosed[inst✝⁸] ↑E₁ ∧
        IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible
tfae_3_to_1 :
  (∃ E₁ F₁,
      IsClosed[inst✝⁸] ↑E₁ ∧
        IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible) →
    u.IsFredholm
⊢ [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u,
      ∃ E₁ F₁,
        IsClosed[inst✝⁸] ↑E₁ ∧
          IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible,
      Nonempty u.FredholmPackage].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteProd

Goal state before:
pp: case inl
α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun n ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))

pp: case inr
α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
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✝ : 𝓕.NeBot
⊢ Tendsto (fun n ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))

Tactic:
·

Goal state after:
case inl
α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun n ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ

pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
·

Goal state after:
case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case pos
𝕜 : 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 : Subsingleton V
⊢ ∃ U, f = U.conjContinuousAlgEquiv

pp: case neg
𝕜 : 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, f = U.conjContinuousAlgEquiv

Tactic:
·

Goal state after:
case pos
𝕜 : 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 : Subsingleton V
⊢ ∃ U, f = U.conjContinuousAlgEquiv
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case pos
𝕜 : 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✝ : Subsingleton V
hV : Subsingleton W
⊢ ∃ U, f = U.conjContinuousAlgEquiv

pp: case neg
𝕜 : 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✝ : Subsingleton V
hV : Nontrivial W
⊢ ∃ U, f = U.conjContinuousAlgEquiv

Tactic:
·

Goal state after:
case pos
𝕜 : 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✝ : Subsingleton V
hV : Subsingleton W
⊢ ∃ U, f = U.conjContinuousAlgEquiv
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ

pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
·

Goal state after:
case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case pos
𝕜 : 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✝ : Subsingleton V
⊢ ∃ U, f = U.conjStarAlgEquiv

pp: case neg
𝕜 : 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
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
·

Goal state after:
case pos
𝕜 : 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✝ : Subsingleton V
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case pos
𝕜 : 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✝¹ : Subsingleton V
h✝ : Subsingleton W
⊢ ∃ U, f = U.conjStarAlgEquiv

pp: case neg
𝕜 : 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✝¹ : Subsingleton V
h✝ : Nontrivial W
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
·

Goal state after:
case pos
𝕜 : 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✝¹ : Subsingleton V
h✝ : Subsingleton W
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
⊢ edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist y (f y) + edist (f x) (f y)

Tactic:
edist_comm y,

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
⊢ edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist (f y) y + edist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint f hf x hx) x

pp: α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid x (efixedPoint f hf y hy)

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint f hf x hx) x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case pos
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

pp: case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
·

Goal state after:
case pos
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
·

Goal state after:
case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
Module: Mathlib.Topology.MetricSpace.Contracting

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

pp: case refine_2
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n ↦ (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case pos
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ

pp: case neg
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ

Tactic:
·

Goal state after:
case pos
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ

Tactic:
·

Goal state after:
case neg
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case pos
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
·

Goal state after:
case pos
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
·

Goal state after:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)
Module: Mathlib.Analysis.ODE.Gronwall

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

pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε ↦ gronwallBound δ K ε x

Tactic:
·

Goal state after:
case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε ↦ gronwallBound δ K ε x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε ↦ gronwallBound δ K ε x

Tactic:
·

Goal state after:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε ↦ gronwallBound δ K ε x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case pos
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : K = 0
⊢ δ + ε * x₁ ≤ δ + ε * x₂

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

Goal state after:
case pos
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : K = 0
⊢ δ + ε * x₁ ≤ δ + ε * x₂
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:
·

Goal state after:
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)
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x

pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid x (efixedPoint' f htc htf hft y hyt hy)

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ gronwallBound δ K ε' (a - a)

pp: case hB
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ ∀ (x : ℝ), HasDerivAt (fun x ↦ gronwallBound δ K ε' (x - a)) (?m.108 x) x

pp: case bound
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ ∀ x ∈ Ico a b, f x = gronwallBound δ K ε' (x - a) → f' x < ?m.108 x

pp: case a
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ x ∈ Icc a b

pp: f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ ℝ → ℝ

Tactic:
·

Goal state after:
case ha
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ gronwallBound δ K ε' (a - a)
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid x y

pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid x y