internlm/Lean-Github huggingface dataset:
Theorem: Arith.Model.Definable.retraction
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : Fin k → Fin n
snd✝ : ℕ
p : HSemiformula L M k (𝚷, snd✝)
h : DefinedWithParam P p
⊢ DefinedWithParam (fun v => P fun i => v (f i)) (HSemiformula.rew (Rew.substs fun i => #(f i)) p)
Tactic:
intro
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : Fin k → Fin n
snd✝ : ℕ
p : HSemiformula L M k (𝚷, snd✝)
h : DefinedWithParam P p
v✝ : Fin n → M
⊢ (fun v => P fun i => v (f i)) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.rew (Rew.substs fun i => #(f i)) p).val
Theorem: Arith.Model.Definable.retraction
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : Fin k → Fin n
snd✝ : ℕ
p : HSemiformula L M k (𝚷, snd✝)
h : DefinedWithParam P p
v✝ : Fin n → M
⊢ (fun v => P fun i => v (f i)) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.rew (Rew.substs fun i => #(f i)) p).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.Definable.retraction
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : Fin k → Fin n
snd✝ : ℕ
p : HSemiformula L M k (𝚫, snd✝)
h : DefinedWithParam P p
⊢ FirstOrder.DefinedWithParam (fun v => P fun i => v (f i)) (HSemiformula.rew (Rew.substs fun i => #(f i)) p).val
Tactic:
intro
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : Fin k → Fin n
snd✝ : ℕ
p : HSemiformula L M k (𝚫, snd✝)
h : DefinedWithParam P p
v✝ : Fin n → M
⊢ (fun v => P fun i => v (f i)) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.rew (Rew.substs fun i => #(f i)) p).val
Theorem: Arith.Model.Definable.retraction
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : Fin k → Fin n
snd✝ : ℕ
p : HSemiformula L M k (𝚫, snd✝)
h : DefinedWithParam P p
v✝ : Fin n → M
⊢ (fun v => P fun i => v (f i)) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.rew (Rew.substs fun i => #(f i)) p).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
⊢ Definable L (?m.560332, 0) fun x => P
Tactic:
by_cases hP : P
Proof state after:
case pos
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : P
⊢ Definable L (?m.560332, 0) fun x => P

case neg
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : ¬P
⊢ Definable L (?m.560332, 0) fun x => P
Theorem: Arith.Model.Definable.const
Proof state before:
case pos
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : P
⊢ Definable L (?m.560332, 0) fun x => P
Tactic:
exact ⟨.mkSigma ⊤ (by simp), by intro; simp[hP]⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : P
⊢ Hierarchy 𝚺 0 ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : P
⊢ DefinedWithParam (fun x => P) (HSemiformula.mkSigma ⊤ ⋯)
Tactic:
intro
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : P
v✝ : Fin k → M
⊢ (fun x => P) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.mkSigma ⊤ ⋯).val
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : P
v✝ : Fin k → M
⊢ (fun x => P) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.mkSigma ⊤ ⋯).val
Tactic:
simp[hP]
Proof state after:
no goals
Theorem: Arith.Model.Definable.const
Proof state before:
case neg
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : ¬P
⊢ Definable L (𝚺, 0) fun x => P
Tactic:
exact ⟨.mkSigma ⊥ (by simp), by intro; simp[hP]⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : ¬P
⊢ Hierarchy 𝚺 0 ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : ¬P
⊢ DefinedWithParam (fun x => P) (HSemiformula.mkSigma ⊥ ⋯)
Tactic:
intro
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : ¬P
v✝ : Fin k → M
⊢ (fun x => P) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.mkSigma ⊥ ⋯).val
Theorem: Arith.Model.Definable.const
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
P : Prop
hP : ¬P
v✝ : Fin k → M
⊢ (fun x => P) v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.mkSigma ⊥ ⋯).val
Tactic:
simp[hP]
Proof state after:
no goals
Theorem: Arith.Model.Definable.and
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
h₁ : Definable L Γ P
h₂ : Definable L Γ Q
⊢ Definable L Γ fun v => P v ∧ Q v
Tactic:
rcases h₁ with ⟨p₁, h₁⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
h₂ : Definable L Γ Q
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
⊢ Definable L Γ fun v => P v ∧ Q v
Theorem: Arith.Model.Definable.and
Proof state before:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
h₂ : Definable L Γ Q
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
⊢ Definable L Γ fun v => P v ∧ Q v
Tactic:
rcases h₂ with ⟨p₂, h₂⟩
Proof state after:
case mk.intro.mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k Γ
h₂ : DefinedWithParam Q p₂
⊢ Definable L Γ fun v => P v ∧ Q v
Theorem: Arith.Model.Definable.and
Proof state before:
case mk.intro.mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k Γ
h₂ : DefinedWithParam Q p₂
⊢ Definable L Γ fun v => P v ∧ Q v
Tactic:
exact ⟨p₁ ⋏ p₂, h₁.and h₂⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.or
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
h₁ : Definable L Γ P
h₂ : Definable L Γ Q
⊢ Definable L Γ fun v => P v ∨ Q v
Tactic:
rcases h₁ with ⟨p₁, h₁⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
h₂ : Definable L Γ Q
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
⊢ Definable L Γ fun v => P v ∨ Q v
Theorem: Arith.Model.Definable.or
Proof state before:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
h₂ : Definable L Γ Q
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
⊢ Definable L Γ fun v => P v ∨ Q v
Tactic:
rcases h₂ with ⟨p₂, h₂⟩
Proof state after:
case mk.intro.mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k Γ
h₂ : DefinedWithParam Q p₂
⊢ Definable L Γ fun v => P v ∨ Q v
Theorem: Arith.Model.Definable.or
Proof state before:
case mk.intro.mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
p₁ : HSemiformula L M k Γ
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k Γ
h₂ : DefinedWithParam Q p₂
⊢ Definable L Γ fun v => P v ∨ Q v
Tactic:
exact ⟨p₁ ⋎ p₂, h₁.or h₂⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.not
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h : Definable L (Γ.alt, m) P
⊢ Definable L (Γ, m) fun v => ¬P v
Tactic:
match Γ with
| 𝚺 => rcases h with ⟨p, h⟩; exact ⟨p.negPi, h.negPi⟩
| 𝚷 => rcases h with ⟨p, h⟩; exact ⟨p.negSigma, h.negSigma⟩
| 𝚫 => rcases h with ⟨p, h⟩; exact ⟨p.negDelta, h.not⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.not
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h : Definable L (𝚺.alt, m) P
⊢ Definable L (𝚺, m) fun v => ¬P v
Tactic:
rcases h with ⟨p, h⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p : HSemiformula L M k (𝚺.alt, m)
h : DefinedWithParam P p
⊢ Definable L (𝚺, m) fun v => ¬P v
Theorem: Arith.Model.Definable.not
Proof state before:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p : HSemiformula L M k (𝚺.alt, m)
h : DefinedWithParam P p
⊢ Definable L (𝚺, m) fun v => ¬P v
Tactic:
exact ⟨p.negPi, h.negPi⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.not
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h : Definable L (𝚷.alt, m) P
⊢ Definable L (𝚷, m) fun v => ¬P v
Tactic:
rcases h with ⟨p, h⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p : HSemiformula L M k (𝚷.alt, m)
h : DefinedWithParam P p
⊢ Definable L (𝚷, m) fun v => ¬P v
Theorem: Arith.Model.Definable.not
Proof state before:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p : HSemiformula L M k (𝚷.alt, m)
h : DefinedWithParam P p
⊢ Definable L (𝚷, m) fun v => ¬P v
Tactic:
exact ⟨p.negSigma, h.negSigma⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.not
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h : Definable L (𝚫.alt, m) P
⊢ Definable L (𝚫, m) fun v => ¬P v
Tactic:
rcases h with ⟨p, h⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p : HSemiformula L M k (𝚫.alt, m)
h : DefinedWithParam P p
⊢ Definable L (𝚫, m) fun v => ¬P v
Theorem: Arith.Model.Definable.not
Proof state before:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p : HSemiformula L M k (𝚫.alt, m)
h : DefinedWithParam P p
⊢ Definable L (𝚫, m) fun v => ¬P v
Tactic:
exact ⟨p.negDelta, h.not⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.imp
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h₁ : Definable L (Γ.alt, m) P
h₂ : Definable L (Γ, m) Q
⊢ Definable L (Γ, m) fun v => P v → Q v
Tactic:
match Γ with
| 𝚺 =>
  rcases h₁ with ⟨p₁, h₁⟩; rcases h₂ with ⟨p₂, h₂⟩
  exact ⟨p₁.negPi.or p₂, (h₁.negPi.or h₂).of_iff (fun x ↦ by simp [imp_iff_not_or])⟩
| 𝚷 =>
  rcases h₁ with ⟨p₁, h₁⟩; rcases h₂ with ⟨p₂, h₂⟩
  exact ⟨p₁.negSigma.or p₂, (h₁.negSigma.or h₂).of_iff (fun x ↦ by simp [imp_iff_not_or])⟩
| 𝚫 =>
  rcases h₁ with ⟨p₁, h₁⟩; rcases h₂ with ⟨p₂, h₂⟩; exact ⟨p₁ ⟶ p₂, h₁.imp h₂⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.imp
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h₁ : Definable L (𝚺.alt, m) P
h₂ : Definable L (𝚺, m) Q
⊢ Definable L (𝚺, m) fun v => P v → Q v
Tactic:
rcases h₁ with ⟨p₁, h₁⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h₂ : Definable L (𝚺, m) Q
p₁ : HSemiformula L M k (𝚺.alt, m)
h₁ : DefinedWithParam P p₁
⊢ Definable L (𝚺, m) fun v => P v → Q v
Theorem: Arith.Model.Definable.imp
Proof state before:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h₂ : Definable L (𝚺, m) Q
p₁ : HSemiformula L M k (𝚺.alt, m)
h₁ : DefinedWithParam P p₁
⊢ Definable L (𝚺, m) fun v => P v → Q v
Tactic:
rcases h₂ with ⟨p₂, h₂⟩
Proof state after:
case mk.intro.mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p₁ : HSemiformula L M k (𝚺.alt, m)
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k (𝚺, m)
h₂ : DefinedWithParam Q p₂
⊢ Definable L (𝚺, m) fun v => P v → Q v
Theorem: Arith.Model.Definable.imp
Proof state before:
case mk.intro.mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p₁ : HSemiformula L M k (𝚺.alt, m)
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k (𝚺, m)
h₂ : DefinedWithParam Q p₂
⊢ Definable L (𝚺, m) fun v => P v → Q v
Tactic:
exact ⟨p₁.negPi.or p₂, (h₁.negPi.or h₂).of_iff (fun x ↦ by simp [imp_iff_not_or])⟩
Proof state after:
no goals
Theorem: Arith.Model.Definable.imp
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
p₁ : HSemiformula L M k (𝚺.alt, m)
h₁ : DefinedWithParam P p₁
p₂ : HSemiformula L M k (𝚺, m)
h₂ : DefinedWithParam Q p₂
x : Fin k → M
⊢ P x → Q x ↔ ¬P x ∨ Q x
Tactic:
simp [imp_iff_not_or]
Proof state after:
no goals
Theorem: Arith.Model.Definable.imp
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h₁ : Definable L (𝚷.alt, m) P
h₂ : Definable L (𝚷, m) Q
⊢ Definable L (𝚷, m) fun v => P v → Q v
Tactic:
rcases h₁ with ⟨p₁, h₁⟩
Proof state after:
case mk.intro
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
h₂ : Definable L (𝚷, m) Q
p₁ : HSemiformula L M k (𝚷.alt, m)
h₁ : DefinedWithParam P p₁
⊢ Definable L (𝚷, m) fun v => P v → Q v