Theorem: aux_dvd_lemma (Jordan/IndexNormal.lean)

State before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ p
Tactic:
rw [← Nat.Coprime.dvd_mul_right _]
State after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ p * ?m.17725

α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ ℕ

α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.Coprime r ?m.17725

State before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.Coprime r (Nat.factorial (p - 1))
Tactic:
rw [Nat.coprime_iff_gcd_eq_one]
State after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.gcd r (Nat.factorial (p - 1)) = 1

State before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.gcd r (Nat.factorial (p - 1)) = 1
Tactic:
by_contra h
State after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
⊢ False

State before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
⊢ False
Tactic:
obtain ⟨l, hl, hl'⟩ := Nat.exists_prime_and_dvd h
State after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ Nat.gcd r (Nat.factorial (p - 1))
⊢ False

State before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ Nat.gcd r (Nat.factorial (p - 1))
⊢ False
Tactic:
rw [Nat.dvd_gcd_iff, Nat.Prime.dvd_factorial hl] at hl'
State after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ False

State before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ False
Tactic:
apply (lt_iff_not_ge p.pred p).mp (Nat.pred_lt (Nat.Prime.ne_zero hp))
State after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ Nat.pred p ≥ p

State before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ Nat.pred p ≥ p
Tactic:
rw [Nat.pred_eq_sub_one]
State after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p - 1 ≥ p

State before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p - 1 ≥ p
Tactic:
rw [ge_iff_le]
State after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p ≤ p - 1

State before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p ≤ p - 1
Tactic:
exact le_trans (hr hl hl'.left) hl'.right
State after:
no goals

State before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ p * ?m.17725
Tactic:
rw [Nat.mul_factorial_pred (Nat.Prime.pos hp)]
State after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ Nat.factorial p

State before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ Nat.factorial p
Tactic:
exact h
State after:
no goals