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 : 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
h₅ 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

Tactic:
rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

Premises used: Set.mem_neg, AddGroupSeminormClass.map_neg_eq_map, neg_add', Seminorm.mem_ball, sub_neg_eq_add
-- 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
h : ∀ (x_1 : E), x_1 ∈ -p.closedBall x r ↔ x_1 ∈ p.closedBall (-x) r
⊢ -p.closedBall x r = p.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 : 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
h₅ 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

Tactic:
rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

Premises used: Set.mem_neg, AddGroupSeminormClass.map_neg_eq_map, neg_add', Seminorm.mem_closedBall, sub_neg_eq_add
-- Module: Mathlib.Analysis.Seminorm
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
inr : Nonempty ι → 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

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Seminorm
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 ι
inl : closedBall.{u_3, u_7} (𝕜 := 𝕜) ⊥ e r = univ
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r

Tactic:
rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]

Premises used: Set.iInter_of_empty, Seminorm.sSup_empty, iSup_of_empty'
-- Module: Mathlib.Analysis.Seminorm
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} (𝕜 := 𝕜) ⊥ e r = univ

Tactic:
closedBall_bot _ hr

Premises used: Seminorm.closedBall_bot
-- Module: Mathlib.Analysis.Seminorm
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} (𝕜 := 𝕜) ⊥ e r = univ

Tactic:
exact closedBall_bot _ hr

Premises used: Seminorm.closedBall_bot
-- Module: Mathlib.Analysis.Seminorm
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 ι
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
⊢ closedBall.{u_3, u_7} (𝕜 := 𝕜) (⨆ (i : ι), p i) e r = ⋂ (i : ι), (p i).closedBall e r

Tactic:
ext x
-- Module: Mathlib.Analysis.Seminorm
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
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) (x - e))

Tactic:
have := Seminorm.bddAbove_range_iff.mp hp (x - e)
-- Module: Mathlib.Analysis.Seminorm
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
this : BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) (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:
simp only [mem_closedBall, mem_iInter, Seminorm.iSup_apply hp, ciSup_le_iff this]

Premises used: ciSup_le_iff, Seminorm.iSup_apply, Set.mem_iInter, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
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)
inr : ∀ (hk : k ≠ 0), p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
⊢ p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r

Tactic:
rcases eq_or_ne k 0 with (rfl | hk)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
inl : ∅ ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)
⊢ p.ball 0 (norm.{u_3} (E := 𝕜) 0 * r) ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)

Tactic:
rw [norm_zero, zero_mul, ball_eq_emptyset _ le_rfl]

Premises used: le_rfl, Seminorm.ball_eq_emptyset, MulZeroClass.zero_mul, norm_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ∅ ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)

Tactic:
empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ∅ ⊆ HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 (p.ball 0 r)

Tactic:
exact empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.Analysis.Seminorm
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 : (p : (a : E) → ℝ) x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x
⊢ x ∈ p.ball 0 (‖k‖ * r) → x ∈ k • p.ball 0 r

Tactic:
rw [Set.mem_smul_set, Seminorm.mem_ball_zero]

Premises used: Seminorm.mem_ball_zero, Set.mem_smul_set
-- Module: Mathlib.Analysis.Seminorm
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

Tactic:
fun hx => ⟨k⁻¹ • x, ?_, ?_⟩

Premises used: Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Seminorm
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
inr₁ : ∀ (hx : (p : (a : E) → ℝ) x < ‖k‖ * r), k • k⁻¹ • x = x
⊢ (p : (a : E) → ℝ) x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x

Tactic:
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
-- Module: Mathlib.Analysis.Seminorm
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
inr₆ : HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((p : (a : E) → ℝ) x : ℝ) < ‖k‖ * r
inr₇ inr₈ inr₉ inr₁₀ : (p : (a : E) → ℝ) x < ‖k‖ * r
⊢ k⁻¹ • x ∈ p.ball 0 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]

Premises used: Iff.mpr, Seminorm.mem_ball_zero, Norm.norm, norm_pos_iff, mul_assoc, ne_of_gt, div_eq_mul_inv, norm_inv, mul_lt_mul_iff_right₀, SeminormClass.map_smul_eq_mul, one_mul, div_self
-- Module: Mathlib.Analysis.Seminorm
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
inr₂ : (k / k) • x = x
inr₃ : HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x = x
inr₄ inr₅ : x = x
⊢ k • k⁻¹ • x = x

Tactic:
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]

