-- Mathlib/Data/List/Forall2.lean
theorem sublistForall₂_map_right_iff {f : γ → β} {l₁ : List α} {l₂ : List γ} :
    SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c => R a (f c)) l₁ l₂

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ Forall₂ (fun a c => R a (f c)) l₁ l' ∧ l' <+ l₂

Tactic:
simpa [hl1] using h1

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun a c => R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
use l1.map f

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun a c => R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ Forall₂ R l₁ (map f l1) ∧ map f l1 <+ map f l₂

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
l1 : List β
h1 : Forall₂ R l₁ l1
h2 : l1 <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2

Result:
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Proof state:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
rintro ⟨l1, h1, h2⟩

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
l1 : List β
h1 : Forall₂ R l₁ l1
h2 : l1 <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
use l'

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ Forall₂ (fun a c => R a (f c)) l₁ l' ∧ l' <+ l₂

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun a c => R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ Forall₂ R l₁ (map f l1) ∧ map f l1 <+ map f l₂

Tactic:
simp [h1, h2.map]

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
rintro ⟨l1, h1, h2⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun a c => R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c => R a (f c)) l₁ l₂

Tactic:
simp only [sublistForall₂_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) ↔ ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) ↔ ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c => R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