awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h_1 : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 (‖x‖ ^ m) < a ^ m
hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m)
h : m = 0
⊢ False

Tactic:
simp only [h, zero_add, pow_zero, max_self, one_smul, lt_self_iff_false] at hm

Premises used: max_self, zero_add, pow_zero, one_smul, lt_self_iff_false
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
⊢ IsUltrametricDist R

Tactic:
isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm (fun x m ↦ ?_)

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
refine : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm (fun x m ↦ ?_)

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
rw : norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
⊢ ‖n • x‖ ≤ ‖x‖

Tactic:
rw [nsmul_eq_mul, norm_mul]

Premises used: norm_mul, nsmul_eq_mul
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
inl : ∀ (hx : 0 = ‖x‖), norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
inr : ∀ (hx : 0 < ‖x‖), norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖
⊢ norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖

Tactic:
rcases (norm_nonneg x).eq_or_lt with hx | hx

Premises used: LE.le.eq_or_lt, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
hx : 0 = ‖x‖
⊢ norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖

Tactic:
simp only [← hx, mul_zero, le_refl]

Premises used: le_refl, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x_1 : R
m : ℕ
x : R
n : ℕ
hx : 0 < ‖x‖
⊢ norm.{u_1} (E := R) (↑n : R) * ‖x‖ ≤ ‖x‖

Tactic:
simpa only [mul_le_iff_le_one_left hx] using h _

Premises used: mul_le_iff_le_one_left
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
h : ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1
x : R
m : ℕ
⊢ ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖

Tactic:
replace h (x : R) (n : ℕ) : ‖n • x‖ ≤ ‖x‖ := by
    rw [nsmul_eq_mul, norm_mul]
    rcases (norm_nonneg x).eq_or_lt with hx | hx
    · simp only [← hx, mul_zero, le_refl]
    · simpa only [mul_le_iff_le_one_left hx] using h _
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
transitivity : ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
transitivity₁ : ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • max 1 (‖x‖ ^ m)
⊢ ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)

Tactic:
transitivity ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

Premises used: Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

Tactic:
simpa only [← norm_pow, (Commute.one_right x).add_pow, one_pow, mul_one, nsmul_eq_mul,
      Nat.cast_comm] using (norm_sum_le _ _).trans (Finset.sum_le_sum fun _ _ ↦ h _ _)

Premises used: Nat.cast_comm, one_pow, norm_pow, Commute.add_pow, nsmul_eq_mul, Finset.sum_le_sum, LE.le.trans, mul_one, Commute.one_right, norm_sum_le
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
rw : LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • max 1 (‖x‖ ^ m)

Tactic:
rw [← Finset.card_range (m + 1), ← Finset.sum_const, Finset.card_range]

Premises used: Finset.card_range, HAdd.hAdd, OfNat.ofNat, Finset.sum_const
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
inl :
  ∀ (hm : max 1 (‖x‖ ^ m) = 1) (hx : ‖x‖ ^ m ≤ 1),
    LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
inr :
  ∀ (hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m) (hx : 1 < ‖x‖ ^ m),
    LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))

Tactic:
rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩ | ⟨hm, hx⟩)

Premises used: Norm.norm, HPow.hPow, max_cases, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
inl : LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), 1)
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))

Tactic:
rw [hm]
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
inr : LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m)
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), max 1 (‖x‖ ^ m))

Tactic:
rw [hm]
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
inl : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), ‖x‖ ^ i ≤ 1
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), 1)

Tactic:
gcongr with i hi
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
inr : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), 1 ≤ ‖x‖
inr₁ : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), i ≤ m
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m)

Tactic:
gcongr with i hi
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
inl :
  ∀ (hm : max 1 (HPow.hPow (β := ℕ) ‖x‖ 0) = 1) (hx : HPow.hPow (β := ℕ) ‖x‖ 0 ≤ 1)
    (hi : i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1)), ‖x‖ ^ i ≤ 1
inl₁ : ∀ (hm : m ≠ 0), ‖x‖ ^ i ≤ 1
⊢ ‖x‖ ^ i ≤ 1

Tactic:
rcases eq_or_ne m 0 with rfl | hm

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : max 1 (HPow.hPow (β := ℕ) ‖x‖ 0) = 1
hx : HPow.hPow (β := ℕ) ‖x‖ 0 ≤ 1
hi : i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1)
⊢ i = 0

Tactic:
simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi

