Theorem: List.forall_multimop_of_subset_multimop (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
⊢ ∀ p ∈ l, ∃ q ∈ s, p = (mop i)^[n] q
Tactic:
intro p hp
State after:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
⊢ ∃ q ∈ s, p = (mop i)^[n] q

State before:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
⊢ ∃ q ∈ s, p = (mop i)^[n] q
Tactic:
obtain ⟨q, _, _⟩ := by simpa only [Set.mem_image] using h p hp;
State after:
case intro.intro
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q✝ : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
q : F
left✝ : q ∈ s
right✝ : (mop i)^[n] q = p
⊢ ∃ q ∈ s, p = (mop i)^[n] q

State before:
case intro.intro
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q✝ : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
q : F
left✝ : q ∈ s
right✝ : (mop i)^[n] q = p
⊢ ∃ q ∈ s, p = (mop i)^[n] q
Tactic:
use q
State after:
case h
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q✝ : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
q : F
left✝ : q ∈ s
right✝ : (mop i)^[n] q = p
⊢ q ∈ s ∧ p = (mop i)^[n] q

State before:
case h
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q✝ : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
q : F
left✝ : q ∈ s
right✝ : (mop i)^[n] q = p
⊢ q ∈ s ∧ p = (mop i)^[n] q
Tactic:
subst_vars
State after:
case h
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q✝ : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
q : F
left✝ : q ∈ s
hp : (mop i)^[n] q ∈ l
⊢ q ∈ s ∧ (mop i)^[n] q = (mop i)^[n] q

State before:
case h
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p q✝ : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
q : F
left✝ : q ∈ s
hp : (mop i)^[n] q ∈ l
⊢ q ∈ s ∧ (mop i)^[n] q = (mop i)^[n] q
Tactic:
simpa
State after:
no goals

State before:
ι : Type u_2
F : Type u_1
inst✝³ : UnaryModalOperator ι F
inst✝² : DecidableEq F
i : ι
n : ℕ
p✝ q : F
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
l : List F
s : Set F
h : ∀ p ∈ l, p ∈ Set.multimop i n s
p : F
hp : p ∈ l
⊢ ?m.51038
Tactic:
simpa only [Set.mem_image] using h p hp
State after:
no goals