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 : 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
⊢ k • k⁻¹ • x = x
have inr₃ : HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : (p : (a : E) → ℝ) x < ‖k‖ * r
inr : (k • k⁻¹) • x = x
inr₁ : (k * k⁻¹) • x = x
inr₂ : (k / k) • x = x
inr₃ : HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x = x
⊢ k • k⁻¹ • x = x
have inr₄ : x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
⊢ k • p.ball 0 r = p.ball 0 (‖k‖ * r)
have h : ∀ (x : E), x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h : k⁻¹ • x ∈ 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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
h : k⁻¹ • x ∈ p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₁ : (p : (a : E) → ℝ) (k⁻¹ • x) < 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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
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)
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₂ : (p : (a : E) → ℝ) (k⁻¹ • x) < r ↔ (p : (a : E) → ℝ) x < ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
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
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₃ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) < r ↔ (p : (a : E) → ℝ) x < ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
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
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₄ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) < r ↔ (p : (a : E) → ℝ) x < ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
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
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₅ : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ‖k‖ < r ↔ (p : (a : E) → ℝ) x < ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
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
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₆ : (p : (a : E) → ℝ) x < r * ‖k‖ ↔ (p : (a : E) → ℝ) x < ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
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
⊢ x ∈ k • p.ball 0 r ↔ x ∈ p.ball 0 (‖k‖ * r)
have h₇ : (p : (a : E) → ℝ) x < ‖k‖ * r ↔ (p : (a : E) → ℝ) x < ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun (x : E) ↦ k • x) y = x
⊢ x ∈ p.closedBall 0 (‖k‖ * r)
have rw : HMul.hMul (β := ℝ) ‖k‖ ((p : (a : E) → ℝ) y : ℝ) ≤ ‖k‖ * r
Tactic: rw [Seminorm.mem_closedBall_zero, ← h, map_smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun (x : E) ↦ k • x) y = x
⊢ HMul.hMul (β := ℝ) ‖k‖ ((p : (a : E) → ℝ) y : ℝ) ≤ ‖k‖ * r
have hy₁ : (p : (a : E) → ℝ) y ≤ r
Tactic: rw [Seminorm.mem_closedBall_zero] at hy
Cleared hypotheses: hy, h
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : (p : (a : E) → ℝ) y ≤ r
h : (fun (x : E) ↦ k • x) y = x
⊢ HMul.hMul (β := ℝ) ‖k‖ ((p : (a : E) → ℝ) y : ℝ) ≤ ‖k‖ * r
have ha : 0 ≤ ‖k‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)
have refine : p.closedBall 0 (‖k‖ * r) ⊆ k • p.closedBall 0 r
Tactic: refine subset_antisymm smul_closedBall_subset ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ x ∈ p.closedBall 0 (‖k‖ * r) → x ∈ k • p.closedBall 0 r
have rw : (p : (a : E) → ℝ) x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x
Tactic: rw [Set.mem_smul_set, Seminorm.mem_closedBall_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ (p : (a : E) → ℝ) x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x
have refine_1 : ∀ (hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r), k⁻¹ • x ∈ p.closedBall 0 r
Tactic: refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
refine_1 : ∀ (hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r), k⁻¹ • x ∈ p.closedBall 0 r
⊢ (p : (a : E) → ℝ) x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x
have refine_2 : ∀ (hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r), k • k⁻¹ • x = x
Tactic: refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ p.closedBall 0 r
have refine_1 : (p : (a : E) → ℝ) (k⁻¹ • x) ≤ r
Tactic: rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
refine_1 : (p : (a : E) → ℝ) (k⁻¹ • x) ≤ r
⊢ k⁻¹ • x ∈ p.closedBall 0 r
have refine_1₁ : HMul.hMul (β := ℝ) ‖k⁻¹‖ ((p : (a : E) → ℝ) x : ℝ) ≤ r
Tactic: rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
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
⊢ k⁻¹ • x ∈ p.closedBall 0 r
have refine_1₂ : HMul.hMul (β := ℝ) ‖k‖⁻¹ ((p : (a : E) → ℝ) x : ℝ) ≤ r
Tactic: rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
⊢ k • k⁻¹ • x = x
have refine_2 : (k • k⁻¹) • x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
refine_2 : (k • k⁻¹) • x = x
⊢ k • k⁻¹ • x = x
have refine_2₁ : (k * k⁻¹) • x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : (p : (a : E) → ℝ) x ≤ ‖k‖ * r
refine_2 : (k • k⁻¹) • x = x
refine_2₁ : (k * k⁻¹) • x = x
⊢ k • k⁻¹ • x = x
have refine_2₂ : (k / k) • x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 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
⊢ k • k⁻¹ • x = x
have refine_2₃ : HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 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
⊢ k • k⁻¹ • x = x
have refine_2₄ : x = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
have rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : r₂ < r * r₁), Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
Tactic: rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
have refine : ∀ (a : 𝕜) (ha : r ≤ ‖a‖) (x : E) (hx : x ∈ p.ball 0 r₂), x ∈ a • p.ball 0 r₁
Tactic: refine .of_norm ⟨r, fun a ha x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ x ∈ a • p.ball 0 r₁
have rw : (p : (a : E) → ℝ) x < ‖a‖ * r₁
Tactic: rw [smul_ball_zero (norm_pos_iff.1 <| hr₀.trans_le ha), p.mem_ball_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
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 < ‖a‖ * r₁
have hx₁ : (p : (a : E) → ℝ) x < r₂
Tactic: rw [p.mem_ball_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : (p : (a : E) → ℝ) x < r₂
⊢ r * r₁ ≤ ‖a‖ * r₁
have ha₁ : 0 ≤ r₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
⊢ Absorbent 𝕜 (p.ball x r)
have refine : ∀ (y : E) (hy : y ∈ p.ball 0 (HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ))), y ∈ p.ball x r
Tactic: refine (p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
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 : ℝ))
⊢ y ∈ p.ball x r
have hy₁ : (p : (a : E) → ℝ) y < HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)
Tactic: rw [p.mem_ball_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : (p : (a : E) → ℝ) x < r
⊢ Absorbent 𝕜 (p.closedBall x r)
have refine : ∀ (y : E) (hy : y ∈ p.closedBall 0 (HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ))), y ∈ p.closedBall x r
Tactic: refine (p.absorbent_closedBall_zero <| sub_pos.2 hpr).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
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 : ℝ))
⊢ y ∈ p.closedBall x r
have hy₁ : (p : (a : E) → ℝ) y ≤ HSub.hSub (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)
Tactic: rw [p.mem_closedBall_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₃ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ < r
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ < r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₄ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) < r
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ < r
rw₄ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) < r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₅ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) < r
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ < r
rw₄ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) < r
rw₅ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) < r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₆ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • x - a • a⁻¹ • y) < r
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.ball y r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) < r ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) < r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ < r
rw₄ : (p : (a : E) → ℝ) (a • x - y) < r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) < r
rw₅ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) < r
rw₆ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • x - a • a⁻¹ • y) < r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.ball y r) x ↔ x ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
have rw₇ : (p : (a : E) → ℝ) (a • x - y) < r ↔ (p : (a : E) → ℝ) (a • x - y) < r
Tactic: rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]