-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem discreteTopology_pi_basisFun [Finite ι] :
    DiscreteTopology (span ℤ (Set.range (Pi.basisFun ℝ ι)))

Proof state:
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
⊢ ∃ y, ↑y = ↑x i

Tactic:
exact ((Pi.basisFun ℝ ι).mem_span_iff_repr_mem ℤ x).mp (SetLike.coe_mem x) i

Result:
no goals

Proof state:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Subtype.val ⁻¹' Metric.ball 0 1 = {0}

Tactic:
ext x

Result:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ x ∈ Subtype.val ⁻¹' Metric.ball 0 1 ↔ x ∈ {0}

Proof state:
ι : Type u_2
inst✝ : Finite ι
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Proof state:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
refine discreteTopology_iff_isOpen_singleton_zero.mpr ⟨Metric.ball 0 1, Metric.isOpen_ball, ?_⟩

Result:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Subtype.val ⁻¹' Metric.ball 0 1 = {0}

Proof state:
case intro.h.intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ |↑x i| < 1 ↔ ↑x i = 0

Tactic:
rw [← hy, ← Int.cast_abs, ← Int.cast_one,  Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]

Result:
no goals

Proof state:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
⊢ |↑x i| < 1 ↔ ↑x i = 0

Tactic:
rsuffices ⟨y, hy⟩ : ∃ (y : ℤ), (y : ℝ) = (x : ι → ℝ) i

Result:
case intro.h.intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ |↑x i| < 1 ↔ ↑x i = 0

ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
⊢ ∃ y, ↑y = ↑x i

Proof state:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), |↑x i| < 1) ↔ ∀ (x_1 : ι), ↑x x_1 = 0

Tactic:
refine forall_congr' (fun i => ?_)

Result:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
⊢ |↑x i| < 1 ↔ ↑x i = 0

Proof state:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), ‖↑x i‖ < 1) ↔ x = 0

Tactic:
simp_rw [← coe_eq_zero, funext_iff, Pi.zero_apply, Real.norm_eq_abs]

Result:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), |↑x i| < 1) ↔ ∀ (x_1 : ι), ↑x x_1 = 0

Proof state:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ x ∈ Subtype.val ⁻¹' Metric.ball 0 1 ↔ x ∈ {0}

Tactic:
rw [Set.mem_preimage, mem_ball_zero_iff, pi_norm_lt_iff zero_lt_one, Set.mem_singleton_iff]

Result:
case intro.h
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), ‖↑x i‖ < 1) ↔ x = 0