awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
⊢ x₁ i j = x₂ i j
have h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
Tactic: have h₁ : σ.permMatrix R i j ∈ openSegment R (x₁ i j) (x₂ i j) :=
    image_openSegment _ (entryLinearMap R R i j).toAffineMap x₁ x₂ ▸ ⟨_, hσ, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
⊢ x₁ i j = x₂ i j
have refine_2 : ∀ (h : x₁ i j ≠ x₂ i j), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1
have rw : Set.Ioo (min (x₁ i j) (x₂ i j)) (max (x₁ i j) (x₂ i j)) ⊆ Set.Ioo 0 1
Tactic: rw [openSegment_eq_Ioo' h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ Set.Ioo (min (x₁ i j) (x₂ i j)) (max (x₁ i j) (x₂ i j)) ⊆ Set.Ioo 0 1
have ha : 0 ≤ min (x₁ i j) (x₂ i j)
Tactic: apply Set.Ioo_subset_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
ha : 0 ≤ min (x₁ i j) (x₂ i j)
⊢ Set.Ioo (min (x₁ i j) (x₂ i j)) (max (x₁ i j) (x₂ i j)) ⊆ Set.Ioo 0 1
have hb : max (x₁ i j) (x₂ i j) ≤ 1
Tactic: apply Set.Ioo_subset_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ False
have h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1
Tactic: have h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1 := by
    rw [openSegment_eq_Ioo' h]
    apply Set.Ioo_subset_Ioo <;>
    simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1
⊢ False
have h₃ : Membership.mem (γ := Set R) (Set.Ioo 0 1) (Equiv.Perm.permMatrix R σ i j)
Tactic: specialize h₂ h₁
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : Membership.mem (γ := Submonoid (Matrix n n ℝ)) (doublyStochastic ℝ n) M
⊢ ‖M‖ ≤ 1
have hM₁ : Membership.mem (γ := Set (Matrix n n ℝ))
  ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
      {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
    Set (Matrix n n ℝ))
  M
Tactic: rw [← SetLike.mem_coe, doublyStochastic_eq_convexHull_permMatrix] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM :
  Membership.mem (γ := Set (Matrix n n ℝ))
    ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
        {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
      Set (Matrix n n ℝ))
    M
⊢ ‖M‖ ≤ 1
have have : ∀ (σ : Equiv.Perm n) (hσ : ‖M‖ ≤ ‖Equiv.Perm.permMatrix ℝ σ‖), ‖M‖ ≤ 1
Tactic: have ⟨_, ⟨σ, rfl⟩, hσ⟩ := convexOn_univ_norm.exists_ge_of_mem_convexHull (by simp) hM
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K L : ConvexBody V
h : K.carrier = L.carrier
⊢ K = L
have mk : ∀ (carrier : Set V) (convex' : Convex ℝ carrier) (isCompact' : IsCompact carrier) (nonempty' : carrier.Nonempty)
  (h :
    { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' :
          ConvexBody V }.carrier =
      L.carrier),
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } = L
Tactic: cases K
Cleared hypotheses: K, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
L : ConvexBody V
carrier : Set V
convex' : Convex ℝ carrier
isCompact' : IsCompact carrier
nonempty' : carrier.Nonempty
h :
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V }.carrier =
    L.carrier
⊢ { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } = L
have mk : ∀ (carrier_1 : Set V) (convex'_1 : Convex ℝ carrier_1) (isCompact'_1 : IsCompact carrier_1)
  (nonempty'_1 : carrier_1.Nonempty)
  (h :
    { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' :
          ConvexBody V }.carrier =
      { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 :
          ConvexBody V }.carrier),
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } =
    { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
⊢ 0 ∈ K
have obtain : ∀ (x : V) (hx : x ∈ (↑K : Set V)), 0 ∈ K
Tactic: obtain ⟨x, hx⟩ := K.nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
⊢ 0 ∈ K
have rw : (1 / 2) • x + (1 / 2) • -x ∈ K
Tactic: rw [show 0 = (1 / 2 : ℝ) • x + (1 / 2 : ℝ) • (-x) by simp]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
⊢ (1 / 2) • x + (1 / 2) • -x ∈ K
have a : 0 < 1 / 2
Tactic: apply convex_iff_forall_pos.mp K.convex hx (h_symm x hx)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
a a₁ : 0 < 1 / 2
⊢ (1 / 2) • x + (1 / 2) • -x ∈ K
have a₂ : 1 / 2 + 1 / 2 = 1
Tactic: apply convex_iff_forall_pos.mp K.convex hx (h_symm x hx)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
⊢ 0 < 1 / 2
have linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < 1 / 2
have linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < 1 / 2
have linarith₂ : 1 / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 / 2
have linarith₃ : 1 / 2 ≤ 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
⊢ 1 / 2 + 1 / 2 = 1
have linarith : 1 / 2 + 1 / 2 < 1 → HMul.hMul (α := ℝ) 1 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ (↑K : Set V)
linarith : 1 / 2 + 1 / 2 < 1 → HMul.hMul (α := ℝ) 1 0 = 0
⊢ 1 / 2 + 1 / 2 = 1
have linarith₁ : 1 < 1 / 2 + 1 / 2 → HMul.hMul (α := ℝ) 1 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
⊢ a • (↑K : Set V) ⊆ b • (↑K : Set V)
have inl : ∀ (h : 0 ≤ b), HSMul.hSMul (α := ℝ≥0) 0 (↑K : Set V) ⊆ b • (↑K : Set V)
Tactic: obtain rfl | ha := eq_zero_or_pos a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
inl : ∀ (h : 0 ≤ b), HSMul.hSMul (α := ℝ≥0) 0 (↑K : Set V) ⊆ b • (↑K : Set V)
⊢ a • (↑K : Set V) ⊆ b • (↑K : Set V)
have inr : ∀ (ha : 0 < a), a • (↑K : Set V) ⊆ b • (↑K : Set V)
Tactic: obtain rfl | ha := eq_zero_or_pos a
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ HSMul.hSMul (α := ℝ≥0) 0 (↑K : Set V) ⊆ b • (↑K : Set V)
have inl : 0 ∈ b • (↑K : Set V)
Tactic: rw [Set.zero_smul_set K.nonempty, Set.zero_subset]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
x : V
hx : x ∈ a • (↑K : Set V)
⊢ x ∈ b • (↑K : Set V)
have inr : ∀ (y : V) (hy : y ∈ (↑K : Set V)) (hx : a • y ∈ a • (↑K : Set V)), a • y ∈ b • (↑K : Set V)
Tactic: obtain ⟨y, hy, rfl⟩ := Set.mem_smul_set.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
⊢ a • y ∈ b • (↑K : Set V)
have inr : y ∈ (a⁻¹ * b) • (↑K : Set V)
Tactic: rw [← Set.mem_inv_smul_set_iff₀ ha.ne', smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
⊢ y ∈ (a⁻¹ * b) • (↑K : Set V)
have inr : 1 ≤ a⁻¹ * b
Tactic: refine Convex.mem_smul_of_zero_mem K.convex h_zero hy (?_ : 1 ≤ a⁻¹ * b)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ (↑K : Set V)
hx : a • y ∈ a • (↑K : Set V)
⊢ 1 ≤ a⁻¹ * b
have inr : a * 1 ≤ b
Tactic: rwa [le_inv_mul_iff₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) = edist K L
have rw : Metric.hausdorffEDist (↑K : Set V) (↑L : Set V) = ENNReal.ofReal (dist K L)
Tactic: rw [edist_dist]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
⊢ ⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V) = (↑K : Set V)
have h : ∀ (x : V), Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x ↔ x ∈ (↑K : Set V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x ↔ x ∈ (↑K : Set V)
have h : ∀ (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x), x ∈ (↑K : Set V)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : ∀ (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x), x ∈ (↑K : Set V)
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x ↔ x ∈ (↑K : Set V)
have h₁ : ∀ (h : x ∈ (↑K : Set V)), Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
⊢ x ∈ (↑K : Set V)
have h₁ : ∀ (C : ℝ) (hC_pos : C > 0) (hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C), x ∈ (↑K : Set V)
Tactic: obtain ⟨C, hC_pos, hC_bdd⟩ := K.isBounded.exists_pos_norm_le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
⊢ x ∈ (↑K : Set V)
have h₁ : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
Tactic: rw [← K.isClosed.closure_eq, SeminormedAddCommGroup.mem_closure_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
⊢ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
have h₁ : ∀ (hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε) (x : V)
  (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x) (C : ℝ) (hC_pos : C > 0)
  (hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C) (ε : ℝ), 0 < ε → ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
Tactic: rw [← NNReal.tendsto_coe, NormedAddCommGroup.tendsto_atTop] at hu
Cleared hypotheses: hu, x, h, C, hC_pos, hC_bdd
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
⊢ ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
have h₁ : ∀ (n : ℕ) (hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C), ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
Tactic: obtain ⟨n, hn⟩ := hu (ε / C) (div_pos hε hC_pos)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
x : V
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
⊢ ∃ b ∈ (↑K : Set V), ‖x - b‖ < ε
have h₁ : ∀ (y : V) (hyK : y ∈ (↑K : Set V))
  (h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)),
  ∃ b ∈ (↑K : Set V), ‖(1 + (↑(u n) : ℝ)) • y - b‖ < ε
Tactic: obtain ⟨y, hyK, rfl⟩ := Set.mem_smul_set.mp (Set.mem_iInter.mp h n)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
⊢ ∃ b ∈ (↑K : Set V), ‖(1 + (↑(u n) : ℝ)) • y - b‖ < ε
have h₁ : ‖(1 + (↑(u n) : ℝ)) • y - y‖ < ε
Tactic: refine ⟨y, hyK, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
⊢ (1 + (↑(u n) : ℝ)) • y - y = (↑(u n) : ℝ) • y
have rw : HSMul.hSMul (α := ℝ) 1 y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
Tactic: rw [add_smul, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
rw : HSMul.hSMul (α := ℝ) 1 y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
⊢ (1 + (↑(u n) : ℝ)) • y - y = (↑(u n) : ℝ) • y
have rw₁ : y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
Tactic: rw [add_smul, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
rw : HSMul.hSMul (α := ℝ) 1 y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
rw₁ : y + (↑(u n) : ℝ) • y - y = (↑(u n) : ℝ) • y
⊢ (1 + (↑(u n) : ℝ)) • y - y = (↑(u n) : ℝ) • y
have rw₂ : (↑(u n) : ℝ) • y = (↑(u n) : ℝ) • y
Tactic: rw [add_smul, one_smul, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
⊢ ‖(1 + (↑(u n) : ℝ)) • y - y‖ < ε
have h₁ : |(↑(u n) : ℝ)| * ‖y‖ < ε
Tactic: rw [show (1 + u n : ℝ) • y - y = (u n : ℝ) • y by rw [add_smul, one_smul, add_sub_cancel_left],
      norm_smul, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (hypothesis)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖(↑(u n_1) : ℝ) - (↑0 : ℝ)‖ < ε / C
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
⊢ |(↑(u n) : ℝ)| * ‖y‖ < ε
have hn₁ : ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε / C
Tactic: specialize hn n le_rfl
Cleared hypotheses: hn