awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
hz : x i - 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i - 3 / 4 * δ) ≤ δ / 4
linarith : y i ≤ z i → 4 / 4 = 1
linarith₁ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : y i ≤ z i → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : y i ≤ z i → 4 / 4 = 1
linarith₄ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₅ : y i ≤ z i → GT.gt (α := ℝ) 4 0
linarith₆ : y i ≤ z i → 4 / 4 = 1
linarith₇ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : y i ≤ z i → HMul.hMul (α := ℝ) 4 1 = 4
linarith₉ : y i ≤ z i → 4 / 4 = 1
linarith₁₀ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₁ : y i ≤ z i → GT.gt (α := ℝ) 4 0
linarith₁₂ : y i ≤ z i → 4 / 4 = 1
linarith₁₃ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₄ : y i ≤ z i → GT.gt (α := ℝ) 4 0
linarith₁₅ : y i ≤ z i → 4 / 4 = 1
linarith₁₆ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₇ : y i ≤ z i → GT.gt (α := ℝ) 4 0
⊢ z i < y i
have linarith₁₈ : y i ≤ z i →
  0 - δ + (4 * x i - 4 * y i - 1 * δ) + (4 * z i - (4 * x i - HMul.hMul (α := ℝ) 1 3 * (1 * δ)) - 1 * δ) +
      4 * (y i - z i) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
⊢ IsClosed (↑(upperClosure s) : Set (ι → ℝ))
have intro : ∀ (val : Fintype ι), IsClosed (↑(upperClosure s) : Set (ι → ℝ))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
⊢ IsClosed (↑(upperClosure s) : Set (ι → ℝ))
have intro : ∀ (f : ℕ → ι → ℝ) (x : ι → ℝ) (hf : ∀ (n : ℕ), f n ∈ (↑(upperClosure s) : Set (ι → ℝ)))
  (hx : Filter.Tendsto f Filter.atTop (nhds x)), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
Tactic: refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ (↑(upperClosure s) : Set (ι → ℝ))
hx : Filter.Tendsto f Filter.atTop (nhds x)
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))
have intro : ∀ (g : (n : ℕ) → ι → ℝ) (hg : ∀ (n : ℕ), g n ∈ s) (hgf : ∀ (n : ℕ), g n ≤ f n), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
Tactic: choose g hg hgf using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))
have intro : ∀ (a : ι → ℝ) (ha : a ∈ upperBounds (range f)), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
Tactic: obtain ⟨a, ha⟩ := hx.bddAbove_range
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))
have intro : ∀ (b : ι → ℝ) (hb : b ∈ closure (s ∩ Iic a)) (φ : ℕ → ℕ) (hφ : StrictMono φ)
  (hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
Tactic: obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddAbove_Iic) fun n ↦
    ⟨hg n, (hgf _).trans <| ha <| mem_range_self _⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
⊢ IsClosed (↑(lowerClosure s) : Set (ι → ℝ))
have intro : ∀ (val : Fintype ι), IsClosed (↑(lowerClosure s) : Set (ι → ℝ))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
⊢ IsClosed (↑(lowerClosure s) : Set (ι → ℝ))
have intro : ∀ (f : ℕ → ι → ℝ) (x : ι → ℝ) (hf : ∀ (n : ℕ), f n ∈ (↑(lowerClosure s) : Set (ι → ℝ)))
  (hx : Filter.Tendsto f Filter.atTop (nhds x)), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
Tactic: refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ (↑(lowerClosure s) : Set (ι → ℝ))
hx : Filter.Tendsto f Filter.atTop (nhds x)
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
have intro : ∀ (g : (n : ℕ) → ι → ℝ) (hg : ∀ (n : ℕ), g n ∈ s) (hfg : ∀ (n : ℕ), f n ≤ g n), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
Tactic: choose g hg hfg using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
have this : BoundedGENhdsClass ℝ
Tactic: haveI : BoundedGENhdsClass ℝ := by infer_instance
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
have intro : ∀ (a : ι → ℝ) (ha : a ∈ lowerBounds (range f)), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
Tactic: obtain ⟨a, ha⟩ := hx.bddBelow_range
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
a : ι → ℝ
ha : a ∈ lowerBounds (range f)
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
have intro : ∀ (b : ι → ℝ) (hb : b ∈ closure (s ∩ Ici a)) (φ : ℕ → ℕ) (hφ : StrictMono φ)
  (hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
Tactic: obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddBelow_Ici) fun n ↦
    ⟨hg n, (ha <| mem_range_self _).trans <| hfg _⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
