internlm/Lean-Github huggingface dataset:
Theorem: Set.union_subset_of_subset_of_subset
Proof state before:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
x✝ : x ∈ s.union t
hxt : x ∈ t
⊢ x ∈ u
Tactic:
exact htu x hxt
Proof state after:
no goals
Theorem: Set.union_subset_union_left
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset t → ∀ (u : Set α), (u.union s).Subset (u.union t)
Tactic:
intro hst u x
Proof state after:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
⊢ x ∈ u.union s → x ∈ u.union t
Theorem: Set.union_subset_union_left
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
⊢ x ∈ u.union s → x ∈ u.union t
Tactic:
intro
| Or.inl hu =>
  left
  exact hu
| Or.inr hs =>
  right
  exact hst x hs
Proof state after:
no goals
Theorem: Set.union_subset_union_left
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ u.union s
hu : x ∈ u
⊢ x ∈ u.union t
Tactic:
left
Proof state after:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ u.union s
hu : x ∈ u
⊢ x ∈ u
Theorem: Set.union_subset_union_left
Proof state before:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ u.union s
hu : x ∈ u
⊢ x ∈ u
Tactic:
exact hu
Proof state after:
no goals
Theorem: Set.union_subset_union_left
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ u.union s
hs : x ∈ s
⊢ x ∈ u.union t
Tactic:
right
Proof state after:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ u.union s
hs : x ∈ s
⊢ x ∈ t
Theorem: Set.union_subset_union_left
Proof state before:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ u.union s
hs : x ∈ s
⊢ x ∈ t
Tactic:
exact hst x hs
Proof state after:
no goals
Theorem: Set.union_subset_union_right
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset t → ∀ (u : Set α), (s.union u).Subset (t.union u)
Tactic:
intro hst u x
Proof state after:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
⊢ x ∈ s.union u → x ∈ t.union u
Theorem: Set.union_subset_union_right
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
⊢ x ∈ s.union u → x ∈ t.union u
Tactic:
intro
| Or.inl hs =>
  left
  exact hst x hs
| Or.inr hu =>
  right
  exact hu
Proof state after:
no goals
Theorem: Set.union_subset_union_right
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ s.union u
hs : x ∈ s
⊢ x ∈ t.union u
Tactic:
left
Proof state after:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ s.union u
hs : x ∈ s
⊢ x ∈ t
Theorem: Set.union_subset_union_right
Proof state before:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ s.union u
hs : x ∈ s
⊢ x ∈ t
Tactic:
exact hst x hs
Proof state after:
no goals
Theorem: Set.union_subset_union_right
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ s.union u
hu : x ∈ u
⊢ x ∈ t.union u
Tactic:
right
Proof state after:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ s.union u
hu : x ∈ u
⊢ x ∈ u
Theorem: Set.union_subset_union_right
Proof state before:
case h
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
x✝ : x ∈ s.union u
hu : x ∈ u
⊢ x ∈ u
Tactic:
exact hu
Proof state after:
no goals
Theorem: Set.union_subset_union
Proof state before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
⊢ s₁.Subset s₂ → t₁.Subset t₂ → (s₁.union t₁).Subset (s₂.union t₂)
Tactic:
intro hs ht x
Proof state after:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
⊢ x ∈ s₁.union t₁ → x ∈ s₂.union t₂
Theorem: Set.union_subset_union
Proof state before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
⊢ x ∈ s₁.union t₁ → x ∈ s₂.union t₂
Tactic:
intro
| Or.inl hs₁ =>
  left
  exact hs x hs₁
| Or.inr ht₁ =>
  right
  exact ht x ht₁
Proof state after:
no goals
Theorem: Set.union_subset_union
Proof state before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
hs₁ : x ∈ s₁
⊢ x ∈ s₂.union t₂
Tactic:
left
Proof state after:
case h
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
hs₁ : x ∈ s₁
⊢ x ∈ s₂
Theorem: Set.union_subset_union
Proof state before:
case h
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
hs₁ : x ∈ s₁
⊢ x ∈ s₂
Tactic:
exact hs x hs₁
Proof state after:
no goals
Theorem: Set.union_subset_union
Proof state before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂.union t₂
Tactic:
right
Proof state after:
case h
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂
Theorem: Set.union_subset_union
Proof state before:
case h
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂
Tactic:
exact ht x ht₁
Proof state after:
no goals
Theorem: Set.inter_subset_left
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
⊢ (s.inter t).Subset s
Tactic:
intro x ⟨hs,_⟩
Proof state after:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
hs : x ∈ s
right✝ : x ∈ t
⊢ x ∈ s
Theorem: Set.inter_subset_left
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
hs : x ∈ s
right✝ : x ∈ t
⊢ x ∈ s
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.inter_subset_right
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
⊢ (s.inter t).Subset t
Tactic:
intro x ⟨_,ht⟩
Proof state after:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
left✝ : x ∈ s
ht : x ∈ t
⊢ x ∈ t
Theorem: Set.inter_subset_right
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
left✝ : x ∈ s
ht : x ∈ t
⊢ x ∈ t
Tactic:
exact ht
Proof state after:
no goals
Theorem: Set.subset_inter_of_subset_of_subset
Proof state before:
α : Sort u_1
s t u : Set α
⊢ u.Subset s → u.Subset t → u.Subset (s.inter t)
Tactic:
intro hus hut x hxu
Proof state after:
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s.inter t
Theorem: Set.subset_inter_of_subset_of_subset
Proof state before:
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s.inter t
Tactic:
constructor
Proof state after:
case left
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s

