internlm/Lean-Github huggingface dataset:
Theorem: Imo2008P3.p_lemma
Proof state before:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Tactic:
have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
Proof state after:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
hcast₂ : ↑n ^ 2 + 1 = ↑p * ↑x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Theorem: Imo2008P3.p_lemma
Proof state before:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
hcast₂ : ↑n ^ 2 + 1 = ↑p * ↑x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Tactic:
linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑k = ↑p - 2 * ↑n
Tactic:
assumption_mod_cast
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑n ^ 2 + 1 = ↑p * ↑x
Tactic:
assumption_mod_cast
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
⊢ ↑k = ↑p - 2 * ↑n
Tactic:
assumption_mod_cast
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑p > 20
Tactic:
assumption_mod_cast
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ↑k ^ 2 + 4 ≥ ↑p
Tactic:
assumption_mod_cast
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ ↑k > 4
Tactic:
refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ 4 ^ 2 < ↑k ^ 2
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ 4 ^ 2 < ↑k ^ 2
Tactic:
linarith only [hreal₂, hreal₃]
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ ↑k > √(2 * ↑n)
Tactic:
refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ √(2 * ↑n) ^ 2 < ↑k ^ 2
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ √(2 * ↑n) ^ 2 < ↑k ^ 2
Tactic:
rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ 2 * ↑n < ↑k ^ 2
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ 2 * ↑n < ↑k ^ 2
Tactic:
linarith only [hreal₁, hreal₃, hreal₅]
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
hreal₆ : ↑k > √(2 * ↑n)
⊢ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
linarith only [hreal₆, hreal₁]
Proof state after:
no goals
Theorem: Usa2023P2.val_div
Proof state before:
a b : ℝ+
⊢ ↑(a / b) = ↑a / ↑b
Tactic:
rfl
Proof state after:
no goals
Theorem: Usa2023P2.lemma_1
Proof state before:
a b c : ℝ+
⊢ (a + b) / c = a / c + b / c
Tactic:
rw [division_def, add_mul, ←division_def, ←division_def]
Proof state after:
no goals
Theorem: Usa2023P2.lemma_3
Proof state before:
a b c : ℝ+
h : a = b + c
⊢ c < a
Tactic:
rw [h]
Proof state after:
a b c : ℝ+
h : a = b + c
⊢ c < b + c
Theorem: Usa2023P2.lemma_3
Proof state before:
a b c : ℝ+
h : a = b + c
⊢ c < b + c
Tactic:
obtain ⟨b, hb⟩ := b
Proof state after:
case mk
a c : ℝ+
b : ℝ
hb : 0 < b
h : a = ⟨b, hb⟩ + c
⊢ c < ⟨b, hb⟩ + c
Theorem: Usa2023P2.lemma_3
Proof state before:
case mk
a c : ℝ+
b : ℝ
hb : 0 < b
h : a = ⟨b, hb⟩ + c
⊢ c < ⟨b, hb⟩ + c
Tactic:
obtain ⟨c, hc⟩ := c
Proof state after:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ⟨c, hc⟩ < ⟨b, hb⟩ + ⟨c, hc⟩
Theorem: Usa2023P2.lemma_3
Proof state before:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ⟨c, hc⟩ < ⟨b, hb⟩ + ⟨c, hc⟩
Tactic:
rw [←Subtype.coe_lt_coe, Positive.coe_add]
Proof state after:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ↑⟨c, hc⟩ < ↑⟨b, hb⟩ + ↑⟨c, hc⟩
Theorem: Usa2023P2.lemma_3
Proof state before:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ↑⟨c, hc⟩ < ↑⟨b, hb⟩ + ↑⟨c, hc⟩
Tactic:
exact lt_add_of_pos_left c hb
Proof state after:
no goals
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
m n : ℕ
⊢ (m + 3) ^ n % 3 = m ^ n % 3
Tactic:
induction' n with pn hpn
Proof state after:
case zero
m : ℕ
⊢ (m + 3) ^ 0 % 3 = m ^ 0 % 3

