Theorem: lt24 (meetings/ex1.lean)

State before:
⊢ {x | |3 * x| < 24} = {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
ext x
State after:
case h
x : ℤ
⊢ x ∈ {x | |3 * x| < 24} ↔ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

State before:
case h
x : ℤ
⊢ x ∈ {x | |3 * x| < 24} ↔ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
constructor
State after:
case h.mp
x : ℤ
⊢ x ∈ {x | |3 * x| < 24} → x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

case h.mpr
x : ℤ
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7} → x ∈ {x | |3 * x| < 24}

State before:
case h.mp
x : ℤ
⊢ x ∈ {x | |3 * x| < 24} → x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
intro hlt
State after:
case h.mp
x : ℤ
hlt : x ∈ {x | |3 * x| < 24}
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

State before:
case h.mp
x : ℤ
hlt : x ∈ {x | |3 * x| < 24}
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
simp only [Set.mem_setOf_eq] at hlt
State after:
case h.mp
x : ℤ
hlt : |3 * x| < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

State before:
case h.mp
x : ℤ
hlt : |3 * x| < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
rw [abs_lt] at hlt
State after:
case h.mp
x : ℤ
hlt : -24 < 3 * x ∧ 3 * x < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

State before:
case h.mp
x : ℤ
hlt : -24 < 3 * x ∧ 3 * x < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
rcases hlt with ⟨hlt, hlt'⟩
State after:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}

State before:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, or_self]
State after:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
⊢ x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7

State before:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
⊢ x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7
Tactic:
by_contra hne
State after:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
hne :
  ¬(x = -7 ∨
      x = -6 ∨
        x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7)
⊢ False

State before:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
hne :
  ¬(x = -7 ∨
      x = -6 ∨
        x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7)
⊢ False
Tactic:
repeat rw [not_or] at hne
State after:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
hne :
  ¬x = -7 ∧
    ¬x = -6 ∧
      ¬x = -5 ∧
        ¬x = -4 ∧ ¬x = -3 ∧ ¬x = -2 ∧ ¬x = -1 ∧ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = 2 ∧ ¬x = 3 ∧ ¬x = 4 ∧ ¬x = 5 ∧ ¬x = 6 ∧ ¬x = 7
⊢ False

State before:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
hne :
  ¬x = -7 ∧
    ¬x = -6 ∧
      ¬x = -5 ∧
        ¬x = -4 ∧ ¬x = -3 ∧ ¬x = -2 ∧ ¬x = -1 ∧ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = 2 ∧ ¬x = 3 ∧ ¬x = 4 ∧ ¬x = 5 ∧ ¬x = 6 ∧ ¬x = 7
⊢ False
Tactic:
rcases hne with ⟨m7, m6, m5, m4, m3, m2, m1, z, p1, p2, p3, p4, p5, p6, p7⟩
State after:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
⊢ False

State before:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
⊢ False
Tactic:
have threedvd : ((3 : ℤ) ∣ 24) := by
  have : (24 : ℤ) = 3 * 8 := by ring_nf
  rw [this]
  simp only [dvd_mul_right]
State after:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
⊢ False

State before:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
⊢ False
Tactic:
rw [mul_comm, ←Int.lt_ediv_iff_mul_lt 3 (by simp) threedvd] at hlt'
State after:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
⊢ False

State before:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
⊢ False
Tactic:
have lt8 : x < 8 := by
  exact hlt'
State after:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
lt8 : x < 8
⊢ False

State before:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
lt8 : x < 8
⊢ False
Tactic:
have gt8 : -8 < x := by
  sorry
State after:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
lt8 : x < 8
gt8 : -8 < x
⊢ False

State before:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
lt8 : x < 8
gt8 : -8 < x
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
hne :
  ¬x = -7 ∧
    ¬x = -6 ∧
      ¬x = -5 ∧
        ¬x = -4 ∧ ¬x = -3 ∧ ¬x = -2 ∧ ¬x = -1 ∧ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = 2 ∧ ¬x = 3 ∧ ¬x = 4 ∧ ¬x = 5 ∧ ¬(x = 6 ∨ x = 7)
