internlm/Lean-Github huggingface dataset:
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √2 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this✝ : √(2 * x - 1) ≤ 1
this : 2 = A * √2 ↔ A = √2
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2
Tactic:
convert this using 2
Proof state after:
case h.e'_1.h.e'_2
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this✝ : √(2 * x - 1) ≤ 1
this : 2 = A * √2 ↔ A = √2
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = 2
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
case h.e'_1.h.e'_2
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this✝ : √(2 * x - 1) ≤ 1
this : 2 = A * √2 ↔ A = √2
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = 2
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
⊢ IsGood x A ↔ A = √(4 * x - 2)
Tactic:
have h₁ : 1 < sqrt (2 * x - 1) := by simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
Proof state after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ IsGood x A ↔ A = √(4 * x - 2)
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ IsGood x A ↔ A = √(4 * x - 2)
Tactic:
have h₂ : 1 / 2 ≤ x := by linarith
Proof state after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ IsGood x A ↔ A = √(4 * x - 2)
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ IsGood x A ↔ A = √(4 * x - 2)
Tactic:
simp only [isGood_iff, h₂, abs_of_pos (sub_pos.2 h₁), add_add_sub_cancel, and_true]
Proof state after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √(2 * x - 1) + √(2 * x - 1) = A * √2 ↔ A = √(4 * x - 2)
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √(2 * x - 1) + √(2 * x - 1) = A * √2 ↔ A = √(4 * x - 2)
Tactic:
rw [← mul_two, ← div_eq_iff (by positivity), mul_div_assoc, div_sqrt, ← sqrt_mul' _ zero_le_two,
  eq_comm]
Proof state after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ A = √((2 * x - 1) * 2) ↔ A = √(4 * x - 2)
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ A = √((2 * x - 1) * 2) ↔ A = √(4 * x - 2)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
⊢ 1 < √(2 * x - 1)
Tactic:
simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ 1 / 2 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_eq_sqrt
Proof state before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √2 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo1959P2.IsGood.sqrt_two_lt_of_one_lt
Proof state before:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ √2 < A
Tactic:
rw [(isGood_iff_eq_sqrt hx).1 h]
Proof state after:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ √2 < √(4 * x - 2)
Theorem: Imo1959P2.IsGood.sqrt_two_lt_of_one_lt
Proof state before:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ √2 < √(4 * x - 2)
Tactic:
refine sqrt_lt_sqrt zero_le_two ?_
Proof state after:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ 2 < 4 * x - 2
Theorem: Imo1959P2.IsGood.sqrt_two_lt_of_one_lt
Proof state before:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ 2 < 4 * x - 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
x A : ℝ
hA : √2 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
Tactic:
have : 0 < A := lt_trans (by simp) hA
Proof state after:
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
Tactic:
constructor
Proof state after:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A → x = (A / 2) ^ 2 + 1 / 2

case mpr
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ x = (A / 2) ^ 2 + 1 / 2 → IsGood x A
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
x A : ℝ
hA : √2 < A
⊢ 0 < √2
Tactic:
simp
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A → x = (A / 2) ^ 2 + 1 / 2
Tactic:
intro h
Proof state after:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ x = (A / 2) ^ 2 + 1 / 2
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ x = (A / 2) ^ 2 + 1 / 2
Tactic:
have hx : 1 < x := by rwa [h.sqrt_two_lt_iff_one_lt] at hA
Proof state after:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
hx : 1 < x
⊢ x = (A / 2) ^ 2 + 1 / 2
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
hx : 1 < x
⊢ x = (A / 2) ^ 2 + 1 / 2
Tactic:
rw [isGood_iff_eq_sqrt hx, eq_comm, sqrt_eq_iff_sq_eq] at h <;> linarith
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ 1 < x
Tactic:
rwa [h.sqrt_two_lt_iff_one_lt] at hA
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mpr
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ x = (A / 2) ^ 2 + 1 / 2 → IsGood x A
Tactic:
rintro rfl
Proof state after:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood ((A / 2) ^ 2 + 1 / 2) A
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood ((A / 2) ^ 2 + 1 / 2) A
Tactic:
rw [isGood_iff_eq_sqrt]
Proof state after:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ A = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)

