α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p l
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
⊢ ∀ (l : List α), p l
let q := fun l ↦ p (reverse l)
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p l
have pq : ∀ l, p (reverse l) → q l := by simp only [reverse_reverse]; intro; exact id
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
⊢ ∀ (l : List α), p l
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l
have qp : ∀ l, q (reverse l) → p l := by simp only [reverse_reverse]; intro; exact id
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p l
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
⊢ ∀ (l : List α), p l
intro l
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q (reverse l)
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p l
apply qp
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l✝ l : List α
⊢ q l
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q (reverse l)
generalize (reverse l) = l
case a.nil
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q []

case a.cons
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (head :: tail)
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l✝ l : List α
⊢ q l
induction' l with head tail ih
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → p (reverse l)
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → q l
simp only [reverse_reverse]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
l✝ : List α
⊢ p (reverse l✝) → p (reverse l✝)
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → p (reverse l)
intro
no goals
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
l✝ : List α
⊢ p (reverse l✝) → p (reverse l✝)
exact id
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l → p l
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), q (reverse l) → p l
simp only [reverse_reverse]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
l✝ : List α
⊢ p l✝ → p l✝
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l → p l
intro
no goals
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
l✝ : List α
⊢ p l✝ → p l✝
exact id
case a.nil.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p (reverse [])
case a.nil
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q []
apply pq
no goals
case a.nil.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p (reverse [])
simp only [reverse_nil, base]
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse (head :: tail))
case a.cons
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (head :: tail)
apply pq
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail ++ [head])
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse (head :: tail))
simp only [reverse_cons]
case a.cons.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail)
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail ++ [head])
apply ind
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (reverse (reverse tail))
case a.cons.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail)
apply qp
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q tail
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (reverse (reverse tail))
rw [reverse_reverse]
no goals
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q tail
exact ih