awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have rcases₁ : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
  (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
Tactic: classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
rcases₁ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have h : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
  (hV : V = (t.sup p).ball 0 r₂),
  ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
Tactic: classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
rcases₁ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
h :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂),
    ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have h₁ : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
  (hV : V = (t.sup p).ball 0 r₂), ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
Tactic: classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
rcases₁ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
h :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂),
    ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
h₁ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂), ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have h₂ : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
  (hV : V = (t.sup p).ball 0 r₂),
  Subset.{u_6} (α := Set E) (⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂))
    ((⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂)
Tactic: classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
⊢ 0 ∈ U
have rcases : ∀ (ι' : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (ι'.sup p).ball 0 r), 0 ∈ U
Tactic: rcases p.basisSets_iff.mp hU with ⟨ι', r, hr, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U
have rcases : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r), ∃ V ∈ p.basisSets, V + V ⊆ U
Tactic: rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U
have h : (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
Tactic: use (s.sup p).ball 0 (r / 2)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
have h : (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
Tactic: refine ⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
have h : (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ U
Tactic: refine Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ U
have h : (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
Tactic: rw [hU, add_zero, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
⊢ (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ U
have h₁ : (s.sup p).ball 0 (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
Tactic: rw [hU, add_zero, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
h₁ : (s.sup p).ball 0 (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
⊢ (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ U
have h₂ : (s.sup p).ball 0 r ⊆ (s.sup p).ball 0 r
Tactic: rw [hU, add_zero, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU' : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) ↦ -x) ⁻¹' U
have rcases : ∀ (s : Finset ι) (r : ℝ), 0 < r → ∀ (hU : U = (s.sup p).ball 0 r), ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) ↦ -x) ⁻¹' U
Tactic: rcases p.basisSets_iff.mp hU' with ⟨s, r, _, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) ↦ -x) ⁻¹' U
have rw : ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r
Tactic: rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU : U ∈ p.basisSets
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U
have rcases : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r), ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U
Tactic: rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U
have rw : Membership.mem (γ := Filter R) (𝓝 0) {x : R | x • v ∈ (s.sup p).ball 0 r}
Tactic: rw [hU, Filter.eventually_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | x • v ∈ (s.sup p).ball 0 r}
have simp_rw : Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
Tactic: simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
have pos : ∀ (h : LT.lt (α := ℝ) (0 : ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ)),
  Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
Tactic: by_cases! h : 0 < (s.sup p) v
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
pos :
  ∀ (h : LT.lt (α := ℝ) (0 : ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ)),
    Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
have neg : ∀ (h : LE.le (α := ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ) (0 : ℝ)),
  Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
Tactic: by_cases! h : 0 < (s.sup p) v
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LT.lt (α := ℝ) (0 : ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ)
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
have pos : Membership.mem (γ := Filter R) (𝓝 0) {x : R | ‖x‖ < HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)}
Tactic: simp_rw [(lt_div_iff₀ h).symm]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LT.lt (α := ℝ) (0 : ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ)
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | ‖x‖ < HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)}
have pos : Membership.mem (γ := Filter R) (𝓝 0) (Metric.ball 0 (HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)))
Tactic: rw [← _root_.ball_zero_eq]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LE.le (α := ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
have neg : Membership.mem (γ := Filter R) (𝓝 0) {x : R | True}
Tactic: simp_rw [le_antisymm h (apply_nonneg _ v), mul_zero, hr]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set E),
        Membership.mem (γ := Set (Set E))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U
have rcases : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r),
  ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set E),
        Membership.mem (γ := Set (Set E))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U
Tactic: rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set E),
        Membership.mem (γ := Set (Set E))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U
have refine : ∃ (W : Set E),
  Membership.mem (γ := Set (Set E)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      W ∧
    HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) W ⊆ U
Tactic: refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ (W : Set E),
    Membership.mem (γ := Set (Set E))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
      HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) W ⊆ U
have refine : HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) ((s.sup p).ball 0 √r) ⊆ U
Tactic: refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) ((s.sup p).ball 0 √r) ⊆ U
have refine : (s.sup p).ball 0 (√r * √r) ⊆ U
Tactic: refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (√r * √r) ⊆ U
have rw : (s.sup p).ball 0 (√r * √r) ⊆ (s.sup p).ball 0 r
Tactic: rw [hU, Real.mul_self_sqrt (le_of_lt hr)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
rw : (s.sup p).ball 0 (√r * √r) ⊆ (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (√r * √r) ⊆ U
have rw₁ : (s.sup p).ball 0 r ⊆ (s.sup p).ball 0 r
Tactic: rw [hU, Real.mul_self_sqrt (le_of_lt hr)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU : U ∈ p.basisSets
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' U
have rcases : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r),
  ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' U
Tactic: rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' U
have rw : ∃ (V : Set F),
  Membership.mem (γ := Set (Set F)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      V ∧
    V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
Tactic: rw [hU]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
have pos : ∀ (h : x ≠ 0),
  ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
Tactic: by_cases h : x ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
pos :
  ∀ (h : x ≠ 0),
    ∃ (V : Set F),
      Membership.mem (γ := Set (Set F))
          (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
        V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
have neg : ∀ (h : ¬x ≠ 0),
  ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
Tactic: by_cases h : x ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
have pos : ∃ (V : Set F),
  Membership.mem (γ := Set (Set F)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      V ∧
    V ⊆ (s.sup p).ball 0 (r / ‖x‖)
Tactic: rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]