case this
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))

G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
have : ∃ n : ℕ, Set.Nonempty (H ∩ Ioc (n • a) ((n + 1) • a))
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
classical rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ¬∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
⊢ False
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
by_contra hxmin
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
⊢ False
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ¬∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
⊢ False
simp only [IsLeast, not_and, mem_setOf_eq, mem_lowerBounds, not_exists, not_forall,
  not_le] at hxmin
case mk.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
⊢ False
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
⊢ False
rcases hxmin x ⟨hxH, (nsmul_nonneg h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩
case mk.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
⊢ False
case mk.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
⊢ False
rcases hex y hy₀ with ⟨m, hm⟩
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inl
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hmn : m < n
⊢ False

case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hnm : n ≤ m
⊢ False
case mk.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
⊢ False
cases' lt_or_le m n with hmn hnm
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g - a ≤ 0 + m • a
hm' : 0 + m • a < g - a + a
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
rcases existsUnique_add_zsmul_mem_Ico h₀ 0 (g - a) with ⟨m, ⟨hm, hm'⟩, -⟩
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g - a ≤ 0 + m • a
hm' : 0 + m • a < g - a + a
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
simp only [zero_add, sub_le_iff_le_add, sub_add_cancel, ← add_one_zsmul] at hm hm'
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ 0 ≤ m

case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℕ
hm : g ≤ (↑m + 1) • a
hm' : ↑m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
lift m to ℕ
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ 0 < (m + 1) • a
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ 0 ≤ m
rw [← Int.lt_add_one_iff, ← zsmul_lt_zsmul_iff h₀, zero_zsmul]
no goals
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ 0 < (m + 1) • a
exact hg.trans_le hm
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℕ
hm : g ≤ Nat.succ m • a
hm' : m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℕ
hm : g ≤ (↑m + 1) • a
hm' : ↑m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
simp only [← Nat.cast_succ, coe_nat_zsmul] at hm hm'
no goals
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℕ
hm : g ≤ Nat.succ m • a
hm' : m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
exact ⟨m, hm', hm⟩
case this.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
g : G
hgH : g ∈ H
hg₀ : g ≠ 0
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
case this
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
rcases (bot_or_exists_ne_zero H).resolve_left hbot with ⟨g, hgH, hg₀⟩
case this.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
g : G
hgH : g ∈ H
hg₀ : g ≠ 0
n : ℕ
hn : abs g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
case this.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
g : G
hgH : g ∈ H
hg₀ : g ≠ 0
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
rcases hex (|g|) (abs_pos.2 hg₀) with ⟨n, hn⟩
no goals
case this.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
g : G
hgH : g ∈ H
hg₀ : g ≠ 0
n : ℕ
hn : abs g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
exact ⟨n, _, (@abs_mem_iff (AddSubgroup G) G _ _).2 hgH, hn⟩
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩
no goals
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inl
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hmn : m < n
⊢ False
exact hmin m hmn ⟨y, hyH, hm⟩
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hnm : n ≤ m
⊢ x < y + a
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hnm : n ≤ m
⊢ False
refine disjoint_left.1 hd (sub_mem hxH hyH) ⟨sub_pos.2 hxy, sub_lt_iff_lt_add'.2 ?_⟩
no goals
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hnm : n ≤ m
⊢ x < y + a
calc x ≤ (n + 1) • a := hxn
_ ≤ (m + 1) • a := nsmul_le_nsmul h₀.le (add_le_add_right hnm _)
_ = m • a + a := succ_nsmul' _ _
_ < y + a := add_lt_add_right hm.1 _