awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ p.ball x r = ∅
have h : ∀ (x_1 : E), x_1 ∈ p.ball x r ↔ Membership.mem (γ := Set E) ∅ x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x_1 : E
⊢ x_1 ∈ p.ball x r ↔ Membership.mem (γ := Set E) ∅ x_1
have h : r ≤ (p : (a : E) → ℝ) (x_1 - x)
Tactic: rw [Seminorm.mem_ball, Set.mem_empty_iff_false, iff_false, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
⊢ p.closedBall x r = ∅
have h : ∀ (x_1 : E), x_1 ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) ∅ x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x_1 : E
⊢ x_1 ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) ∅ x_1
have h : r < (p : (a : E) → ℝ) (x_1 - x)
Tactic: rw [Seminorm.mem_closedBall, Set.mem_empty_iff_false, iff_false, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.closedBall 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)
have simp : ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b < r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂
Tactic: simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b < r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂
have refine : ∀ (a : 𝕜) (ha : ‖a‖ ≤ r₁) (b : E) (hb : (p : (a : E) → ℝ) b < r₂), 0 < r₁
Tactic: refine fun a ha b hb ↦ mul_lt_mul' ha hb (apply_nonneg _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.closedBall 0 r₂) ⊆ p.ball 0 (r₁ * r₂)
have simp : ∀ (a : 𝕜), ‖a‖ < r₁ → ∀ (b : E), (p : (a : E) → ℝ) b ≤ r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂
Tactic: simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
    map_smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) < r₁ * r₂
