internlm/Lean-Github huggingface dataset:
Theorem: chapter44.friendship_theorem
Proof state before:
case h
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x✝ : V
hx_left : ¬v = x✝
hx_right : ¬G.Adj v x✝
this : (G.neighborFinset v).card = 2
x : V
⊢ x ∈ G.neighborFinset v → x ∈ univ.erase v
Tactic:
rw [mem_neighborFinset, Finset.mem_erase]
Proof state after:
case h
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x✝ : V
hx_left : ¬v = x✝
hx_right : ¬G.Adj v x✝
this : (G.neighborFinset v).card = 2
x : V
⊢ G.Adj v x → x ≠ v ∧ x ∈ univ
Theorem: chapter44.friendship_theorem
Proof state before:
case h
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x✝ : V
hx_left : ¬v = x✝
hx_right : ¬G.Adj v x✝
this : (G.neighborFinset v).card = 2
x : V
⊢ G.Adj v x → x ≠ v ∧ x ∈ univ
Tactic:
exact fun h => ⟨(G.ne_of_adj h).symm, Finset.mem_univ _⟩
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof state before:
case h.e'_3
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ (univ.erase v).card = 2
Tactic:
convert_to _ = Fintype.card V - 1
Proof state after:
case h.e'_3
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ 2 = Fintype.card V - 1

case h.e'_3.convert_2
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ (univ.erase v).card = Fintype.card V - 1
Theorem: chapter44.friendship_theorem
Proof state before:
case h.e'_3
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ 2 = Fintype.card V - 1
Tactic:
rw [(show Fintype.card V = n by rfl), eq₁]
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof state before:
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ Fintype.card V = n
Tactic:
rfl
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof state before:
case h.e'_3.convert_2
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ (univ.erase v).card = Fintype.card V - 1
Tactic:
exact Finset.card_erase_of_mem (Finset.mem_univ _)
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof state before:
case h₂.convert_2
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ 2 ≤ (G.neighborFinset v).card
Tactic:
rw [hregular]
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof state before:
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
hregular : G.IsRegularOfDegree k
n : ℕ := Fintype.card V
eq₁ : n = k ^ 2 - k + 1
this : 2 < k
A : Matrix V V R := adjMatrix R G
⊢ A ^ 2 = (k - 1) • 1 + of fun x x => 1
Tactic:
sorry
Proof state after:
no goals
Theorem: le_abs_of_dvd
Proof state before:
i j : ℤ
gj : 0 ≠ j
h : i ∣ j
⊢ |i| ≤ |j|
Tactic:
dsimp [Dvd.dvd] at h
Proof state after:
i j : ℤ
gj : 0 ≠ j
h : ∃ c, j = i * c
⊢ |i| ≤ |j|
Theorem: le_abs_of_dvd
Proof state before:
i j : ℤ
gj : 0 ≠ j
h : ∃ c, j = i * c
⊢ |i| ≤ |j|
Tactic:
cases' h with c h₀
Proof state after:
case intro
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
⊢ |i| ≤ |j|
Theorem: le_abs_of_dvd
Proof state before:
case intro
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
⊢ |i| ≤ |j|
Tactic:
cases' em (c = 0) with hc h
Proof state after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
⊢ |i| ≤ |j|

case intro.inr
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |j|
Theorem: le_abs_of_dvd
Proof state before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
⊢ |i| ≤ |j|
Tactic:
by_contra
Proof state after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
Theorem: le_abs_of_dvd
Proof state before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
Tactic:
rw [hc] at h₀
Proof state after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * 0
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
Theorem: le_abs_of_dvd
Proof state before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * 0
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
Tactic:
simp only [mul_zero] at h₀
Proof state after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
hc : c = 0
x✝ : ¬|i| ≤ |j|
h₀ : j = 0
⊢ False
Theorem: le_abs_of_dvd
Proof state before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
hc : c = 0
x✝ : ¬|i| ≤ |j|
h₀ : j = 0
⊢ False
Tactic:
exact gj (Eq.symm h₀)
Proof state after:
no goals
Theorem: le_abs_of_dvd
Proof state before:
case intro.inr
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |j|
Tactic:
calc
  |i| ≤ (|i|)*|c| := by
      exact le_mul_of_le_of_one_le' rfl.ge (Int.one_le_abs h) (abs_nonneg c) (abs_nonneg i)
    _ = |i*c| := Eq.symm (abs_mul i c)
    _ = |j| := by rw [Eq.symm h₀]
