Theorem: IMOSL.IMO2014A4.exists_ne_pow_eq (IMOSLLean4/IMO2014/A4/A4.lean)

State before:
k : ℤ
h : k ≠ 0
b : ℤ
h0 : Set.MapsTo (fun x => b ^ x % k) Set.univ ↑(Finset.Ico 0 |k|)
⊢ ∃ m n, m ≠ n ∧ b ^ m % k = b ^ n % k
Tactic:
obtain ⟨m, -, n, -, h, h0⟩ :=
  Set.infinite_univ.exists_ne_map_eq_of_mapsTo h0 (Set.toFinite _)
State after:
case intro.intro.intro.intro.intro
k : ℤ
h✝ : k ≠ 0
b : ℤ
h0✝ : Set.MapsTo (fun x => b ^ x % k) Set.univ ↑(Finset.Ico 0 |k|)
m n : ℕ
h : m ≠ n
h0 : b ^ m % k = b ^ n % k
⊢ ∃ m n, m ≠ n ∧ b ^ m % k = b ^ n % k

State before:
case intro.intro.intro.intro.intro
k : ℤ
h✝ : k ≠ 0
b : ℤ
h0✝ : Set.MapsTo (fun x => b ^ x % k) Set.univ ↑(Finset.Ico 0 |k|)
m n : ℕ
h : m ≠ n
h0 : b ^ m % k = b ^ n % k
⊢ ∃ m n, m ≠ n ∧ b ^ m % k = b ^ n % k
Tactic:
exact ⟨m, n, h, h0⟩
State after:
no goals

State before:
k : ℤ
h : k ≠ 0
b : ℤ
x : ℕ
x✝ : x ∈ Set.univ
⊢ (fun x => b ^ x % k) x ∈ ↑(Finset.Ico 0 |k|)
Tactic:
rw [Finset.coe_Ico, Set.mem_Ico]
State after:
k : ℤ
h : k ≠ 0
b : ℤ
x : ℕ
x✝ : x ∈ Set.univ
⊢ 0 ≤ (fun x => b ^ x % k) x ∧ (fun x => b ^ x % k) x < |k|

State before:
k : ℤ
h : k ≠ 0
b : ℤ
x : ℕ
x✝ : x ∈ Set.univ
⊢ 0 ≤ (fun x => b ^ x % k) x ∧ (fun x => b ^ x % k) x < |k|
Tactic:
exact ⟨(b ^ x).emod_nonneg h, (b ^ x).emod_lt h⟩
State after:
no goals