Premises used: Finset.mem_singleton, zero_add, Finset.range_one
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : max 1 (HPow.hPow (β := ℕ) ‖x‖ 0) = 1
hx : HPow.hPow (β := ℕ) ‖x‖ 0 ≤ 1
hi : i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1)
⊢ ‖x‖ ^ i ≤ 1

Tactic:
simp only [pow_zero, le_refl,
        show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]

Premises used: le_refl, pow_zero
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm_1 : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
inl : ∀ (hx : ‖x‖ ≤ 1) (i : ℕ) (hi : i ∈ Finset.range (m + 1)) (hm : m ≠ 0), ‖x‖ ^ i ≤ 1
⊢ ‖x‖ ^ i ≤ 1

Tactic:
rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx

Premises used: pow_le_one_iff_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm_1 : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
pow_le_one₀ (norm_nonneg _) hx

Premises used: norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm_1 : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx

Premises used: norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
inr : ∀ (hx : ‖x‖ < 1), ‖x‖ ^ m ≤ 1
⊢ 1 ≤ ‖x‖

Tactic:
contrapose! hx
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
hx : ‖x‖ < 1
⊢ ‖x‖ ^ m ≤ 1

Tactic:
pow_le_one₀ (norm_nonneg _) hx.le

Premises used: LT.lt.le, norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
hx : ‖x‖ < 1
⊢ ‖x‖ ^ m ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx.le

Premises used: LT.lt.le, norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
simpa [Nat.lt_succ_iff] using hi

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Analysis.Normed.Field.Ultra
Goal:
R : Type u_1
inst : NormedDivisionRing R
⊢ IsUltrametricDist R ↔ ∀ (n : ℕ), norm.{u_1} (E := R) (↑n : R) ≤ 1

Tactic:
⟨fun _ => IsUltrametricDist.norm_natCast_le_one R,
      IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one⟩

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one, Iff.intro, IsUltrametricDist.norm_natCast_le_one
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : Membership.mem (γ := Set 𝕜) (ball 0 1) a
hy : Membership.mem (γ := Set 𝕜) (ball 0 1) b
rw : ∀ (hx : ‖a‖ < 1) (hy : ‖b‖ < 1), ‖a * b‖ < 1
⊢ Membership.mem (γ := Set 𝕜) (ball 0 1) (a * b)

Tactic:
rw [mem_ball_zero_iff] at *

Premises used: mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : ‖a‖ < 1
hy : ‖b‖ < 1
⊢ ‖a * b‖ < 1

Tactic:
(norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)

Premises used: mul_lt_one_of_nonneg_of_lt_one_left, LT.lt.le, norm_mul_le, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : ‖a‖ < 1
hy : ‖b‖ < 1
⊢ ‖a * b‖ < 1

Tactic:
exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)

Premises used: mul_lt_one_of_nonneg_of_lt_one_left, LT.lt.le, norm_mul_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
x : 𝕜
⊢ Membership.mem (γ := Subsemigroup 𝕜) (unitBall 𝕜) x ↔ ‖x‖ < 1

Tactic:
simp [Subsemigroup.unitBall]

Premises used: Subsemigroup.unitBall
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NonUnitalSeminormedRing 𝕜
⊢ ContinuousMul.{u_1} (↑(ball 0 1) : Type u_1)

Tactic:
(Subsemigroup.unitBall 𝕜).continuousMul

