internlm/Lean-Github huggingface dataset:
Theorem: r5_not_weak_order
Proof state before:
case inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS2 : ¬S p.1 p.1 ∧ ¬S p.1 p.1 ∧ p.1 = p.1
⊢ False
Tactic:
exact hS2.left hS1
Proof state after:
no goals
Theorem: r5_not_weak_order
Proof state before:
case inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS3 : ¬S p.1 p.1 ∧ S p.1 p.1 ∧ ¬p.1 = p.1
⊢ False
Tactic:
exact hS3.left hS1
Proof state after:
no goals
Theorem: r5_not_weak_order
Proof state before:
case inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS4 : S p.1 p.1 ∧ ¬S p.1 p.1 ∧ ¬p.1 = p.1
⊢ False
Tactic:
have := hS4.right.right
Proof state after:
case inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS4 : S p.1 p.1 ∧ ¬S p.1 p.1 ∧ ¬p.1 = p.1
this : ¬p.1 = p.1
⊢ False
Theorem: r5_not_weak_order
Proof state before:
case inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS4 : S p.1 p.1 ∧ ¬S p.1 p.1 ∧ ¬p.1 = p.1
this : ¬p.1 = p.1
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: r5_not_weak_order
Proof state before:
case inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
⊢ False
Tactic:
rcases hT.trich p.2 p.2 with (hT2 | hT3 | hT4)
Proof state after:
case inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT2 : ¬T p.2 p.2 ∧ ¬T p.2 p.2 ∧ p.2 = p.2
⊢ False

case inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT3 : ¬T p.2 p.2 ∧ T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False

case inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False
Theorem: r5_not_weak_order
Proof state before:
case inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT2 : ¬T p.2 p.2 ∧ ¬T p.2 p.2 ∧ p.2 = p.2
⊢ False
Tactic:
exact hT2.left hT1
Proof state after:
no goals
Theorem: r5_not_weak_order
Proof state before:
case inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT3 : ¬T p.2 p.2 ∧ T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False
Tactic:
exact hT3.left hT1
Proof state after:
no goals
Theorem: r5_not_weak_order
Proof state before:
case inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False
Tactic:
have := hT4.right.right
Proof state after:
case inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
this : ¬p.2 = p.2
⊢ False
Theorem: r5_not_weak_order
Proof state before:
case inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
this : ¬p.2 = p.2
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: R5'_false
Proof state before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
⊢ R5' p [] ↔ False
Tactic:
simp
Proof state after:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
⊢ ¬R5' p []
Theorem: R5'_false
Proof state before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
⊢ ¬R5' p []
Tactic:
intro hr
Proof state after:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ False
Theorem: R5'_false
Proof state before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ False
Tactic:
rw [R5'] at hr
Proof state after:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
⊢ False

case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False

case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False
Theorem: R5'_false
Proof state before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
⊢ False
Tactic:
exact hr
Proof state after:
no goals
Theorem: R5'_false
Proof state before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False
Tactic:
intro heq
Proof state after:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False
Theorem: R5'_false
Proof state before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False
Tactic:
rw [heq] at hr
Proof state after:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False
Theorem: R5'_false
Proof state before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False
Tactic:
rw [R5'] at hr
Proof state after:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False
Theorem: R5'_false
Proof state before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False
Tactic:
exact hr
Proof state after:
no goals
Theorem: R5'_false
Proof state before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False
Tactic:
intro heq
Proof state after:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False
Theorem: R5'_false
Proof state before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False
Tactic:
rw [heq] at hr
Proof state after:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False
Theorem: R5'_false
Proof state before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False
Tactic:
rw [R5'] at hr
Proof state after:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False
Theorem: R5'_false
Proof state before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False
Tactic:
exact hr
Proof state after:
no goals
Theorem: idx_set_union
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ⋃ j ∈ J, A j ⊆ ⋃ i ∈ I, A i
Tactic:
intros x hx
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ x ∈ ⋃ i ∈ I, A i
Theorem: idx_set_union
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ x ∈ ⋃ i ∈ I, A i
Tactic:
simp only [Set.mem_iUnion, exists_prop]
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ ∃ i ∈ I, x ∈ A i
Theorem: idx_set_union
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ ∃ i ∈ I, x ∈ A i
Tactic:
simp only [Set.mem_iUnion, exists_prop] at hx
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : ∃ i ∈ J, x ∈ A i
⊢ ∃ i ∈ I, x ∈ A i
Theorem: idx_set_union
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : ∃ i ∈ J, x ∈ A i
⊢ ∃ i ∈ I, x ∈ A i
Tactic:
rcases hx with ⟨j, ⟨hj, hxj⟩⟩
Proof state after:
case intro.intro
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ ∃ i ∈ I, x ∈ A i
Theorem: idx_set_union
Proof state before:
case intro.intro
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ ∃ i ∈ I, x ∈ A i
Tactic:
use j
Proof state after:
case h
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I ∧ x ∈ A j
Theorem: idx_set_union
Proof state before:
case h
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I ∧ x ∈ A j
Tactic:
constructor
Proof state after:
case h.left
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I

case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
Theorem: idx_set_union
Proof state before:
case h.left
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I

case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
Tactic:
exact hsub hj
Proof state after:
case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
Theorem: idx_set_union
Proof state before:
case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
Tactic:
exact hxj
Proof state after:
no goals
Theorem: idx_set_not_inter
Proof state before:
⊢ ∃ α β J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use ℕ
Proof state after:
case h

⊢ ∃ β J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Theorem: idx_set_not_inter
Proof state before:
case h

⊢ ∃ β J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use ℕ
Proof state after:
case h

⊢ ∃ J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Theorem: idx_set_not_inter
Proof state before:
case h

⊢ ∃ J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use {1}
Proof state after:
case h

⊢ ∃ I A, {1} ⊆ I ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ I, A i
Theorem: idx_set_not_inter
Proof state before:
case h

⊢ ∃ I A, {1} ⊆ I ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use {1, 2}
Proof state after:
case h

⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Theorem: idx_set_not_inter
Proof state before:
case h

⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Tactic:
let A := λ n : ℕ => ({0, n} : Set ℕ)
Proof state after:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Theorem: idx_set_not_inter
Proof state before:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Tactic:
use A
Proof state after:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Theorem: idx_set_not_inter
Proof state before:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Tactic:
simp only [Set.mem_singleton_iff, OfNat.one_ne_ofNat, Set.singleton_subset_iff,
  Set.mem_insert_iff, or_false, Set.iInter_iInter_eq_left, Set.iInter_iInter_eq_or_left,
  Set.subset_inter_iff, not_false_eq_true, Set.insert_subset_insert_iff, Set.subset_singleton_iff,
  imp_self, forall_const, forall_eq, and_false, and_self]
Proof state after:
no goals
Theorem: idx_set_inter_rev
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ⋂ i ∈ I, A i ⊆ ⋂ j ∈ J, A j
Tactic:
simp only [Set.subset_iInter_iff]
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ∀ i ∈ J, ⋂ i ∈ I, A i ⊆ A i
Theorem: idx_set_inter_rev
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
⊢ ∀ i ∈ J, ⋂ i ∈ I, A i ⊆ A i
Tactic:
intros x hx b hb
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : b ∈ ⋂ i ∈ I, A i
⊢ b ∈ A x
Theorem: idx_set_inter_rev
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : b ∈ ⋂ i ∈ I, A i
⊢ b ∈ A x
Tactic:
simp at hb
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : ∀ i ∈ I, b ∈ A i
⊢ b ∈ A x
Theorem: idx_set_inter_rev
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : ∀ i ∈ I, b ∈ A i
⊢ b ∈ A x
Tactic:
specialize hb x
Proof state after:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : x ∈ I → b ∈ A x
⊢ b ∈ A x
Theorem: idx_set_inter_rev
Proof state before:
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : x ∈ I → b ∈ A x
⊢ b ∈ A x
Tactic:
exact hb (hsub hx)
Proof state after:
no goals
Theorem: sq_diophantine
Proof state before:
x y : ℝ
⊢ x ^ 2 + 5 * y = y ^ 2 + 5 * x → x = y ∨ x + y = 5
Tactic:
intro h
Proof state after:
x y : ℝ
h : x ^ 2 + 5 * y = y ^ 2 + 5 * x
⊢ x = y ∨ x + y = 5
Theorem: sq_diophantine
Proof state before:
x y : ℝ
h : x ^ 2 + 5 * y = y ^ 2 + 5 * x
⊢ x = y ∨ x + y = 5
Tactic:
apply_fun (λ eq => eq - 5 * y - y ^ 2) at h
Proof state after:
x y : ℝ
h : x ^ 2 + 5 * y - 5 * y - y ^ 2 = y ^ 2 + 5 * x - 5 * y - y ^ 2
⊢ x = y ∨ x + y = 5
Theorem: sq_diophantine
Proof state before:
x y : ℝ
h : x ^ 2 + 5 * y - 5 * y - y ^ 2 = y ^ 2 + 5 * x - 5 * y - y ^ 2
⊢ x = y ∨ x + y = 5
Tactic:
ring_nf at h
Proof state after:
x y : ℝ
h : x ^ 2 - y ^ 2 = x * 5 - y * 5
⊢ x = y ∨ x + y = 5
Theorem: sq_diophantine
Proof state before:
x y : ℝ
h : x ^ 2 - y ^ 2 = x * 5 - y * 5
⊢ x = y ∨ x + y = 5
Tactic:
rw [sq_sub_sq, ←mul_sub_right_distrib, mul_comm] at h
Proof state after:
x y : ℝ
h : (x - y) * (x + y) = (x - y) * 5
⊢ x = y ∨ x + y = 5
Theorem: sq_diophantine
Proof state before:
x y : ℝ
h : (x - y) * (x + y) = (x - y) * 5
⊢ x = y ∨ x + y = 5
Tactic:
rw [mul_eq_mul_left_iff, sub_eq_zero, or_comm] at h
Proof state after:
x y : ℝ
h : x = y ∨ x + y = 5
⊢ x = y ∨ x + y = 5
Theorem: sq_diophantine
Proof state before:
x y : ℝ
h : x = y ∨ x + y = 5
⊢ x = y ∨ x + y = 5
Tactic:
exact h
Proof state after:
no goals
Theorem: sqrt17
Proof state before:
⊢ {x | x ^ 2 = 17} = {Real.sqrt 17, -Real.sqrt 17}
Tactic:
ext x
Proof state after:
case h
x : ℝ
⊢ x ∈ {x | x ^ 2 = 17} ↔ x ∈ {Real.sqrt 17, -Real.sqrt 17}
Theorem: sqrt17
Proof state before:
case h
x : ℝ
⊢ x ∈ {x | x ^ 2 = 17} ↔ x ∈ {Real.sqrt 17, -Real.sqrt 17}
Tactic:
simp
Proof state after:
case h
x : ℝ
⊢ x ^ 2 = 17 ↔ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Theorem: sqrt17
Proof state before:
case h
x : ℝ
⊢ x ^ 2 = 17 ↔ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
constructor
Proof state after:
case h.mp
x : ℝ
⊢ x ^ 2 = 17 → x = Real.sqrt 17 ∨ x = -Real.sqrt 17

case h.mpr
x : ℝ
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17 → x ^ 2 = 17
Theorem: sqrt17
Proof state before:
case h.mp
x : ℝ
⊢ x ^ 2 = 17 → x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
intro hsq
Proof state after:
case h.mp
x : ℝ
hsq : x ^ 2 = 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Theorem: sqrt17
Proof state before:
case h.mp
x : ℝ
hsq : x ^ 2 = 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
apply_fun (λ eq => Real.sqrt eq) at hsq
Proof state after:
case h.mp
x : ℝ
hsq : Real.sqrt (x ^ 2) = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Theorem: sqrt17
Proof state before:
case h.mp
x : ℝ
hsq : Real.sqrt (x ^ 2) = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
rw [Real.sqrt_sq_eq_abs] at hsq
Proof state after:
case h.mp
x : ℝ
hsq : |x| = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Theorem: sqrt17
Proof state before:
case h.mp
x : ℝ
hsq : |x| = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
exact eq_or_eq_neg_of_abs_eq hsq
Proof state after:
no goals
Theorem: sqrt17
Proof state before:
case h.mpr
x : ℝ
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17 → x ^ 2 = 17
Tactic:
intro hor
Proof state after:
case h.mpr
x : ℝ
hor : x = Real.sqrt 17 ∨ x = -Real.sqrt 17
⊢ x ^ 2 = 17
Theorem: sqrt17
Proof state before:
case h.mpr
x : ℝ
hor : x = Real.sqrt 17 ∨ x = -Real.sqrt 17
⊢ x ^ 2 = 17
Tactic:
rcases hor with (hpos | hneg)
Proof state after:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ x ^ 2 = 17

case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ x ^ 2 = 17
Theorem: sqrt17
Proof state before:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ x ^ 2 = 17
Tactic:
rw [hpos]
Proof state after:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17
Theorem: sqrt17
Proof state before:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17
Tactic:
exact Real.sq_sqrt (by norm_num)
Proof state after:
no goals
Theorem: sqrt17
Proof state before:
x : ℝ
hpos : x = Real.sqrt 17
⊢ 0 ≤ 17
Tactic:
norm_num
Proof state after:
no goals
Theorem: sqrt17
Proof state before:
case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ x ^ 2 = 17
Tactic:
rw [hneg, neg_sq]
Proof state after:
case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17
Theorem: sqrt17
Proof state before:
case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17
Tactic:
exact Real.sq_sqrt (by norm_num)
Proof state after:
no goals
Theorem: sqrt17
Proof state before:
x : ℝ
hneg : x = -Real.sqrt 17
⊢ 0 ≤ 17
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt24
Proof state before:
⊢ {x | |3 * x| < 24} = {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Tactic:
ext x
Proof 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}
Theorem: lt24
Proof 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
Proof 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}
Theorem: lt24
Proof 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
Proof 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}
Theorem: lt24
Proof 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
Proof 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}
Theorem: lt24
Proof 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
Proof 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}
Theorem: lt24
Proof 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'⟩
Proof 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}
Theorem: lt24
Proof 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]
Proof 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
Theorem: lt24
Proof 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
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:
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
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