awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x_1 : E
h :
  Membership.mem (γ := Set E) {y : E | (p.comp f : (a : E) → ℝ) (y - x) ≤ r} x_1 ↔
    Membership.mem (γ := Set E)
      (preimage.{u_7, u_8} (β := E₂) (⇑f : (a : E) → E₂)
        {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r})
      x_1
⊢ x_1 ∈ (p.comp f).closedBall x r ↔
    Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.closedBall ((f : (a : E) → E₂) x) r) x_1
have h₁ : Membership.mem (γ := Set E) {y : E | (p.comp f : (a : E) → ℝ) (y - x) ≤ r} x_1 ↔
  Membership.mem.{u_8, u_8} (α := E₂) (γ := Set E₂)
    {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r} ((f : (a : E) → E₂) x_1 : E₂)
Tactic: simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x_1 : E
h :
  Membership.mem (γ := Set E) {y : E | (p.comp f : (a : E) → ℝ) (y - x) ≤ r} x_1 ↔
    Membership.mem (γ := Set E)
      (preimage.{u_7, u_8} (β := E₂) (⇑f : (a : E) → E₂)
        {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r})
      x_1
h₁ :
  Membership.mem (γ := Set E) {y : E | (p.comp f : (a : E) → ℝ) (y - x) ≤ r} x_1 ↔
    Membership.mem.{u_8, u_8} (α := E₂) (γ := Set E₂)
      {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r}
      ((f : (a : E) → E₂) x_1 : E₂)
⊢ x_1 ∈ (p.comp f).closedBall x r ↔
    Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.closedBall ((f : (a : E) → E₂) x) r) x_1
have h₂ : Membership.mem (γ := Set E) {y : E | (p : (a : E₂) → ℝ) ((f : (a : E) → E₂) (y - x) : E₂) ≤ r} x_1 ↔
  Membership.mem.{u_8, u_8} (α := E₂) (γ := Set E₂)
    {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r} ((f : (a : E) → E₂) x_1 : E₂)
Tactic: simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x_1 : E
h :
  Membership.mem (γ := Set E) {y : E | (p.comp f : (a : E) → ℝ) (y - x) ≤ r} x_1 ↔
    Membership.mem (γ := Set E)
      (preimage.{u_7, u_8} (β := E₂) (⇑f : (a : E) → E₂)
        {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r})
      x_1
h₁ :
  Membership.mem (γ := Set E) {y : E | (p.comp f : (a : E) → ℝ) (y - x) ≤ r} x_1 ↔
    Membership.mem.{u_8, u_8} (α := E₂) (γ := Set E₂)
      {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r}
      ((f : (a : E) → E₂) x_1 : E₂)
h₂ :
  Membership.mem (γ := Set E) {y : E | (p : (a : E₂) → ℝ) ((f : (a : E) → E₂) (y - x) : E₂) ≤ r} x_1 ↔
    Membership.mem.{u_8, u_8} (α := E₂) (γ := Set E₂)
      {y : E₂ | (p : (a : E₂) → ℝ) (HSub.hSub (β := E₂) y ((f : (a : E) → E₂) x : E₂)) ≤ r}
      ((f : (a : E) → E₂) x_1 : E₂)
⊢ x_1 ∈ (p.comp f).closedBall x r ↔
    Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.closedBall ((f : (a : E) → E₂) x) r) x_1
have h₃ : (p : (a : E₂) → ℝ) ((f : (a : E) → E₂) (x_1 - x) : E₂) ≤ r ↔
  (p : (a : E₂) → ℝ) (HSub.hSub (α := E₂) (β := E₂) ((f : (a : E) → E₂) x_1 : E₂) ((f : (a : E) → E₂) x : E₂)) ≤ r
Tactic: simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]
-- 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 : ℝ
⊢ Eq (α := Set E) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r)) {x : E | (p : (a : E) → ℝ) x < r}
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r)) x ↔
    Membership.mem (γ := Set E) {x : E | (p : (a : E) → ℝ) x < r} x
Tactic: ext x
-- 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 : ℝ
⊢ Eq (α := Set E) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r)) {x : E | (p : (a : E) → ℝ) x ≤ r}
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r)) x ↔
    Membership.mem (γ := Set E) {x : E | (p : (a : E) → ℝ) x ≤ r} x
