Theorem: Set.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
s t : Set F
h : s ⊆ Set.multimop i n t
⊢ ∀ p ∈ s, ∃ q ∈ t, 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
s t : Set F
h : s ⊆ Set.multimop i n t
p : F
hp : p ∈ s
⊢ ∃ q ∈ t, 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
s t : Set F
h : s ⊆ Set.multimop i n t
p : F
hp : p ∈ s
⊢ ∃ q ∈ t, p = (mop i)^[n] q
Tactic:
obtain ⟨q, hq₁, hq₂⟩ := h hp
State after:
case intro.intro
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p✝ q✝ : F
s t : Set F
h : s ⊆ Set.multimop i n t
p : F
hp : p ∈ s
q : F
hq₁ : q ∈ t
hq₂ : (mop i)^[n] q = p
⊢ ∃ q ∈ t, 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
s t : Set F
h : s ⊆ Set.multimop i n t
p : F
hp : p ∈ s
q : F
hq₁ : q ∈ t
hq₂ : (mop i)^[n] q = p
⊢ ∃ q ∈ t, 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
s t : Set F
h : s ⊆ Set.multimop i n t
p : F
hp : p ∈ s
q : F
hq₁ : q ∈ t
hq₂ : (mop i)^[n] q = p
⊢ q ∈ t ∧ 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
s t : Set F
h : s ⊆ Set.multimop i n t
p : F
hp : p ∈ s
q : F
hq₁ : q ∈ t
hq₂ : (mop i)^[n] q = p
⊢ q ∈ t ∧ p = (mop i)^[n] q
Tactic:
simp_all
State after:
no goals