Theorem: Set.eq_premultimop_multimop_of_subset_premultimop (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
⊢ Set.multimop i n (Set.premultimop i n s) = s
Tactic:
apply Set.eq_of_subset_of_subset
State after:
case a
ι : 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
⊢ Set.multimop i n (Set.premultimop i n s) ⊆ s

case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)

State before:
case a
ι : 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
⊢ Set.multimop i n (Set.premultimop i n s) ⊆ s

case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)
Tactic:
. intro p hp;
  obtain ⟨q, hq₁, hq₂⟩ := hp;
  simp_all [Set.premultimop];
State after:
case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)

State before:
case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)
Tactic:
. intro p hp;
  obtain ⟨q, _, hq₂⟩ := forall_multimop_of_subset_multimop h p hp;
  simp_all [Set.premultimop];
State after:
no goals

State before:
case a
ι : 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
⊢ Set.multimop i n (Set.premultimop i n s) ⊆ s
Tactic:
intro p hp
State after:
case a
ι : 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 ∈ Set.multimop i n (Set.premultimop i n s)
⊢ p ∈ s

State before:
case a
ι : 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 ∈ Set.multimop i n (Set.premultimop i n s)
⊢ p ∈ s
Tactic:
obtain ⟨q, hq₁, hq₂⟩ := hp
State after:
case a.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 q : F
hq₁ : q ∈ Set.premultimop i n s
hq₂ : (mop i)^[n] q = p
⊢ p ∈ s

State before:
case a.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 q : F
hq₁ : q ∈ Set.premultimop i n s
hq₂ : (mop i)^[n] q = p
⊢ p ∈ s
Tactic:
simp_all [Set.premultimop]
State after:
no goals

State before:
case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)
Tactic:
intro p hp
State after:
case a
ι : 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
⊢ p ∈ Set.multimop i n (Set.premultimop i n s)

State before:
case a
ι : 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
⊢ p ∈ Set.multimop i n (Set.premultimop i n s)
Tactic:
obtain ⟨q, _, hq₂⟩ := forall_multimop_of_subset_multimop h p hp
State after:
case a.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
left✝ : q ∈ t
hq₂ : p = (mop i)^[n] q
⊢ p ∈ Set.multimop i n (Set.premultimop i n s)

State before:
case a.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
left✝ : q ∈ t
hq₂ : p = (mop i)^[n] q
⊢ p ∈ Set.multimop i n (Set.premultimop i n s)
Tactic:
simp_all [Set.premultimop]
State after:
no goals