have rw : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) b : ℝ) ‖a‖ < r₂ * r₁
Tactic: rw [mul_comm, mul_comm r₁]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) b : ℝ) ‖a‖ < r₂ * r₁
have refine : ¬r₂ < 0
Tactic: refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_gt.resolve_left ?_)
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)
have inl : HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 0) ⊆ p.ball 0 (r₁ * 0)
Tactic: rcases eq_or_ne r₂ 0 with rfl | hr₂
Cleared hypotheses: r₂
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
inl : HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 0) ⊆ p.ball 0 (r₁ * 0)
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)
have inr : ∀ (hr₂ : r₂ ≠ 0), HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.ball 0 r₁) (p.ball 0 r₂) ⊆ p.ball 0 (r₁ * r₂)
Tactic: rcases eq_or_ne r₂ 0 with rfl | hr₂
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := Set 𝕜) (Metric.closedBall 0 r₁) (p.closedBall 0 r₂) ⊆ p.closedBall 0 (r₁ * r₂)
have simp : ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), (p : (a : E) → ℝ) b ≤ r₂ → HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) ≤ r₁ * r₂
Tactic: simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : (p : (a : E) → ℝ) b ≤ r₂
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) b : ℝ) ≤ r₁ * r₂
have b0 : 0 ≤ r₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -p.ball x r = p.ball (-x) r
have h : ∀ (x_1 : E), x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
⊢ x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
have h : -x_1 ∈ p.ball x r ↔ x_1 ∈ p.ball (-x) r
Tactic: rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.ball x r ↔ x_1 ∈ p.ball (-x) r
⊢ x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
have h₁ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ x_1 ∈ p.ball (-x) r
Tactic: rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.ball x r ↔ x_1 ∈ p.ball (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ x_1 ∈ p.ball (-x) r
⊢ x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
have h₂ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
Tactic: rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.ball x r ↔ x_1 ∈ p.ball (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ x_1 ∈ p.ball (-x) r
h₂ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
⊢ x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
have h₃ : (p : (a : E) → ℝ) (-(x_1 + x)) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
Tactic: rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.ball x r ↔ x_1 ∈ p.ball (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ x_1 ∈ p.ball (-x) r
h₂ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
h₃ : (p : (a : E) → ℝ) (-(x_1 + x)) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
⊢ x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
have h₄ : (p : (a : E) → ℝ) (-(x_1 + x)) < r ↔ (p : (a : E) → ℝ) (x_1 + x) < r
Tactic: rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.ball x r ↔ x_1 ∈ p.ball (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ x_1 ∈ p.ball (-x) r
h₂ : (p : (a : E) → ℝ) (-x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
h₃ : (p : (a : E) → ℝ) (-(x_1 + x)) < r ↔ (p : (a : E) → ℝ) (x_1 - -x) < r
h₄ : (p : (a : E) → ℝ) (-(x_1 + x)) < r ↔ (p : (a : E) → ℝ) (x_1 + x) < r
⊢ x_1 ∈ -p.ball x r ↔ x_1 ∈ p.ball (-x) r
have h₅ : (p : (a : E) → ℝ) (x_1 + x) < r ↔ (p : (a : E) → ℝ) (x_1 + x) < r
Tactic: rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -p.closedBall x r = p.closedBall (-x) r
have h : ∀ (x_1 : E), x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
⊢ x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
have h : -x_1 ∈ p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
Tactic: rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
⊢ x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
have h₁ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall (-x) r
Tactic: rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall (-x) r
⊢ x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
have h₂ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
Tactic: rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall (-x) r
h₂ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
⊢ x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
have h₃ : (p : (a : E) → ℝ) (-(x_1 + x)) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
Tactic: rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall (-x) r
h₂ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
h₃ : (p : (a : E) → ℝ) (-(x_1 + x)) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
⊢ x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
have h₄ : (p : (a : E) → ℝ) (-(x_1 + x)) ≤ r ↔ (p : (a : E) → ℝ) (x_1 + x) ≤ r
Tactic: rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x_1 : E
h : -x_1 ∈ p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
h₁ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall (-x) r
h₂ : (p : (a : E) → ℝ) (-x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
h₃ : (p : (a : E) → ℝ) (-(x_1 + x)) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - -x) ≤ r
h₄ : (p : (a : E) → ℝ) (-(x_1 + x)) ≤ r ↔ (p : (a : E) → ℝ) (x_1 + x) ≤ r
⊢ x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
have h₅ : (p : (a : E) → ℝ) (x_1 + x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 + x) ≤ r
Tactic: rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
have inl : IsEmpty ι → closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
inl : IsEmpty ι → closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
have inr : Nonempty ι → closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h : IsEmpty ι
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
have inl : closedBall.{u_3, u_7} (𝕜 := 𝕜) ⊥ e r = univ
Tactic: rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h : Nonempty ι
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r
have inr : ∀ (x : E),
  x ∈ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r ↔
    Membership.mem (γ := Set E) (⋂ (i : ι), (p i).closedBall e r) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h : Nonempty ι
x : E
⊢ x ∈ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r ↔
    Membership.mem (γ := Set E) (⋂ (i : ι), (p i).closedBall e r) x
have this : BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) (x - e))
Tactic: have := Seminorm.bddAbove_range_iff.mp hp (x - e)
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
⊢ p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
have inl : p.ball 0 (norm.{u_3} (E := 𝕜) 0 * r) ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)
Tactic: rcases eq_or_ne k 0 with (rfl | hk)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
inl : p.ball 0 (norm.{u_3} (E := 𝕜) 0 * r) ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)
⊢ p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
have inr : ∀ (hk : k ≠ 0), p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
Tactic: rcases eq_or_ne k 0 with (rfl | hk)
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 (norm.{u_3} (E := 𝕜) 0 * r) ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)
have inl : ∅ ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)
Tactic: rw [norm_zero, zero_mul, ball_eq_emptyset _ le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
⊢ x ∈ p.ball 0 (‖k‖ * r) → x ∈ k • p.ball 0 r
have inr : (p : (a : E) → ℝ) x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x
Tactic: rw [Set.mem_smul_set, Seminorm.mem_ball_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
⊢ (p : (a : E) → ℝ) x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x
have inr : ∀ (hx : (p : (a : E) → ℝ) x < ‖k‖ * r), k⁻¹ • x ∈ p.ball 0 r
Tactic: refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
inr : ∀ (hx : (p : (a : E) → ℝ) x < ‖k‖ * r), k⁻¹ • x ∈ p.ball 0 r
⊢ (p : (a : E) → ℝ) x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x
have inr₁ : ∀ (hx : (p : (a : E) → ℝ) x < ‖k‖ * r), k • k⁻¹ • x = x
Tactic: refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
inr₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
inr₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r
inr₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr₃ : ‖k‖ * HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
inr₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r
inr₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r
inr₃ : ‖k‖ * HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr₄ : HMul.hMul (β := ℝ) (‖k‖ * ‖k‖⁻¹) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
inr₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r
inr₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r
inr₃ : ‖k‖ * HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
inr₄ : HMul.hMul (β := ℝ) (‖k‖ * ‖k‖⁻¹) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr₅ : HMul.hMul (β := ℝ) (‖k‖ / ‖k‖) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (p : (a : E) → ℝ) (k⁻¹ • x) < r
inr₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r
inr₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r
inr₃ : ‖k‖ * HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
inr₄ : HMul.hMul (β := ℝ) (‖k‖ * ‖k‖⁻¹) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
inr₅ : HMul.hMul (β := ℝ) (‖k‖ / ‖k‖) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
⊢ k⁻¹ • x ∈ p.ball 0 r
have inr₆ : HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
Tactic: rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
⊢ k • k⁻¹ • x = x
have inr : (k • k⁻¹) • x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (k • k⁻¹) • x = x
⊢ k • k⁻¹ • x = x
have inr₁ : (k * k⁻¹) • x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (k • k⁻¹) • x = x
inr₁ : (k * k⁻¹) • x = x
⊢ k • k⁻¹ • x = x
have inr₂ : (k / k) • x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]