Theorem: Set.subset_premulitimop_iff_multimop_subset (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.premultimop i n t
⊢ Set.multimop i n s ⊆ t
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.premultimop i n t
p : F
hp : p ∈ Set.multimop i n s
⊢ p ∈ t

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.premultimop i n t
p : F
hp : p ∈ Set.multimop i n s
⊢ p ∈ t
Tactic:
obtain ⟨_, h₁, h₂⟩ := multimop_subset 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.premultimop i n t
p : F
hp : p ∈ Set.multimop i n s
w✝ : F
h₁ : w✝ ∈ Set.premultimop i n t
h₂ : (mop i)^[n] w✝ = p
⊢ p ∈ t

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.premultimop i n t
p : F
hp : p ∈ Set.multimop i n s
w✝ : F
h₁ : w✝ ∈ Set.premultimop i n t
h₂ : (mop i)^[n] w✝ = p
⊢ p ∈ t
Tactic:
subst h₂
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.premultimop i n t
w✝ : F
h₁ : w✝ ∈ Set.premultimop i n t
hp : (mop i)^[n] w✝ ∈ Set.multimop i n s
⊢ (mop i)^[n] w✝ ∈ t

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.premultimop i n t
w✝ : F
h₁ : w✝ ∈ Set.premultimop i n t
hp : (mop i)^[n] w✝ ∈ Set.multimop i n s
⊢ (mop i)^[n] w✝ ∈ t
Tactic:
assumption
State after:
no goals