awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ LT.lt (α := ℚ) 0 3

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ LE.le (α := ℚ) 3 (↑(↑p : ℕ) : ℚ)

Tactic:
exact_mod_cast H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹

Tactic:
have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ LT.lt (α := ℚ) 0 3

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ LE.le (α := ℚ) 3 (↑(↑q : ℕ) : ℚ)

Tactic:
exact_mod_cast h3q
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹

Tactic:
have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3q)
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ LT.lt (α := ℚ) 0 3

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ LE.le (α := ℚ) 3 (↑(↑r : ℕ) : ℚ)

Tactic:
exact_mod_cast h3r
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 3⁻¹

Tactic:
have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3r)
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ HAdd.hAdd (α := ℚ) 3⁻¹ 3⁻¹ + 3⁻¹

Tactic:
add_le_add (add_le_add hp hq) hr

Premises used: add_le_add
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ HAdd.hAdd (α := ℚ) 3⁻¹ 3⁻¹ + 3⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 3⁻¹
add_le_add : HAdd.hAdd (α := ℚ) 3⁻¹ 3⁻¹ + 3⁻¹ = 1
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1

Tactic:
calc
    (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
    _ = 1 := by norm_num

Premises used: PNat.val, add_le_add, Nat.cast
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
contrapose! : ∀ (H : 4 ≤ q), sumInv {2, q, r} ≤ 1
⊢ q < 4

Tactic:
contrapose! H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
rw : HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
⊢ sumInv {2, q, r} ≤ 1

Tactic:
rw [sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ 4 ≤ r

Tactic:
have h4r := H.trans hqr
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
⊢ LT.lt (α := ℚ) 0 4

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
⊢ LE.le (α := ℚ) 4 (↑(↑q : ℕ) : ℚ)

Tactic:
exact_mod_cast H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
⊢ LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹

Tactic:
have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ LT.lt (α := ℚ) 0 4

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ LE.le (α := ℚ) 4 (↑(↑r : ℕ) : ℚ)

Tactic:
exact_mod_cast h4r
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 4⁻¹

Tactic:
have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h4r)
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ HAdd.hAdd (α := ℚ) 2⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ HAdd.hAdd (α := ℚ) 2⁻¹ 4⁻¹ + 4⁻¹

Tactic:
add_le_add (add_le_add le_rfl hq) hr

Premises used: le_rfl, add_le_add
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ HAdd.hAdd (α := ℚ) 2⁻¹ 4⁻¹ + 4⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 4⁻¹
add_le_add : HAdd.hAdd (α := ℚ) 2⁻¹ 4⁻¹ + 4⁻¹ = 1
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1

Tactic:
calc
    (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
    _ = 1 := by norm_num

Premises used: PNat.val, le_rfl, add_le_add, Nat.cast, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
contrapose! : ∀ (H : 6 ≤ r), sumInv {2, 3, r} ≤ 1
⊢ r < 6

Tactic:
contrapose! H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
rw : HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
⊢ sumInv {2, 3, r} ≤ 1

Tactic:
rw [sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
⊢ LT.lt (α := ℚ) 0 6

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
⊢ LE.le (α := ℚ) 6 (↑(↑r : ℕ) : ℚ)

Tactic:
exact_mod_cast H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
⊢ LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 6⁻¹

Tactic:
have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 6⁻¹
⊢ HAdd.hAdd (α := ℚ) 2⁻¹ 3⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ HAdd.hAdd (α := ℚ) 2⁻¹ 3⁻¹ + 6⁻¹

Tactic:
add_le_add (add_le_add le_rfl le_rfl) hr

Premises used: le_rfl, add_le_add
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 6⁻¹
⊢ HAdd.hAdd (α := ℚ) 2⁻¹ 3⁻¹ + 6⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 6 ≤ r
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 6⁻¹
add_le_add : HAdd.hAdd (α := ℚ) 2⁻¹ 3⁻¹ + 6⁻¹ = 1
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1

Tactic:
calc
    (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
    _ = 1 := by norm_num

Premises used: PNat.val, le_rfl, add_le_add, Nat.cast, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ p < 3

Tactic:
have hp3 : p < 3 := lt_three hpq hqr H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p < 3
⊢ Membership.mem (γ := Finset ℕ+) (Finset.Iio 3) p

Tactic:
replace hp3 := Finset.mem_Iio.mpr hp3
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : Membership.mem (γ := Finset ℕ+) (Finset.Iio 3) p
⊢ Membership.mem (γ := Multiset ℕ+) {1, 2} p

Tactic:
conv at hp3 => change p ∈ ({1, 2} : Multiset ℕ+)

Premises used: Insert.insert, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : Membership.mem (γ := Multiset ℕ+) {1, 2} p
0 : ∀ (hpq : 1 ≤ q) (H : 1 < sumInv {1, q, r}), Admissible {1, q, r}
1 : ∀ (hpq : 2 ≤ q) (H : 1 < sumInv {2, q, r}), Admissible {2, q, r}
⊢ Admissible {p, q, r}

Tactic:
fin_cases hp3
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}

Tactic:
admissible_A' q r

Premises used: ADEInequality.admissible_A', ADEInequality.A'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
hpq : 1 ≤ q
H : 1 < sumInv {1, q, r}
⊢ Admissible {1, q, r}

Tactic:
exact admissible_A' q r

Premises used: ADEInequality.admissible_A'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ q < 4

Tactic:
have hq4 : q < 4 := lt_four hqr H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Membership.mem (γ := Finset ℕ+) (Finset.Ico 2 4) q

Tactic:
replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : Membership.mem (γ := Finset ℕ+) (Finset.Ico 2 4) q
⊢ Membership.mem (γ := Multiset ℕ+) {2, 3} q

Tactic:
conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)

Premises used: Insert.insert, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : Membership.mem (γ := Multiset ℕ+) {2, 3} q
1 : ∀ (hqr : 2 ≤ r) (H : 1 < sumInv {2, 2, r}), Admissible {2, 2, r}
h : ∀ (hqr : 3 ≤ r) (H : 1 < sumInv {2, 3, r}), Admissible {2, 3, r}
⊢ Admissible {2, q, r}

Tactic:
fin_cases hq4
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

Tactic:
admissible_D' r

Premises used: ADEInequality.D', ADEInequality.admissible_D'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
hqr : 2 ≤ r
H : 1 < sumInv {2, 2, r}
⊢ Admissible {2, 2, r}

Tactic:
exact admissible_D' r

Premises used: ADEInequality.admissible_D'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ r < 6

Tactic:
have hr6 : r < 6 := lt_six H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Membership.mem (γ := Finset ℕ+) (Finset.Ico 3 6) r

Tactic:
replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : Membership.mem (γ := Finset ℕ+) (Finset.Ico 3 6) r
⊢ Membership.mem (γ := Multiset ℕ+) {3, 4, 5} r

Tactic:
conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)

Premises used: Insert.insert, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : Membership.mem (γ := Multiset ℕ+) {3, 4, 5} r
1 : ∀ (H : 1 < sumInv {2, 3, 3}), Admissible {2, 3, 3}
h : ∀ (H : 1 < sumInv {2, 3, 4}), Admissible {2, 3, 4}
h_1 : ∀ (H : 1 < sumInv {2, 3, 5}), Admissible {2, 3, 5}
⊢ Admissible {2, 3, r}

Tactic:
fin_cases hr6
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}

