awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
have rw₁ : s₁ ×ˢ s₂ ⊆ Prod.swap ⁻¹' R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
rw₁ : s₁ ×ˢ s₂ ⊆ Prod.swap ⁻¹' R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
have rw₂ : Prod.swap '' s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
rw₁ : s₁ ×ˢ s₂ ⊆ Prod.swap ⁻¹' R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₂ : Prod.swap '' s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
have rw₃ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
rw₁ : s₁ ×ˢ s₂ ⊆ Prod.swap ⁻¹' R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₂ : Prod.swap '' s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₃ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
have rw₄ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R.inv
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst : R.IsSymm
rw : s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
rw₁ : s₁ ×ˢ s₂ ⊆ Prod.swap ⁻¹' R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₂ : Prod.swap '' s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₃ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
rw₄ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R.inv
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
have rw₅ : s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s : Set α
R : SetRel α α
inst : R.IsSymm
⊢ R.preimage s = R.image s
have rw : R.preimage s = R.inv.preimage s
Tactic: rw [← preimage_inv, inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
s : Set α
R : SetRel α α
inst : R.IsSymm
rw : R.preimage s = R.inv.preimage s
⊢ R.preimage s = R.image s
have rw₁ : R.preimage s = R.preimage s
Tactic: rw [← preimage_inv, inv_eq_self]
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∃! f : α → β, Function.graph f = R) ↔ ∀ (a : α), ∃! b : β, (a, b) ∈ R
have mp : (∃! f : α → β, Function.graph f = R) → ∀ (a : α), ∃! b : β, (a, b) ∈ R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
mp : (∃! f : α → β, Function.graph f = R) → ∀ (a : α), ∃! b : β, (a, b) ∈ R
⊢ (∃! f : α → β, Function.graph f = R) ↔ ∀ (a : α), ∃! b : β, (a, b) ∈ R
have mpr : (∀ (a : α), ∃! b : β, (a, b) ∈ R) → ∃! f : α → β, Function.graph f = R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
⊢ ∃! f : α → β, Function.graph f = R
have mpr : ∀ (f : (x : α) → β) (hf : ∀ (x : α), (x, f x) ∈ R), ∃! f : α → β, Function.graph f = R
Tactic: choose f hf using fun x ↦ (h x).exists
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
⊢ ∃! f : α → β, Function.graph f = R
have mpr : (fun (f : α → β) ↦ Function.graph f = R) f
Tactic: refine ⟨f, ?_, by aesop⟩
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
⊢ (fun (f : α → β) ↦ Function.graph f = R) f
have mpr : ∀ (a : α) (b : β), (a, b) ∈ Function.graph f ↔ (a, b) ∈ R
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ Function.graph f ↔ (a, b) ∈ R
have mpr : (a, b) ∈ Function.graph f → (a, b) ∈ R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rel (goal)
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b : β, (a, b) ∈ R
f : (x : α) → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
mpr : (a, b) ∈ Function.graph f → (a, b) ∈ R
⊢ (a, b) ∈ Function.graph f ↔ (a, b) ∈ R
have mpr₁ : (a, b) ∈ R → (a, b) ∈ Function.graph f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s
have refine : ∀ (h : q₁.s = q₂.s), q₁ = q₂
Tactic: refine ⟨congr_arg _, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂
have obtain : ∀ (s : Set α) (v₁ : Trunc (↑s : Type u_1)) (h : { s := s, val := v₁ : Semiquot α }.s = q₂.s),
  { s := s, val := v₁ : Semiquot α } = q₂
Tactic: obtain ⟨_, v₁⟩ := q₁
Cleared hypotheses: q₁, h
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q₂ : Semiquot α
s : Set α
v₁ : Trunc (↑s : Type u_1)
h : { s := s, val := v₁ : Semiquot α }.s = q₂.s
⊢ { s := s, val := v₁ : Semiquot α } = q₂
have obtain : ∀ (s_1 : Set α) (v₂ : Trunc (↑s_1 : Type u_1)) (h : { s := s, val := v₁ : Semiquot α }.s = { s := s_1, val := v₂ }.s),
  { s := s, val := v₁ : Semiquot α } = { s := s_1, val := v₂ }