Premises used: Set.Mem, setOf, Metric.ball, Subsemigroup.continuousMul, Subsemigroup.unitBall
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NonUnitalSeminormedRing 𝕜
x y : (↑(ball 0 1) : Type u_1)
⊢ (↑(x * y) : 𝕜) = (↑x : 𝕜) * (↑y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : Zero 𝕜
inst_1 : PseudoMetricSpace 𝕜
⊢ Membership.mem (γ := Set 𝕜) (ball 0 1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : Zero 𝕜
inst_1 : PseudoMetricSpace 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑0 : 𝕜) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : Zero 𝕜
inst_1 : PseudoMetricSpace 𝕜
a : (↑(ball 0 1) : Type u_1)
⊢ (↑a : 𝕜) = 0 ↔ a = 0

Tactic:
Subtype.val_injective.eq_iff' unitBall.coe_zero

Premises used: Subtype.val_injective, Function.Injective.eq_iff', Metric.unitBall.coe_zero
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NonUnitalSeminormedRing 𝕜
inst_1 : IsLeftCancelMulZero 𝕜
⊢ IsLeftCancelMulZero.{u_1} (↑(ball 0 1) : Type u_1)

Tactic:
Subtype.val_injective.isLeftCancelMulZero _ rfl fun _ _ ↦ rfl

Premises used: Subtype.val_injective, Function.Injective.isLeftCancelMulZero, rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NonUnitalSeminormedRing 𝕜
inst_1 : IsRightCancelMulZero 𝕜
⊢ IsRightCancelMulZero.{u_1} (↑(ball 0 1) : Type u_1)

Tactic:
Subtype.val_injective.isRightCancelMulZero _ rfl fun _ _ ↦ rfl

Premises used: Subtype.val_injective, Function.Injective.isRightCancelMulZero, rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : Membership.mem (γ := Set 𝕜) (closedBall 0 1) a
hy : Membership.mem (γ := Set 𝕜) (closedBall 0 1) b
rw : ∀ (hx : ‖a‖ ≤ 1) (hy : ‖b‖ ≤ 1), ‖a * b‖ ≤ 1
⊢ Membership.mem (γ := Set 𝕜) (closedBall 0 1) (a * b)

Tactic:
rw [mem_closedBall_zero_iff] at *

Premises used: mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : ‖a‖ ≤ 1
hy : ‖b‖ ≤ 1
⊢ ‖a * b‖ ≤ 1

Tactic:
(norm_mul_le _ _).trans (mul_le_one₀ hx (norm_nonneg _) hy)

Premises used: mul_le_one₀, LE.le.trans, norm_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : ‖a‖ ≤ 1
hy : ‖b‖ ≤ 1
⊢ ‖a * b‖ ≤ 1

Tactic:
exact (norm_mul_le _ _).trans (mul_le_one₀ hx (norm_nonneg _) hy)

Premises used: mul_le_one₀, LE.le.trans, norm_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NonUnitalSeminormedRing 𝕜
⊢ ContinuousMul.{u_1} (↑(closedBall 0 1) : Type u_1)

Tactic:
(Subsemigroup.unitClosedBall 𝕜).continuousMul

Premises used: Set.Mem, setOf, Subsemigroup.continuousMul, Metric.closedBall, Subsemigroup.unitClosedBall
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NonUnitalSeminormedRing 𝕜
x y : (↑(closedBall 0 1) : Type u_1)
⊢ (↑(x * y) : 𝕜) = (↑x : 𝕜) * (↑y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : Zero 𝕜
inst_1 : PseudoMetricSpace 𝕜
⊢ Membership.mem (γ := Set 𝕜) (closedBall 0 1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : Zero 𝕜
inst_1 : PseudoMetricSpace 𝕜
a : (↑(closedBall 0 1) : Type u_1)
⊢ (↑a : 𝕜) = 0 ↔ a = 0

Tactic:
Subtype.val_injective.eq_iff' unitClosedBall.coe_zero

Premises used: Subtype.val_injective, Function.Injective.eq_iff', Metric.unitClosedBall.coe_zero
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormOneClass 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑1 : 𝕜) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormOneClass 𝕜
a : (↑(closedBall 0 1) : Type u_1)
⊢ (↑a : 𝕜) = 1 ↔ a = 1

Tactic:
Subtype.val_injective.eq_iff' unitClosedBall.coe_one

Premises used: Subtype.val_injective, Function.Injective.eq_iff', Metric.unitClosedBall.coe_one
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormOneClass 𝕜
x : (↑(closedBall 0 1) : Type u_1)
n : ℕ
⊢ (↑(x ^ n) : 𝕜) = (↑x : 𝕜) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : IsCancelMulZero 𝕜
inst_2 : NormOneClass 𝕜
⊢ IsCancelMulZero.{u_1} (↑(closedBall 0 1) : Type u_1)

Tactic:
Subtype.val_injective.isCancelMulZero _ rfl fun _ _ ↦ rfl

Premises used: Function.Injective.isCancelMulZero, Subtype.val_injective, rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
a b : 𝕜
hx : Membership.mem (γ := Set 𝕜) (sphere 0 1) a
hy : Membership.mem (γ := Set 𝕜) (sphere 0 1) b
rw : ∀ (hx : ‖a‖ = 1) (hy : ‖b‖ = 1), ‖a * b‖ = 1
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) (a * b)

Tactic:
rw [mem_sphere_zero_iff_norm] at *

Premises used: mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
a b : 𝕜
hx : ‖a‖ = 1
hy : ‖b‖ = 1
⊢ ‖a * b‖ = 1

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖⁻¹ = 1
rw₁ : Eq (α := ℝ) 1⁻¹ 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ ‖(↑x : 𝕜)⁻¹‖ = 1

Tactic:
rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]

