Theorem: LO.Cumulative.subset_of_le (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
⊢ T s₁ ⊆ T s₂
Tactic:
suffices ∀ s d, T s ⊆ T (s + d) by
  simpa[Nat.add_sub_of_le h] using this s₁ (s₂ - s₁)
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
⊢ ∀ (s d : ℕ), T s ⊆ T (s + d)

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
⊢ ∀ (s d : ℕ), T s ⊆ T (s + d)
Tactic:
intro s d
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
⊢ T s ⊆ T (s + d)

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
⊢ T s ⊆ T (s + d)
Tactic:
induction' d with d ih
State after:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T (s + 0)

case succ
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
ih : T s ⊆ T (s + d)
⊢ T s ⊆ T (s + (d + 1))

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
this : ∀ (s d : ℕ), T s ⊆ T (s + d)
⊢ T s₁ ⊆ T s₂
Tactic:
simpa[Nat.add_sub_of_le h] using this s₁ (s₂ - s₁)
State after:
no goals

State before:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T (s + 0)
Tactic:
simp
State after:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T s

State before:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T s
Tactic:
rfl
State after:
no goals

State before:
case succ
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
ih : T s ⊆ T (s + d)
⊢ T s ⊆ T (s + (d + 1))
Tactic:
simpa only [Nat.add_succ, add_zero] using subset_trans ih (H (s + d))
State after:
no goals