awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
h : (p : (a : E) → ℝ) (y - x) ≤ r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
h₁ : (p : (a : E) → ℝ) (y - x) ≤ r ↔ ∀ (i : ℝ) (j : i > r), y ∈ p.ball x i
h₂ : (p : (a : E) → ℝ) (y - x) ≤ r ↔ ∀ (i : ℝ) (j : i > r), (p : (a : E) → ℝ) (y - x) < i
⊢ y ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y

Tactic:
simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]

Premises used: Set.mem_iInter₂, forall_gt_iff_le, Seminorm.mem_ball, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
rw : ∀ (x_1 : E), Membership.mem (γ := Set E) {y : E | (0 : (a : E) → ℝ) (y - x) < r} x_1
⊢ ball.{u_3, u_7} (𝕜 := 𝕜) 0 x r = univ

Tactic:
rw [Set.eq_univ_iff_forall, ball]

Premises used: Set.eq_univ_iff_forall, Seminorm.ball
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ∀ (x_1 : E), Membership.mem (γ := Set E) {y : E | (0 : (a : E) → ℝ) (y - x) < r} x_1

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) 0 x r = univ

Tactic:
eq_univ_of_subset (ball_subset_closedBall _ _ _) (ball_zero' x hr)

Premises used: Set.eq_univ_of_subset, Seminorm.ball_zero', Seminorm.ball_subset_closedBall
-- Module: Mathlib.Analysis.Seminorm
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
h : ∀ (x_1 : E), x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
⊢ (c • p).ball x r = p.ball x (r / (↑c : ℝ))

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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.ball 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 : ℝ)
h₆ h₇ :
  HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) < r ↔
    HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) < r
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))

Tactic:
rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]

Premises used: Iff.mpr, lt_div_iff₀, NNReal.smul_def, Seminorm.mem_ball, mul_comm, NNReal.coe_pos, Seminorm.smul_apply, smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
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
h : ∀ (x_1 : E), x_1 ∈ (c • p).closedBall x r ↔ x_1 ∈ p.closedBall x (r / (↑c : ℝ))
⊢ (c • p).closedBall x r = p.closedBall x (r / (↑c : ℝ))

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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 : ℝ)
h₆ h₇ :
  HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) ≤ r ↔
    HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) ≤ r
⊢ x_1 ∈ (c • p).closedBall 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)]

Premises used: Iff.mpr, NNReal.smul_def, mul_comm, NNReal.coe_pos, Seminorm.smul_apply, smul_eq_mul, le_div_iff₀, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
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}
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}
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r

Tactic:
simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]

Premises used: Set.setOf_and, Seminorm.coe_sup, Seminorm.ball, Pi.sup_apply, sup_lt_iff
-- Module: Mathlib.Analysis.Seminorm
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}
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}
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r

Tactic:
simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]