Premises used: Subtype.coe_prop, inv_one, mem_sphere_zero_iff_norm, norm_inv, Iff.mp
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
⊢ (↑x⁻¹ : 𝕜) = (↑x : 𝕜)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖ / ‖(↑y : 𝕜)‖ = 1
rw₁ : 1 / ‖(↑y : 𝕜)‖ = 1
rw₂ : 1 / 1 = 1
rw₃ rw₄ : Eq (α := ℝ) 1 1
⊢ ‖(↑x : 𝕜) / (↑y : 𝕜)‖ = 1

Tactic:
rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]

Premises used: Subtype.coe_prop, mem_sphere_zero_iff_norm, norm_div, Iff.mp, div_one, Subtype.property
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
⊢ (↑(x / y) : 𝕜) = (↑x : 𝕜) / (↑y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℤ
rw : ‖(↑x : 𝕜) ^ n‖ = 1
rw₁ : ‖(↑x : 𝕜)‖ ^ n = 1
rw₂ : HPow.hPow (α := ℝ) 1 n = 1
rw₃ rw₄ : Eq (α := ℝ) 1 1
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) ((↑x : 𝕜) ^ n)

Tactic:
rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]

Premises used: Subtype.coe_prop, one_zpow, mem_sphere_zero_iff_norm, Iff.mp, norm_zpow
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℤ
⊢ (↑(x ^ n) : 𝕜) = (↑x : 𝕜) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑1 : 𝕜) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
x y : (↑(sphere 0 1) : Type u_1)
⊢ (↑(x * y) : 𝕜) = (↑x : 𝕜) * (↑y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℕ
⊢ (↑(x ^ n) : 𝕜) = (↑x : 𝕜) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
⊢ (↑((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) x) : 𝕜) = (↑x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
h :
  Eq (α := 𝕜ˣ) ((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) x : 𝕜ˣ)
    ((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) y : 𝕜ˣ)
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) x) : 𝕜)
    (↑((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) y) : 𝕜)

Tactic:
congr_arg Units.val h

Premises used: Units.val, congr_arg
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
h :
  Eq (α := 𝕜ˣ) ((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) x : 𝕜ˣ)
    ((unitSphereToUnits 𝕜 : (a : (↑(sphere 0 1) : Type u_1)) → 𝕜ˣ) y : 𝕜ˣ)
⊢ (↑x : 𝕜) = (↑y : 𝕜)

Tactic:
convert! congr_arg Units.val h

Premises used: Units.val, congr_arg
-- Module: Mathlib.Analysis.Normed.Field.UnitBall
Goal:
𝕜 : Type u_1
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
⊢ ContinuousMul.{u_1} (↑(sphere 0 1) : Type u_1)

Tactic:
(Submonoid.unitSphere 𝕜).continuousMul

Premises used: Set.Mem, setOf, Submonoid.continuousMul, Submonoid.unitSphere, Metric.sphere
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
T : Type u_3
inst_3 : Field T
v : AbsoluteValue R S
inst_4 : Module R T
inst_5 : FiniteDimensional R T
⊢ FiniteDimensional.{u_1, u_3} (WithAbs v) T

Tactic:
Module.Finite.of_restrictScalars_finite R (WithAbs v) T

Premises used: WithAbs, Module.Finite.of_restrictScalars_finite
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
T : Type u_3
inst_3 : Field T
v : AbsoluteValue R S
inst_4 : Module T R
inst_5 : FiniteDimensional T R
⊢ FiniteDimensional.{u_3, u_1} T (WithAbs v)

Tactic:
Module.Finite.equiv (linearEquiv T v).symm

Premises used: LinearEquiv.symm, WithAbs.linearEquiv, Module.Finite.equiv
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
T : Type u_3
inst_3 : Field T
v : AbsoluteValue R S
inst_4 : Algebra R T
inst_5 : Algebra.IsSeparable R T
a :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := T)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (WithAbs v) T)
              (↑(equiv v).symm : R →+* WithAbs v) :
            (a : R) → T)
          x :
        T)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.refl T) : T →+* T) (algebraMap R T) :
            (a : R) → T)
          x :
        T)
⊢ Eq (α := R →+* T)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (WithAbs v) T) (↑(equiv v).symm : R →+* WithAbs v))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.refl T) : T →+* T) (algebraMap R T))

Tactic:
ext