internlm/Lean-Github huggingface dataset:
Theorem: Imo2019P2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ Cospherical {cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂}
Tactic:
haveI := someOrientation V
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ Cospherical {cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂}
Theorem: Imo2019P2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ Cospherical {cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂}
Tactic:
rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁,
  Set.pair_comm]
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ Cospherical {cfg.C, cfg.A₂, cfg.Q₁, cfg.A₁}
Theorem: Imo2019P2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ Cospherical {cfg.C, cfg.A₂, cfg.Q₁, cfg.A₁}
Tactic:
exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear
  cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁ cfg.not_collinear_CA₂A₁
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace Pt
inst✝¹ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.Q cfg.Q₁ cfg.A₂ = 2 • ∡ cfg.A₁ cfg.Q₁ cfg.A₂
Tactic:
rw [cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_left]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace Pt
inst✝¹ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.A₁ cfg.C cfg.A₂ = 2 • ∡ cfg.B cfg.C cfg.A₂
Tactic:
rw [cfg.sbtw_B_A₁_C.symm.oangle_eq_left]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_mem_ω
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ 0 ≠ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_mem_ω
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ 0 ≠ 2
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_mem_ω
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
this : Module.Oriented ℝ V (Fin 2)
⊢ 1 ≠ 2
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.P₁_mem_ω
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.P₁ ∈ cfg.ω
Tactic:
rw [← symm_ω]
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.P₁ ∈ cfg.symm.ω
Theorem: Imo2019P2.Imo2019q2Cfg.P₁_mem_ω
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.P₁ ∈ cfg.symm.ω
Tactic:
exact cfg.symm.Q₁_mem_ω
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.result
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ Concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
Tactic:
refine ⟨?_, coplanar_of_fact_finrank_eq_two _⟩
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ Cospherical {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
Theorem: Imo2019P2.Imo2019q2Cfg.result
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ Cospherical {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
Tactic:
rw [cospherical_iff_exists_sphere]
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ ∃ s, {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere s.center s.radius
Theorem: Imo2019P2.Imo2019q2Cfg.result
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ ∃ s, {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere s.center s.radius
Tactic:
refine ⟨cfg.ω, ?_⟩
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere cfg.ω.center cfg.ω.radius
Theorem: Imo2019P2.Imo2019q2Cfg.result
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere cfg.ω.center cfg.ω.radius
Tactic:
simp only [Set.insert_subset_iff, Set.singleton_subset_iff]
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.P ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
    cfg.Q ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
      cfg.P₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧ cfg.Q₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius
Theorem: Imo2019P2.Imo2019q2Cfg.result
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.P ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
    cfg.Q ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
      cfg.P₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧ cfg.Q₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius
Tactic:
exact ⟨cfg.P_mem_ω, cfg.Q_mem_ω, cfg.P₁_mem_ω, cfg.Q₁_mem_ω⟩
Proof state after:
no goals
Theorem: Imo2014P1.lemma0
Proof state before:
p : ℕ → Prop
h : ∃! n, p (n + 1)
⊢ ∃! n, 0 < n ∧ p n
Tactic:
obtain ⟨n, hn1, hn2⟩ := h
Proof state after:
case intro.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∃! n, 0 < n ∧ p n
Theorem: Imo2014P1.lemma0
Proof state before:
case intro.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∃! n, 0 < n ∧ p n
Tactic:
use n + 1
Proof state after:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ (fun n => 0 < n ∧ p n) (n + 1) ∧ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
Theorem: Imo2014P1.lemma0
Proof state before:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ (fun n => 0 < n ∧ p n) (n + 1) ∧ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
Tactic:
refine ⟨⟨Nat.succ_pos n, hn1⟩, ?_⟩
Proof state after:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
Theorem: Imo2014P1.lemma0
Proof state before:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
Tactic:
rintro m ⟨hm1, hm2⟩
Proof state after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
⊢ m = n + 1
Theorem: Imo2014P1.lemma0
Proof state before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
⊢ m = n + 1
Tactic:
have hm3 := hn2 (m - 1)
Proof state after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : (fun n => p (n + 1)) (m - 1) → m - 1 = n
⊢ m = n + 1
Theorem: Imo2014P1.lemma0
Proof state before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : (fun n => p (n + 1)) (m - 1) → m - 1 = n
⊢ m = n + 1
Tactic:
dsimp only at hm3
Proof state after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p (m - 1 + 1) → m - 1 = n
⊢ m = n + 1
Theorem: Imo2014P1.lemma0
Proof state before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p (m - 1 + 1) → m - 1 = n
⊢ m = n + 1
Tactic:
rw [Nat.sub_add_cancel hm1] at hm3
Proof state after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p m → m - 1 = n
⊢ m = n + 1
Theorem: Imo2014P1.lemma0
Proof state before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p m → m - 1 = n
⊢ m = n + 1
Tactic:
exact Nat.eq_add_of_sub_eq hm1 (hm3 hm2)
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Tactic:
have hmono : StrictMono s := strictMono_nat_of_lt_succ hs
Proof state after:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Tactic:
let S := { i | z ≤ s (i + 1) }
Proof state after:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Tactic:
use Nat.find h3
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (fun i => s i < z ∧ z ≤ s (i + 1)) (Nat.find h3) ∧ ∀ (y : ℕ), (fun i => s i < z ∧ z ≤ s (i + 1)) y → y = Nat.find h3
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (fun i => s i < z ∧ z ≤ s (i + 1)) (Nat.find h3) ∧ ∀ (y : ℕ), (fun i => s i < z ∧ z ≤ s (i + 1)) y → y = Nat.find h3
Tactic:
dsimp [S]
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (s (Nat.find h3) < z ∧ z ≤ s (Nat.find h3 + 1)) ∧ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (s (Nat.find h3) < z ∧ z ≤ s (Nat.find h3 + 1)) ∧ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3
Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
Proof state after:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ s (Nat.find h3) < z

case h.refine_2
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ z ≤ s (Nat.find h3 + 1)

case h.refine_3
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ ∃ j, j ∈ S
Tactic:
use Int.toNat (z - s 0)
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ (z - s 0).toNat ∈ S
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ (z - s 0).toNat ∈ S
Tactic:
rw [Set.mem_setOf_eq]
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h8 := h5 (Int.toNat (z - s 0))
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h6 : 0 ≤ z - s 0 := by omega
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h7 : ((Int.toNat (z - s 0)) :ℤ) = z - s 0 := Int.toNat_of_nonneg h6
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
rw [h7] at h8
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + (z - s 0) ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + (z - s 0) ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
rw [add_sub_cancel] at h8
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h12 : s (Int.toNat (z - s 0)) < s (Int.toNat (z - s 0) + 1) := hs _
Proof state after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
h12 : s (z - s 0).toNat < s ((z - s 0).toNat + 1)
⊢ z ≤ s ((z - s 0).toNat + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
h12 : s (z - s 0).toNat < s ((z - s 0).toNat + 1)
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
⊢ s 0 + ↑i ≤ s i
Tactic:
induction' i with i ih
Proof state after:
case zero
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
⊢ s 0 + ↑0 ≤ s 0

case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case zero
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
⊢ s 0 + ↑0 ≤ s 0
Tactic:
simp
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)
Tactic:
have h10 : (Nat.succ i : ℤ) = (i : ℤ) + 1 := by norm_cast
Proof state after:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)
Tactic:
rw [h10, ←add_assoc]
Proof state after:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑i + 1 ≤ s (i + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑i + 1 ≤ s (i + 1)
Tactic:
exact add_le_of_add_le_right (hs i) ih
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
⊢ ↑i.succ = ↑i + 1
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ 0 ≤ z - s 0
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ s (Nat.find h3) < z
Tactic:
have h4 := Nat.find_min h3 (m := (Nat.find h3 - 1))
Proof state after:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
Tactic:
cases' Nat.eq_zero_or_pos (Nat.find h3) with h5 h5
Proof state after:
case h.refine_1.inl
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 = 0
⊢ s (Nat.find h3) < z

case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
⊢ s (Nat.find h3) < z
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1.inl
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 = 0
⊢ s (Nat.find h3) < z
Tactic:
rwa [h5]
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
⊢ s (Nat.find h3) < z
Tactic:
have h6 : Nat.find h3 - 1 < Nat.find h3 :=
  Nat.sub_one_lt_of_le h5 Nat.le.refl
Proof state after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
⊢ s (Nat.find h3) < z