Tactic: obtain ⟨_, v₂⟩ := q₂
Cleared hypotheses: q₂, h
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
s : Set α
v₁ : Trunc (↑s : Type u_1)
s_1 : Set α
v₂ : Trunc (↑s_1 : Type u_1)
h : { s := s, val := v₁ : Semiquot α }.s = { s := s_1, val := v₂ }.s
⊢ { s := s, val := v₁ : Semiquot α } = { s := s_1, val := v₂ }
have h₁ : v₁ ≍ v₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ q.blur' (s := s ∪ q.s) ⋯ = q.blur' (s := s) h
have e_s : s ∪ q.s = s
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ a ∈ q, ∀ b ∈ q, f a = f b
a : α
aq : a ∈ q
⊢ q.liftOn f h = f a
have revert : ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a
have rw : ∀ (h : ∀ a_1 ∈ mk (s := q.s) aq, ∀ b ∈ mk (s := q.s) aq, f a_1 = f b), (mk (s := q.s) aq).liftOn f h = f a
Tactic: rw [eq_mk_of_mem aq]
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a
have simp_rw : b ∈ q.bind f ↔ ∃ (a : α) (_ : a ∈ q), b ∈ f a
Tactic: simp_rw [← exists_prop]
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ Membership.mem (γ := Semiquot γ) (s >>= fun (x : α) ↦ f x >>= g) a
have simp : ∀ (a : γ), (∃ (a_1 : β), (∃ a ∈ s, a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1 ∈ s, ∃ a_2 ∈ f a_1, a ∈ g a_2
Tactic: simp only [bind_def, mem_bind]
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
⊢ q.get p ∈ q
have let : ∀ (a : α) (h : a ∈ q), q.get p ∈ q
Tactic: let ⟨a, h⟩ := exists_mem q
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.get p ∈ q
have unfold : q.liftOn id p ∈ q
Tactic: unfold get
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q
have rw : id a ∈ q
Tactic: rw [liftOn_ofMem q _ _ a h]
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
a b : α
ab : Membership.mem (γ := Semiquot α) (pure a) b
c : α
ac : Membership.mem (γ := Semiquot α) (pure a) c
⊢ b = c
have rw : ∀ (ab : b = a) (c : α) (ac : c = a), b = c
Tactic: rw [mem_pure] at ab ac
Cleared hypotheses: ab, c, ac
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
have rwa : ∀ (ab : b = c) (ac : c = a), b = c
Tactic: rwa [← ac] at ab
Cleared hypotheses: ab, ac
-- Lean 4 proof step from Mathlib.Data.Semiquot (goal)
Goal:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ t ≤ s
have rw : LE.le (α := Semiquot α) (pure (t.get h)) (pure (s.get sorry))
Tactic: rw [eq_pure h, eq_pure (h.mono st)]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
⊢ length.{u} (α := α) nil ⋯ = 0
have simp : TerminatedAt.{u} (α := α) nil 0
Tactic: simp [length]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
s : Seq α
h : s.Terminates
⊢ (cons x s).length ⋯ = s.length h + 1
have h0 : ¬(cons x s).TerminatedAt 0
Tactic: apply Nat.find_comp_succ
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
s : Seq α
⊢ (cons x s).length' = s.length' + 1
have pos : ∀ (h : (cons x s).Terminates), (cons x s).length' = s.length' + 1
Tactic: by_cases h : (cons x s).Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
s : Seq α
pos : ∀ (h : (cons x s).Terminates), (cons x s).length' = s.length' + 1
⊢ (cons x s).length' = s.length' + 1
have neg : ∀ (h : ¬(cons x s).Terminates), (cons x s).length' = s.length' + 1
Tactic: by_cases h : (cons x s).Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
x : α
s : Seq α
h h' : (cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1
have h'₁ : s.Terminates
Tactic: rw [terminates_cons_iff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
x : α
s : Seq α
h h' : ¬(cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1
have h'₁ : ¬s.Terminates
Tactic: rw [terminates_cons_iff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ s.length' = 0 ↔ s = nil
have nil : length'.{u} (α := α) nil = 0 ↔ Eq.{u + 1} (α := Seq α) nil nil
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
nil : length'.{u} (α := α) Seq.nil = 0 ↔ Eq.{u + 1} (α := Seq α) Seq.nil Seq.nil
⊢ s.length' = 0 ↔ s = Seq.nil
have cons : ∀ (x : α) (s : Seq α), (cons x s).length' = 0 ↔ cons x s = Seq.nil
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ s.length' ≠ 0 ↔ ∃ (x : α) (s' : Seq α), s = cons x s'
have nil : length'.{u} (α := α) nil ≠ 0 ↔ ∃ (x : α) (s' : Seq α), nil = cons x s'
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
nil : length'.{u} (α := α) Seq.nil ≠ 0 ↔ ∃ (x : α) (s' : Seq α), Seq.nil = cons x s'
⊢ s.length' ≠ 0 ↔ ∃ (x : α) (s' : Seq α), s = cons x s'
have cons : ∀ (x : α) (s : Seq α), (cons x s).length' ≠ 0 ↔ ∃ (x_1 : α) (s' : Seq α), cons x s = cons x_1 s'
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (∃ (h : s.Terminates), s.length h ≤ n) ↔ s.TerminatedAt n
have simp : ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none
Tactic: simp only [length, Nat.find_le_iff, TerminatedAt, Terminates, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none
have refine_1 : ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
refine_1 : ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none
⊢ ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none
have refine_2 : s.get? n = none → (∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ s.TerminatedAt n
have rw : s.length h ≤ n ↔ ∃ (h : s.Terminates), s.length h ≤ n
Tactic: rw [← length_le_iff']
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
have pos : ∀ (h : s.Terminates), s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
Tactic: by_cases h : s.Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
pos : ∀ (h : s.Terminates), s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
⊢ s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
have neg : ∀ (h : ¬s.Terminates), s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
Tactic: by_cases h : s.Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (h : s.Terminates), n < s.length h) ↔ ∃ (a : α), a ∈ s.get? n
have simp : (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) ↔ ¬s.get? n = none
Tactic: simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
    ← Option.ne_none_iff_exists', ne_eq]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) ↔ ¬s.get? n = none
have refine_1 : (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
refine_1 : (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none
⊢ (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) ↔ ¬s.get? n = none
have refine_2 : ¬s.get? n = none → ∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∃ (a : α), a ∈ s.get? n
have rw : n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h
Tactic: rw [← lt_length_iff']
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
have pos : ∀ (h : s.Terminates), (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
Tactic: by_cases h : s.Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
pos : ∀ (h : s.Terminates), (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
⊢ (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
have neg : ∀ (h : ¬s.Terminates), (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
Tactic: by_cases h : s.Terminates
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
have neg : ∃ (a : α), s.get? n = some a
Tactic: simp only [length'_of_not_terminates h, ENat.coe_lt_top, Option.mem_def, true_iff]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ∃ (a : α), s.get? n = some a
have h₁ : ∀ (n : ℕ), (s.get? n).isSome = true
Tactic: rw [not_terminates_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ ∃ (a : α), s.get? n = some a
have neg : (s.get? n).isSome = true
Tactic: rw [← Option.isSome_iff_exists]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s : Stream' α
⊢ (↑(a :: s) : Seq α) = cons a (↑s : Seq α)
have a₁ : (↑(↑(a :: s) : Seq α) : Stream' (Option α)) = (↑(cons a (↑s : Seq α)) : Stream' (Option α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s
have a₁ : some a :: Stream'.map some s = some a :: Stream'.map some s
Tactic: rw [Stream'.map_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := List α) (take n nil) []
have zero : Eq.{u + 1} (α := List α) (take 0 nil) []
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
zero : Eq.{u + 1} (α := List α) (take 0 nil) []
⊢ Eq.{u + 1} (α := List α) (take n nil) []
have succ : ∀ (n : ℕ), Eq.{u + 1} (α := List α) (take (n + 1) nil) []
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ take 0 s = []
have nil : Eq.{u + 1} (α := List α) (take 0 nil) []
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
nil : Eq.{u + 1} (α := List α) (take 0 Seq.nil) []
⊢ take 0 s = []
have cons : ∀ (x : α) (s : Seq α), take 0 (cons x s) = []
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n k : ℕ
s : Seq α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (k + 1) s) n =
    if n < k + 1 then s.get? n else none
have rw : getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
    (match (motive := Option (Seq1 α) → List α) s.destruct with
      | none => []
      | some (x, r) => x :: take k r :
      List α)
    n =
  if n < k + 1 then s.get? n else none
Tactic: rw [take]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none
have rw : getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
    (match (motive := Option (Seq1 α) → List α) some (x, r) with
      | none => []
      | some (x, r) => x :: take k r :
      List α)
    n =
  if n < k + 1 then (cons x r).get? n else none
Tactic: rw [destruct_eq_cons h]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n k : ℕ
s : Seq α
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) s.destruct with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none
have cases : ∀ (x : Option (Seq1 α)) (h : s.destruct = x),
  getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) x with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none
Tactic: cases h : destruct s with
    | none =>
      simp [destruct_eq_none h]
    | some a =>
      match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
⊢ x ∈ take n s
have zero : ∀ (l : ℕ) (hl : l + 1 = n), x ∈ take n s
Tactic: obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈ take n s
have zero : Membership.mem (γ := List α)
  (match (motive := Option (Seq1 α) → List α) (cons x s.tail).destruct with
    | none => []
    | some (x, r) => x :: take l r :
    List α)
  x
Tactic: rw [← hl, take, head_eq_some h_get]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
n : ℕ
h_mn : k + 1 < n
h_get : s.get? (k + 1) = some x
⊢ x ∈ take n s
have succ : ∀ (l : ℕ) (h_mn : k + 1 < k + 1 + l + 1), x ∈ take (k + 1 + l + 1) s
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt h_mn
Cleared hypotheses: n, h_mn
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
⊢ ∃ (y : α), s.get? 0 = some y
have apply : 0 ≤ k + 1
Tactic: apply ge_stable _ _ h_get
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
⊢ x ∈ take (k + 1 + l + 1) s
have this : ∃ (y : α), s.get? 0 = some y
Tactic: have : ∃ y, s.get? 0 = some y := by
      apply ge_stable _ _ h_get
      simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
this : ∃ (y : α), s.get? 0 = some y
⊢ x ∈ take (k + 1 + l + 1) s
have succ : ∀ (y : α) (hy : s.get? 0 = some y), x ∈ take (k + 1 + l + 1) s
Tactic: obtain ⟨y, hy⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x ∈ take (k + 1 + l + 1) s
have succ : Membership.mem (γ := List α)
  (match (motive := Option (Seq1 α) → List α) (cons y s.tail).destruct with
    | none => []
    | some (x, r) => x :: take (k + 1 + l) r :
    List α)
  x
Tactic: rw [take, head_eq_some hy]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ Membership.mem (γ := List α)
    (match (motive := Option (Seq1 α) → List α) (cons y s.tail).destruct with
      | none => []
      | some (x, r) => x :: take (k + 1 + l) r :
      List α)
    x
have succ : x = y ∨ x ∈ take (k + 1 + l) s.tail
Tactic: simp only [destruct_cons, List.mem_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x = y ∨ x ∈ take (k + 1 + l) s.tail
have succ : x ∈ take (k + 1 + l) s.tail
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x ∈ take (k + 1 + l) s.tail
have succ : s.tail.get? k = some x
Tactic: apply ih (by lia)