awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
have case : (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
  (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
Tactic: classical
  constructor
  case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
  rcases eq_or_lt_of_le hs with rfl | hs
  case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)
  rintro ⟨hM₁, hM₂, hM₃⟩
  exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
case :
  (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
have mpr : ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
  ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
Tactic: classical
  constructor
  case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
  rcases eq_or_lt_of_le hs with rfl | hs
  case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)
  rintro ⟨hM₁, hM₂, hM₃⟩
  exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
case :
  (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
mpr mpr₁ :
  ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
have case₁ : ∀ (hs : LE.le.{u_1} (α := R) 0 0),
  ((∀ (i j : n), 0 ≤ M i j) ∧
      (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
    ∃ (M' : Matrix n n R),
      Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
Tactic: classical
  constructor
  case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
  rcases eq_or_lt_of_le hs with rfl | hs
  case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)
  rintro ⟨hM₁, hM₂, hM₃⟩
  exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
case :
  (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
mpr mpr₁ :
  ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
case₁ :
  ∀ (hs : LE.le.{u_1} (α := R) 0 0),
    ((∀ (i j : n), 0 ≤ M i j) ∧
        (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
      ∃ (M' : Matrix n n R),
        Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
have mpr₂ : ∀ (hs : 0 < s),
  ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
Tactic: classical
  constructor
  case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
  rcases eq_or_lt_of_le hs with rfl | hs
  case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)
  rintro ⟨hM₁, hM₂, hM₃⟩
  exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.DoublyStochasticMatrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
case :
  (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
mpr mpr₁ :
  ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
case₁ :
  ∀ (hs : LE.le.{u_1} (α := R) 0 0),
    ((∀ (i j : n), 0 ≤ M i j) ∧
        (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 0) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 0) →
      ∃ (M' : Matrix n n R),
        Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
mpr₂ mpr₃ :
  ∀ (hs : 0 < s),
    ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
      ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
⊢ (∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M') ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
have mpr₄ : ∀ (hs : 0 < s) (hM₁ : ∀ (i j : n), 0 ≤ M i j) (hM₂ : ∀ (i : n), ∑ j : n, M i j = s)
  (hM₃ : ∀ (j : n), ∑ i : n, M i j = s),
  ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
Tactic: classical
  constructor
  case mp =>
    rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
  rcases eq_or_lt_of_le hs with rfl | hs
  case inl =>
    simp only [zero_smul, exists_and_right, and_imp]
    intro h₁ h₂ _
    refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
    ext i j
    specialize h₂ i
    rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
    exact h₂ _ (by simp)
  rintro ⟨hM₁, hM₂, hM₃⟩
  exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ (↑‖c‖₊⁻¹ : ℝ≥0∞)
have rw : egauge 𝕜 s x ≤ (↑‖c⁻¹‖₊ : ℝ≥0∞)
Tactic: rw [← nnnorm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹
have inl : ∀ (h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x ∈ s), egauge 𝕜 s x ≤ (enorm.{u_1} (E := 𝕜) 0)⁻¹
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
inl : ∀ (h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x ∈ s), egauge 𝕜 s x ≤ (enorm.{u_1} (E := 𝕜) 0)⁻¹
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹
have inr : ∀ (hc : c ≠ 0), egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
⊢ egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s
have refine : (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s
Tactic: refine (iInf₂_eq_bot _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
⊢ (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s
have rw : (∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : 𝕜) (_ : x ∈ i • s), ‖i‖ₑ < b) ↔
  ∀ (i : ℝ≥0∞),
    0 < i →
      ∃ (x_1 : 𝕜),
        Membership.mem (γ := Set 𝕜) {y : 𝕜 | Membership.mem (γ := SetRel 𝕜 𝕜) {p : 𝕜 × 𝕜 | edist p.1 p.2 < i} (y, 0)}
            x_1 ∧
          x ∈ x_1 • s
Tactic: rw [(nhds_basis_uniformity uniformity_basis_edist).frequently_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ egauge 𝕜 univ x = 0
have rw : ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c univ
Tactic: rw [egauge_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c univ
have refine : ∀ (c : 𝕜) (hc : c ∉ {0}), x ∈ HSMul.hSMul (β := Set E) c univ
Tactic: refine (frequently_iff_neBot.2 ‹_›).mono fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : s.Nonempty
⊢ egauge 𝕜 s 0 = 0
have this : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
Tactic: have : 0 ∈ (0 : 𝕜) • s := by simp [zero_smul_set hs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
h : x ∈ s
⊢ egauge 𝕜 s x ≤ 1
have h₁ : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s
Tactic: rw [← one_smul 𝕜 s] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
⊢ r ≤ egauge 𝕜 s x
have rw : ∀ (c : 𝕜), x ∈ c • s → r ≤ ‖c‖ₑ
Tactic: rw [le_egauge_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
⊢ r ≤ ‖c‖ₑ
have inl : ∀ (hc₀ : c ≠ 0), r ≤ ‖c‖ₑ
Tactic: rcases ne_or_eq c 0 with hc₀ | rfl
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
inl : ∀ (hc₀ : c ≠ 0), r ≤ ‖c‖ₑ
⊢ r ≤ ‖c‖ₑ
have inr : ∀ (hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s), r ≤ enorm.{u_1} (E := 𝕜) 0
Tactic: rcases ne_or_eq c 0 with hc₀ | rfl
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
⊢ r ≤ enorm.{u_1} (E := 𝕜) 0
have h₁ : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
Tactic: obtain rfl : x = 0 := by
    grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc
Cleared hypotheses: x, h, hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
h₁ : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
⊢ r ≤ enorm.{u_1} (E := 𝕜) 0
have hc₁ : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
Tactic: obtain rfl : x = 0 := by
    grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc
Cleared hypotheses: x, h, hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
⊢ r ≤ enorm.{u_1} (E := 𝕜) 0
have inr : ∀ (c : ℝ≥0∞), enorm.{u_1} (E := 𝕜) 0 < c → r < c
Tactic: apply le_of_forall_gt
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s
b : ℝ≥0∞
hb : enorm.{u_1} (E := 𝕜) 0 < b
⊢ r < b
have inr : ∀ (c : 𝕜) (hc₀ : Membership.mem (γ := Set 𝕜) {0}ᶜ c) (hcb : Membership.mem (γ := Set 𝕜) (eball 0 b) c), r < b
Tactic: rcases Filter.nonempty_of_mem <|
    inter_mem_nhdsWithin {(0 : 𝕜)}ᶜ (Metric.eball_mem_nhds 0 (by simpa using hb))
    with ⟨c, hc₀, hcb⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x
have simp_rw : ∀ (c_1 : 𝕜), x ∈ (c_1 * c) • s → egauge 𝕜 s x / ‖c‖ₑ ≤ ‖c_1‖ₑ
Tactic: simp_rw [le_egauge_iff, smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) / ‖c‖ₑ ≤ ‖a‖ₑ
have h : egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a‖ₑ * ‖c‖ₑ
Tactic: apply ENNReal.div_le_of_le_mul
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a‖ₑ * ‖c‖ₑ
have h : egauge 𝕜 s ((fun (x : E) ↦ (a * c) • x) x) ≤ ‖a * c‖ₑ
Tactic: rw [← enorm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ
have refine : egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ
Tactic: refine le_antisymm ?_ (le_egauge_smul_left _ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ
have rw : egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x
Tactic: rw [ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ
have rw : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c‖ₑ⁻¹
Tactic: rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
rw : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c‖ₑ⁻¹
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ
have rw₁ : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x * ‖c‖ₑ⁻¹⁻¹
Tactic: rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
rw : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c‖ₑ⁻¹
rw₁ : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x * ‖c‖ₑ⁻¹⁻¹
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ
have rw₂ : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x * ‖c‖ₑ
Tactic: rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c⁻¹ • c • s) x = egauge 𝕜 s x
have rw : egauge 𝕜 s x = egauge 𝕜 s x
Tactic: rw [inv_smul_smul₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x
have egauge : egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ
Tactic: calc
    egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
      rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
    _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
    _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
egauge : _root_.egauge 𝕜 (c • s) x * ‖c‖ₑ = _root_.egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ
⊢ _root_.egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ _root_.egauge 𝕜 s x
have egauge₁ : _root_.egauge 𝕜 (c⁻¹ • c • s) x = _root_.egauge 𝕜 s x
Tactic: calc
    egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
      rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
    _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
    _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)
have rw : ∀ (c_1 : 𝕜), c • x ∈ c_1 • s → ‖c‖ₑ * egauge 𝕜 s x ≤ ‖c_1‖ₑ
Tactic: rw [le_egauge_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
have inl : ∀ (hxy : (fun (x : E) ↦ a • x) y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x),
  enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x ≤ ‖a‖ₑ
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
inl :
  ∀ (hxy : (fun (x : E) ↦ a • x) y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x),
    enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x ≤ ‖a‖ₑ
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
have inr : ∀ (hc : c ≠ 0), ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
have inr : egauge 𝕜 s x ≤ (↑(‖a‖₊ / ‖c‖₊) : ℝ≥0∞)
Tactic: refine ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ (↑(‖a‖₊ / ‖c‖₊) : ℝ≥0∞)
have inr : egauge 𝕜 s x ≤ (↑‖c⁻¹ * a‖₊ : ℝ≥0∞)
Tactic: rw [div_eq_inv_mul, ← nnnorm_inv, ← nnnorm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun (x : E) ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ (↑‖c⁻¹ * a‖₊ : ℝ≥0∞)
have inr : (fun (x : E) ↦ (c⁻¹ * a) • x) y = x
Tactic: refine egauge_le_of_mem_smul ⟨y, hy, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
⊢ egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x
have refine : egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
Tactic: refine le_antisymm ?_ (le_egauge_smul_right c s x)
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
⊢ egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
have inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) 0 0 → s.Nonempty),
  egauge 𝕜 s (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) ≤ enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c, h