internlm/Lean-Github huggingface dataset:
Theorem: lt24
Proof 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⟩
Proof 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
Theorem: lt24
Proof 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]
Proof 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
Theorem: lt24
Proof 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'
Proof 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
Theorem: lt24
Proof 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'
Proof 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
Theorem: lt24
Proof 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
Proof 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
Theorem: lt24
Proof 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
Proof state after:
no goals
Theorem: lt24
Proof 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
Proof 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
Theorem: lt24
Proof 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
Proof 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
Theorem: lt24
Proof 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]
Proof 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
Theorem: lt24
Proof 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]
Proof state after:
no goals
Theorem: lt24
Proof 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
Proof state after:
no goals
Theorem: lt24
Proof 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
Proof state after:
no goals
Theorem: lt24
Proof 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'
Proof state after:
no goals
Theorem: lt24
Proof 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
Proof state after:
no goals
Theorem: lt24
Proof 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
Proof 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}
Theorem: lt24
Proof 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
Proof 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}
Theorem: lt24
Proof 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]
Proof 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
Theorem: lt24
Proof 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)
Proof 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
Theorem: lt24
Proof 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
Proof state after:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |21| < 24
Theorem: lt24
Proof 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]
Proof state after:
case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ -24 < 21 ∧ 21 < 24
Theorem: lt24
Proof 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
Proof 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
Theorem: lt24
Proof 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
Proof state after:
no goals
Theorem: lt24
Proof 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
Proof state after:
no goals
Theorem: circle_area_subset_square_area
Proof state before:
⊢ {p | p.1 ^ 2 + p.2 ^ 2 < 1} ⊆ Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1
Tactic:
intros p hmem
Proof state after:
p : ℝ × ℝ
hmem : p ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1
Theorem: circle_area_subset_square_area
Proof state before:
p : ℝ × ℝ
hmem : p ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1
Tactic:
simp at *
Proof state after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
Theorem: circle_area_subset_square_area
Proof state before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
Tactic:
simp only [sq_le_one_iff_abs_le_one, abs_le] at h
Proof state after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : (-1 ≤ p.1 ∧ p.1 ≤ 1) ∧ -1 ≤ p.2 ∧ p.2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
Theorem: circle_area_subset_square_area
Proof state before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : (-1 ≤ p.1 ∧ p.1 ≤ 1) ∧ -1 ≤ p.2 ∧ p.2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
Tactic:
exact ⟨⟨h.1.1, h.2.1⟩, ⟨h.1.2, h.2.2⟩⟩
Proof state after:
no goals
Theorem: circle_area_subset_square_area
Proof state before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Tactic:
have p1nonneg := sq_nonneg (p.1)
Proof state after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Theorem: circle_area_subset_square_area
Proof state before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Tactic:
have p2nonneg := sq_nonneg (p.2)
Proof state after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Theorem: circle_area_subset_square_area
Proof state before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Tactic:
constructor
Proof state after:
case left
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1

case right
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.2 ^ 2 ≤ 1
Theorem: circle_area_subset_square_area
Proof state before:
case left
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: circle_area_subset_square_area
Proof state before:
case right
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.2 ^ 2 ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: square_area_not_subset_circle_area
Proof state before:
⊢ ¬Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1 ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
Tactic:
intro sub
Proof state after:
sub : Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1 ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Theorem: square_area_not_subset_circle_area
Proof state before:
sub : Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1 ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Tactic:
simp at *
Proof state after:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Theorem: square_area_not_subset_circle_area
Proof state before:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Tactic:
have hel : ((-1, -1) : ℝ × ℝ) ∈ Set.Icc (-1, -1) (1, 1) := by
  simp
