awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
⊢ Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)

Tactic:
have h_tendsto : Tendsto (fun n : ℕ => (c ^ n)⁻¹ • u n) atTop (𝓝 (0 : E)) := by
    apply bE.tendsto
    intro n
    simpa only [Set.mem_smul_set_iff_inv_smul_mem₀ (pow_ne_zero n c_ne)] using hu n
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)

Tactic:
have h_bounded : IsVonNBounded 𝕜 (Set.range fun n : ℕ => (c ^ n)⁻¹ • u n) :=
    h_tendsto.isVonNBounded_range 𝕜
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
⊢ IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n))

Tactic:
specialize hf _ h_bounded
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n))
⊢ IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))

Tactic:
simp only [← Set.range_comp', LinearMap.map_smulₛₗ, map_inv₀, map_pow] at hf

Premises used: map_inv₀, map_pow, LinearMap.map_smulₛₗ, Set.range_comp'
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
⊢ norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') < 1

Tactic:
simpa using hc1
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
⊢ Tendsto.{0, u_2} (β := 𝕜') (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) atTop (𝓝 0)

Tactic:
have : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0) :=
      tendsto_pow_atTop_nhds_zero_of_norm_lt_one (by simpa using hc1)
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this : Tendsto.{0, u_2} (β := 𝕜') (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) atTop (𝓝 0)
⊢ Tendsto
    (HSMul.hSMul.{u_2, u_4, u_4} (α := ℕ → 𝕜') (β := ℕ → F)
      (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) fun (n : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n)⁻¹ ((f : (a : E) → F) (u n) : F))
    atTop (𝓝 0)

Tactic:
have := hf.smul_tendsto_zero (.of_forall fun n ↦ Set.mem_range_self n) this
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this_1 : Tendsto.{0, u_2} (β := 𝕜') (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) atTop (𝓝 0)
this :
  Tendsto
    (HSMul.hSMul.{u_2, u_4, u_4} (α := ℕ → 𝕜') (β := ℕ → F)
      (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) fun (n : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n)⁻¹ ((f : (a : E) → F) (u n) : F))
    atTop (𝓝 0)
n : ℕ
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := ℕ → 𝕜') (β := ℕ → F)
      (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n)
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n)⁻¹ ((f : (a : E) → F) (u n) : F))
      n =
    ((⇑f : (a : E) → F) ∘ u) n

Tactic:
simp [c_ne]
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this_1 : Tendsto.{0, u_2} (β := 𝕜') (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) atTop (𝓝 0)
this :
  Tendsto
    (HSMul.hSMul.{u_2, u_4, u_4} (α := ℕ → 𝕜') (β := ℕ → F)
      (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n) fun (n : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') n)⁻¹ ((f : (a : E) → F) (u n) : F))
    atTop (𝓝 0)
⊢ Tendsto.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)

Tactic:
exact this.congr fun n ↦ by simp [c_ne]

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
⊢ Tendsto.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)

Tactic:
have : Tendsto (f ∘ u) atTop (𝓝 0) := by
    have : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0) :=
      tendsto_pow_atTop_nhds_zero_of_norm_lt_one (by simpa using hc1)
    have := hf.smul_tendsto_zero (.of_forall fun n ↦ Set.mem_range_self n) this
    exact this.congr fun n ↦ by simp [c_ne]
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this : Tendsto.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)
⊢ False

Tactic:
frequently_false (atTop : Filter ℕ) <| Eventually.frequently ?_

Premises used: Filter.frequently_false, Filter.atTop, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this : Tendsto.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)
refine : ∀ᶠ (x : ℕ) in atTop, False
⊢ False

Tactic:
refine frequently_false (atTop : Filter ℕ) <| Eventually.frequently ?_

Premises used: Filter.frequently_false, Filter.atTop, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this : Tendsto.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)
⊢ ∀ (a : ℕ), ((⇑f : (a : E) → F) ∘ u) a ∈ V → False

Tactic:
hu'

Premises used: Set.Mem, Not
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
u : (i : ℕ) → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V
h_tendsto : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n)
hf :
  IsVonNBounded.{u_2, u_4} 𝕜' (E := F)
    (Set.range fun (x : ℕ) ↦
      HSMul.hSMul (β := F) (HPow.hPow (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') x)⁻¹ ((f : (a : E) → F) (u x) : F))
this : Tendsto.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ((⇑f : (a : E) → F) ∘ u) x ∈ V) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ False) x} x}
      a
h₁ : ∀ (a : ℕ), ((⇑f : (a : E) → F) ∘ u) a ∈ V → False
⊢ ∀ᶠ (x : ℕ) in atTop, False

Tactic:
filter_upwards [this.eventually_mem hV] using hu'

Premises used: Filter.Tendsto.eventually_mem
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
inst_12 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
⊢ Continuous[inst_1, inst_4] (⇑f : (a : E) → F)

Tactic:
continuous_of_continuousAt_zero f (f.continuousAt_zero_of_locally_bounded hf)

Premises used: continuous_of_continuousAt_zero, LinearMap.continuousAt_zero_of_locally_bounded
-- Module: Mathlib.Analysis.LocallyConvex.Montel
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : Zero E
inst_2 : SMul 𝕜 E
inst_3 : TopologicalSpace E
hm : MontelSpace 𝕜 E
s : Set E
h_closed : IsClosed[inst_3] s
h_bounded : IsVonNBounded 𝕜 s
⊢ IsCompact s

Tactic:
hm.heine_borel s h_closed h_bounded

Premises used: MontelSpace.heine_borel
-- Module: Mathlib.Analysis.LocallyConvex.Montel
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
hM : MontelSpace 𝕜 E
⊢ FiniteDimensional 𝕜 E

Tactic:
FiniteDimensional.of_isCompact_closedBall₀ 𝕜 zero_lt_one
    (isCompact_of_isClosed_of_isVonNBounded 𝕜 Metric.isClosed_closedBall
      (NormedSpace.isVonNBounded_closedBall _ _ _))

Premises used: MontelSpace.isCompact_of_isClosed_of_isVonNBounded, Metric.isClosed_closedBall, NormedSpace.isVonNBounded_closedBall, FiniteDimensional.of_isCompact_closedBall₀, zero_lt_one