awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have bE' : HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
Tactic: have bE' : (𝓝 (0 : E)).HasBasis (fun _ ↦ True) (fun n : ℕ ↦ (c ^ n) • b n) := by
    refine bE.1.to_hasBasis' ?_ ?_
    · intro n _
      use n
      exact ⟨trivial, (bE1 n).2 _ (by grw [norm_pow, hc1, one_pow])⟩
    · intro n _
      simpa using smul_mem_nhds_smul₀ (pow_ne_zero n c_ne) (bE1 n).1
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have simp_rw : ∀ (t : Set F),
  Membership.mem (γ := Filter F) (𝓝 0) t →
    ∃ (i : ℕ), ∀ ⦃x : E⦄, x ∈ c ^ i • b i → Membership.mem (α := F) t ((f : (a : E) → F) x : F)
Tactic: simp_rw [ContinuousAt, map_zero, bE'.tendsto_left_iff, true_and, Set.MapsTo]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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
⊢ ∀ (t : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) t →
      ∃ (i : ℕ), ∀ ⦃x : E⦄, x ∈ c ^ i • b i → Membership.mem (α := F) t ((f : (a : E) → F) x : F)
have by_contra! : ∀
  (h :
    ∃ (t : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) t ∧ ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, ((f : (a : E) → F) x : F) ∉ t),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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
h : ∃ (t : Set F), Membership.mem (γ := Filter F) (𝓝 0) t ∧ ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, ((f : (a : E) → F) x : F) ∉ t
⊢ False
have rcases : ∀ (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V)
  (h : ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, ((f : (a : E) → F) x : F) ∉ V), False
Tactic: rcases h with ⟨V, hV, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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
h : ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, ((f : (a : E) → F) x : F) ∉ V
⊢ False
have choose! : ∀ (u : (i : ℕ) → E) (hu : ∀ (i : ℕ), u i ∈ c ^ i • b i) (hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V), False
Tactic: choose! u hu hu' using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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)
have apply : ∀ (i : ℕ), (c ^ i)⁻¹ • u i ∈ b i
Tactic: apply bE.tendsto
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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
⊢ False
have h_tendsto : 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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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)
⊢ False
have h_bounded : 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 𝕜
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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)
⊢ False
have 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))
Tactic: specialize hf _ h_bounded
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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))
⊢ False
have 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))
Tactic: simp only [← Set.range_comp', LinearMap.map_smulₛₗ, map_inv₀, map_pow] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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)
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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.{0, u_4} (β := F) ((⇑f : (a : E) → F) ∘ u) atTop (𝓝 0)
have 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)
Tactic: have := hf.smul_tendsto_zero (.of_forall fun n ↦ Set.mem_range_self n) this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
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))
⊢ False
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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
have refine : ∀ᶠ (x : ℕ) in atTop, False
Tactic: refine frequently_false (atTop : Filter ℕ) <| Eventually.frequently ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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)
⊢ ∀ᶠ (x : ℕ) in atTop, False
have 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
Tactic: filter_upwards [this.eventually_mem hV] using hu'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
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
⊢ ∀ᶠ (x : ℕ) in atTop, False
have h₁ : ∀ (a : ℕ), ((⇑f : (a : E) → F) ∘ u) a ∈ V → False
Tactic: filter_upwards [this.eventually_mem hV] using hu'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Montel (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : T1Space E
inst_13 : MontelSpace 𝕜₁ E
⊢ Continuous[topologicalSpace, UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}]
    (AddHom.toFun
      (LinearMap.toAddHom
        ((↑(LinearEquiv.toCompactConvergenceCLM σ E F) : (E →SL[σ] F) →ₗ[𝕜₂] E →SL_c[σ] F) :
          (E →SL[σ] F) →ₗ[𝕜₂] E →SL_c[σ] F)))
have simp : ∀ (s : Set (E →SL_c[σ] F)),
  IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | IsCompact S}] s →
    IsOpen[topologicalSpace]
      ((⇑(LinearEquiv.toCompactConvergenceCLM σ E F : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SL_c[σ] F) :
          (a : E →SL[σ] F) → E →SL_c[σ] F) ⁻¹'
        s)
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, continuous_def]