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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ (c • p).closedBall x r = p.closedBall x (r / (↑c : ℝ))
have h : ∀ (x_1 : E), x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h₁ : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h₄ : HMul.hMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₄ : HMul.hMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h₅ : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₄ : HMul.hMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
h₅ : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) ≤ r ↔ (p : (a : E) → ℝ) (x_1 - x) ≤ r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
have h₆ : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) ≤ r ↔
  HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) ≤ r
Tactic: rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
have simp_rw : Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
  ({y : E | (p : (a : E) → ℝ) (y - e) < r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) < r})
Tactic: simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
    ({y : E | (p : (a : E) → ℝ) (y - e) < r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) < r})
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
have simp_rw₁ : Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
  {a : E | (p : (a : E) → ℝ) (a - e) < r ∧ (q : (a : E) → ℝ) (a - e) < r}
Tactic: simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
    ({y : E | (p : (a : E) → ℝ) (y - e) < r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) < r})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
    {a : E | (p : (a : E) → ℝ) (a - e) < r ∧ (q : (a : E) → ℝ) (a - e) < r}
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
have simp_rw₂ : Eq.{u_7 + 1} (α := Set E) {y : E | ((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (y - e) < r}
  {a : E | (p : (a : E) → ℝ) (a - e) < r ∧ (q : (a : E) → ℝ) (a - e) < r}
Tactic: simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
    ({y : E | (p : (a : E) → ℝ) (y - e) < r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) < r})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) < r}
    {a : E | (p : (a : E) → ℝ) (a - e) < r ∧ (q : (a : E) → ℝ) (a - e) < r}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (y - e) < r}
    {a : E | (p : (a : E) → ℝ) (a - e) < r ∧ (q : (a : E) → ℝ) (a - e) < r}
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
have simp_rw₃ : Eq.{u_7 + 1} (α := Set E) {y : E | max ((p : (a : E) → ℝ) (y - e)) ((q : (a : E) → ℝ) (y - e)) < r}
  {a : E | (p : (a : E) → ℝ) (a - e) < r ∧ (q : (a : E) → ℝ) (a - e) < r}
Tactic: simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
have simp_rw : Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
  ({y : E | (p : (a : E) → ℝ) (y - e) ≤ r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) ≤ r})
Tactic: simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
    ({y : E | (p : (a : E) → ℝ) (y - e) ≤ r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) ≤ r})
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
have simp_rw₁ : Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
  {a : E | (p : (a : E) → ℝ) (a - e) ≤ r ∧ (q : (a : E) → ℝ) (a - e) ≤ r}