Proof state after:
no goals
Theorem: le_abs_of_dvd
Proof state before:
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |i| * |c|
Tactic:
exact le_mul_of_le_of_one_le' rfl.ge (Int.one_le_abs h) (abs_nonneg c) (abs_nonneg i)
Proof state after:
no goals
Theorem: le_abs_of_dvd
Proof state before:
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i * c| = |j|
Tactic:
rw [Eq.symm h₀]
Proof state after:
no goals
Theorem: phi_dvd
Proof state before:
n : ℕ
⊢ phi n ∣ X ^ n - 1
Tactic:
rw [phi]
Proof state after:
n : ℕ
⊢ cyclotomic n ℤ ∣ X ^ n - 1
Theorem: phi_dvd
Proof state before:
n : ℕ
⊢ cyclotomic n ℤ ∣ X ^ n - 1
Tactic:
exact cyclotomic.dvd_X_pow_sub_one n ℤ
Proof state after:
no goals
Theorem: phi_div_2
Proof state before:
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1
Tactic:
have h_proper_div : k ∈ n.properDivisors := Nat.mem_properDivisors.mpr ⟨h₂, h₃⟩
Proof state after:
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
h_proper_div : k ∈ n.properDivisors
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1
Theorem: phi_div_2
Proof state before:
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
h_proper_div : k ∈ n.properDivisors
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1
Tactic:
exact X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd ℤ h_proper_div
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
let a := lamb.re
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
let b := lamb.im
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
intro h
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have h_lamb: lamb ≠ 1 := by sorry
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have h_a_lt_one: ‖a‖ < 1 := by sorry
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have h_ineq :
    ‖((X - C lamb).eval (q : ℂ))‖^2 > ((q : ℝ) - 1)^2  := by
  calc
    _ = ‖q - lamb‖^2 := by
      simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
    _ = ‖(q : ℂ) - a - I*b‖^2 := by sorry
    _ = ‖(q : ℂ) - a‖^2 + ‖b‖^2 := by sorry
    _ = (q : ℝ)^2 - 2*‖a‖*q + ‖a‖^2 + ‖b‖^2 := by sorry
    _ > ((q : ℝ) - 1)^2 := by sorry
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have : 0 ≤ ((q : ℝ) - 1)^2 := by exact sq_nonneg ((q : ℝ) - 1)
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have g := (Real.sqrt_lt_sqrt_iff this).mpr (h_ineq)
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have : Real.sqrt (((q:ℝ) - 1) ^ 2) = ((q : ℝ) - 1) := by sorry
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
rw [this] at g
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
rw [norm_eq_abs, Real.sqrt_sq] at g
Proof state after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < Complex.abs (eval (↑q) (X - C lamb))
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (Complex.abs (eval (↑q) (X - C lamb)) ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ 0 ≤ Complex.abs (eval (↑q) (X - C lamb))
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ lamb ≠ 1
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
⊢ ‖a‖ < 1
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
Tactic:
calc
  _ = ‖q - lamb‖^2 := by
    simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
  _ = ‖(q : ℂ) - a - I*b‖^2 := by sorry
  _ = ‖(q : ℂ) - a‖^2 + ‖b‖^2 := by sorry
  _ = (q : ℝ)^2 - 2*‖a‖*q + ‖a‖^2 + ‖b‖^2 := by sorry
  _ > ((q : ℝ) - 1)^2 := by sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ ^ 2 = ‖↑q - lamb‖ ^ 2
Tactic:
simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖↑q - lamb‖ ^ 2 = ‖↑q - ↑a - I * ↑b‖ ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖↑q - ↑a - I * ↑b‖ ^ 2 = ‖↑q - ↑a‖ ^ 2 + ‖b‖ ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖↑q - ↑a‖ ^ 2 + ‖b‖ ^ 2 = ↑q ^ 2 - 2 * ‖a‖ * ↑q + ‖a‖ ^ 2 + ‖b‖ ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ↑q ^ 2 - 2 * ‖a‖ * ↑q + ‖a‖ ^ 2 + ‖b‖ ^ 2 > (↑q - 1) ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
⊢ 0 ≤ (↑q - 1) ^ 2
Tactic:
exact sq_nonneg ((q : ℝ) - 1)
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ((↑q - 1) ^ 2).sqrt = ↑q - 1
Tactic:
sorry
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < Complex.abs (eval (↑q) (X - C lamb))
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
exact g
Proof state after:
no goals
Theorem: h_lamb_gt_q_sub_one
Proof state before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (Complex.abs (eval (↑q) (X - C lamb)) ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ 0 ≤ Complex.abs (eval (↑q) (X - C lamb))
Tactic:
aesop
Proof state after:
no goals
Theorem: div_of_qpoly_div
Proof state before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
hn : 0 < n
H : q ^ k - 1 ∣ q ^ n - 1
⊢ k ∣ n
Tactic:
revert H
Proof state after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
hn : 0 < n
⊢ q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Theorem: div_of_qpoly_div
Proof state before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
hn : 0 < n
⊢ q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Tactic:
revert hn
Proof state after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Theorem: div_of_qpoly_div
Proof state before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Tactic:
apply Nat.strongInductionOn n
Proof state after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ ∀ (n : ℕ), (∀ m < n, 0 < m → q ^ k - 1 ∣ q ^ m - 1 → k ∣ m) → 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Theorem: div_of_qpoly_div
Proof state before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
⊢ ∀ (n : ℕ), (∀ m < n, 0 < m → q ^ k - 1 ∣ q ^ m - 1 → k ∣ m) → 0 < n → q ^ k - 1 ∣ q ^ n - 1 → k ∣ n
Tactic:
intro m h hm H
Proof state after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
⊢ k ∣ m
Theorem: div_of_qpoly_div
Proof state before:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
⊢ k ∣ m
Tactic:
have hq' := zero_lt_of_lt hq
Proof state after:
R : Type ?u.38021
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
k n q : ℕ
hq : 1 < q
hk : 0 < k
m : ℕ
h : ∀ m_1 < m, 0 < m_1 → q ^ k - 1 ∣ q ^ m_1 - 1 → k ∣ m_1
hm : 0 < m
H : q ^ k - 1 ∣ q ^ m - 1
hq' : 0 < q
⊢ k ∣ m