Theorem: LO.FirstOrder.Arith.Model.two_dvd_mul (Arithmetization/Basic/IOpen.lean)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
⊢ 2 ∣ a * b → 2 ∣ a ∨ 2 ∣ b
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
⊢ 2 ∣ a ∨ 2 ∣ b

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
⊢ 2 ∣ a ∨ 2 ∣ b
Tactic:
by_contra A
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬(2 ∣ a ∨ 2 ∣ b)
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬(2 ∣ a ∨ 2 ∣ b)
⊢ False
Tactic:
simp [not_or] at A
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
⊢ False
Tactic:
have ha : a % 2 = 1 := by
  have : a % 2 = 0 ∨ a % 2 = 1 := mod_two a
  simpa [show a % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.1] using this
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ False
Tactic:
have hb : b % 2 = 1 := by
  have : b % 2 = 0 ∨ b % 2 = 1 :=
    le_one_iff_eq_zero_or_one.mp <| lt_two_iff_le_one.mp <| mod_lt b (b := 2) (by simp)
  simpa [show b % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.2] using this
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ False
Tactic:
have : a * b % 2 = 1 := by simp [mod_mul, ha, hb]
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ False
Tactic:
have : ¬2 ∣ a * b := by simp [←mod_eq_zero_iff_dvd, this]
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this✝ : a * b % 2 = 1
this : ¬2 ∣ a * b
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this✝ : a * b % 2 = 1
this : ¬2 ∣ a * b
⊢ False
Tactic:
contradiction
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
⊢ a % 2 = 1
Tactic:
have : a % 2 = 0 ∨ a % 2 = 1 := mod_two a
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
this : a % 2 = 0 ∨ a % 2 = 1
⊢ a % 2 = 1

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
this : a % 2 = 0 ∨ a % 2 = 1
⊢ a % 2 = 1
Tactic:
simpa [show a % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.1] using this
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
this : a % 2 = 0 ∨ a % 2 = 1
⊢ a % 2 ≠ 0
Tactic:
simpa [←mod_eq_zero_iff_dvd] using A.1
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ b % 2 = 1
Tactic:
have : b % 2 = 0 ∨ b % 2 = 1 :=
  le_one_iff_eq_zero_or_one.mp <| lt_two_iff_le_one.mp <| mod_lt b (b := 2) (by simp)
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
this : b % 2 = 0 ∨ b % 2 = 1
⊢ b % 2 = 1

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
this : b % 2 = 0 ∨ b % 2 = 1
⊢ b % 2 = 1
Tactic:
simpa [show b % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.2] using this
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ 0 < 2
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
this : b % 2 = 0 ∨ b % 2 = 1
⊢ b % 2 ≠ 0
Tactic:
simpa [←mod_eq_zero_iff_dvd] using A.2
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ a * b % 2 = 1
Tactic:
simp [mod_mul, ha, hb]
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ ¬2 ∣ a * b
Tactic:
simp [←mod_eq_zero_iff_dvd, this]
State after:
no goals