awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' :
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mp : ∀ (h' : dlookup (β := β) x (s₁.entries (β := β)) = some y),
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' :
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
mp :
  ∀ (h' : dlookup (β := β) x (s₁.entries (β := β)) = some y),
    dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
      ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mp₁ : ∀ (h' : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y),
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mp : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
Tactic: right
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mp : ¬x ∈ s₂.entries (β := β).keys (β := β)
Tactic: refine ⟨?_, h'⟩
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ ¬x ∈ s₂.entries (β := β).keys (β := β)
have mp : x ∈ s₁.keys (β := β)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ x ∈ s₁.keys (β := β)
have mp : (some y).isSome = true
Tactic: rw [keys, ← List.dlookup_isSome, h']
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mp : dlookup (β := β) x (s₂.entries (β := β)) = some y
Tactic: left
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₂.entries (β := β)) = some y
have mp : some y = some y
Tactic: rw [h'.2]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' :
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
have mpr : ∀ (h' : dlookup (β := β) x (s₂.entries (β := β)) = some y),
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' :
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
mpr :
  ∀ (h' : dlookup (β := β) x (s₂.entries (β := β)) = some y),
    dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
      ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
have mpr₁ : ∀ (h' : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y),
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
have mpr : ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
Tactic: right
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
⊢ ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
have mpr : ¬x ∈ s₁.entries (β := β).keys (β := β)
Tactic: refine ⟨?_, h'⟩
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
h'' : x ∈ s₁.entries (β := β).keys (β := β)
⊢ False
have mpr : x ∈ s₂.keys (β := β)
Tactic: apply h _ h''
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₂.entries (β := β)) = some y
h'' : x ∈ s₁.entries (β := β).keys (β := β)
⊢ x ∈ s₂.keys (β := β)
have mpr : (some y).isSome = true
Tactic: rw [keys, ← List.dlookup_isSome, h']
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
have mpr : dlookup (β := β) x (s₁.entries (β := β)) = some y
Tactic: left
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mpr : some y = some y
Tactic: rw [h'.2]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
⊢ a = b ∨ a ≠ b ∧ a ∈ l
have pos : ∀ (hab : a = b), a = b ∨ a ≠ b ∧ a ∈ l
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
pos : ∀ (hab : a = b), a = b ∨ a ≠ b ∧ a ∈ l
⊢ a = b ∨ a ≠ b ∧ a ∈ l
have neg : ∀ (hab : ¬a = b), a = b ∨ a ≠ b ∧ a ∈ l
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b c : α
⊢ a ∈ [b, c] ↔ a = b ∨ a = c
have rw : a = b ∨ a ∈ [c] ↔ a = b ∨ a = c
Tactic: rw [mem_cons, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b c : α
rw : a = b ∨ a ∈ [c] ↔ a = b ∨ a = c
⊢ a ∈ [b, c] ↔ a = b ∨ a = c
have rw₁ : a = b ∨ a = c ↔ a = b ∨ a = c
Tactic: rw [mem_cons, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
f : α → α
hf : Involutive f
a : α
l : List α
⊢ a ∈ map f l ↔ f a ∈ l
have rw : (∃ (a_1 : α), a_1 ∈ l ∧ f a_1 = a) ↔ f a ∈ l
Tactic: rw [mem_map, hf.exists_mem_and_apply_eq_iff]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
f : α → α
hf : Involutive f
a : α
l : List α
rw : (∃ (a_1 : α), a_1 ∈ l ∧ f a_1 = a) ↔ f a ∈ l
⊢ a ∈ map f l ↔ f a ∈ l
have rw₁ : f a ∈ l ↔ f a ∈ l
Tactic: rw [mem_map, hf.exists_mem_and_apply_eq_iff]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
⊢ Injective.{u + 1, 1} (α := List α) length ↔ Subsingleton α
have mp : Injective.{u + 1, 1} (α := List α) length → Subsingleton α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
mp : Injective.{u + 1, 1} (α := List α) length → Subsingleton α
⊢ Injective.{u + 1, 1} (α := List α) length ↔ Subsingleton α
have mpr : Subsingleton α → Injective.{u + 1, 1} (α := List α) length
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
⊢ Subsingleton α
have mp : ∀ (x y : α), x = y
Tactic: refine ⟨fun x y => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
x y : α
⊢ x = y
have mp : [x] = [y]
Tactic: suffices [x] = [y] by simpa using this
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
h : Injective.{u + 1, 1} (α := List α) length
x y : α
⊢ [x] = [y]
have mp : [x].length = [y].length
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
⊢ l1 = l2
have mpr : ∀ ⦃l2 : List α⦄ (hl : length.{u} (α := α) [] = l2.length), [] = l2
Tactic: induction l1 generalizing l2
Cleared hypotheses: l1, l2, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
mpr : ∀ ⦃l2 : List α⦄ (hl : length.{u} (α := α) [] = l2.length), [] = l2
⊢ l1 = l2
have mpr₁ : ∀ (head : α) (tail : List α),
  (∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2) →
    ∀ ⦃l2 : List α⦄ (hl : (head :: tail).length = l2.length), head :: tail = l2
Tactic: induction l1 generalizing l2
Cleared hypotheses: l1, l2, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
l2 : List α
hl : length.{u} (α := α) [] = l2.length
⊢ [] = l2
have mpr : ∀ (hl : length.{u} (α := α) [] = length.{u} (α := α) []), Eq.{u + 1} (α := List α) [] []
Tactic: cases l2
Cleared hypotheses: l2, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
l2 : List α
hl : length.{u} (α := α) [] = l2.length
mpr : ∀ (hl : length.{u} (α := α) [] = length.{u} (α := α) []), Eq.{u + 1} (α := List α) [] []
⊢ [] = l2
have mpr₁ : ∀ (head : α) (tail : List α) (hl : length.{u} (α := α) [] = (head :: tail).length), [] = head :: tail
Tactic: cases l2
Cleared hypotheses: l2, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
tail_ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
l2 : List α
hl : (head :: tail).length = l2.length
⊢ head :: tail = l2
have mpr : ∀ (hl : (head :: tail).length = length.{u} (α := α) []), head :: tail = []
Tactic: cases l2
Cleared hypotheses: l2, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
tail_ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
l2 : List α
hl : (head :: tail).length = l2.length
mpr : ∀ (hl : (head :: tail).length = length.{u} (α := α) []), head :: tail = []
⊢ head :: tail = l2
have mpr₁ : ∀ (head_1 : α) (tail_1 : List α) (hl : (head :: tail).length = (head_1 :: tail_1).length),
  head :: tail = head_1 :: tail_1
Tactic: cases l2
Cleared hypotheses: l2, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
⊢ head :: tail = head_1 :: tail_1
have e_head : head = head_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
e_head : head = head_1
⊢ head :: tail = head_1 :: tail_1
have e_tail : tail = tail_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
hα : Subsingleton α
head : α
tail : List α
ih : ∀ ⦃l2 : List α⦄ (hl : tail.length = l2.length), tail = l2
head_1 : α
tail_1 : List α
hl : (head :: tail).length = (head_1 :: tail_1).length
⊢ tail = tail_1
have e_tail : tail.length = tail_1.length
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
h : l ≠ []
⊢ l.length = 2 ↔ l = [l.head h, l.getLast h]
have rw : (∃ (a : α), ∃ (b : α), l = [a, b]) ↔ l = [l.head h, l.getLast h]
Tactic: rw [length_eq_two]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
x y : α
h : x ≠ y
⊢ {x, y} = [x, y]
have rw : ¬Membership.mem (γ := List α) {y} x
Tactic: rw [insert_neg, singleton_eq]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬Membership.mem (γ := List α) {y} x
have rwa : ¬x ∈ [y]
Tactic: rwa [singleton_eq, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
x y : α
h : x ≠ y
rwa : ¬x ∈ [y]
⊢ ¬Membership.mem (γ := List α) {y} x
have rwa₁ : ¬x = y
Tactic: rwa [singleton_eq, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂
have refine : map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
Tactic: refine ⟨?_, map_subset f⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
⊢ x ∈ l₂
have rcases : ∀ (x' : α) (hx' : x' ∈ l₂) (hxx' : f x' = f x), x ∈ l₂
Tactic: rcases mem_map.1 (h2 (mem_map_of_mem hx)) with ⟨x', hx', hxx'⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
hx'₁ : x ∈ l₂
⊢ x ∈ l₂
have hxx'₁ : f x = f x
Tactic: cases h hxx'
Cleared hypotheses: x', hx', hxx'
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a ++ replicate n a
have rw : replicate (m + n) a = replicate (m + n) a
Tactic: rw [replicate_append_replicate]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.head? = l.head?
have obtain : ∀ (n : ℕ) (h : n.succ ≠ 0), (replicate n.succ l).flatten.head? = l.head?
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ l).flatten.head? = l.head?
have nil : Eq.{u + 1} (α := Option α) (head? (flatten (replicate n.succ []))) (head? [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n.succ ≠ 0
nil : Eq.{u + 1} (α := Option α) (head? (flatten (replicate n.succ []))) (head? [])
⊢ (replicate n.succ l).flatten.head? = l.head?
have cons : ∀ (head : α) (tail : List α),
  (replicate n.succ tail).flatten.head? = tail.head? →
    (replicate n.succ (head :: tail)).flatten.head? = (head :: tail).head?
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.getLast? = l.getLast?
have rw : (replicate n l).flatten.reverse.head? = l.getLast?
Tactic: rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
rw : (replicate n l).flatten.reverse.head? = l.getLast?
⊢ (replicate n l).flatten.getLast? = l.getLast?
have rw₁ : (replicate n l).flatten.reverse.head? = l.reverse.head?
Tactic: rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
rw : (replicate n l).flatten.reverse.head? = l.getLast?
rw₁ : (replicate n l).flatten.reverse.head? = l.reverse.head?
⊢ (replicate n l).flatten.getLast? = l.getLast?
have rw₂ : (map reverse (replicate n l)).reverse.flatten.head? = l.reverse.head?
Tactic: rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
rw : (replicate n l).flatten.reverse.head? = l.getLast?
rw₁ : (replicate n l).flatten.reverse.head? = l.reverse.head?
rw₂ : (map reverse (replicate n l)).reverse.flatten.head? = l.reverse.head?
⊢ (replicate n l).flatten.getLast? = l.getLast?
have rw₃ : (replicate n l.reverse).reverse.flatten.head? = l.reverse.head?
Tactic: rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
rw : (replicate n l).flatten.reverse.head? = l.getLast?
rw₁ : (replicate n l).flatten.reverse.head? = l.reverse.head?
rw₂ : (map reverse (replicate n l)).reverse.flatten.head? = l.reverse.head?
rw₃ : (replicate n l.reverse).reverse.flatten.head? = l.reverse.head?
⊢ (replicate n l).flatten.getLast? = l.getLast?
have rw₄ : (replicate n l.reverse).flatten.head? = l.reverse.head?
Tactic: rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
rw : (replicate n l).flatten.reverse.head? = l.getLast?
rw₁ : (replicate n l).flatten.reverse.head? = l.reverse.head?
rw₂ : (map reverse (replicate n l)).reverse.flatten.head? = l.reverse.head?
rw₃ : (replicate n l.reverse).reverse.flatten.head? = l.reverse.head?
rw₄ : (replicate n l.reverse).flatten.head? = l.reverse.head?
⊢ (replicate n l).flatten.getLast? = l.getLast?
have rw₅ : l.reverse.head? = l.reverse.head?
Tactic: rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
a : α
⊢ (l ++ [a]).reverse = a :: l.reverse
have rw : [a].reverse ++ l.reverse = a :: l.reverse
Tactic: rw [reverse_append]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h
have nil : ([] ++ l₂).getLast sorry = l₂.getLast h
Tactic: induction l₁ with grind
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
nil : ([] ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h
have cons : ∀ (head : α) (tail : List α), (tail ++ l₂).getLast sorry = l₂.getLast h → (head :: tail ++ l₂).getLast sorry = l₂.getLast h
Tactic: induction l₁ with grind
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l
have rw : a :: ((b :: l).dropLast ++ [(b :: l).getLast sorry]) = a :: b :: l
Tactic: rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l
have e_tail : (b :: l).dropLast ++ [(b :: l).getLast sorry] = b :: l
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
h₁ : l₁ ≠ []
h₂ : l₂ ≠ []
h₃ : l₁ = l₂
⊢ l₁.getLast h₁ = l₂.getLast h₂
have subst : ∀ (h₁ : l₂ ≠ []), l₂.getLast h₁ = l₂.getLast h₂
Tactic: subst l₁
Cleared hypotheses: l₁, h₁, h₃
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
m : ℕ
a : α
⊢ (replicate (m + 1) a).getLast ⋯ = a
have simp : (replicate m a ++ [a]).getLast sorry = a
Tactic: simp only [replicate_succ']
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
have hc₁ : c ∈ (b :: l).getLast?
Tactic: rw [getLast?_cons_cons] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
have rw : a :: (b :: l).dropLast ++ [c] = a :: b :: l
Tactic: rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
rw : a :: (b :: l).dropLast ++ [c] = a :: b :: l
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
have rw₁ : a :: ((b :: l).dropLast ++ [c]) = a :: b :: l
Tactic: rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
rw : a :: (b :: l).dropLast ++ [c] = a :: b :: l
rw₁ : a :: ((b :: l).dropLast ++ [c]) = a :: b :: l
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
have rw₂ : a :: b :: l = a :: b :: l
Tactic: rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
have rw : (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
Tactic: rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
rw : (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
have rw₁ : (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
Tactic: rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]