case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) ^ (pn + 1) % 3 = m ^ (pn + 1) % 3
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case zero
m : ℕ
⊢ (m + 3) ^ 0 % 3 = m ^ 0 % 3
Tactic:
simp only [Nat.zero_eq, pow_zero, Nat.one_mod]
Proof state after:
no goals
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) ^ (pn + 1) % 3 = m ^ (pn + 1) % 3
Tactic:
rw [Nat.pow_succ']
Proof state after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3
Tactic:
have h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn := by ring
Proof state after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3
Tactic:
rw [h1]
Proof state after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
Tactic:
have h2 : 3 * (m + 3) ^ pn % 3 = 0 := Nat.mul_mod_right 3 _
Proof state after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
Tactic:
rw[Nat.add_mod, h2, add_zero, Nat.mod_mod, Nat.pow_succ']
Proof state after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ m * (m + 3) ^ pn % 3 = m * m ^ pn % 3
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ m * (m + 3) ^ pn % 3 = m * m ^ pn % 3
Tactic:
exact Nat.ModEq.mul rfl hpn
Proof state after:
no goals
Theorem: Bulgaria1998P11.mod_plus_pow
Proof state before:
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
Tactic:
ring
Proof state after:
no goals
Theorem: Bulgaria1998P11.foo1
Proof state before:
m n : ℕ
ho : Odd m
⊢ (m + 3) ^ n.succ % 2 = 0
Tactic:
cases' ho with w hw
Proof state after:
case intro
m n w : ℕ
hw : m = 2 * w + 1
⊢ (m + 3) ^ n.succ % 2 = 0
Theorem: Bulgaria1998P11.foo1
Proof state before:
case intro
m n w : ℕ
hw : m = 2 * w + 1
⊢ (m + 3) ^ n.succ % 2 = 0
Tactic:
rw[hw, Nat.pow_succ, show 2 * w + 1 + 3 = 2 * (w + 2) by ring, Nat.mul_mod,
   Nat.mul_mod_right, mul_zero, Nat.zero_mod]
Proof state after:
no goals
Theorem: Bulgaria1998P11.foo1
Proof state before:
m n w : ℕ
hw : m = 2 * w + 1
⊢ 2 * w + 1 + 3 = 2 * (w + 2)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1963P1.iff_comm
Proof state before:
a b c : Prop
⊢ (a → c) → (b → c) → (c → (a ↔ b)) → (a ↔ b)
Tactic:
tauto
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ s ∈ solution_set
Tactic:
rw [Set.mem_Ioo]
Proof state after:
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ 1 < s ∧ s < 2
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ 1 < s ∧ s < 2
Tactic:
obtain ⟨a, b, c, d, ha, hb, hc, hd, rfl⟩ := h
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) ∧
    a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) ∧
    a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h8 : a / (a + b + c + d) < a / (a + b + d) :=
   div_lt_div_of_pos_left ha (by linarith) (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h9 : b / (a + b + c + d) < b / (a + b + c) :=
   div_lt_div_of_pos_left hb (by linarith) (lt_add_of_pos_right _ hd)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h10 : c / (a + b + c + d) < c / (b + c + d) :=
   div_lt_div_of_pos_left hc (by linarith) (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h11 : d / (a + b + c + d) < d / (a + c + d) :=
   div_lt_div_of_pos_left hd (by linarith) (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
calc 1 = a / (a + b + c + d) + b / (a + b + c + d) +
         c / (a + b + c + d) + d / (a + b + c + d) := by field_simp
     _ < _ := by gcongr
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 0 < a + b + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ a + b + d < a + b + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
⊢ 0 < a + b + c
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ 0 < b + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ b + c + d < a + b + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ 0 < a + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ a + c + d < a + b + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ 1 = a / (a + b + c + d) + b / (a + b + c + d) + c / (a + b + c + d) + d / (a + b + c + d)
Tactic:
field_simp
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ a / (a + b + c + d) + b / (a + b + c + d) + c / (a + b + c + d) + d / (a + b + c + d) <
    a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h3 : a / (a + b + d) < a / (a + b) :=
   div_lt_div_of_pos_left ha (add_pos ha hb) (lt_add_of_pos_right _ hd)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h4 : b / (a + b + c) < b / (a + b) :=
   div_lt_div_of_pos_left hb (add_pos ha hb) (lt_add_of_pos_right _ hc)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h5 : c / (b + c + d) < c / (c + d) :=
   div_lt_div_of_pos_left hc (add_pos hc hd) (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2