Premises used: smul_assoc, div_eq_mul_inv, one_smul, smul_eq_mul, div_self
-- Module: Mathlib.Analysis.Seminorm
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
h : ∀ (x : E), x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
⊢ k • p.ball 0 r = p.ball 0 (‖k‖ * r)

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
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
h : k⁻¹ • x ∈ p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
h₁ : (p : (a : E) → ℝ) (k⁻¹ • x) < r ↔ x ∈ p.ball 0 (‖k‖ * r)
h₂ : (p : (a : E) → ℝ) (k⁻¹ • x) < r ↔ (p : (a : E) → ℝ) x < ‖k‖ * r
h₃ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r ↔ (p : (a : E) → ℝ) x < ‖k‖ * r
h₄ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r ↔ (p : (a : E) → ℝ) x < ‖k‖ * r
h₅ : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ‖k‖ < r ↔ (p : (a : E) → ℝ) x < ‖k‖ * r
h₆ : (p : (a : E) → ℝ) x < r * ‖k‖ ↔ (p : (a : E) → ℝ) x < ‖k‖ * r
h₇ h₈ : (p : (a : E) → ℝ) x < ‖k‖ * r ↔ (p : (a : E) → ℝ) x < ‖k‖ * r
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hk, p.mem_ball_zero, p.mem_ball_zero, map_smul_eq_mul,
    norm_inv, ← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hk), mul_comm]

Premises used: Iff.mpr, Seminorm.mem_ball_zero, norm_pos_iff, div_lt_iff₀, norm_inv, SeminormClass.map_smul_eq_mul, mul_comm, div_eq_inv_mul, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun (x : E) ↦ k • x) y = x
rw : HMul.hMul (β := ℝ) ‖k‖ ((p : (a : E) → ℝ) y : ℝ) ≤ ‖k‖ * r
⊢ x ∈ p.closedBall 0 (‖k‖ * r)

Tactic:
rw [Seminorm.mem_closedBall_zero, ← h, map_smul_eq_mul]

Premises used: Seminorm.mem_closedBall_zero, SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun (x : E) ↦ k • x) y = x
⊢ (p : (a : E) → ℝ) y ≤ r

Tactic:
rw [Seminorm.mem_closedBall_zero] at hy

Premises used: Seminorm.mem_closedBall_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun (x : E) ↦ k • x) y = x
hy₁ : (p : (a : E) → ℝ) y ≤ r
⊢ (fun (x : E) ↦ k • x) y = x

Tactic:
rw [Seminorm.mem_closedBall_zero] at hy

Premises used: Seminorm.mem_closedBall_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : (p : (a : E) → ℝ) y ≤ r
h : (fun (x : E) ↦ k • x) y = x
ha : 0 ≤ ‖k‖
⊢ HMul.hMul (β := ℝ) ‖k‖ ((p : (a : E) → ℝ) y : ℝ) ≤ ‖k‖ * r

Tactic:
gcongr
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)

Tactic:
subset_antisymm smul_closedBall_subset ?_

Premises used: subset_antisymm, Seminorm.smul_closedBall_subset
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
refine : p.closedBall 0 (‖k‖ * r) ⊆ k • p.closedBall 0 r
⊢ k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)

Tactic:
refine subset_antisymm smul_closedBall_subset ?_

Premises used: subset_antisymm, Seminorm.smul_closedBall_subset
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
rw : (p : (a : E) → ℝ) x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x
⊢ x ∈ p.closedBall 0 (‖k‖ * r) → x ∈ k • p.closedBall 0 r

Tactic:
rw [Set.mem_smul_set, Seminorm.mem_closedBall_zero]

Premises used: Seminorm.mem_closedBall_zero, Set.mem_smul_set
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ (p : (a : E) → ℝ) x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x

Tactic:
fun hx => ⟨k⁻¹ • x, ?_, ?_⟩

Premises used: Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
refine_1 : ∀ (hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r), k⁻¹ • x ∈ p.closedBall 0 r
refine_2 : ∀ (hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r), k • k⁻¹ • x = x
⊢ (p : (a : E) → ℝ) x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x

Tactic:
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
refine_1 : (p : (a : E) → ℝ) (k⁻¹ • x) ≤ r
refine_1₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) ≤ r
refine_1₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) ≤ r
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ p.closedBall 0 r

Tactic:
rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]

Premises used: Seminorm.mem_closedBall_zero, norm_inv, inv_mul_le_iff₀, SeminormClass.map_smul_eq_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
refine_2 : (k • k⁻¹) • x = x
refine_2₁ : (k * k⁻¹) • x = x
refine_2₂ : (k / k) • x = x
refine_2₃ : HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x = x
refine_2₄ refine_2₅ : x = x
⊢ k • k⁻¹ • x = x

Tactic:
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]

Premises used: norm_pos_iff, smul_assoc, div_eq_mul_inv, one_smul, Iff.mp, smul_eq_mul, div_self
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : r₂ < r * r₁), Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩

Premises used: exists_pos_lt_mul
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
.of_norm ⟨r, fun a ha x hx => ?_⟩

Premises used: Exists.intro, Absorbs.of_norm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
refine : ∀ (a : 𝕜) (ha : r ≤ ‖a‖) (x : E) (hx : x ∈ p.ball 0 r₂), x ∈ a • p.ball 0 r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
refine .of_norm ⟨r, fun a ha x hx => ?_⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
rw : (p : (a : E) → ℝ) x < ‖a‖ * r₁
⊢ x ∈ a • p.ball 0 r₁