x y : α
⊢ norm (E := α) ((AddMonoidHom.mulRight x : (a : α) → α) y : α) ≤ ‖x‖ * ‖y‖
have rw : norm (E := α) ((AddMonoidHom.mulRight x : (a : α) → α) y : α) ≤ ‖y‖ * ‖x‖
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
⊢ max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖) ≤ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖
have ha : 0 ≤ ‖x.1‖
Tactic: apply max_mul_mul_le_max_mul_max
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
ha : 0 ≤ ‖x.1‖
⊢ max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖) ≤ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖
have hd : 0 ≤ ‖y.2‖
Tactic: apply max_mul_mul_le_max_mul_max
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
n : ℕ
⊢ norm.{u_2} (E := α) (↑(n + 1) : α) ≤ (↑(n + 1) : ℝ) * norm.{u_2} (E := α) 1
have rw : ‖HAdd.hAdd (α := α) (↑n : α) 1‖ ≤ (↑n : ℝ) * norm.{u_2} (E := α) 1 + norm.{u_2} (E := α) 1
Tactic: rw [n.cast_succ, n.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ ‖(a :: b :: l).prod‖ ≤ (map norm (a :: b :: l)).prod
have rw : ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod
Tactic: rw [List.map_cons, List.prod_cons, List.prod_cons (a := ‖a‖)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod
have refine : ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod
Tactic: refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ norm.{u_5} (E := α) (∏ i ∈ s, f i) ≤ ∏ i ∈ s, ‖f i‖
have mk : ∀ (val : Multiset ι) (l : List ι) (hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))
  (hs : { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }.Nonempty),
  norm.{u_5} (E := α)
      (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖
Tactic: rcases s with ⟨⟨l⟩, hl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (hypothesis)
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
f : ι → α
val : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }.Nonempty
⊢ norm.{u_5} (E := α)
      (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖
have this : List.map f l ≠ []
Tactic: have : l.map f ≠ [] := by simpa using hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
inst_1 : NormOneClass α
s : Finset ι
f : ι → α
⊢ norm.{u_5} (E := α) (∏ i ∈ s, f i) ≤ ∏ i ∈ s, ‖f i‖
have mk : ∀ (val : Multiset ι) (l : List ι) (hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)),
  norm.{u_5} (E := α)
      (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖
Tactic: rcases s with ⟨⟨l⟩, hl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inl : ∀ (hz : z = (↑z.natAbs : ℤ)), norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rcases z.natAbs_eq with hz | hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
inl : ∀ (hz : z = (↑z.natAbs : ℤ)), norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inr : ∀ (hz : z = -(↑z.natAbs : ℤ)), norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rcases z.natAbs_eq with hz | hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = (↑z.natAbs : ℤ)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inl : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rw [← Int.cast_natCast, ← hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = (↑z.natAbs : ℤ)
inl : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inl₁ : norm.{u_2} (E := α) (↑z : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rw [← Int.cast_natCast, ← hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = -(↑z.natAbs : ℤ)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inr : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = -(↑z.natAbs : ℤ)
inr : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inr₁ : norm.{u_2} (E := α) (-(↑(↑z.natAbs : ℤ) : α)) = norm.{u_2} (E := α) (↑z : α)
Tactic: rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = -(↑z.natAbs : ℤ)
inr : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
inr₁ : norm.{u_2} (E := α) (-(↑(↑z.natAbs : ℤ) : α)) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inr₂ : norm.{u_2} (E := α) (↑(-(↑z.natAbs : ℤ)) : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = -(↑z.natAbs : ℤ)
inr : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
inr₁ : norm.{u_2} (E := α) (-(↑(↑z.natAbs : ℤ) : α)) = norm.{u_2} (E := α) (↑z : α)
inr₂ : norm.{u_2} (E := α) (↑(-(↑z.natAbs : ℤ)) : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
have inr₃ : norm.{u_2} (E := α) (↑z : α) = norm.{u_2} (E := α) (↑z : α)
Tactic: rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a * (1 - b)‖ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖
have bc : ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a‖ * ‖1 - b‖ ≤ ‖c - a‖ + 1 * ‖1 - b‖
have bc : 0 ≤ ‖1 - b‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖
have rw : ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖(↑a : α) * (↑b : α) - (↑b : α) * (↑a : α)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ =
    ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖
have simp_rw : ‖(↑a : α) * (↑b : α) - (↑b : α) * (↑a : α)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ =
  ‖(↑a : α) * (↑b : α) - (↑a : α) - ((↑b : α) - 1) - ((↑b : α) * (↑a : α) - (↑b : α) - ((↑a : α) - 1))‖ * ‖(↑a⁻¹ : α)‖ *
    ‖(↑b⁻¹ : α)‖
Tactic: simp_rw [sub_one_mul, mul_sub_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ ≤
    (‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖
have hbc : ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤
  ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ (‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ ≤
    (‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖ + ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖
have hbc : ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ ≤ ‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
hbc : ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ ≤ ‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖
⊢ (‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ ≤
    (‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖ + ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖
have hbc₁ : ‖((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤ ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
x : ℝ≥0
⊢ ‖(↑x : ℝ)‖ = (↑x : ℝ)
have rw : |(↑x : ℝ)| = (↑x : ℝ)
Tactic: rw [Real.norm_eq_abs, x.abs_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
x : ℝ≥0
rw : |(↑x : ℝ)| = (↑x : ℝ)
⊢ ‖(↑x : ℝ)‖ = (↑x : ℝ)
have rw₁ : (↑x : ℝ) = (↑x : ℝ)
Tactic: rw [Real.norm_eq_abs, x.abs_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
x : ℝ≥0
⊢ ‖(↑x : ℝ)‖₊ = x
have a : (↑‖(↑x : ℝ)‖₊ : ℝ) = (↑x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_2
inst : NormedAddCommGroup α
inst_1 : MulOneClass α
inst_2 : NormMulClass α
inst_3 : Nontrivial α
⊢ norm.{u_2} (E := α) 1 = 1
have obtain : ∀ (u : α) (hu : u ≠ 0), norm.{u_2} (E := α) 1 = 1
Tactic: obtain ⟨u, hu⟩ := exists_ne (0 : α)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
have rw : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
Tactic: rw [add_comm (-x), add_comm (-y), ← sub_eq_add_neg, v.map_sub, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
rw : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
have rw₁ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
Tactic: rw [add_comm (-x), add_comm (-y), ← sub_eq_add_neg, v.map_sub, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
rw : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
rw₁ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
have rw₂ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y - x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
Tactic: rw [add_comm (-x), add_comm (-y), ← sub_eq_add_neg, v.map_sub, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
rw : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
rw₁ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
rw₂ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y - x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
have rw₃ : Eq (α := ℝ) ((v : (a : R) → ℝ) (x - y) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
Tactic: rw [add_comm (-x), add_comm (-y), ← sub_eq_add_neg, v.map_sub, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
rw : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
rw₁ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
rw₂ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y - x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
rw₃ : Eq (α := ℝ) ((v : (a : R) → ℝ) (x - y) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
have rw₄ : Eq (α := ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
Tactic: rw [add_comm (-x), add_comm (-y), ← sub_eq_add_neg, v.map_sub, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (hypothesis)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) (0 : ℝ)
⊢ x = y
have hxy₁ : y = x
Tactic: rw [add_comm, ← sub_eq_add_neg, AbsoluteValue.map_sub_eq_zero_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inl : IsEmpty ι →
  ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
Tactic: rcases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
inl :
  IsEmpty ι →
    ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inr : Nonempty ι →
  ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
Tactic: rcases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inr : IsEmpty ι' →
  ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
inr :
  IsEmpty ι' →
    ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inr₁ : Nonempty ι' →
  ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
Tactic: rcases isEmpty_or_nonempty ι'