internlm/Lean-Github huggingface dataset:
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ w = w.head ::ᵥ w.tail
Tactic:
simp
Proof state after:
no goals
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
⊢ ∅ ⊆ ⋃₀ c → ∃ t ∈ c, ∅ ⊆ t
Tactic:
rcases hc with ⟨t, ht⟩
Proof state after:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
⊢ ∅ ⊆ ⋃₀ c → ∃ t ∈ c, ∅ ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
⊢ ∅ ⊆ ⋃₀ c → ∃ t ∈ c, ∅ ⊆ t
Tactic:
intro
Proof state after:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
a✝ : ∅ ⊆ ⋃₀ c
⊢ ∃ t ∈ c, ∅ ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
a✝ : ∅ ⊆ ⋃₀ c
⊢ ∃ t ∈ c, ∅ ⊆ t
Tactic:
exact ⟨t, ht, by simp⟩
Proof state after:
no goals
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
a✝ : ∅ ⊆ ⋃₀ c
⊢ ∅ ⊆ t
Tactic:
simp
Proof state after:
no goals
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
⊢ ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → (s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t) → insert a s ⊆ ⋃₀ c → ∃ t ∈ c, insert a s ⊆ t
Tactic:
intro a s _ _ ih h
Proof state after:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
have : ∃ t ∈ c, s ⊆ t := ih (subset_trans (Set.subset_insert a s) h)
Proof state after:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
this : ∃ t ∈ c, s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
this : ∃ t ∈ c, s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
rcases this with ⟨t, htc, ht⟩
Proof state after:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
have : ∃ u ∈ c, a ∈ u := by simp [Set.insert_subset_iff] at h; exact h.1
Proof state after:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
this : ∃ u ∈ c, a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
this : ∃ u ∈ c, a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
rcases this with ⟨u, huc, hu⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
have : ∃ z ∈ c, t ⊆ z ∧ u ⊆ z := IsChain.directedOn hchain t htc u huc
Proof state after:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
this : ∃ z ∈ c, t ⊆ z ∧ u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
this : ∃ z ∈ c, t ⊆ z ∧ u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
rcases this with ⟨z, hzc, htz, huz⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
z : Set α
hzc : z ∈ c
htz : t ⊆ z
huz : u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
z : Set α
hzc : z ∈ c
htz : t ⊆ z
huz : u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
exact ⟨z, hzc, Set.insert_subset (huz hu) (Set.Subset.trans ht htz)⟩
Proof state after:
no goals
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ u ∈ c, a ∈ u
Tactic:
simp [Set.insert_subset_iff] at h
Proof state after:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
t : Set α
htc : t ∈ c
ht : s ⊆ t
h : (∃ t ∈ c, a ∈ t) ∧ s ⊆ ⋃₀ c
⊢ ∃ u ∈ c, a ∈ u
Theorem: Set.subset_mem_chain_of_finite
Proof state before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
t : Set α
htc : t ∈ c
ht : s ⊆ t
h : (∃ t ∈ c, a ∈ t) ∧ s ⊆ ⋃₀ c
⊢ ∃ u ∈ c, a ∈ u
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Nat.exp_succ
Proof state before:
n : ℕ
⊢ exp (n + 1) = 2 * exp n
Tactic:
simp [exp_def, pow_succ, mul_comm]
Proof state after:
no goals
Theorem: Set.subset_triunion₃
Proof state before:
F : Type u_1
s₁ s₂ s₃ s₄ : Set F
⊢ s₃ ⊆ s₁ ∪ s₂ ∪ s₃
Tactic:
simp only [subset_union_right]
Proof state after:
no goals
Theorem: Set.subset_tetraunion₃
Proof state before:
F : Type u_1
s₁ s₂ s₃ s₄ : Set F
⊢ s₃ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄
Tactic:
simp only [subset_triunion₂]
Proof state after:
no goals
Theorem: Set.subset_tetraunion₄
Proof state before:
F : Type u_1
s₁ s₂ s₃ s₄ : Set F
⊢ s₄ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄
Tactic:
simp only [subset_union_right]
Proof state after:
no goals
Theorem: not_acc_iff
Proof state before:
α : Sort u
r : α → α → Prop
x : α
⊢ ¬Acc r x → ∃ y, r y x ∧ ¬Acc r y
Tactic:
contrapose
Proof state after:
α : Sort u
r : α → α → Prop
x : α
⊢ (¬∃ y, r y x ∧ ¬Acc r y) → ¬¬Acc r x
Theorem: not_acc_iff
Proof state before:
α : Sort u
r : α → α → Prop
x : α
⊢ (¬∃ y, r y x ∧ ¬Acc r y) → ¬¬Acc r x
Tactic:
simp
Proof state after:
α : Sort u
r : α → α → Prop
x : α
⊢ (∀ (x_1 : α), r x_1 x → Acc r x_1) → Acc r x
Theorem: not_acc_iff
Proof state before:
α : Sort u
r : α → α → Prop
x : α
⊢ (∀ (x_1 : α), r x_1 x → Acc r x_1) → Acc r x
Tactic:
exact Acc.intro x
Proof state after:
no goals
Theorem: not_acc_iff
Proof state before:
α : Sort u
r : α → α → Prop
x : α
⊢ (∃ y, r y x ∧ ¬Acc r y) → ¬Acc r x
Tactic:
contrapose
Proof state after:
α : Sort u
r : α → α → Prop
x : α
⊢ ¬¬Acc r x → ¬∃ y, r y x ∧ ¬Acc r y
Theorem: not_acc_iff
Proof state before:
α : Sort u
r : α → α → Prop
x : α
⊢ ¬¬Acc r x → ¬∃ y, r y x ∧ ¬Acc r y
Tactic:
simp
Proof state after:
α : Sort u
r : α → α → Prop
x : α
⊢ Acc r x → ∀ (x_1 : α), r x_1 x → Acc r x_1
Theorem: not_acc_iff
Proof state before:
α : Sort u
r : α → α → Prop
x : α
⊢ Acc r x → ∀ (x_1 : α), r x_1 x → Acc r x_1
Tactic:
rintro ⟨h⟩
Proof state after:
case intro
α : Sort u
r : α → α → Prop
x : α
h✝ : ∀ (y : α), r y x → Acc r y
⊢ ∀ (x_1 : α), r x_1 x → Acc r x_1
Theorem: not_acc_iff
Proof state before:
case intro
α : Sort u
r : α → α → Prop
x : α
h✝ : ∀ (y : α), r y x → Acc r y
⊢ ∀ (x_1 : α), r x_1 x → Acc r x_1
Tactic:
assumption
Proof state after:
no goals
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ IsInfiniteDescendingChain r (descendingChain r z)
Tactic:
intro i
Proof state after:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
i : ℕ
⊢ r (descendingChain r z (i + 1)) (descendingChain r z i)
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
i : ℕ
⊢ r (descendingChain r z (i + 1)) (descendingChain r z i)
Tactic:
simpa using (this (i + 1)).1
Proof state after:
no goals
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
Tactic:
intro i
Proof state after:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
⊢ (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
⊢ (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
Tactic:
induction' i with i ih
Proof state after:
case zero
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ (0 ≠ 0 → r (descendingChain r z 0) (descendingChain r z (Nat.pred 0))) ∧ ¬Acc r (descendingChain r z 0)

case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ (i + 1 ≠ 0 → r (descendingChain r z (i + 1)) (descendingChain r z (i + 1).pred)) ∧
    ¬Acc r (descendingChain r z (i + 1))
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
case zero
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ (0 ≠ 0 → r (descendingChain r z 0) (descendingChain r z (Nat.pred 0))) ∧ ¬Acc r (descendingChain r z 0)
Tactic:
simpa using hz
Proof state after:
no goals
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ (i + 1 ≠ 0 → r (descendingChain r z (i + 1)) (descendingChain r z (i + 1).pred)) ∧
    ¬Acc r (descendingChain r z (i + 1))
Tactic:
simp[descendingChain]
Proof state after:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)
Tactic:
have : ∃ y, y ≺ (descendingChain r z i) ∧ ¬Acc r y := (not_acc_iff r).mp ih.2
Proof state after:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
this : ∃ y, r y (descendingChain r z i) ∧ ¬Acc r y
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)
Theorem: isInfiniteDescendingChain_of_non_acc
Proof state before:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
this : ∃ y, r y (descendingChain r z i) ∧ ¬Acc r y
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)
Tactic:
exact Classical.epsilon_spec this
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_KD_KT
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ 𝐊𝐃 ≤ₛ 𝐊𝐓
Tactic:
apply reducible_of_geach_defnability
Proof state after:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐃) F
Theorem: LO.Modal.Standard.reducible_KD_KT
Proof state before:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐃) F
Tactic:
simp_all [serial_of_refl]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_S4_S5
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ≤ₛ 𝐒𝟓
Tactic:
apply reducible_of_geach_defnability
Proof state after:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟒) F
Theorem: LO.Modal.Standard.reducible_S4_S5
Proof state before:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟒) F
Tactic:
simp_all [trans_of_refl_eucl]
Proof state after:
no goals
Theorem: LO.Modal.Standard.equiv_S5_KT4B
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ 𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁
Tactic:
apply equiv_of_geach_defnability
Proof state after:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F ↔
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓𝟒𝐁) F
Theorem: LO.Modal.Standard.equiv_S5_KT4B
Proof state before:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F ↔
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓𝟒𝐁) F
Tactic:
intros
Proof state after:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
F✝ : Frame
⊢ MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F✝ ↔
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓𝟒𝐁) F✝
Theorem: LO.Modal.Standard.equiv_S5_KT4B
Proof state before:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
F✝ : Frame
⊢ MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F✝ ↔
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓𝟒𝐁) F✝
Tactic:
constructor <;> simp_all [symm_of_refl_eucl, trans_of_refl_eucl, eucl_of_symm_trans]
Proof state after:
no goals
Theorem: Nat.pos_of_eq_one
Proof state before:
n : ℕ
h : n = 1
⊢ 0 < n
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Nat.isEqNat_pos_iff
Proof state before:
n m : ℕ
⊢ 0 < n.isEqNat m ↔ n = m
Tactic:
simp[isEqNat]
Proof state after:
n m : ℕ
⊢ (0 < if n = m then 1 else 0) ↔ n = m
Theorem: Nat.isEqNat_pos_iff
Proof state before:
n m : ℕ
⊢ (0 < if n = m then 1 else 0) ↔ n = m
Tactic:
by_cases n = m <;> simp[*]
Proof state after:
no goals
Theorem: Nat.isLtNat_pos_iff
Proof state before:
n m : ℕ
⊢ 0 < n.isLtNat m ↔ n < m
Tactic:
simp[isLtNat]
Proof state after:
n m : ℕ
⊢ (0 < if n < m then 1 else 0) ↔ n < m
Theorem: Nat.isLtNat_pos_iff
Proof state before:
n m : ℕ
⊢ (0 < if n < m then 1 else 0) ↔ n < m
Tactic:
by_cases n < m <;> simp[*]
Proof state after:
no goals
Theorem: Nat.isLeNat_pos_iff
Proof state before:
n m : ℕ
⊢ 0 < n.isLeNat m ↔ n ≤ m
Tactic:
simp[isLeNat]
Proof state after:
n m : ℕ
⊢ (0 < if n ≤ m then 1 else 0) ↔ n ≤ m
Theorem: Nat.isLeNat_pos_iff
Proof state before:
n m : ℕ
⊢ (0 < if n ≤ m then 1 else 0) ↔ n ≤ m
Tactic:
by_cases n ≤ m <;> simp[*]
Proof state after:
no goals
Theorem: Nat.isDvdNat_pos_iff
Proof state before:
n m : ℕ
⊢ 0 < n.isDvdNat m ↔ n ∣ m
Tactic:
simp[isDvdNat]
Proof state after:
n m : ℕ
⊢ (0 < if n ∣ m then 1 else 0) ↔ n ∣ m
Theorem: Nat.isDvdNat_pos_iff
Proof state before:
n m : ℕ
⊢ (0 < if n ∣ m then 1 else 0) ↔ n ∣ m
Tactic:
by_cases n ∣ m <;> simp[*]
Proof state after:
no goals
Theorem: Nat.inv_iff_ne_zero
Proof state before:
n : ℕ
⊢ n.inv = 0 ↔ 0 < n
Tactic:
simp[inv, isEqNat, zero_lt_iff]
Proof state after:
no goals
Theorem: Nat.inv_ne_zero
Proof state before:
n : ℕ
h : n ≠ 0
⊢ n.inv = 0
Tactic:
simp[inv, isEqNat, h]
Proof state after:
no goals
Theorem: Nat.pos_ne_zero
Proof state before:
n : ℕ
h : n ≠ 0
⊢ n.pos = 1
Tactic:
simp[pos, isLtNat, h]
Proof state after:
no goals
Theorem: Nat.and_eq
Proof state before:
n m : ℕ
⊢ n.and m = if 0 < n ∧ 0 < m then 1 else 0
Tactic:
simp[and, isLtNat]
Proof state after:
no goals
Theorem: Nat.and_eq_one
Proof state before:
n m : ℕ
⊢ n.and m = 1 ↔ 0 < n ∧ 0 < m
Tactic:
simp[and_eq, imp_false, Nat.pos_iff_ne_zero]
Proof state after:
no goals
Theorem: Nat.or_eq
Proof state before:
n m : ℕ
⊢ n.or m = if 0 < n ∨ 0 < m then 1 else 0
Tactic:
simp[or, isLtNat]
Proof state after:
no goals
Theorem: Nat.and_pos_iff
Proof state before:
n m : ℕ
⊢ 0 < n.and m ↔ 0 < n ∧ 0 < m
Tactic:
simp[and_eq]
Proof state after:
n m : ℕ
⊢ (0 < if 0 < n ∧ 0 < m then 1 else 0) ↔ 0 < n ∧ 0 < m
Theorem: Nat.and_pos_iff
Proof state before:
n m : ℕ
⊢ (0 < if 0 < n ∧ 0 < m then 1 else 0) ↔ 0 < n ∧ 0 < m
Tactic:
by_cases 0 < n ∧ 0 < m <;> simp[*]
Proof state after:
no goals
Theorem: Nat.or_pos_iff
Proof state before:
n m : ℕ
⊢ 0 < n.or m ↔ 0 < n ∨ 0 < m
Tactic:
simp[or_eq]
Proof state after:
n m : ℕ
⊢ (0 < if 0 < n ∨ 0 < m then 1 else 0) ↔ 0 < n ∨ 0 < m
Theorem: Nat.or_pos_iff
Proof state before:
n m : ℕ
⊢ (0 < if 0 < n ∨ 0 < m then 1 else 0) ↔ 0 < n ∨ 0 < m
Tactic:
by_cases 0 < n ∨ 0 < m <;> simp[*]
Proof state after:
no goals
Theorem: Nat.inv_pos_iff
Proof state before:
n : ℕ
⊢ 0 < n.inv ↔ ¬0 < n
Tactic:
simp[inv]
Proof state after:
no goals
Theorem: Nat.pos_pos_iff
Proof state before:
n : ℕ
⊢ 0 < n.pos ↔ 0 < n
Tactic:
simp[pos]
Proof state after:
no goals
Theorem: Nat.ball_pos_iff
Proof state before:
p : ℕ → ℕ
n : ℕ
⊢ 0 < n.ball p ↔ ∀ m < n, 0 < p m
Tactic:
induction' n with n ih <;> simp[ball, Nat.lt_succ_iff] at*
Proof state after:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m ≤ n, 0 < p m
Theorem: Nat.ball_pos_iff
Proof state before:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ 0 < p n ∧ 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m ≤ n, 0 < p m
Tactic:
simp[ih]
Proof state after:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (0 < p n ∧ ∀ m < n, 0 < p m) ↔ ∀ m ≤ n, 0 < p m
Theorem: Nat.ball_pos_iff
Proof state before:
case succ
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (0 < p n ∧ ∀ m < n, 0 < p m) ↔ ∀ m ≤ n, 0 < p m
Tactic:
exact ⟨
by rintro ⟨hn, hp⟩ m hm; rcases lt_or_eq_of_le hm with (hm | rfl); { exact hp _ hm }; { exact hn },
by intro h; exact ⟨h n (Nat.le_refl n), fun m hm => h m (le_of_lt hm)⟩⟩
Proof state after:
no goals
Theorem: Nat.ball_pos_iff
Proof state before:
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
⊢ (0 < p n ∧ ∀ m < n, 0 < p m) → ∀ m ≤ n, 0 < p m
Tactic:
rintro ⟨hn, hp⟩ m hm
Proof state after:
case intro
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm : m ≤ n
⊢ 0 < p m
Theorem: Nat.ball_pos_iff
Proof state before:
case intro
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm : m ≤ n
⊢ 0 < p m
Tactic:
rcases lt_or_eq_of_le hm with (hm | rfl)
Proof state after:
case intro.inl
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm✝ : m ≤ n
hm : m < n
⊢ 0 < p m

case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Theorem: Nat.ball_pos_iff
Proof state before:
case intro.inl
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm✝ : m ≤ n
hm : m < n
⊢ 0 < p m

case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Tactic:
{ exact hp _ hm }
Proof state after:
case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Theorem: Nat.ball_pos_iff
Proof state before:
case intro.inr
p : ℕ → ℕ
m : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) m ↔ ∀ m_1 < m, 0 < p m_1
hn : 0 < p m
hp : ∀ m_1 < m, 0 < p m_1
hm : m ≤ m
⊢ 0 < p m
Tactic:
{ exact hn }
Proof state after:
no goals
Theorem: Nat.ball_pos_iff
Proof state before:
case intro.inl
p : ℕ → ℕ
n : ℕ
ih : 0 < rec 1 (fun n ih => (p n).pos.and ih) n ↔ ∀ m < n, 0 < p m
hn : 0 < p n
hp : ∀ m < n, 0 < p m
m : ℕ
hm✝ : m ≤ n
hm : m < n
⊢ 0 < p m
Tactic:
exact hp _ hm
Proof state after:
no goals