-- Mathlib/Topology/Algebra/Order/Group.lean
theorem denseRange_zsmul_iff_surjective {a : G} :
    DenseRange (· • a : ℤ → G) ↔ Surjective (· • a : ℤ → G)

Proof state:
case intro.intro.inr.inl
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : b < (m - 1) • a
⊢ b + a + a < (m + 1) • a

Tactic:
simpa only [add_smul, sub_smul, one_smul, lt_sub_iff_add_lt, add_lt_add_iff_right] using hlt

Result:
no goals

Proof state:
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
⊢ Surjective fun x => x • a

Tactic:
wlog ha₀ : 0 < a generalizing a

Result:
case inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
this : ∀ {a : G}, (DenseRange fun x => x • a) → 0 < a → Surjective fun x => x • a
ha₀ : ¬0 < a
⊢ Surjective fun x => x • a

G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
⊢ Surjective fun x => x • a

Proof state:
case intro.intro.inr.inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : (m - 1) • a < b
⊢ (Ioo (m • a) ((m + 1) • a)).Nonempty

Tactic:
use b + a

Result:
case h
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : (m - 1) • a < b
⊢ b + a ∈ Ioo (m • a) ((m + 1) • a)

Proof state:
case intro.intro.inl
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
m : ℤ
hm : (m - 1) • a < m • a
hm' : m • a < (m - 1) • a + a + a
⊢ ∃ a_1, (fun x => x • a) a_1 = (m - 1) • a

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
⊢ (Ioo (m • a) ((m + 1) • a)).Nonempty

Tactic:
rcases hne.lt_or_lt with hlt | hlt

Result:
case intro.intro.inr.inl
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : b < (m - 1) • a
⊢ (Ioo (m • a) ((m + 1) • a)).Nonempty

case intro.intro.inr.inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : (m - 1) • a < b
⊢ (Ioo (m • a) ((m + 1) • a)).Nonempty

Proof state:
case intro.intro.inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Tactic:
suffices (Ioo (m • a) ((m + 1) • a)).Nonempty by
  rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
  have : m < l ∧ l < m + 1 := by simpa [zsmul_lt_zsmul_iff_left ha₀] using hl
  omega

Result:
case intro.intro.inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
⊢ (Ioo (m • a) ((m + 1) • a)).Nonempty

Proof state:
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
this : (Ioo (m • a) ((m + 1) • a)).Nonempty
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Tactic:
rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩

Result:
case intro
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
this : (Ioo (m • a) ((m + 1) • a)).Nonempty
l : ℤ
hl : l • a ∈ Ioo (m • a) ((m + 1) • a)
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Proof state:
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
⊢ ∃ m, m • a ∈ Ioo b (b + a + a)

Tactic:
have hne : (Ioo b (b + a + a)).Nonempty := ⟨b + a, by simpa⟩

Result:
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
hne : (Ioo b (b + a + a)).Nonempty
⊢ ∃ m, m • a ∈ Ioo b (b + a + a)

Proof state:
case h
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : (m - 1) • a < b
⊢ b + a ∈ Ioo (m • a) ((m + 1) • a)

Tactic:
simp only [mem_Ioo, add_smul, sub_smul, one_smul, add_lt_add_iff_right] at hlt ⊢

Result:
case h
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
m : ℤ
hm : b < m • a
hm' : m • a < b + a + a
hne : b ≠ (m - 1) • a
hlt : m • a - a < b
⊢ m • a < b + a ∧ b < m • a

Proof state:
case inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x => x • a)
ha₀ : ¬0 < a
this : ∀ {a : G}, Dense (range fun x => x • a) → 0 < a → (range fun x => x • a) = univ
⊢ (range fun x => x • a) = univ

Tactic:
rcases (not_lt.1 ha₀).eq_or_lt with rfl | hlt

Result:
case inr.inl
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
this : ∀ {a : G}, Dense (range fun x => x • a) → 0 < a → (range fun x => x • a) = univ
h : Dense (range fun x => x • 0)
ha₀ : ¬0 < 0
⊢ (range fun x => x • 0) = univ

case inr.inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x => x • a)
ha₀ : ¬0 < a
this : ∀ {a : G}, Dense (range fun x => x • a) → 0 < a → (range fun x => x • a) = univ
hlt : a < 0
⊢ (range fun x => x • a) = univ

Proof state:
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
ha₀ : 0 < a
b : G
hne : (Ioo b (b + a + a)).Nonempty
⊢ ∃ m, m • a ∈ Ioo b (b + a + a)

Tactic:
simpa using h.exists_mem_open isOpen_Ioo hne

Result:
no goals

Proof state:
case inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x => x • a
this : ∀ {a : G}, (DenseRange fun x => x • a) → 0 < a → Surjective fun x => x • a
ha₀ : ¬0 < a
⊢ Surjective fun x => x • a

Tactic:
simp only [← range_eq_univ, DenseRange] at *

Result:
case inr
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x => x • a)
ha₀ : ¬0 < a
this : ∀ {a : G}, Dense (range fun x => x • a) → 0 < a → (range fun x => x • a) = univ
⊢ (range fun x => x • a) = univ