case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ A = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)
Tactic:
conv_lhs => rw [← sqrt_sq this.le]
Proof state after:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ √(A ^ 2) = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ √(A ^ 2) = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2
Tactic:
rw [sqrt_lt' this] at hA
Proof state after:
case mpr
A : ℝ
hA : 2 < A ^ 2
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2
Theorem: Imo1959P2.isGood_iff_of_sqrt_two_lt
Proof state before:
case mpr
A : ℝ
hA : 2 < A ^ 2
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
⊢ ∀ n ≥ 2, (∃ m ≥ 2, m ≠ n ∧ m ∣ n) → ¬Prime n
Tactic:
intro n hn h p
Proof state after:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
⊢ False
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
⊢ False
Tactic:
have ngt0 : 0 < n := by omega
Proof state after:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
ngt0 : 0 < n
⊢ False
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
ngt0 : 0 < n
⊢ False
Tactic:
have p := (Nat.prime_iff).mpr p
Proof state after:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
⊢ False
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
⊢ False
Tactic:
obtain ⟨m, ⟨h1, ⟨h2, h3⟩⟩⟩ := h
Proof state after:
case intro.intro.intro
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ False
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
case intro.intro.intro
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ False
Tactic:
apply (Nat.not_prime_iff_minFac_lt hn).mpr _ p
Proof state after:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ n.minFac < n
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ n.minFac < n
Tactic:
have h4 : m < n := lt_of_le_of_ne (Nat.le_of_dvd ngt0 h3) h2
Proof state after:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
⊢ n.minFac < n
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
⊢ n.minFac < n
Tactic:
have h5 : Nat.minFac n ≤ m := Nat.minFac_le_of_dvd h1 h3
Proof state after:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
h5 : n.minFac ≤ m
⊢ n.minFac < n
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
h5 : n.minFac ≤ m
⊢ n.minFac < n
Tactic:
apply lt_of_le_of_lt h5 h4
Proof state after:
no goals
Theorem: Usa1982P4.not_prime_of_dvd
Proof state before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
⊢ 0 < n
Tactic:
omega
Proof state after:
no goals
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
⊢ ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → d ^ n ≡ d ^ a [MOD c]
Tactic:
intros n a b c d h1 h2
Proof state after:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
⊢ d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
wlog h : n ≤ a with H
Proof state after:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]

n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
have han : a ≤ n := (Nat.le_total n a).resolve_left h
Proof state after:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
symm
Proof state after:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ a ≡ d ^ n [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ a ≡ d ^ n [MOD c]
Tactic:
apply H a n b c d h1.symm h2 han
Proof state after:
no goals
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [(by simp : d ^ n = 1 * d ^ n)]
Proof state after:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
have ann : a = (a - n + n) := by exact (Nat.sub_eq_iff_eq_add h).mp rfl
Proof state after:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [←(zero_add n : 0 + n = n)] at h1
Proof state after:
n a b c d : ℕ
h1 : 0 + n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : 0 + n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [ann] at h1
Proof state after:
n a b c d : ℕ
h1 : 0 + n ≡ a - n + n [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : 0 + n ≡ a - n + n [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
apply Nat.ModEq.add_right_cancel' at h1
Proof state after:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
Tactic:
rw [ann, pow_add]
Proof state after:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ (a - n) * d ^ n [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 * d ^ n ≡ d ^ (a - n) * d ^ n [MOD c]
Tactic:
apply Nat.ModEq.mul
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]

case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]

case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]
Tactic:
swap
Proof state after:
case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]

case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]

case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
Tactic:
rfl
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
Tactic:
unfold Nat.ModEq
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c
Tactic:
unfold Nat.ModEq at h2
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ (a - n) % c
Tactic:
rw [←(Nat.div_add_mod' (a - n) b)]
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + (a - n) % b) % c
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + (a - n) % b) % c
Tactic:
rw [←h1]
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + 0 % b) % c
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b + 0 % b) % c
Tactic:
simp only [Nat.zero_mod, add_zero]
Proof state after:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b) % c
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b) % c
Tactic:
rw [mul_comm, pow_mul, Nat.pow_mod, h2, ←Nat.pow_mod, one_pow]
Proof state after:
no goals
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ d ^ n = 1 * d ^ n
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1982P4.some_useful_mod_lemma
Proof state before:
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ a = a - n + n
Tactic:
exact (Nat.sub_eq_iff_eq_add h).mp rfl
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
⊢ ¬∃ f, ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
Tactic:
intro hf
Proof state after:
m : ℕ
hf : ∃ f, ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
hf : ∃ f, ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
Tactic:
obtain ⟨f, hf⟩ := hf
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
Tactic:
have f_injective : f.Injective := by
  intro n m hnm; have hfn := hf n; simp_all only [add_left_inj]
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
⊢ False
Tactic:
let NN : Set ℕ := Set.univ
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
⊢ False
Tactic:
let A : Set ℕ := NN \ (f '' NN)
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
⊢ False
Tactic:
let B : Set ℕ := f '' A
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
⊢ False
Tactic:
have hid := Set.image_diff f_injective NN (f '' NN)
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : f '' (NN \ f '' NN) = f '' NN \ f '' (f '' NN)
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : f '' (NN \ f '' NN) = f '' NN \ f '' (f '' NN)
⊢ False
Tactic:
rw [show f '' (NN \ f '' NN) = B by rfl] at hid
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
⊢ False
Tactic:
have ab_disjoint : Disjoint A B := by
  intro _C hca hcb c hc
  exact Set.not_mem_of_mem_diff (hca hc) (Set.image_subset f sdiff_le (hcb hc))
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ False
Tactic:
have ab_fintype : Fintype ↑(A ∪ B) := by rw [ab_range]; exact inferInstance
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
⊢ False
Tactic:
have h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1 := by
  have hc := @Fintype.card_congr' ↑(A ∪ B)
                {x | x < 2 * m + 1} _ _ (by rw [ab_range])
  simp only [hc, Fintype.card_ofFinset, Finset.card_range]
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
⊢ False