internlm/Lean-Github huggingface dataset:
Theorem: Set.multimop_subset
Proof 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 ⊆ t
⊢ Set.multimop i n s ⊆ Set.multimop i n t
Tactic:
simp_all [Set.subset_def]
Proof state after:
no goals
Theorem: Set.premultimop_subset
Proof 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 ⊆ t
⊢ Set.premultimop i n s ⊆ Set.premultimop i n t
Tactic:
simp_all [Set.subset_def]
Proof state after:
no goals
Theorem: Set.subset_premulitimop_iff_multimop_subset
Proof 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
Proof 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
Theorem: Set.subset_premulitimop_iff_multimop_subset
Proof 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
Proof 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
Theorem: Set.subset_premulitimop_iff_multimop_subset
Proof 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₂
Proof 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
Theorem: Set.subset_premulitimop_iff_multimop_subset
Proof 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
Proof state after:
no goals
Theorem: Set.subset_multimop_iff_premulitimop_subset
Proof 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.premultimop i n s ⊆ t
Tactic:
intro p hp
Proof 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 ∈ Set.premultimop i n s
⊢ p ∈ t
Theorem: Set.subset_multimop_iff_premulitimop_subset
Proof 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 ∈ Set.premultimop i n s
⊢ p ∈ t
Tactic:
obtain ⟨_, h₁, h₂⟩ := premultimop_subset h hp
Proof 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 ∈ Set.premultimop i n s
w✝ : F
h₁ : w✝ ∈ t
h₂ : (mop i)^[n] w✝ = (mop i)^[n] p
⊢ p ∈ t
Theorem: Set.subset_multimop_iff_premulitimop_subset
Proof 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 ∈ Set.premultimop i n s
w✝ : F
h₁ : w✝ ∈ t
h₂ : (mop i)^[n] w✝ = (mop i)^[n] p
⊢ p ∈ t
Tactic:
simp_all
Proof state after:
no goals
Theorem: Set.forall_multimop_of_subset_multimop
Proof 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
Proof 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
Theorem: Set.forall_multimop_of_subset_multimop
Proof 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
Proof 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
Theorem: Set.forall_multimop_of_subset_multimop
Proof 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
Proof 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
Theorem: Set.forall_multimop_of_subset_multimop
Proof 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
Proof state after:
no goals
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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
Proof 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)
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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];
Proof 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)
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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];
Proof state after:
no goals
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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
Proof 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
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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
Proof 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
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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]
Proof state after:
no goals
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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
Proof 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)
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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
Proof 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)
Theorem: Set.eq_premultimop_multimop_of_subset_premultimop
Proof 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]
Proof state after:
no goals
Theorem: Finset.iff_mop_multimop_one
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ Finset.mop i s = Finset.multimop i 1 s
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.iff_premop_premultimop_one
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ Finset.premop i s = Finset.premultimop i 1 s
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.multimop_coe
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ ↑(Finset.multimop i n s) = Set.multimop i n ↑s
Tactic:
simp_all
Proof state after:
no goals
Theorem: Finset.multimop_mem_coe
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ p ∈ Finset.multimop i n s ↔ p ∈ Set.multimop i n ↑s
Tactic:
constructor <;> simp_all
Proof state after:
no goals
Theorem: Finset.premultimop_coe
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ ↑(Finset.premultimop i n s) = Set.premultimop i n ↑s
Tactic:
apply Finset.coe_preimage
Proof state after:
no goals
Theorem: Finset.premultimop_multimop_eq_of_subset_multimop
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Tactic:
have := Set.eq_premultimop_multimop_of_subset_premultimop hs
Proof state after:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : Set.multimop i n (Set.premultimop i n ↑s) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Theorem: Finset.premultimop_multimop_eq_of_subset_multimop
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : Set.multimop i n (Set.premultimop i n ↑s) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Tactic:
rw [←premultimop_coe, ←multimop_coe] at this
Proof state after:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : ↑(Finset.multimop i n (Finset.premultimop i n s)) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Theorem: Finset.premultimop_multimop_eq_of_subset_multimop
Proof state before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s✝ t✝ s : Finset F
t : Set F
hs : ↑s ⊆ Set.multimop i n t
this : ↑(Finset.multimop i n (Finset.premultimop i n s)) = ↑s
⊢ Finset.multimop i n (Finset.premultimop i n s) = s
Tactic:
exact Finset.coe_inj.mp this
Proof state after:
no goals
Theorem: List.mop_iff_multimop_one
Proof 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
⊢ List.mop i l = List.multimop i 1 l
Tactic:
rfl
Proof state after:
no goals
Theorem: List.iff_premop_premultimop_one
Proof 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
⊢ List.premop i l = List.premultimop i 1 l
Tactic:
rfl
Proof state after:
no goals
Theorem: List.multimop_nil
Proof 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
⊢ List.multimop i n [] = []
Tactic:
simp
Proof state after:
no goals
Theorem: List.multimop_single
Proof 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
⊢ List.multimop i n [p] = [(mop i)^[n] p]
Tactic:
simp
Proof state after:
no goals
Theorem: List.multimop_cons
Proof 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
hl : p ∉ l
⊢ List.multimop i n (p :: l) ~ (mop i)^[n] p :: List.multimop i n l
Tactic:
simp [List.multimop]
Proof 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
hl : p ∉ l
⊢ (insert ((mop i)^[n] p) (Finset.image (mop i)^[n] l.toFinset)).toList ~
    (mop i)^[n] p :: (Finset.multimop i n l.toFinset).toList
