awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : BddAbove (range p)
⊢ ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)

Tactic:
rw [Seminorm.bddAbove_range_iff] at bdd

Premises used: Seminorm.bddAbove_range_iff
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
⊢ LowerSemicontinuous (β := ℝ) fun (x' : E) ↦ ⨆ (i : ι), (fun (i : ι) (x : E) ↦ ((p i : (a : E) → ℝ) x : ℝ)) i x'

Tactic:
lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)

Premises used: lowerSemicontinuous_ciSup, Continuous.lowerSemicontinuous
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
h : ∀ (x : E), Eq (α := ℝ) ((⨆ (i : ι), (⇑(p i) : (a : E) → ℝ)) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)
⊢ LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))

Tactic:
convert! lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)

Premises used: lowerSemicontinuous_ciSup, Continuous.lowerSemicontinuous
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
x : E
⊢ Eq (α := ℝ) ((⨆ (i : ι), (⇑(p i) : (a : E) → ℝ)) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)

Tactic:
iSup_apply

Premises used: iSup_apply
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
x : E
⊢ Eq (α := ℝ) ((⨆ (i : ι), (⇑(p i) : (a : E) → ℝ)) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)

Tactic:
exact iSup_apply

Premises used: iSup_apply
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
n : ℕ
⊢ IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))

Tactic:
simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n

Premises used: Nat.cast, LowerSemicontinuous.isClosed_preimage, Seminorm.closedBall_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
⊢ ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))

Tactic:
have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
      simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
⊢ Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ

Tactic:
have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
      eq_univ_of_forall fun x ↦ mem_iUnion.mpr (exists_nat_ge <| p (x - 0))
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
rcases : ∀ (n : ℕ) (x : E) (hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))), Continuous[inst_7, _] (⇑p : (a : E) → ℝ)
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)

Tactic:
rcases nonempty_interior_of_iUnion_of_closed h₁ h₂ with ⟨n, ⟨x, hxn⟩⟩

Premises used: nonempty_interior_of_iUnion_of_closed
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.continuous' (r := n + n) ?_

Premises used: Seminorm.continuous'
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))
refine : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)))
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)

Tactic:
refine Seminorm.continuous' (r := n + n) ?_

Premises used: Seminorm.continuous'
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))
rw :
  ∀ (hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x),
    Membership.mem (γ := Filter E) (𝓝 0) {y : E | (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)}
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)))

Tactic:
rw [p.closedBall_zero_eq] at hxn ⊢

Premises used: Seminorm.closedBall_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
⊢ Membership.mem (γ := Set E) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)} x

Tactic:
interior_subset hxn

Premises used: interior_subset
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
convert! interior_subset hxn

Premises used: interior_subset
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
have hxn' : p x ≤ n := by convert! interior_subset hxn
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
⊢ Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}

Tactic:
rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn

Premises used: mem_interior_iff_mem_nhds, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
hxn₁ :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn

Premises used: mem_interior_iff_mem_nhds, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
h :
  ∀ (y : E)
    (hy :
      Membership.mem (γ := Set E)
        (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)})
        y),
    (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ Membership.mem (γ := Filter E) (𝓝 0) {y : E | (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)}

Tactic:
filter_upwards [hxn] with y hy
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
y : E
hy :
  Membership.mem (γ := Set E)
    (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) y
rw rw₁ : Eq (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((p : (a : E) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((p : (a : E) → ℝ) (x + y - x) : ℝ)

Tactic:
rw [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
y : E
hy :
  Membership.mem (γ := Set E)
    (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) y
⊢ (p : (a : E) → ℝ) (x + y - x) ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
map_sub_le_add _ _ _

Premises used: map_sub_le_add
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
y : E
hy :
  Membership.mem (γ := Set E)
    (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) y
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) ((p : (a : E) → ℝ) x : ℝ) ≤
    HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)

Tactic:
add_le_add hy hxn'

Premises used: add_le_add
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
y : E
hy :
  Membership.mem (γ := Set E)
    (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) y
calc : Eq (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((p : (a : E) → ℝ) (x + y - x) : ℝ)
⊢ (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)

Tactic:
calc p y = p (x + y - x) := by rw [add_sub_cancel_left]
      _ ≤ p (x + y) + p x := map_sub_le_add _ _ _
      _ ≤ n + n := add_le_add hy hxn'

Premises used: add_le_add, HSub.hSub, HAdd.hAdd, map_sub_le_add, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)

Tactic:
(hq.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup (toLinearMap ∘ 𝓕)).mpr ?_

Premises used: Iff.mpr, Function.comp, ContinuousLinearMap.toLinearMap, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
refine :
  ∀ (i : κ),
    BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (k : ι) ↦ (q i).comp ((toLinearMap ∘ 𝓕) k)) ∧
      Continuous[inst_7.toTopologicalSpace, _] (⨆ (k : ι), (⇑((q i).comp ((toLinearMap ∘ 𝓕) k)) : (a : E) → ℝ))
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)

Tactic:
refine (hq.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup (toLinearMap ∘ 𝓕)).mpr ?_

Premises used: Iff.mpr, Function.comp, ContinuousLinearMap.toLinearMap, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
rw : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ ((q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F) : (a : E) → ℝ) x)
⊢ BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (i : ι) ↦ (q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F))

Tactic:
rw [Seminorm.bddAbove_range_iff]

Premises used: Seminorm.bddAbove_range_iff