-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
    l₁.isSublist l₂ ↔ l₁ <+ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ (if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true) ↔
    hd₁ :: tl₁ <+ hd₂ :: tl₂

Tactic:
simp only [beq_iff_eq, h_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ (if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true) ↔ hd₁ :: tl₁ <+ hd₂ :: tl₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : hd₁ = hd₂
⊢ (if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true) ↔
    hd₁ :: tl₁ <+ hd₂ :: tl₂

Tactic:
simp [h_eq, cons_sublist_cons, isSublist_iff_sublist]

Result:
no goals

Proof state:
case mpr.cons₂
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ tl₂ : List α
h_eq : ¬hd₁ = hd₁
a✝ : tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Tactic:
case cons₂ =>
  contradiction

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : hd₁ :: tl₁ <+ hd₂ :: tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Tactic:
cases h_sub

Result:
case mpr.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
a✝ : hd₁ :: tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

case mpr.cons₂
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ tl₂ : List α
h_eq : ¬hd₁ = hd₁
a✝ : tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Proof state:
case mpr.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
a✝ : hd₁ :: tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

case mpr.cons₂
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ tl₂ : List α
h_eq : ¬hd₁ = hd₁
a✝ : tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Tactic:
case cons h_sub =>
  exact isSublist_iff_sublist.mpr h_sub

Result:
case mpr.cons₂
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ tl₂ : List α
h_eq : ¬hd₁ = hd₁
a✝ : tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ (if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true) ↔ hd₁ :: tl₁ <+ hd₂ :: tl₂

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ (if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true) → hd₁ :: tl₁ <+ hd₂ :: tl₂

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ hd₁ :: tl₁ <+ hd₂ :: tl₂ → if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true
⊢ hd₁ :: tl₁ <+ hd₂ :: tl₂

Tactic:
apply Sublist.cons

Result:
case mp.a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true
⊢ hd₁ :: tl₁ <+ tl₂

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ (if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true) → hd₁ :: tl₁ <+ hd₂ :: tl₂

Tactic:
intro h_sub

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true
⊢ hd₁ :: tl₁ <+ hd₂ :: tl₂

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
⊢ hd₁ :: tl₁ <+ hd₂ :: tl₂ → if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Tactic:
intro h_sub

Result:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : hd₁ :: tl₁ <+ hd₂ :: tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Proof state:
case mp.a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true
⊢ hd₁ :: tl₁ <+ tl₂

Tactic:
exact isSublist_iff_sublist.mp h_sub

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ : List α
hd₂ : α
tl₂ : List α
h_eq : ¬hd₁ = hd₂
h_sub : hd₁ :: tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Tactic:
exact isSublist_iff_sublist.mpr h_sub

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
⊢ l₁.isSublist l₂ = true ↔ l₁ <+ l₂

Tactic:
cases l₁ <;> cases l₂ <;> simp [isSublist]

Result:
case cons.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
⊢ (if (head✝¹ == head✝) = true then tail✝¹.isSublist tail✝ = true else (head✝¹ :: tail✝¹).isSublist tail✝ = true) ↔
    head✝¹ :: tail✝¹ <+ head✝ :: tail✝

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hd₁ : α
tl₁ tl₂ : List α
h_eq : ¬hd₁ = hd₁
a✝ : tl₁ <+ tl₂
⊢ if False then tl₁.isSublist tl₂ = true else (hd₁ :: tl₁).isSublist tl₂ = true

Tactic:
contradiction

Result:
no goals