case right
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ t
Theorem: Set.subset_inter_of_subset_of_subset
Proof state before:
case left
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s
Tactic:
exact hus x hxu
Proof state after:
no goals
Theorem: Set.subset_inter_of_subset_of_subset
Proof state before:
case right
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ t
Tactic:
exact hut x hxu
Proof state after:
no goals
Theorem: Set.inter_subset_inter_left
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset t → ∀ (u : Set α), (u.inter s).Subset (u.inter t)
Tactic:
intro hst u x ⟨hu, hs⟩
Proof state after:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hu : x ∈ u
hs : x ∈ s
⊢ x ∈ u.inter t
Theorem: Set.inter_subset_inter_left
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hu : x ∈ u
hs : x ∈ s
⊢ x ∈ u.inter t
Tactic:
constructor
Proof state after:
case left
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hu : x ∈ u
hs : x ∈ s
⊢ x ∈ u

case right
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hu : x ∈ u
hs : x ∈ s
⊢ x ∈ t
Theorem: Set.inter_subset_inter_left
Proof state before:
case left
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hu : x ∈ u
hs : x ∈ s
⊢ x ∈ u
Tactic:
exact hu
Proof state after:
no goals
Theorem: Set.inter_subset_inter_left
Proof state before:
case right
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hu : x ∈ u
hs : x ∈ s
⊢ x ∈ t
Tactic:
exact hst x hs
Proof state after:
no goals
Theorem: Set.inter_subset_inter_right
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset t → ∀ (u : Set α), (s.inter u).Subset (t.inter u)
Tactic:
intro hst u x ⟨hs, hu⟩
Proof state after:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hs : x ∈ s
hu : x ∈ u
⊢ x ∈ t.inter u
Theorem: Set.inter_subset_inter_right
Proof state before:
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hs : x ∈ s
hu : x ∈ u
⊢ x ∈ t.inter u
Tactic:
constructor
Proof state after:
case left
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hs : x ∈ s
hu : x ∈ u
⊢ x ∈ t

case right
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hs : x ∈ s
hu : x ∈ u
⊢ x ∈ u
Theorem: Set.inter_subset_inter_right
Proof state before:
case left
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hs : x ∈ s
hu : x ∈ u
⊢ x ∈ t
Tactic:
exact hst x hs
Proof state after:
no goals
Theorem: Set.inter_subset_inter_right
Proof state before:
case right
α : Sort u_1
s t u✝ : Set α
hst : s.Subset t
u : Set α
x : α
hs : x ∈ s
hu : x ∈ u
⊢ x ∈ u
Tactic:
exact hu
Proof state after:
no goals
Theorem: Set.inter_subset_inter
Proof state before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
⊢ s₁.Subset s₂ → t₁.Subset t₂ → (s₁.inter t₁).Subset (s₂.inter t₂)
Tactic:
intro hs ht x ⟨hs₁,ht₁⟩
Proof state after:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂.inter t₂
Theorem: Set.inter_subset_inter
Proof state before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂.inter t₂
Tactic:
constructor
Proof state after:
case left
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂

case right
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂
Theorem: Set.inter_subset_inter
Proof state before:
case left
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂
Tactic:
exact hs x hs₁
Proof state after:
no goals
Theorem: Set.inter_subset_inter
Proof state before:
case right
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂
Tactic:
exact ht x ht₁
Proof state after:
no goals
Theorem: Set.map_subset_map
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
⊢ s.Subset t → (f <$> s).Subset (f <$> t)
Tactic:
intro hst y ⟨x,hx,h⟩
Proof state after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ f <$> t
Theorem: Set.map_subset_map
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ f <$> t
Tactic:
cases h
Proof state after:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x ∈ f <$> t
Theorem: Set.map_subset_map
Proof state before:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x ∈ f <$> t
Tactic:
exists x
Proof state after:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t ∧ f x = f x
Theorem: Set.map_subset_map
Proof state before:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t ∧ f x = f x
Tactic:
constructor
Proof state after:
case refl.left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t