Proof state after:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
⊢ False
Theorem: square_area_not_subset_circle_area
Proof state before:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
⊢ False
Tactic:
specialize sub hel
Proof state after:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : (-1, -1) ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Theorem: square_area_not_subset_circle_area
Proof state before:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : (-1, -1) ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Tactic:
simp at sub
Proof state after:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : 1 < 0
⊢ False
Theorem: square_area_not_subset_circle_area
Proof state before:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : 1 < 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: square_area_not_subset_circle_area
Proof state before:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
Tactic:
simp
Proof state after:
no goals
Theorem: nat_subset_real
Proof state before:
⊢ heterogeneous_subset Set.univ Set.univ
Tactic:
intro n _
Proof state after:
n : ℕ
a✝ : n ∈ Set.univ
⊢ Coe.coe n ∈ Set.univ
Theorem: nat_subset_real
Proof state before:
n : ℕ
a✝ : n ∈ Set.univ
⊢ Coe.coe n ∈ Set.univ
Tactic:
simp only [Set.mem_univ]
Proof state after:
no goals
Theorem: union_even_up_to
Proof state before:
⊢ ⋃ j ∈ Set.univ, even_up_to j = {m | Even m}
Tactic:
simp
Proof state after:
⊢ ⋃ j, even_up_to j = {m | Even m}
Theorem: union_even_up_to
Proof state before:
⊢ ⋃ j, even_up_to j = {m | Even m}
Tactic:
simp_rw [even_up_to, Set.ext_iff]
Proof state after:
⊢ ∀ (x : ℕ), x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ {m | Even m}
Theorem: union_even_up_to
Proof state before:
⊢ ∀ (x : ℕ), x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ {m | Even m}
Tactic:
intro x
Proof state after:
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ {m | Even m}
Theorem: union_even_up_to
Proof state before:
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ {m | Even m}
Tactic:
constructor
Proof state after:
case mp
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ {m | Even m}

case mpr
x : ℕ
⊢ x ∈ {m | Even m} → x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m}
Theorem: union_even_up_to
Proof state before:
case mp
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ {m | Even m}
Tactic:
simp
Proof state after:
no goals
Theorem: union_even_up_to
Proof state before:
case mpr
x : ℕ
⊢ x ∈ {m | Even m} → x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m}
Tactic:
simp
Proof state after:
case mpr
x : ℕ
⊢ Even x → (∃ x_1, x ≤ 2 * x_1) ∧ Even x
Theorem: union_even_up_to
Proof state before:
case mpr
x : ℕ
⊢ Even x → (∃ x_1, x ≤ 2 * x_1) ∧ Even x
Tactic:
intro heven
Proof state after:
case mpr
x : ℕ
heven : Even x
⊢ (∃ x_1, x ≤ 2 * x_1) ∧ Even x
Theorem: union_even_up_to
Proof state before:
case mpr
x : ℕ
heven : Even x
⊢ (∃ x_1, x ≤ 2 * x_1) ∧ Even x
Tactic:
constructor
Proof state after:
case mpr.left
x : ℕ
heven : Even x
⊢ ∃ x_1, x ≤ 2 * x_1

case mpr.right
x : ℕ
heven : Even x
⊢ Even x
Theorem: union_even_up_to
Proof state before:
case mpr.left
x : ℕ
heven : Even x
⊢ ∃ x_1, x ≤ 2 * x_1
Tactic:
use x
Proof state after:
case h
x : ℕ
heven : Even x
⊢ x ≤ 2 * x
Theorem: union_even_up_to
Proof state before:
case h
x : ℕ
heven : Even x
⊢ x ≤ 2 * x
Tactic:
linarith
Proof state after:
no goals
Theorem: union_even_up_to
Proof state before:
case mpr.right
x : ℕ
heven : Even x
⊢ Even x
Tactic:
exact heven
Proof state after:
no goals
Theorem: inter_even_up_to
Proof state before:
⊢ ⋂ j ∈ Set.univ, even_up_to j = Set.singleton 0
Tactic:
simp
Proof state after:
⊢ ⋂ j, even_up_to j = Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
⊢ ⋂ j, even_up_to j = Set.singleton 0
Tactic:
simp_rw [even_up_to, Set.ext_iff]
Proof state after:
⊢ ∀ (x : ℕ), x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
⊢ ∀ (x : ℕ), x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0
Tactic:
intro x
Proof state after:
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0
Tactic:
constructor
Proof state after:
case mp
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ Set.singleton 0