Theorem: List.multimop_cons
Proof 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
hl : p ∉ l
⊢ (insert ((mop i)^[n] p) (Finset.image (mop i)^[n] l.toFinset)).toList ~
    (mop i)^[n] p :: (Finset.multimop i n l.toFinset).toList
Tactic:
apply Finset.toList_insert
Proof 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
hl : p ∉ l
⊢ (mop i)^[n] p ∉ Finset.image (mop i)^[n] l.toFinset
Theorem: List.multimop_cons
Proof 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
hl : p ∉ l
⊢ (mop i)^[n] p ∉ Finset.image (mop i)^[n] l.toFinset
Tactic:
simp_all
Proof state after:
no goals
Theorem: List.premultimop_nil
Proof 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
⊢ List.premultimop i n [] = []
Tactic:
simp
Proof state after:
no goals
Theorem: List.forall_multimop_of_subset_multimop
Proof 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
Proof 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
Theorem: List.forall_multimop_of_subset_multimop
Proof 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;
Proof 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
Theorem: List.forall_multimop_of_subset_multimop
Proof 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
Proof 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
Theorem: List.forall_multimop_of_subset_multimop
Proof 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
Proof 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
Theorem: List.forall_multimop_of_subset_multimop
Proof 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
Proof state after:
no goals
Theorem: List.forall_multimop_of_subset_multimop
Proof 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
Proof state after:
no goals
Theorem: LO.StandardModalLogicalConnective.duality'
Proof state before:
F : Type u_1
inst✝ : StandardModalLogicalConnective F
p : F
⊢ ◇p = ~(□~p)
Tactic:
apply duality
Proof state after:
no goals
Theorem: LO.FirstOrder.ModelsTheory.of_provably_subtheory
Proof state before:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
⊢ ∀ ⦃f : Sentence L⦄, f ∈ T → inst✝.toStruc ⊧ f
Tactic:
intro p hp
Proof state after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
⊢ inst✝.toStruc ⊧ p
Theorem: LO.FirstOrder.ModelsTheory.of_provably_subtheory
Proof state before:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
⊢ inst✝.toStruc ⊧ p
Tactic:
have : U ⊢ p := System.Subtheory.prf (System.byAxm hp)
Proof state after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
this : U ⊢ p
⊢ inst✝.toStruc ⊧ p
Theorem: LO.FirstOrder.ModelsTheory.of_provably_subtheory
Proof state before:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
this : U ⊢ p
⊢ inst✝.toStruc ⊧ p
Tactic:
exact consequence_iff'.{u, w}.mp (sound! ⟨this⟩) M
Proof state after:
no goals
Theorem: LO.FirstOrder.ModelsTheory.of_add_left
Proof state before:
L : Language
M : Type w
inst✝² : Nonempty M
inst✝¹ : Structure L M
T U V : Theory L
inst✝ : M ⊧ₘ* T + U
⊢ T ⊆ T + U
Tactic:
simp [Theory.add_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.ModelsTheory.of_add_right
Proof state before:
L : Language
M : Type w
inst✝² : Nonempty M
inst✝¹ : Structure L M
T U V : Theory L
inst✝ : M ⊧ₘ* T + U
⊢ U ⊆ T + U
Tactic:
simp [Theory.add_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x : M), x + 0 = x
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addZero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_assoc
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y z : M), x + y + z = x + (y + z)
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addAssoc
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_comm
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y : M), x + y = y + x
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addComm
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_eq_of_lt
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y : M), x < y → ∃ z, x + z = y
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addEqOfLt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_le
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x : M), 0 ≤ x
Tactic:
simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.peanoMinus.zeroLe
Proof state after:
no goals