Theorem: LO.FirstOrder.Arith.Theory.indScheme_subset (Arithmetization/Basic/Ind.lean)

State before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
⊢ indScheme L C ⊆ indScheme L C'
Tactic:
intro _
State after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ a✝ ∈ indScheme L C → a✝ ∈ indScheme L C'

State before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ a✝ ∈ indScheme L C → a✝ ∈ indScheme L C'
Tactic:
simp [indScheme]
State after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ ∀ (x : Semiformula L ℕ 1), C x → a✝ = ∀ᶠ* succInd x → ∃ p, C' p ∧ a✝ = ∀ᶠ* succInd p

State before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ ∀ (x : Semiformula L ℕ 1), C x → a✝ = ∀ᶠ* succInd x → ∃ p, C' p ∧ a✝ = ∀ᶠ* succInd p
Tactic:
rintro p hp rfl
State after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C' p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1

State before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C' p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1
Tactic:
exact ⟨p, h hp, rfl⟩
State after:
no goals