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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩

Result:
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

Proof state:
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
H : (range fun x => x • -a) = range fun x => x • a
⊢ (range fun x => x • -a) = univ

Tactic:
apply this <;> simpa only [H, neg_pos]

Result:
no goals

Proof state:
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)
this : m < l ∧ l < m + 1
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Tactic:
omega

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
ha₀ : 0 < a
b : G
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Tactic:
obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, m • a ∈ Ioo b (b + a + a) := by
  have hne : (Ioo b (b + a + a)).Nonempty := ⟨b + a, by simpa⟩
  simpa using h.exists_mem_open isOpen_Ioo hne

Result:
case intro.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
⊢ ∃ a_1, (fun x => x • a) a_1 = b

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
⊢ (Ioo (m • a) ((m + 1) • a)).Nonempty

Tactic:
refine ⟨b + a + a, hm', ?_⟩

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
⊢ b + a + a < (m + 1) • 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 • a - a < b
⊢ m • a < b + a ∧ b < m • a

Tactic:
exact ⟨sub_lt_iff_lt_add.1 hlt, hm⟩

Result:
no goals

Proof state:
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
H : (range fun x => x • -a) = range fun x => x • a
⊢ (range fun x => x • a) = univ

Tactic:
rw [← H]

Result:
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
H : (range fun x => x • -a) = range fun x => x • a
⊢ (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
⊢ b + a ∈ Ioo b (b + a + a)

Tactic:
simpa

Result:
no goals

Proof state:
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

Tactic:
have : m < l ∧ l < m + 1 := by simpa [zsmul_lt_zsmul_iff_left ha₀] using 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)
this : m < l ∧ l < m + 1
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Proof state:
case intro.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
⊢ ∃ a_1, (fun x => x • a) a_1 = b

Tactic:
rcases eq_or_ne b ((m - 1) • a) with rfl | hne

Result:
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

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

Proof state:
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

Tactic:
simpa only [smul_zero, range_const, dense_iff_closure_eq, closure_singleton] using h

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
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)
⊢ m < l ∧ l < m + 1

Tactic:
simpa [zsmul_lt_zsmul_iff_left ha₀] using hl

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
ha₀ : 0 < a
⊢ Surjective fun x => x • a

Tactic:
intro b

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
⊢ ∃ a_1, (fun x => x • a) a_1 = b