Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain (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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
⊢ IsMapping (m₁ ∪ m₂)
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain (m₁ ∪ m₂) → ∃! y, ⟪x, y⟫ ∈ m₁ ∪ m₂

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain (m₁ ∪ m₂) → ∃! y, ⟪x, y⟫ ∈ m₁ ∪ m₂
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain m₁ ∨ x ∈ domain m₂ → ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
⊢ x ∈ domain m₁ ∨ x ∈ domain m₂ → ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂
Tactic:
rintro (hx | hx)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
⊢ ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
⊢ ∃! y, ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
⊢ ⟪x, h₁.get hx⟫ ∈ m₁ ∨ ⟪x, h₁.get hx⟫ ∈ m₂
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
⊢ ∀ (y : M), ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₁.get hx
Tactic:
intro y
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₁.get hx

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₁.get hx
Tactic:
rintro (hy | hy)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₁.get hx

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₁.get hx

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₁.get hx
Tactic:
exact h₁.get_uniq hx hy
State after:
no goals

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₁.get hx
Tactic:
by_contra
State after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
x✝ : ¬y = h₁.get hx
⊢ False

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
x✝ : ¬y = h₁.get hx
⊢ False
Tactic:
exact Disjoint.not_of_mem hx (mem_domain_of_pair_mem hy) disjoint
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
⊢ ⟪x, h₂.get hx⟫ ∈ m₁ ∨ ⟪x, h₂.get hx⟫ ∈ m₂
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
⊢ ∀ (y : M), ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₂.get hx
Tactic:
intro y
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₂.get hx

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₂.get hx
Tactic:
rintro (hy | hy)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₂.get hx

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₂.get hx

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₂.get hx
Tactic:
by_contra
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
x✝ : ¬y = h₂.get hx
⊢ False

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
x✝ : ¬y = h₂.get hx
⊢ False
Tactic:
exact Disjoint.not_of_mem hx (mem_domain_of_pair_mem hy) disjoint.symm
State after:
no goals

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₂.get hx
Tactic:
exact h₂.get_uniq hx hy
State after:
no goals