Tactic: ext x
-- 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 : ℝ
⊢ p.ball 0 r = preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r)
have rw : Eq (α := Set E) {y : E | (p : (a : E) → ℝ) y < r} (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r))
Tactic: rw [ball_zero_eq, preimage_metric_ball]
-- 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 : ℝ
rw : Eq (α := Set E) {y : E | (p : (a : E) → ℝ) y < r} (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r))
⊢ p.ball 0 r = preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r)
have rw₁ : Eq.{u_7 + 1} (α := Set E) {y : E | (p : (a : E) → ℝ) y < r} {x : E | (p : (a : E) → ℝ) x < r}
Tactic: rw [ball_zero_eq, preimage_metric_ball]
-- 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 : ℝ
⊢ p.closedBall 0 r = preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r)
have rw : Eq (α := Set E) {y : E | (p : (a : E) → ℝ) y ≤ r} (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r))
Tactic: rw [closedBall_zero_eq, preimage_metric_closedBall]
-- 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 : ℝ
rw : Eq (α := Set E) {y : E | (p : (a : E) → ℝ) y ≤ r} (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r))
⊢ p.closedBall 0 r = preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r)
have rw₁ : Eq.{u_7 + 1} (α := Set E) {y : E | (p : (a : E) → ℝ) y ≤ r} {x : E | (p : (a : E) → ℝ) x ≤ r}
Tactic: rw [closedBall_zero_eq, preimage_metric_closedBall]
-- 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 : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ x ∈ p.ball 0 r
have rw : HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) < r
Tactic: rw [mem_ball_zero, ← hx, 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 : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ (p : (a : E) → ℝ) y < r
have rwa : ∀ (hy : (p : (a : E) → ℝ) y < r) (hx : (fun (x : E) ↦ a • x) y = x), (p : (a : E) → ℝ) y < r
Tactic: rwa [mem_ball_zero] at hy
Cleared hypotheses: hy, hx
-- 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 : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) < r
have _ : (p : (a : E) → ℝ) y < r
Tactic: calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ < r := by rwa [mem_ball_zero] at hy
-- 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 : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ x ∈ p.closedBall 0 r
have rw : HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) ≤ r
Tactic: rw [mem_closedBall_zero, ← hx, 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 : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ (p : (a : E) → ℝ) y ≤ r
have rwa : ∀ (hy : (p : (a : E) → ℝ) y ≤ r) (hx : (fun (x : E) ↦ a • x) y = x), (p : (a : E) → ℝ) y ≤ r
Tactic: rwa [mem_closedBall_zero] at hy
Cleared hypotheses: hy, hx
-- 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 : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.closedBall 0 r
hx : (fun (x : E) ↦ a • x) y = x
⊢ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) y : ℝ) ≤ r
have _ : (p : (a : E) → ℝ) y ≤ r
Tactic: calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ ≤ r := by rwa [mem_closedBall_zero] at hy
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⋂ i ∈ s, (p i).ball x r
have lift : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)), (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
Tactic: lift r to NNReal using hr.le
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
have simp_rw : Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
  (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
Tactic: simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
have simp_rw₁ : Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
Tactic: simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
have simp_rw₂ : Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) sorry) : ℝ) < (↑r : ℝ)}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
Tactic: simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
have simp_rw₃ : Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) sorry) < r}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
Tactic: simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₃ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) < r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
have simp_rw₄ : Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) (y - x)) sorry < r}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
Tactic: simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) < (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) < (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₃ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) < r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
simp_rw₄ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) (y - x)) ⋯ < r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
⊢ (s.sup p).ball x (↑r : ℝ) = ⋂ i ∈ s, (p i).ball x (↑r : ℝ)
have simp_rw₅ : Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, (↑(NNReal.mk ((p b : (a : E) → ℝ) (y - x)) sorry) : ℝ) < (↑r : ℝ)}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) < (↑r : ℝ)}
Tactic: simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
    Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r
have lift : ∀ (r : ℝ≥0), (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
Tactic: lift r to NNReal using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
have simp_rw : Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
  (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
Tactic: simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
have simp_rw₁ : Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
Tactic: simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
have simp_rw₂ : Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) sorry) : ℝ) ≤ (↑r : ℝ)}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
Tactic: simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
have simp_rw₃ : Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) sorry) ≤ r}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
Tactic: simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₃ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) ≤ r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
have simp_rw₄ : Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) (y - x)) sorry ≤ r}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
Tactic: simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    (⋂ i ∈ s, {y : E | (p i : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup p : (a : E) → ℝ) (y - x) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) : ℝ) ≤ (↑r : ℝ)}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₃ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) (y - x)) ⋯) ≤ r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
simp_rw₄ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) (y - x)) ⋯ ≤ r}
    {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
⊢ (s.sup p).closedBall x (↑r : ℝ) = ⋂ i ∈ s, (p i).closedBall x (↑r : ℝ)
have simp_rw₅ : Eq.{u_7 + 1} (α := Set E) {y : E | ∀ b ∈ s, (↑(NNReal.mk ((p b : (a : E) → ℝ) (y - x)) sorry) : ℝ) ≤ (↑r : ℝ)}
  {x_1 : E | ∀ (i : ι) (i_1 : i ∈ s), (p i : (a : E) → ℝ) (x_1 - x) ≤ (↑r : ℝ)}
Tactic: simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = s.inf fun (i : ι) ↦ (p i).ball x r
have rw : (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r
Tactic: rw [Finset.inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = s.inf fun (i : ι) ↦ (p i).closedBall x r
have rw : (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r
Tactic: rw [Finset.inf_eq_iInf]