Theorem: LO.FirstOrder.Arith.Model.domain_union (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 ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ ∀ (i : M), i ∈ domain (a ∪ b) ↔ i ∈ domain a ∪ domain b
Tactic:
simp [mem_domain_iff]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ ∀ (i : M), (∃ y, ⟪i, y⟫ ∈ a ∨ ⟪i, y⟫ ∈ b) ↔ (∃ y, ⟪i, y⟫ ∈ a) ∨ ∃ y, ⟪i, y⟫ ∈ b

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ ∀ (i : M), (∃ y, ⟪i, y⟫ ∈ a ∨ ⟪i, y⟫ ∈ b) ↔ (∃ y, ⟪i, y⟫ ∈ a) ∨ ∃ y, ⟪i, y⟫ ∈ b
Tactic:
intro x
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) ↔ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) ↔ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
constructor
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) → (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ ((∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b) → ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ (∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b) → (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
rintro ⟨y, (hy | hy)⟩
State after:
case mp.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b

case mp.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b

State before:
case mp.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
left
State after:
case mp.intro.inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a

State before:
case mp.intro.inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a
Tactic:
exact ⟨y, hy⟩
State after:
no goals

State before:
case mp.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ (∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
right
State after:
case mp.intro.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ b

State before:
case mp.intro.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ b
Tactic:
exact ⟨y, hy⟩
State after:
no goals

State before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x : M
⊢ ((∃ y, ⟪x, y⟫ ∈ a) ∨ ∃ y, ⟪x, y⟫ ∈ b) → ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Tactic:
rintro (⟨y, hy⟩ | ⟨y, hy⟩)
State after:
case mpr.inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b

case mpr.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b

State before:
case mpr.inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ a
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Tactic:
exact ⟨y, Or.inl hy⟩
State after:
no goals

State before:
case mpr.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b x y : M
hy : ⟪x, y⟫ ∈ b
⊢ ∃ y, ⟪x, y⟫ ∈ a ∨ ⟪x, y⟫ ∈ b
Tactic:
exact ⟨y, Or.inr hy⟩
State after:
no goals