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 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
⊢ x⁻¹ • V ⊆ (⇑f : (a : E) → F) ⁻¹' U

Tactic:
have : x⁻¹ • V ⊆ f ⁻¹' U :=
      calc
        x⁻¹ • V ⊆ x⁻¹ • f ⁻¹' f '' V := Set.smul_set_mono (Set.subset_preimage_image (⇑f) V)
        _ ⊆ x⁻¹ • f ⁻¹' (σ x • U) := Set.smul_set_mono (Set.preimage_mono h)
        _ = f ⁻¹' U := by rw [x_ne.isUnit.preimage_smul_setₛₗ _, inv_smul_smul₀ x_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 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ (⇑f : (a : E) → F) ⁻¹' U
grw : Membership.mem (γ := Filter E) (𝓝 0) (x⁻¹ • V)
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)

Tactic:
grw [← 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 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ (⇑f : (a : E) → F) ⁻¹' U
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ Membership.mem (γ := Filter E) (𝓝 0) (x⁻¹ • V)

Tactic:
rwa [set_smul_mem_nhds_zero_iff (inv_ne_zero x_ne)]

Premises used: set_smul_mem_nhds_zero_iff, inv_ne_zero
-- 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 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
h :
  ∃ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ∧ IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
⊢ (↑(f.clmOfExistsBoundedImage h) : E →ₛₗ[σ] F) = f

Tactic:
rfl

Premises used: rfl
-- 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 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
h :
  ∃ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ∧ IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
x : E
⊢ Eq.{u_4 + 1} (α := F) ((f.clmOfExistsBoundedImage h : (a : E) → F) x : F) ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- 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)
obtain : ∀ (c : 𝕜) (hc0 : 0 < ‖c‖) (hc1 : ‖c‖ < 1), ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0

Tactic:
obtain ⟨c, hc0, hc1⟩ := NormedField.exists_norm_lt_one 𝕜

Premises used: NormedField.exists_norm_lt_one
-- 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 ≠ 0

Tactic:
have c_ne := norm_pos_iff.mp hc0
-- 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
rcases :
  ∀ (b : ℕ → Set E) (bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i))
    (bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ _root_.id (b i)),
    ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0

Tactic:
rcases (nhds_basis_balanced 𝕜 E).exists_antitone_subbasis with ⟨b, bE1, bE⟩

Premises used: Filter.HasBasis.exists_antitone_subbasis, nhds_basis_balanced
-- 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
⊢ HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n

Tactic:
bE.1.to_hasBasis' ?_ ?_

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.to_hasBasis'
-- 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
refine_1 : ∀ (i : ℕ), True → ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b i
refine_2 : ∀ (i' : ℕ), True → Membership.mem (γ := Filter E) (𝓝 0) (c ^ i' • b i')
⊢ HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n

Tactic:
refine bE.1.to_hasBasis' ?_ ?_

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.to_hasBasis'
-- 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
n : ℕ
refine_1 : True → ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b n
⊢ True → ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b n

Tactic:
_
-- 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
n : ℕ
h_1 : True
h : True ∧ c ^ n • b n ⊆ b n
⊢ ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b n

Tactic:
use 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
n : ℕ
h : True
grw : ‖c‖ ^ n ≤ 1
grw₁ : HPow.hPow (α := ℝ) 1 n ≤ 1
grw₂ grw₃ : LE.le (α := ℝ) 1 1
⊢ ‖c ^ n‖ ≤ 1

Tactic:
grw [norm_pow, hc1, one_pow]

Premises used: one_pow, norm_pow
-- 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
n : ℕ
h : True
⊢ True ∧ c ^ n • b n ⊆ b n

Tactic:
exact ⟨trivial, (bE1 n).2 _ (by grw [norm_pow, hc1, one_pow])⟩
-- 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
n : ℕ
refine_2 : True → Membership.mem (γ := Filter E) (𝓝 0) (c ^ n • b n)
⊢ True → Membership.mem (γ := Filter E) (𝓝 0) (c ^ n • b n)

Tactic:
_
-- 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
n : ℕ
h : True
⊢ Membership.mem (γ := Filter E) (𝓝 0) (c ^ n • b n)

Tactic:
simpa using smul_mem_nhds_smul₀ (pow_ne_zero n c_ne) (bE1 n).1

Premises used: smul_mem_nhds_smul₀, pow_ne_zero, And.left
-- 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
⊢ 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
-- 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
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)
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0

Tactic:
simp_rw [ContinuousAt, map_zero, bE'.tendsto_left_iff, true_and, Set.MapsTo]

Premises used: ContinuousAt, map_zero, Set.MapsTo, Filter.HasBasis.tendsto_left_iff, true_and
-- 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
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
⊢ ∀ (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:
by_contra! h
-- 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
h : ∃ (t : Set F), Membership.mem (γ := Filter F) (𝓝 0) t ∧ ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, ((f : (a : E) → F) x : F) ∉ t
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
⊢ False

Tactic:
rcases h with ⟨V, hV, h⟩
-- 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
h : ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, ((f : (a : E) → F) x : F) ∉ V
choose! :
  ∀ (u : (i : ℕ) → E) (hu : ∀ (i : ℕ), u i ∈ c ^ i • b i) (hu' : ∀ (i : ℕ), ((f : (a : E) → F) (u i) : F) ∉ V), False
⊢ False

Tactic:
choose! u hu hu' using h
-- 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
apply : ∀ (i : ℕ), (c ^ i)⁻¹ • u i ∈ b i
⊢ Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)

Tactic:
apply bE.tendsto

Premises used: Filter.HasAntitoneBasis.tendsto
-- 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
n : ℕ
⊢ (c ^ n)⁻¹ • u n ∈ b n

Tactic:
simpa only [Set.mem_smul_set_iff_inv_smul_mem₀ (pow_ne_zero n c_ne)] using hu n

Premises used: pow_ne_zero, Set.mem_smul_set_iff_inv_smul_mem₀