Tactic: simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
    ({y : E | (p : (a : E) → ℝ) (y - e) ≤ r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) ≤ r})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
    {a : E | (p : (a : E) → ℝ) (a - e) ≤ r ∧ (q : (a : E) → ℝ) (a - e) ≤ r}
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
have simp_rw₂ : Eq.{u_7 + 1} (α := Set E) {y : E | ((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (y - e) ≤ r}
  {a : E | (p : (a : E) → ℝ) (a - e) ≤ r ∧ (q : (a : E) → ℝ) (a - e) ≤ r}
Tactic: simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]
-- 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 : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
simp_rw :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
    ({y : E | (p : (a : E) → ℝ) (y - e) ≤ r} ∩ {y : E | (q : (a : E) → ℝ) (y - e) ≤ r})
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set E) {y : E | (p ⊔ q : (a : E) → ℝ) (y - e) ≤ r}
    {a : E | (p : (a : E) → ℝ) (a - e) ≤ r ∧ (q : (a : E) → ℝ) (a - e) ≤ r}
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set E) {y : E | ((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (y - e) ≤ r}
    {a : E | (p : (a : E) → ℝ) (a - e) ≤ r ∧ (q : (a : E) → ℝ) (a - e) ≤ r}
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
have simp_rw₃ : Eq.{u_7 + 1} (α := Set E) {y : E | max ((p : (a : E) → ℝ) (y - e)) ((q : (a : E) → ℝ) (y - e)) ≤ r}
  {a : E | (p : (a : E) → ℝ) (a - e) ≤ r ∧ (q : (a : E) → ℝ) (a - e) ≤ r}
Tactic: simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]
-- 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 : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
⊢ (s.sup' H p).ball e r = s.inf' H fun (i : ι) ↦ (p i).ball e r
have singleton : ∀ (a : ι), (Finset.sup' {a} sorry p).ball e r = Finset.inf' {a} sorry fun (i : ι) ↦ (p i).ball e r
Tactic: induction H using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih =>
    simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup, inf_eq_inter, ih]
Cleared hypotheses: H
-- 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 : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
singleton : ∀ (a : ι), (Finset.sup' {a} ⋯ p).ball e r = Finset.inf' {a} ⋯ fun (i : ι) ↦ (p i).ball e r
⊢ (s.sup' H p).ball e r = s.inf' H fun (i : ι) ↦ (p i).ball e r
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty)
  (ih : (s.sup' hs p).ball e r = s.inf' hs fun (i : ι) ↦ (p i).ball e r),
  ((Finset.cons a s h).sup' sorry p).ball e r = (Finset.cons a s h).inf' sorry fun (i : ι) ↦ (p i).ball e r
Tactic: induction H using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih =>
    simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup, inf_eq_inter, ih]
Cleared hypotheses: H
-- 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 : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
⊢ (s.sup' H p).closedBall e r = s.inf' H fun (i : ι) ↦ (p i).closedBall e r
have singleton : ∀ (a : ι), (Finset.sup' {a} sorry p).closedBall e r = Finset.inf' {a} sorry fun (i : ι) ↦ (p i).closedBall e r
Tactic: induction H using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih =>
    simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, closedBall_sup, inf_eq_inter, ih]
Cleared hypotheses: H
-- 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 : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
singleton : ∀ (a : ι), (Finset.sup' {a} ⋯ p).closedBall e r = Finset.inf' {a} ⋯ fun (i : ι) ↦ (p i).closedBall e r
⊢ (s.sup' H p).closedBall e r = s.inf' H fun (i : ι) ↦ (p i).closedBall e r
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty)
  (ih : (s.sup' hs p).closedBall e r = s.inf' hs fun (i : ι) ↦ (p i).closedBall e r),
  ((Finset.cons a s h).sup' sorry p).closedBall e r = (Finset.cons a s h).inf' sorry fun (i : ι) ↦ (p i).closedBall e r
Tactic: induction H using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih =>
    simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, closedBall_sup, inf_eq_inter, ih]
Cleared hypotheses: H
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ (fun (x1 x2 : E) ↦ x1 + x2) y₁ y₂ ∈ p.ball (x₁ + x₂) (r₁ + r₂)
have rw : (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂
Tactic: rw [mem_ball, add_sub_add_comm]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.closedBall x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.closedBall x₂ r₂
⊢ (fun (x1 x2 : E) ↦ x1 + x2) y₁ y₂ ∈ p.closedBall (x₁ + x₂) (r₁ + r₂)
have rw : (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂
Tactic: rw [mem_closedBall, add_sub_add_comm]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.ball x r = Metric.ball x r
have h : ∀ (x_1 : E), x_1 ∈ p.ball x r ↔ x_1 ∈ Metric.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 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
x_1 : E
⊢ x_1 ∈ p.ball x r ↔ x_1 ∈ Metric.ball x r
have h : x_1 ∈ p.ball x r ↔ ‖x_1 - x‖ < r
Tactic: simp only [mem_ball_iff_norm]
-- 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 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.closedBall x r = Metric.closedBall x r
have h : ∀ (x_1 : E), x_1 ∈ p.closedBall x r ↔ x_1 ∈ Metric.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 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
x_1 : E
⊢ x_1 ∈ p.closedBall x r ↔ x_1 ∈ Metric.closedBall x r
have h : x_1 ∈ p.closedBall x r ↔ ‖x_1 - x‖ ≤ r
Tactic: simp only [mem_closedBall_iff_norm]
-- 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 : ℝ
⊢ (p.comp f).ball x r = (⇑f : (a : E) → E₂) ⁻¹' p.ball ((f : (a : E) → E₂) x) r
have h : ∀ (x_1 : E),
  x_1 ∈ (p.comp f).ball x r ↔ Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.ball ((f : (a : E) → E₂) x) r) x_1
Tactic: ext
-- 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
⊢ x_1 ∈ (p.comp f).ball x r ↔ Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.ball ((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 (γ := 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
Tactic: simp_rw [ball, 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
⊢ x_1 ∈ (p.comp f).ball x r ↔ Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.ball ((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 [ball, 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).ball x r ↔ Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.ball ((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 [ball, 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).ball x r ↔ Membership.mem (γ := Set E) ((⇑f : (a : E) → E₂) ⁻¹' p.ball ((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 [ball, 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 : ℝ
⊢ (p.comp f).closedBall x r = (⇑f : (a : E) → E₂) ⁻¹' p.closedBall ((f : (a : E) → E₂) x) r
have h : ∀ (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
Tactic: ext
-- 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
⊢ 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 (γ := 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
Tactic: simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]