case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m}
Theorem: inter_even_up_to
Proof state before:
case mp
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ Set.singleton 0
Tactic:
simp
Proof state after:
case mp
x : ℕ
⊢ (∀ (i : ℕ), x ≤ 2 * i ∧ Even x) → x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
case mp
x : ℕ
⊢ (∀ (i : ℕ), x ≤ 2 * i ∧ Even x) → x ∈ Set.singleton 0
Tactic:
intro imp
Proof state after:
case mp
x : ℕ
imp : ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
⊢ x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
case mp
x : ℕ
imp : ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
⊢ x ∈ Set.singleton 0
Tactic:
specialize imp 0
Proof state after:
case mp
x : ℕ
imp : x ≤ 2 * 0 ∧ Even x
⊢ x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
case mp
x : ℕ
imp : x ≤ 2 * 0 ∧ Even x
⊢ x ∈ Set.singleton 0
Tactic:
simp at imp
Proof state after:
case mp
x : ℕ
imp : x = 0 ∧ Even x
⊢ x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
case mp
x : ℕ
imp : x = 0 ∧ Even x
⊢ x ∈ Set.singleton 0
Tactic:
rcases imp with ⟨hle, _⟩
Proof state after:
case mp.intro
x : ℕ
hle : x = 0
right✝ : Even x
⊢ x ∈ Set.singleton 0
Theorem: inter_even_up_to
Proof state before:
case mp.intro
x : ℕ
hle : x = 0
right✝ : Even x
⊢ x ∈ Set.singleton 0
Tactic:
exact Set.mem_singleton_of_eq hle
Proof state after:
no goals
Theorem: inter_even_up_to
Proof state before:
case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m}
Tactic:
simp
Proof state after:
case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
Theorem: inter_even_up_to
Proof state before:
case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
Tactic:
intros mem i
Proof state after:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
⊢ x ≤ 2 * i ∧ Even x
Theorem: inter_even_up_to
Proof state before:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
⊢ x ≤ 2 * i ∧ Even x
Tactic:
have mem' := Set.eq_of_mem_singleton mem
Proof state after:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i ∧ Even x
Theorem: inter_even_up_to
Proof state before:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i ∧ Even x
Tactic:
constructor
Proof state after:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i

case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even x
Theorem: inter_even_up_to
Proof state before:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i
Tactic:
rw [mem']
Proof state after:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ 0 ≤ 2 * i
Theorem: inter_even_up_to
Proof state before:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ 0 ≤ 2 * i
Tactic:
linarith
Proof state after:
no goals
Theorem: inter_even_up_to
Proof state before:
case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even x
Tactic:
rw [mem']
Proof state after:
case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even 0
Theorem: inter_even_up_to
Proof state before:
case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even 0
Tactic:
simp
Proof state after:
no goals
Theorem: inter_rectangles
Proof state before:
⊢ ⋂ α ∈ Set.Icc 0 1, rectangle α = Set.singleton (1, 0)
Tactic:
simp only [ge_iff_le, zero_le_one, not_true, gt_iff_lt, Set.mem_Icc]
Proof state after:
⊢ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), rectangle α = Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
⊢ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), rectangle α = Set.singleton (1, 0)
Tactic:
simp_rw [rectangle, Set.ext_iff]
Proof state after:
⊢ ∀ (x : ℝ × ℝ), x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
⊢ ∀ (x : ℝ × ℝ), x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)
Tactic:
intro x
Proof state after:
x : ℝ × ℝ
⊢ x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
x : ℝ × ℝ
⊢ x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)
Tactic:
simp only [ge_iff_le, not_le, gt_iff_lt, Set.Icc_prod_Icc, Prod.mk_le_mk, not_and, Prod.mk_lt_mk, Set.mem_iInter, Set.mem_Icc, and_imp]
Proof state after:
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) ↔ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) ↔ x ∈ Set.singleton (1, 0)
Tactic:
constructor
Proof state after:
case mp
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) → x ∈ Set.singleton (1, 0)

case mpr
x : ℝ × ℝ
⊢ x ∈ Set.singleton (1, 0) → ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) → x ∈ Set.singleton (1, 0)
Tactic:
intro imp
Proof state after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
⊢ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have h1 := imp 0
Proof state after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
⊢ x ∈ Set.singleton (1, 0)