Tactic:
admissible_E6

Premises used: ADEInequality.E', ADEInequality.admissible_E6, ADEInequality.E6
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}

Tactic:
exact admissible_E6

Premises used: ADEInequality.admissible_E6
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

Tactic:
admissible_E7

Premises used: ADEInequality.admissible_E7, ADEInequality.E', ADEInequality.E7
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

Tactic:
exact admissible_E7

Premises used: ADEInequality.admissible_E7
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
admissible_E8

Premises used: ADEInequality.E', ADEInequality.E8, ADEInequality.admissible_E8
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
exact admissible_E8

Premises used: ADEInequality.admissible_E8
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
⊢ (p ≤ q ∧ p ≤ r) ∧ q ≤ r

Tactic:
simpa using hs.pairwise

Premises used: List.SortedLE.pairwise
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
⊢ q ≤ r

Tactic:
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r := by simpa using hs.pairwise

Premises used: LE.le, And
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
hqr : q ≤ r
⊢ p ≤ q

Tactic:
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r := by simpa using hs.pairwise

Premises used: LE.le, And
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible (↑[p, q, r] : Multiset ℕ+)

Tactic:
admissible_of_one_lt_sumInv_aux' hpq hqr H

Premises used: Multiset.cons, ADEInequality.admissible_of_one_lt_sumInv_aux', Multiset.ofList
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible (↑[p, q, r] : Multiset ℕ+)

Tactic:
exact admissible_of_one_lt_sumInv_aux' hpq hqr H

Premises used: ADEInequality.admissible_of_one_lt_sumInv_aux'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
⊢ S.SortedLE

Tactic:
have hS : S.SortedLE := (pairwise_sort _ _).sortedLE
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
⊢ {p, q, r} = (↑S : Multiset ℕ+)