Premises used: Set.setOf_and, Seminorm.coe_sup, Seminorm.closedBall, sup_le_iff, Pi.sup_apply
-- Module: Mathlib.Analysis.Seminorm
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 ι
e : E
r : ℝ
a : ι
⊢ (Finset.sup' {a} ⋯ p).ball e r = Finset.inf' {a} ⋯ fun (i : ι) ↦ (p i).ball e r

Tactic:
simp
-- Module: Mathlib.Analysis.Seminorm
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 ι
e : E
r : ℝ
a : ι
s_1 : Finset ι
h : a ∉ s_1
hs : s_1.Nonempty
ih : (s_1.sup' hs p).ball e r = s_1.inf' hs fun (i : ι) ↦ (p i).ball e r
⊢ ((Finset.cons a s_1 h).sup' ⋯ p).ball e r = (Finset.cons a s_1 h).inf' ⋯ fun (i : ι) ↦ (p i).ball e r

Tactic:
simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup, inf_eq_inter, ih]

Premises used: Seminorm.ball_sup, Finset.inf'_cons, Set.inf_eq_inter, Finset.sup'_cons
-- Module: Mathlib.Analysis.Seminorm
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
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' ⋯ p).ball e r = (Finset.cons a s h).inf' ⋯ fun (i : ι) ↦ (p i).ball e r
⊢ (s.sup' H p).ball e r = s.inf' H 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]

Premises used: Seminorm.ball_sup, Set.inf_eq_inter, Singleton.singleton
-- Module: Mathlib.Analysis.Seminorm
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 ι
e : E
r : ℝ
a : ι
⊢ (Finset.sup' {a} ⋯ p).closedBall e r = Finset.inf' {a} ⋯ fun (i : ι) ↦ (p i).closedBall e r

Tactic:
simp
-- Module: Mathlib.Analysis.Seminorm
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 ι
e : E
r : ℝ
a : ι
s_1 : Finset ι
h : a ∉ s_1
hs : s_1.Nonempty
ih : (s_1.sup' hs p).closedBall e r = s_1.inf' hs fun (i : ι) ↦ (p i).closedBall e r
⊢ ((Finset.cons a s_1 h).sup' ⋯ p).closedBall e r = (Finset.cons a s_1 h).inf' ⋯ fun (i : ι) ↦ (p i).closedBall e r

Tactic:
simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, closedBall_sup, inf_eq_inter, ih]

Premises used: Seminorm.closedBall_sup, Finset.inf'_cons, Set.inf_eq_inter, Finset.sup'_cons
-- Module: Mathlib.Analysis.Seminorm
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
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' ⋯ p).closedBall e r = (Finset.cons a s h).inf' ⋯ fun (i : ι) ↦ (p i).closedBall e r
⊢ (s.sup' H p).closedBall e r = s.inf' H 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]

Premises used: Seminorm.closedBall_sup, Set.inf_eq_inter, Singleton.singleton
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
x : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
h : r₁ ≤ r₂
⊢ p.ball x r₁ ⊆ p.ball x r₂

Tactic:
fun _ (hx : _ < _) => hx.trans_le h

Premises used: Set.Mem, setOf, Set.Subset, Seminorm.ball, LT.lt.trans_le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
x : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
h : r₁ ≤ r₂
⊢ p.closedBall x r₁ ⊆ p.closedBall x r₂

Tactic:
fun _ (hx : _ ≤ _) => hx.trans h

Premises used: Set.Mem, setOf, Seminorm.closedBall, Set.Subset, LE.le.trans
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
x : E
r : ℝ
p q : Seminorm 𝕜 E
h : q ≤ p
⊢ p.ball x r ⊆ q.ball x r

Tactic:
fun _ =>
  (h _).trans_lt

Premises used: Set.Mem, setOf, HSub.hSub, Set.Subset, Seminorm.ball, LE.le.trans_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
x : E
r : ℝ
p q : Seminorm 𝕜 E
h : q ≤ p
⊢ p.closedBall x r ⊆ q.closedBall x r

Tactic:
fun _ => (h _).trans

Premises used: Set.Mem, setOf, HSub.hSub, Seminorm.closedBall, Set.Subset, LE.le.trans
-- Module: Mathlib.Analysis.Seminorm
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₂
rw : (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂
⊢ (fun (x1 x2 : E) ↦ x1 + x2) y₁ y₂ ∈ p.ball (x₁ + x₂) (r₁ + r₂)

Tactic:
rw [mem_ball, add_sub_add_comm]

Premises used: Seminorm.mem_ball, add_sub_add_comm
-- Module: Mathlib.Analysis.Seminorm
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₂
⊢ (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂

Tactic:
(map_add_le_add p _ _).trans_lt (add_lt_add hy₁ hy₂)

Premises used: add_lt_add, LE.le.trans_lt, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Seminorm
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₂
⊢ (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂

Tactic:
exact (map_add_le_add p _ _).trans_lt (add_lt_add hy₁ hy₂)

Premises used: add_lt_add, LE.le.trans_lt, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Seminorm
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₂
rw : (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂
⊢ (fun (x1 x2 : E) ↦ x1 + x2) y₁ y₂ ∈ p.closedBall (x₁ + x₂) (r₁ + r₂)

Tactic:
rw [mem_closedBall, add_sub_add_comm]

Premises used: add_sub_add_comm, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
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₂
⊢ (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂

Tactic:
(map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)

Premises used: add_le_add, LE.le.trans, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Seminorm
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₂
⊢ (p : (a : E) → ℝ) (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂

Tactic:
exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)

Premises used: add_le_add, LE.le.trans, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
h : ∀ (x_1 : E), x_1 ∈ p.ball x r ↔ x_1 ∈ Metric.ball x r
⊢ p.ball x r = Metric.ball x r

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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
h : x_1 ∈ p.ball x r ↔ ‖x_1 - x‖ < r
⊢ x_1 ∈ p.ball x r ↔ x_1 ∈ Metric.ball x r

Tactic:
simp only [mem_ball_iff_norm]

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Seminorm
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 - x‖ < r

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
h : ∀ (x_1 : E), x_1 ∈ p.closedBall x r ↔ x_1 ∈ Metric.closedBall x r
⊢ p.closedBall x r = Metric.closedBall x r

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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
h : x_1 ∈ p.closedBall x r ↔ ‖x_1 - x‖ ≤ r
⊢ x_1 ∈ p.closedBall x r ↔ x_1 ∈ Metric.closedBall x r

Tactic:
simp only [mem_closedBall_iff_norm]

Premises used: mem_closedBall_iff_norm
-- Module: Mathlib.Analysis.Seminorm
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 - x‖ ≤ r

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
this : SeminormedAddCommGroup E := p.toSeminormedAddCommGroup
⊢ x +ᵥ p.ball y r = p.ball (x +ᵥ y) r

Tactic:
simp [ball_eq_metric]

Premises used: Seminorm.ball_eq_metric
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
this : SeminormedAddCommGroup E := p.toSeminormedAddCommGroup
⊢ x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r

Tactic:
simp [closedBall_eq_metric]

Premises used: Seminorm.closedBall_eq_metric
-- Module: Mathlib.Analysis.Seminorm
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 : ℝ
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
⊢ (p.comp f).ball x r = (⇑f : (a : E) → E₂) ⁻¹' p.ball ((f : (a : E) → E₂) x) r

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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₂)
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
⊢ 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:
simp_rw [ball, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]

Premises used: map_sub, Set.mem_setOf_eq, Seminorm.comp_apply, Seminorm.ball, Set.mem_preimage
-- Module: Mathlib.Analysis.Seminorm
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 : ℝ
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
⊢ (p.comp f).closedBall x r = (⇑f : (a : E) → E₂) ⁻¹' p.closedBall ((f : (a : E) → E₂) x) r

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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₂)
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
⊢ 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:
simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]

Premises used: map_sub, Seminorm.closedBall, Set.mem_setOf_eq, Seminorm.comp_apply, Set.mem_preimage
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
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
⊢ Eq (α := Set E) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r)) {x : E | (p : (a : E) → ℝ) x < r}

Tactic:
ext x
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
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:
simp only [mem_setOf, mem_preimage, mem_ball_zero_iff, Real.norm_of_nonneg (apply_nonneg p _)]

Premises used: Set.mem_setOf, NonnegHomClass.apply_nonneg, Set.mem_preimage, mem_ball_zero_iff, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
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
⊢ Eq (α := Set E) (preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.closedBall 0 r)) {x : E | (p : (a : E) → ℝ) x ≤ r}

Tactic:
ext x
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
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:
simp only [mem_setOf, mem_preimage, mem_closedBall_zero_iff,
    Real.norm_of_nonneg (apply_nonneg p _)]

Premises used: Set.mem_setOf, NonnegHomClass.apply_nonneg, mem_closedBall_zero_iff, Set.mem_preimage, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Seminorm
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))
rw₁ rw₂ : Eq.{u_7 + 1} (α := Set E) {y : E | (p : (a : E) → ℝ) y < r} {x : E | (p : (a : E) → ℝ) x < r}
⊢ p.ball 0 r = preimage (β := ℝ) (⇑p : (a : E) → ℝ) (Metric.ball 0 r)

Tactic:
rw [ball_zero_eq, preimage_metric_ball]

Premises used: Seminorm.preimage_metric_ball, Seminorm.ball_zero_eq