Theorem: LO.FirstOrder.Arith.Model.domain_bitRemove_of_isMapping_of_mem (Arithmetization/ISigmaOne/HFS/Seq.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ domain (bitRemove ⟪x, y⟫ s) = bitRemove x (domain 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), i ∈ domain (bitRemove ⟪x, y⟫ s) ↔ i ∈ bitRemove x (domain 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), i ∈ domain (bitRemove ⟪x, y⟫ s) ↔ i ∈ bitRemove x (domain s)
Tactic:
simp [mem_domain_iff]
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), (∃ y_1, (i = x → ¬y_1 = y) ∧ ⟪i, y_1⟫ ∈ s) ↔ ¬i = x ∧ ∃ y, ⟪i, y⟫ ∈ 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
⊢ ∀ (i : M), (∃ y_1, (i = x → ¬y_1 = y) ∧ ⟪i, y_1⟫ ∈ s) ↔ ¬i = x ∧ ∃ y, ⟪i, y⟫ ∈ 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) ↔ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ 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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) ↔ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) → ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s) → ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s

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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s) → ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Tactic:
rintro ⟨y₁, hy₁, hx₁y₁⟩
State after:
case h.mp.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ y₁ : M
hy₁ : x₁ = x → ¬y₁ = y
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s

State before:
case h.mp.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ y₁ : M
hy₁ : x₁ = x → ¬y₁ = y
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s
Tactic:
exact ⟨by rintro rfl; exact hy₁ rfl (hs.uniq hx₁y₁ hxy), y₁, hx₁y₁⟩
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ y₁ : M
hy₁ : x₁ = x → ¬y₁ = y
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ¬x₁ = x
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 ⊧ₘ* 𝐈𝚺₁
y s : M
hs : IsMapping s
x₁ y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
hxy : ⟪x₁, y⟫ ∈ s
hy₁ : x₁ = x₁ → ¬y₁ = y
⊢ False

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
y s : M
hs : IsMapping s
x₁ y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
hxy : ⟪x₁, y⟫ ∈ s
hy₁ : x₁ = x₁ → ¬y₁ = y
⊢ False
Tactic:
exact hy₁ rfl (hs.uniq hx₁y₁ hxy)
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
⊢ (¬x₁ = x ∧ ∃ y, ⟪x₁, y⟫ ∈ s) → ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s
Tactic:
intro ⟨hx, y₁, hx₁y₁⟩
State after:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s

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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ ∃ y_1, (x₁ = x → ¬y_1 = y) ∧ ⟪x₁, y_1⟫ ∈ s
Tactic:
exact ⟨y₁, by intro _; contradiction, hx₁y₁⟩
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 ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
⊢ x₁ = x → ¬y₁ = y
Tactic:
intro _
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
a✝ : x₁ = x
⊢ ¬y₁ = y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y s : M
hs : IsMapping s
hxy : ⟪x, y⟫ ∈ s
x₁ : M
hx : ¬x₁ = x
y₁ : M
hx₁y₁ : ⟪x₁, y₁⟫ ∈ s
a✝ : x₁ = x
⊢ ¬y₁ = y
Tactic:
contradiction
State after:
no goals