harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDerivWithin_comp_le_aux {Fu Gu : Type u} [NormedAddCommGroup Fu]
    [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu] {g : Fu → Gu} {f : E → Fu} {n : ℕ}
    {s : Set E} {t : Set Fu} {x : E} (hg : ContDiffOn 𝕜 n g t) (hf : ContDiffOn 𝕜 n f s)
    (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hst : MapsTo f s t) (hx : x ∈ s) {C : ℝ}
    {D : ℝ} (hC : ∀ i, i ≤ n → ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C)
    (hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) :
    ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ n ! * C * D ^ n

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu Gu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
f : E → Fu
n : ℕ
s : Set E
t : Set Fu
x : E
hg : ContDiffOn 𝕜 (↑n) g t
hf : ContDiffOn 𝕜 (↑n) f s
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n

Tactic:
induction' n using Nat.case_strong_induction_on with n IH generalizing Gu

Result:
case hz
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑0) g t
hf : ContDiffOn 𝕜 (↑0) f s
hC : ∀ i ≤ 0, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ 0 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 0 (g ∘ f) s x‖ ≤ ↑0! * C * D ^ 0

case hi
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x‖ ≤ ↑(n + 1)! * C * D ^ (n + 1)
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDerivWithin_comp_le_aux {Fu Gu : Type u} [NormedAddCommGroup Fu]
    [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu] {g : Fu → Gu} {f : E → Fu} {n : ℕ}
    {s : Set E} {t : Set Fu} {x : E} (hg : ContDiffOn 𝕜 n g t) (hf : ContDiffOn 𝕜 n f s)
    (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hst : MapsTo f s t) (hx : x ∈ s) {C : ℝ}
    {D : ℝ} (hC : ∀ i, i ≤ n → ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C)
    (hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) :
    ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ n ! * C * D ^ n

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
⊢ ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i

Tactic:
intro i hi

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.continuous {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) :
    Continuous f

Proof state:
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ ‖σ₁₂ c‖

Tactic:
rw [RingHomIsometric.is_iso]

Result:
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ ‖c‖

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
⊢ Continuous ⇑f

Tactic:
refine continuous_of_continuousAt_zero f fun U hU => ?_

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
this✝ : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 (f 0)
⊢ U ∈ map (⇑f) (𝓝 0)
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem le_sum_caratheodory {ι} (m : ι → OuterMeasure α) :
    ⨅ i, (m i).caratheodory ≤ (sum m).caratheodory := fun s h t => by
  simp [fun i => MeasurableSpace.measurableSet_iInf.1 h i t, ENNReal.tsum_add]

Proof state:
α : Type u_1
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ (sum m) t = (sum m) (t ∩ s) + (sum m) (t \ s)

Tactic:
simp [fun i => MeasurableSpace.measurableSet_iInf.1 h i t, ENNReal.tsum_add]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma two_mul_ediv_two_add_one_of_odd : Odd n → 2 * (n / 2) + 1 = n

Proof state:
case intro
c : ℤ
⊢ 2 * ((2 * c + 1) / 2) + 1 = 2 * c + 1

Tactic:
rw [mul_comm]

Result:
case intro
c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1

Proof state:
case intro
c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1

Tactic:
convert Int.ediv_add_emod' (2 * c + 1) 2

Result:
case h.e'_2.h.e'_6
c : ℤ
⊢ 1 = (2 * c + 1) % 2

Proof state:
n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n

Tactic:
rintro ⟨c, rfl⟩

Result:
case intro
c : ℤ
⊢ 2 * ((2 * c + 1) / 2) + 1 = 2 * c + 1

Proof state:
case h.e'_2.h.e'_6
c : ℤ
⊢ 1 = (2 * c + 1) % 2

Tactic:
simp [Int.add_emod]

Result:
no goals
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem difference_quotients_converge_uniformly
    {E : Type*} [NormedAddCommGroup E] {𝕜 : Type*} [RCLike 𝕜]
    [NormedSpace 𝕜 E] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ι → E → G}
    {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E}
    (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : ∀ᶠ y : E in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) :
    TendstoUniformlyOnFilter (fun n : ι => fun y : E => (‖y - x‖⁻¹ : 𝕜) • (f n y - f n x))
      (fun y : E => (‖y - x‖⁻¹ : 𝕜) • (g y - g x)) l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
⊢ TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)

Tactic:
let A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _

Result:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem difference_quotients_converge_uniformly
    {E : Type*} [NormedAddCommGroup E] {𝕜 : Type*} [RCLike 𝕜]
    [NormedSpace 𝕜 E] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ι → E → G}
    {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E}
    (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : ∀ᶠ y : E in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) :
    TendstoUniformlyOnFilter (fun n : ι => fun y : E => (‖y - x‖⁻¹ : 𝕜) • (f n y - f n x))
      (fun y : E => (‖y - x‖⁻¹ : 𝕜) • (g y - g x)) l (𝓝 x)

