Theorem: LO.FirstOrder.Arith.Model.sUnion_graph (Arithmetization/ISigmaOne/HFS/Basic.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
⊢ u = ⋃ʰᶠ s → ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
Tactic:
rintro rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ ∀ x < ⋃ʰᶠ s + s, x ∈ ⋃ʰᶠ s ↔ ∃ t ∈ s, x ∈ t

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
⊢ ∀ x < ⋃ʰᶠ s + s, x ∈ ⋃ʰᶠ s ↔ ∃ t ∈ s, x ∈ t
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
⊢ (∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t) → u = ⋃ʰᶠ s
Tactic:
intro h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ u = ⋃ʰᶠ s

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ u = ⋃ʰᶠ s
Tactic:
apply mem_ext
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ ∀ (i : M), i ∈ u ↔ i ∈ ⋃ʰᶠ s

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
⊢ ∀ (i : M), i ∈ u ↔ i ∈ ⋃ʰᶠ s
Tactic:
intro x
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ ⋃ʰᶠ s

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ ⋃ʰᶠ s
Tactic:
simp
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ ∃ c ∈ s, x ∈ c

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ ∃ c ∈ s, x ∈ c
Tactic:
constructor
State after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u → ∃ c ∈ s, x ∈ c

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ (∃ c ∈ s, x ∈ c) → x ∈ u

State before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u → ∃ c ∈ s, x ∈ c
Tactic:
intro hx
State after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
hx : x ∈ u
⊢ ∃ c ∈ s, x ∈ c

State before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
hx : x ∈ u
⊢ ∃ c ∈ s, x ∈ c
Tactic:
exact h x (lt_of_lt_of_le (lt_of_mem hx) (by simp)) |>.mp hx
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
hx : x ∈ u
⊢ u ≤ u + s
Tactic:
simp
State after:
no goals

State before:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ (∃ c ∈ s, x ∈ c) → x ∈ u
Tactic:
rintro ⟨c, hc, hx⟩
State after:
case h.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x c : M
hc : c ∈ s
hx : x ∈ c
⊢ x ∈ u

State before:
case h.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x c : M
hc : c ∈ s
hx : x ∈ c
⊢ x ∈ u
Tactic:
exact h x (lt_of_lt_of_le (lt_trans _ _ _ (lt_of_mem hx) (lt_of_mem hc)) (by simp)) |>.mpr ⟨c, hc, hx⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x c : M
hc : c ∈ s
hx : x ∈ c
⊢ s ≤ u + s
Tactic:
simp
State after:
no goals