⊢ False
Tactic:
rw [not_or] at hne
State after:
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
hne :
  ¬x = -7 ∧
    ¬x = -6 ∧
      ¬x = -5 ∧
        ¬x = -4 ∧ ¬x = -3 ∧ ¬x = -2 ∧ ¬x = -1 ∧ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = 2 ∧ ¬x = 3 ∧ ¬x = 4 ∧ ¬x = 5 ∧ ¬x = 6 ∧ ¬x = 7
⊢ False

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
⊢ 3 ∣ 24
Tactic:
have : (24 : ℤ) = 3 * 8 := by ring_nf
State after:
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
this : 24 = 3 * 8
⊢ 3 ∣ 24

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
this : 24 = 3 * 8
⊢ 3 ∣ 24
Tactic:
rw [this]
State after:
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
this : 24 = 3 * 8
⊢ 3 ∣ 3 * 8

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
this : 24 = 3 * 8
⊢ 3 ∣ 3 * 8
Tactic:
simp only [dvd_mul_right]
State after:
no goals

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
⊢ 24 = 3 * 8
Tactic:
ring_nf
State after:
no goals

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : x * 3 < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
⊢ 0 < 3
Tactic:
simp
State after:
no goals

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
⊢ x < 8
Tactic:
exact hlt'
State after:
no goals

State before:
x : ℤ
hlt : -24 < 3 * x
hlt' : x < 24 / 3
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
threedvd : 3 ∣ 24
lt8 : x < 8
⊢ -8 < x
Tactic:
sorry
State after:
no goals

State before:
case h.mpr
x : ℤ
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7} → x ∈ {x | |3 * x| < 24}
Tactic:
intro hor
State after:
case h.mpr
x : ℤ
hor : x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
⊢ x ∈ {x | |3 * x| < 24}

State before:
case h.mpr
x : ℤ
hor : x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
⊢ x ∈ {x | |3 * x| < 24}
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, or_self] at hor
State after:
case h.mpr
x : ℤ
hor :
  x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7
⊢ x ∈ {x | |3 * x| < 24}

State before:
case h.mpr
x : ℤ
hor :
  x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7
⊢ x ∈ {x | |3 * x| < 24}
Tactic:
simp only [Set.mem_setOf_eq]
State after:
case h.mpr
x : ℤ
hor :
  x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7
⊢ |3 * x| < 24

State before:
case h.mpr
x : ℤ
hor :
  x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7
⊢ |3 * x| < 24
Tactic:
rcases hor with (rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl)
State after:
case h.mpr.inl

⊢ |3 * -7| < 24

case h.mpr.inr.inl

⊢ |3 * -6| < 24

case h.mpr.inr.inr.inl

⊢ |3 * -5| < 24

case h.mpr.inr.inr.inr.inl

⊢ |3 * -4| < 24

case h.mpr.inr.inr.inr.inr.inl

⊢ |3 * -3| < 24

case h.mpr.inr.inr.inr.inr.inr.inl

⊢ |3 * -2| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * -1| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 0| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 1| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 2| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 3| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 4| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 5| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 6| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |3 * 7| < 24

State before:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |3 * 7| < 24
Tactic:
ring_nf
State after:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |21| < 24

State before:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |21| < 24
Tactic:
simp only [abs_neg, abs_lt]
State after:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ -24 < 21 ∧ 21 < 24

State before:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ -24 < 21 ∧ 21 < 24
Tactic:
constructor
State after:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl.left

⊢ -24 < 21

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl.right

⊢ 21 < 24

State before:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl.left

⊢ -24 < 21
Tactic:
norm_num
State after:
no goals

State before:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl.right

⊢ 21 < 24
Tactic:
norm_num
State after:
no goals