case refl.right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x = f x
Theorem: Set.map_subset_map
Proof state before:
case refl.left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t
Tactic:
exact hst x hx
Proof state after:
no goals
Theorem: Set.map_subset_map
Proof state before:
case refl.right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.bind_subset_bind
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
⊢ s.Subset t → (s >>= f).Subset (t >>= f)
Tactic:
intro hst y ⟨x,hx,h⟩
Proof state after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ t >>= f
Theorem: Set.bind_subset_bind
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ t >>= f
Tactic:
exists x
Proof state after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t ∧ y ∈ f x
Theorem: Set.bind_subset_bind
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t ∧ y ∈ f x
Tactic:
constructor
Proof state after:
case left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t

case right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ f x
Theorem: Set.bind_subset_bind
Proof state before:
case left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ x ∈ t
Tactic:
exact hst x hx
Proof state after:
no goals
Theorem: Set.bind_subset_bind
Proof state before:
case right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : y ∈ f x
⊢ y ∈ f x
Tactic:
exact h
Proof state after:
no goals
Theorem: Set.val_subset_bind
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
⊢ x ∈ s → (f x).Subset (s >>= f)
Tactic:
intro hxs y hfxy
Proof state after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
hxs : x ∈ s
y : β
hfxy : y ∈ f x
⊢ y ∈ s >>= f
Theorem: Set.val_subset_bind
Proof state before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
hxs : x ∈ s
y : β
hfxy : y ∈ f x
⊢ y ∈ s >>= f
Tactic:
exists x
Proof state after:
no goals
Theorem: Set.bind_subset_of_val_subset
Proof state before:
α : Type u_1
s t✝ u : Set α
β : Type u_1
t : Set β
f : α → Set β
⊢ (∀ (x : α), x ∈ s → (f x).Subset t) → (s >>= f).Subset t
Tactic:
intro h y ⟨x, hxs, hfxy⟩
Proof state after:
α : Type u_1
s t✝ u : Set α
β : Type u_1
t : Set β
f : α → Set β
h : ∀ (x : α), x ∈ s → (f x).Subset t
y : β
x : α
hxs : x ∈ s
hfxy : y ∈ f x
⊢ y ∈ t
Theorem: Set.bind_subset_of_val_subset
Proof state before:
α : Type u_1
s t✝ u : Set α
β : Type u_1
t : Set β
f : α → Set β
h : ∀ (x : α), x ∈ s → (f x).Subset t
y : β
x : α
hxs : x ∈ s
hfxy : y ∈ f x
⊢ y ∈ t
Tactic:
exact h x hxs y hfxy
Proof state after:
no goals
Theorem: Option.orElse_none_left
Proof state before:
α : Type u_1
x : Option α
⊢ (HOrElse.hOrElse none fun x_1 => x) = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Option.orElse_none_right
Proof state before:
α : Type u_1
x : Option α
⊢ (HOrElse.hOrElse x fun x => none) = x
Tactic:
cases x <;> rfl
Proof state after:
no goals
Theorem: Option.orElse_assoc
Proof state before:
α : Type u_1
x y z : Option α
⊢ (HOrElse.hOrElse (HOrElse.hOrElse x fun x => y) fun x => z) = HOrElse.hOrElse x fun x => HOrElse.hOrElse y fun x => z
Tactic:
cases x <;> cases y <;> cases z <;> rfl
Proof state after:
no goals
Theorem: Option.first_cons
Proof state before:
α : Type u_1
x : Option α
xs : List (Option α)
⊢ first (x :: xs) = HOrElse.hOrElse x fun x => first xs
Tactic:
cases x <;> rfl
Proof state after:
no goals
Theorem: Option.first_pure
Proof state before:
α : Type u_1
x : Option α
⊢ first [x] = x
Tactic:
cases x <;> rfl
Proof state after:
no goals
Theorem: Option.first_append
Proof state before:
α : Type u_1
xs ys : List (Option α)
⊢ first (xs ++ ys) = HOrElse.hOrElse (first xs) fun x => first ys
Tactic:
induction xs with
| nil => rfl
| cons x xs ih => simp [orElse_assoc, ih]
Proof state after:
no goals
Theorem: Option.first_append
Proof state before:
case nil
α : Type u_1
ys : List (Option α)
⊢ first ([] ++ ys) = HOrElse.hOrElse (first []) fun x => first ys
Tactic:
rfl
Proof state after:
no goals
Theorem: Option.first_append
Proof state before:
case cons
α : Type u_1
ys : List (Option α)
x : Option α
xs : List (Option α)
ih : first (xs ++ ys) = HOrElse.hOrElse (first xs) fun x => first ys
⊢ first (x :: xs ++ ys) = HOrElse.hOrElse (first (x :: xs)) fun x => first ys
Tactic:
simp [orElse_assoc, ih]
Proof state after:
no goals
Theorem: Relation.Quasiorder.asymm
Proof state before:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
⊢ r x y → ¬r y x
Tactic:
intro hxy hyx
Proof state after:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ False
Theorem: Relation.Quasiorder.asymm
Proof state before:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ False
Tactic:
apply self.irrefl x
Proof state after:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ r x x
Theorem: Relation.Quasiorder.asymm
Proof state before:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ r x x
Tactic:
exact self.trans hxy hyx
Proof state after:
no goals
Theorem: Relation.Preorder.co_irrefl
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
⊢ ¬coRel r x x
Tactic:
exact not_not_intro Reflexive.rfl
Proof state after:
no goals
Theorem: Relation.Preorder.co_compare
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
⊢ coRel r x y → ∀ (z : α), coRel r x z ∨ coRel r z y
Tactic:
intro cxy z
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y
Theorem: Relation.Preorder.co_compare
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y
Tactic:
rw [←Logic.nand_iff_not_or_not]
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ ¬(r z x ∧ r y z)
Theorem: Relation.Preorder.co_compare
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ ¬(r z x ∧ r y z)
Tactic:
intro ⟨hzx, hyz⟩
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
hzx : r z x
hyz : r y z
⊢ False
Theorem: Relation.Preorder.co_compare
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
hzx : r z x
hyz : r y z
⊢ False
Tactic:
absurd cxy
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
hzx : r z x
hyz : r y z
⊢ r y x
Theorem: Relation.Preorder.co_compare
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
hzx : r z x
hyz : r y z
⊢ r y x
Tactic:
exact Transitive.trans hyz hzx
Proof state after:
no goals
Theorem: Relation.Preorder.as_irrefl
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
⊢ ¬asymRel r x x
Tactic:
intro ⟨_, cxx⟩
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
left✝ : r x x
cxx : coRel r x x
⊢ False
Theorem: Relation.Preorder.as_irrefl
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
left✝ : r x x
cxx : coRel r x x
⊢ False
Tactic:
exact co_irrefl x cxx
Proof state after:
no goals
Theorem: Relation.Preorder.as_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z
Tactic:
intro ⟨hxy, cxy⟩ ⟨hyz, _⟩
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ asymRel r x z
Theorem: Relation.Preorder.as_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ asymRel r x z
Tactic:
constructor
Proof state after:
case left
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ r x z