Tactic:
rw [smul_ball_zero (norm_pos_iff.1 <| hr₀.trans_le ha), p.mem_ball_zero]

Premises used: Seminorm.mem_ball_zero, norm_pos_iff, LT.lt.trans_le, Iff.mp, Seminorm.smul_ball_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ (p : (a : E) → ℝ) x < r₂

Tactic:
rw [p.mem_ball_zero] at hx

Premises used: Seminorm.mem_ball_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : (p : (a : E) → ℝ) x < r₂
ha₁ : 0 ≤ r₁
⊢ r * r₁ ≤ ‖a‖ * r₁

Tactic:
gcongr
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : (p : (a : E) → ℝ) x < r₂
⊢ (p : (a : E) → ℝ) x < ‖a‖ * r₁

Tactic:
exact hx.trans (hr.trans_le <| by gcongr)

Premises used: LT.lt.trans_le, LT.lt.trans
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 (p.ball 0 r)

Tactic:
absorbent_iff_forall_absorbs_singleton.2 fun _ =>
    (p.ball_zero_absorbs_ball_zero hr).mono_right <|
      singleton_subset_iff.2 <| p.mem_ball_zero.2 <| lt_add_one _

Premises used: Iff.mpr, Seminorm.mem_ball_zero, Set.singleton_subset_iff, lt_add_one, Seminorm.ball_zero_absorbs_ball_zero, absorbent_iff_forall_absorbs_singleton, Absorbs.mono_right, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 (p.closedBall 0 r)

Tactic:
(p.absorbent_ball_zero hr).mono (p.ball_subset_closedBall _ _)

Premises used: Seminorm.absorbent_ball_zero, Seminorm.ball_subset_closedBall, Absorbent.mono
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
⊢ Absorbent 𝕜 (p.ball x r)

Tactic:
(p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => ?_

Premises used: Iff.mpr, sub_pos, Seminorm.absorbent_ball_zero, Absorbent.mono
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
refine : ∀ (y : E) (hy : y ∈ p.ball 0 (HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ))), y ∈ p.ball x r
⊢ Absorbent 𝕜 (p.ball x r)

Tactic:
refine (p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => ?_

Premises used: Iff.mpr, sub_pos, Seminorm.absorbent_ball_zero, Absorbent.mono
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
y : E
hy : y ∈ p.ball 0 (HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ))
⊢ (p : (a : E) → ℝ) y < HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rw [p.mem_ball_zero] at hy

Premises used: Seminorm.mem_ball_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
y : E
hy : (p : (a : E) → ℝ) y < HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)
⊢ y ∈ p.ball x r

Tactic:
p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)

Premises used: Iff.mpr, add_lt_of_lt_sub_right, Seminorm.mem_ball, map_sub_le_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
y : E
hy : (p : (a : E) → ℝ) y < HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)
⊢ y ∈ p.ball x r

Tactic:
exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)

Premises used: Iff.mpr, add_lt_of_lt_sub_right, Seminorm.mem_ball, map_sub_le_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
⊢ Absorbent 𝕜 (p.closedBall x r)

Tactic:
(p.absorbent_closedBall_zero <| sub_pos.2 hpr).mono fun y hy => ?_

Premises used: Seminorm.absorbent_closedBall_zero, Iff.mpr, sub_pos, Absorbent.mono
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
refine : ∀ (y : E) (hy : y ∈ p.closedBall 0 (HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ))), y ∈ p.closedBall x r
⊢ Absorbent 𝕜 (p.closedBall x r)

Tactic:
refine (p.absorbent_closedBall_zero <| sub_pos.2 hpr).mono fun y hy => ?_

Premises used: Seminorm.absorbent_closedBall_zero, Iff.mpr, sub_pos, Absorbent.mono
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
y : E
hy : y ∈ p.closedBall 0 (HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ))
⊢ (p : (a : E) → ℝ) y ≤ HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rw [p.mem_closedBall_zero] at hy

Premises used: Seminorm.mem_closedBall_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
y : E
hy : (p : (a : E) → ℝ) y ≤ HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)
⊢ y ∈ p.closedBall x r

Tactic:
p.mem_closedBall.2 ((map_sub_le_add p _ _).trans <| add_le_of_le_sub_right hy)

Premises used: Iff.mpr, map_sub_le_add, LE.le.trans, add_le_of_le_sub_right, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
y : E
hy : (p : (a : E) → ℝ) y ≤ HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)
⊢ y ∈ p.closedBall x r

Tactic:
exact p.mem_closedBall.2 ((map_sub_le_add p _ _).trans <| add_le_of_le_sub_right hy)

Premises used: Iff.mpr, map_sub_le_add, LE.le.trans, add_le_of_le_sub_right, Seminorm.mem_closedBall