Proof state:
case neg
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : ↑q < ε
hfg' : ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ↑q
this :
  ∀ᶠ (x : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
    HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧
      HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2
a : ι × ι → Prop
b : ∀ᶠ (x : ι × ι) in l ×ˢ l, a x
c : E → Prop
d : ∀ᶠ (y : E) in 𝓝 x, c y
r : ℝ
hr : 0 < r
hr' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x r → c x_1
n : ι × ι
hn : a n
y : E
hy : (fun e => Metric.ball x r e) y
hyz' : ¬x = y
hyz : 0 < ‖y - x‖
e :
  ∀ {x : ι × ι},
    a x →
      ∀ {y : E}, c y → ‖f' x.1 y - f' x.2 y‖ < ↑q ∧ HasFDerivAt (f x.1) (f' x.1 y) y ∧ HasFDerivAt (f x.2) (f' x.2 y) y
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ ≤ ↑q * ‖y - x‖

Tactic:
refine
  Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
    (fun y hy => ((e hn (hr' hy)).2.1.sub (e hn (hr' hy)).2.2).hasFDerivWithinAt)
    (fun y hy => (e hn (hr' hy)).1.le) (convex_ball x r) (Metric.mem_ball_self hr) hy

Result:
no goals
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem difference_quotients_converge_uniformly
    {E : Type*} [NormedAddCommGroup E] {𝕜 : Type*} [RCLike 𝕜]
    [NormedSpace 𝕜 E] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ι → E → G}
    {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E}
    (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : ∀ᶠ y : E in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) :
    TendstoUniformlyOnFilter (fun n : ι => fun y : E => (‖y - x‖⁻¹ : 𝕜) • (f n y - f n x))
      (fun y : E => (‖y - x‖⁻¹ : 𝕜) • (g y - g x)) l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : UniformCauchySeqOnFilter f' l (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hfg'

Result:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : TendstoUniformlyOnFilter (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
-- Mathlib/Algebra/Module/PID.lean
theorem equiv_free_prod_directSum [h' : Module.Finite R N] :
    ∃ (n : ℕ) (ι : Type u) (_ : Fintype ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i) (e : ι → ℕ),
      Nonempty <| N ≃ₗ[R] (Fin n →₀ R) × ⨁ i : ι, R ⧸ R ∙ p i ^ e i

Proof state:
case intro.intro.intro.intro.intro.intro.mk.ofRepr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
this✝¹ : IsNoetherian R ↥(torsion R N)
this✝ : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
this : Projective R (N ⧸ torsion R N)
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
obtain ⟨f, hf⟩ := Module.projective_lifting_property _ LinearMap.id (torsion R N).mkQ_surjective

Result:
case intro.intro.intro.intro.intro.intro.mk.ofRepr.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
this✝¹ : IsNoetherian R ↥(torsion R N)
this✝ : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
this : Projective R (N ⧸ torsion R N)
f : N ⧸ torsion R N →ₗ[R] N
hf : (torsion R N).mkQ ∘ₗ f = LinearMap.id
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
this✝ : IsNoetherian R ↥(torsion R N)
this : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
obtain ⟨n, ⟨g⟩⟩ := @Module.basisOfFiniteTypeTorsionFree' R _ (N ⧸ torsion R N) _ _ _ _ _ _

Result:
case intro.intro.intro.intro.intro.intro.mk.ofRepr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
this✝ : IsNoetherian R ↥(torsion R N)
this : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
theorem setOf_prime_and_eq_mod_infinite (ha : IsUnit a) :
    {p : ℕ | p.Prime ∧ (p : ZMod q) = a}.Infinite

Proof state:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : ¬{p | Prime p ∧ ↑p = a}.Infinite
⊢ False

Tactic:
rw [Set.not_infinite] at H

Result:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : {p | Prime p ∧ ↑p = a}.Finite
⊢ False

Proof state:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : {p | Prime p ∧ ↑p = a}.Finite
⊢ False

Tactic:
exact not_summable_residueClass_prime_div ha <|
  summable_of_finite_support <| support_residueClass_prime_div a ▸ H

Result:
no goals

Proof state:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
⊢ {p | Prime p ∧ ↑p = a}.Infinite

Tactic:
by_contra H

Result:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : ¬{p | Prime p ∧ ↑p = a}.Infinite
⊢ False
-- Mathlib/Analysis/Seminorm.lean
theorem ball_add_ball_subset (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
    p.ball (x₁ : E) r₁ + p.ball (x₂ : E) r₂ ⊆ p.ball (x₁ + x₂) (r₁ + r₂)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ : E
⊢ p.ball x₁ r₁ + p.ball x₂ r₂ ⊆ p.ball (x₁ + x₂) (r₁ + r₂)

Tactic:
rintro x ⟨y₁, hy₁, y₂, hy₂, rfl⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ (fun x1 x2 => x1 + x2) y₁ y₂ ∈ p.ball (x₁ + x₂) (r₁ + r₂)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ p (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂

Tactic:
exact (map_add_le_add p _ _).trans_lt (add_lt_add hy₁ hy₂)

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ (fun x1 x2 => x1 + x2) y₁ y₂ ∈ p.ball (x₁ + x₂) (r₁ + r₂)

Tactic:
rw [mem_ball, add_sub_add_comm]

Result:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ p (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