case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ coRel r x z
Theorem: Relation.Preorder.as_trans
Proof state before:
case left
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ r x z
Tactic:
exact Transitive.trans hxy hyz
Proof state after:
no goals
Theorem: Relation.Preorder.as_trans
Proof state before:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ coRel r x z
Tactic:
intro hzx
Proof state after:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ False
Theorem: Relation.Preorder.as_trans
Proof state before:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ False
Tactic:
absurd cxy
Proof state after:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ r y x
Theorem: Relation.Preorder.as_trans
Proof state before:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ r y x
Tactic:
exact Transitive.trans hyz hzx
Proof state after:
no goals
Theorem: Relation.PartialOrder.co_connex
Proof state before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
⊢ x ≠ y → coRel r x y ∨ coRel r y x
Tactic:
intro hne
Proof state after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ coRel r x y ∨ coRel r y x
Theorem: Relation.PartialOrder.co_connex
Proof state before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ coRel r x y ∨ coRel r y x
Tactic:
rw [←nand_iff_not_or_not]
Proof state after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ ¬(r y x ∧ r x y)
Theorem: Relation.PartialOrder.co_connex
Proof state before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ ¬(r y x ∧ r x y)
Tactic:
intro ⟨hyx, hxy⟩
Proof state after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ False
Theorem: Relation.PartialOrder.co_connex
Proof state before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ False
Tactic:
absurd hne
Proof state after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ x = y
Theorem: Relation.PartialOrder.co_connex
Proof state before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ x = y
Tactic:
exact Antisymmetric.antisymm hxy hyx
Proof state after:
no goals
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y ↔ asymRel r x y
Tactic:
constructor
Proof state after:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y → asymRel r x y

case mpr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ asymRel r x y → coRel r x y