Tactic:
have hpqr : ({p, q, r} : Multiset ℕ+) = S := (sort_eq {p, q, r} LE.le).symm
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
rw :
  (∃ (q : ℕ+) (r : ℕ+), A' q r = (↑S : Multiset ℕ+)) ∨
    (∃ (r : ℕ+), D' r = (↑S : Multiset ℕ+)) ∨
      E' 3 = (↑S : Multiset ℕ+) ∨ E' 4 = (↑S : Multiset ℕ+) ∨ E' 5 = (↑S : Multiset ℕ+)
⊢ (∃ (q_1 : ℕ+) (r_1 : ℕ+), A' q_1 r_1 = {p, q, r}) ∨
    (∃ (r_1 : ℕ+), D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}

Tactic:
rw [hpqr]
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
⊢ 1 < sumInv (↑S : Multiset ℕ+)

Tactic:
rw [hpqr] at H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
H₁ : 1 < sumInv (↑S : Multiset ℕ+)
⊢ S.SortedLE

Tactic:
rw [hpqr] at H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
H₁ : 1 < sumInv (↑S : Multiset ℕ+)
hS₁ : S.SortedLE
⊢ {p, q, r} = (↑S : Multiset ℕ+)

Tactic:
rw [hpqr] at H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
H : 1 < sumInv (↑S : Multiset ℕ+)
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
apply : S.length = 3
⊢ (∃ (q : ℕ+) (r : ℕ+), A' q r = (↑S : Multiset ℕ+)) ∨
    (∃ (r : ℕ+), D' r = (↑S : Multiset ℕ+)) ∨
      E' 3 = (↑S : Multiset ℕ+) ∨ E' 4 = (↑S : Multiset ℕ+) ∨ E' 5 = (↑S : Multiset ℕ+)

Tactic:
apply admissible_of_one_lt_sumInv_aux hS _ H

Premises used: ADEInequality.admissible_of_one_lt_sumInv_aux
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
H : 1 < sumInv (↑S : Multiset ℕ+)
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
⊢ S.length = 3

Tactic:
simp only [S, insert_eq_cons, length_sort, card_cons, card_singleton]

Premises used: Multiset.card_singleton, Multiset.card_cons, Multiset.length_sort, Multiset.insert_eq_cons
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
⊢ 1 < sumInv {p, q, r} ↔ Admissible {p, q, r}

Tactic:
⟨admissible_of_one_lt_sumInv, Admissible.one_lt_sumInv⟩

Premises used: ADEInequality.admissible_of_one_lt_sumInv, ADEInequality.Admissible.one_lt_sumInv, Iff.intro
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
h :
  ∀ (t : ℝ)
    (h : Set.Ico (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t = Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t)
    (ht : t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)
⊢ ∀ᵐ (t : ℝ),
    t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)

Tactic:
filter_upwards [Ico_ae_eq_Icc] with t h ht

Premises used: MeasureTheory.Ico_ae_eq_Icc
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t = Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t
ht : t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h₁ h₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m n, c k) (∑ k ∈ Icc m n, c k)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)

Tactic:
rw [Nat.floor_eq_on_Ico _ _ (h.mpr ht)]

Premises used: Eq.mpr, Nat.floor_eq_on_Ico
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
have h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc n (n + 1) :=
    Set.uIoc_of_le h ▸ Set.Ioc_subset_Icc_self.trans <| Set.Icc_subset_Icc h₁ h₂
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ [[t₁, t₂]] ⊆ Set.Icc a b

Tactic:
have h_inc₂ : Set.uIcc t₁ t₂ ⊆ Set.Icc a b := Set.uIcc_of_le h ▸ Set.Icc_subset_Icc h₃ h₄
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
rw :
  Eq.{u_1 + 1} (α := 𝕜) (∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    (∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k)
rw₁ : IntervalIntegrable (deriv f) volume t₁ t₂
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k

Tactic:
rw [← integral_deriv_eq_sub (fun t ht ↦ hf_diff t (h_inc₂ ht)),
      ← intervalIntegral.integral_mul_const]

Premises used: intervalIntegral.integral_deriv_eq_sub, intervalIntegral.integral_mul_const
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    (∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k)

Tactic:
integral_congr_ae ?_

Premises used: intervalIntegral.integral_congr_ae
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
refine : ∀ᵐ (x : ℝ), x ∈ Ι t₁ t₂ → deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k = deriv f x * ∑ k ∈ Icc 0 n, c k
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    (∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k)

Tactic:
refine integral_congr_ae ?_
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
h₅ :
  ∀ (t : ℝ)
    (h :
      t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
        Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc 0 ⌊t⌋₊, c k) (∑ k ∈ Icc 0 n, c k))
    (h' : t ∈ Ι t₁ t₂), deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
⊢ ∀ᵐ (x : ℝ), x ∈ Ι t₁ t₂ → deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k = deriv f x * ∑ k ∈ Icc 0 n, c k

Tactic:
filter_upwards [sumlocc c n] with t h h'

Premises used: _private.0.abelSummationProof.sumlocc
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h_1 : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
t : ℝ
h :
  t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc 0 ⌊t⌋₊, c k) (∑ k ∈ Icc 0 n, c k)
h' : t ∈ Ι t₁ t₂
h₅ h₆ : deriv f t * ∑ k ∈ Icc 0 n, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
⊢ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k

Tactic:
rw [h (h_inc₁ h')]