internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
⊢ s ∈ a ^ˢ k ×ˢ a
Tactic:
have : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x := Seq.cases_iff.mp Hs
Proof state after:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
this : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
⊢ s ∈ a ^ˢ k ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
this : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
⊢ s ∈ a ^ˢ k ×ˢ a
Tactic:
rcases this with (rfl | ⟨x, s, Hs', rfl⟩)
Proof state after:
case mpr.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Hs : Seq ∅
hsk : lh ∅ = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a
⊢ ∅ ∈ a ^ˢ k ×ˢ a

case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Hs : Seq ∅
hsk : lh ∅ = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a
⊢ ∅ ∈ a ^ˢ k ×ˢ a
Tactic:
simp [eq_comm] at hsk
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
have hsk : lh s = k := by simpa [Hs'] using hsk
Proof state after:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
have hx : x ∈ a := hs k x (by simp [←hsk])
Proof state after:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
have hs : s ∈ a ^ˢ k := @ih s |>.mpr ⟨Hs', hsk, fun i z hiz ↦ hs i z (Seq.subset_seqCons s x hiz)⟩
Proof state after:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs✝ : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
hs : s ∈ a ^ˢ k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs✝ : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
hs : s ∈ a ^ˢ k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
exact seqCons_mem_seqProduct hs hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ lh s = k
Tactic:
simpa [Hs'] using hsk
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
⊢ ⟪k, x⟫ ∈ s ⁀' x
Tactic:
simp [←hsk]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Monotone.term_monotone
Proof state before:
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
t : Semiterm L ξ n
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
⊢ Semiterm.valm M e₁ ε₁ t ≤ Semiterm.valm M e₂ ε₂ t
Tactic:
induction t <;> simp [*, Semiterm.val_func]
Proof state after:
case func
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.valm M e₁ ε₁ (a✝ a) ≤ Semiterm.valm M e₂ ε₂ (a✝ a)
⊢ (func a✝¹ fun i => Semiterm.val inst✝¹ e₁ ε₁ (a✝ i)) ≤ func a✝¹ fun i => Semiterm.val inst✝¹ e₂ ε₂ (a✝ i)
Theorem: LO.FirstOrder.Structure.Monotone.term_monotone
Proof state before:
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
ih : ∀ (a : Fin k), Semiterm.valm M e₁ ε₁ (v a) ≤ Semiterm.valm M e₂ ε₂ (v a)
⊢ (func f fun i => Semiterm.val inst✝¹ e₁ ε₁ (v i)) ≤ func f fun i => Semiterm.val inst✝¹ e₂ ε₂ (v i)
Tactic:
case func k f v ih =>
  exact Monotone.monotone f _ _ ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Monotone.term_monotone
Proof state before:
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
ih : ∀ (a : Fin k), Semiterm.valm M e₁ ε₁ (v a) ≤ Semiterm.valm M e₂ ε₂ (v a)
⊢ (func f fun i => Semiterm.val inst✝¹ e₁ ε₁ (v i)) ≤ func f fun i => Semiterm.val inst✝¹ e₂ ε₂ (v i)
Tactic:
exact Monotone.monotone f _ _ ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.numeral_two_eq_two
Proof 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 c : M
⊢ ORingSymbol.numeral 2 = 2
Tactic:
simp [numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.numeral_three_eq_three
Proof 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 c : M
⊢ ORingSymbol.numeral 3 = 3
Tactic:
simp [numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.numeral_four_eq_four
Proof 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 c : M
⊢ ORingSymbol.numeral 4 = 4
Tactic:
simp [numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_iff_succ_le
Proof 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 c : M
⊢ a < b ↔ a + 1 ≤ b
Tactic:
simp [le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.succ_le_iff_lt
Proof 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 c : M
⊢ a + 1 ≤ b ↔ a < b
Tactic:
simp [le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_iff_one_le
Proof 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 c : M
⊢ 0 < a ↔ 1 ≤ a
Tactic:
simp [lt_iff_succ_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.one_lt_iff_two_le
Proof 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 c : M
⊢ 1 < a ↔ 2 ≤ a
Tactic:
simp [lt_iff_succ_le, one_add_one_eq_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_nonpos
Proof 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 c a : M
⊢ ¬a < 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_two_iff_le_one
Proof 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 c : M
⊢ a < 2 ↔ a ≤ 1
Tactic:
simp [lt_iff_succ_le,
  show a + 1 ≤ 2 ↔ a ≤ 1 from by
    rw[show (2 : M) = 1 + 1 from one_add_one_eq_two.symm]; exact add_le_add_iff_right 1]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_two_iff_le_one
Proof 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 c : M
⊢ a + 1 ≤ 2 ↔ a ≤ 1
Tactic:
rw[show (2 : M) = 1 + 1 from one_add_one_eq_two.symm]
Proof 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 c : M
⊢ a + 1 ≤ 1 + 1 ↔ a ≤ 1
Theorem: LO.FirstOrder.Arith.Model.lt_two_iff_le_one
Proof 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 c : M
⊢ a + 1 ≤ 1 + 1 ↔ a ≤ 1
Tactic:
exact add_le_add_iff_right 1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof 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 c : M
⊢ a < 1 → a = 0
Tactic:
intro hx
Proof 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 c : M
hx : a < 1
⊢ a = 0
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof 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 c : M
hx : a < 1
⊢ a = 0
Tactic:
have : a ≤ 0 := by exact le_iff_lt_succ.mpr (show a < 0 + 1 from by simpa using hx)
Proof 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 c : M
hx : a < 1
this : a ≤ 0
⊢ a = 0
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof 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 c : M
hx : a < 1
this : a ≤ 0
⊢ a = 0
Tactic:
exact nonpos_iff_eq_zero.mp this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof 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 c : M
hx : a < 1
⊢ a ≤ 0
Tactic:
exact le_iff_lt_succ.mpr (show a < 0 + 1 from by simpa using hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof 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 c : M
hx : a < 1
⊢ a < 0 + 1
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof 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 c : M
⊢ a = 0 → a < 1
Tactic:
rintro rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 0 < 1
Theorem: LO.FirstOrder.Arith.Model.lt_one_iff_eq_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 0 < 1
Tactic:
exact zero_lt_one
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_one_iff_eq_zero_or_one
Proof 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 c : M
⊢ a ≤ 1 → a = 0 ∨ a = 1
Tactic:
intro h
Proof 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 c : M
h : a ≤ 1
⊢ a = 0 ∨ a = 1
Theorem: LO.FirstOrder.Arith.Model.le_one_iff_eq_zero_or_one
Proof 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 c : M
h : a ≤ 1
⊢ a = 0 ∨ a = 1
Tactic:
rcases h with (rfl | ltx)
Proof 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 1 = 0 ∨ 1 = 1

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ltx : a < 1
⊢ a = 0 ∨ a = 1
Theorem: LO.FirstOrder.Arith.Model.le_one_iff_eq_zero_or_one
Proof 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 1 = 0 ∨ 1 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_one_iff_eq_zero_or_one
Proof 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
ltx : a < 1
⊢ a = 0 ∨ a = 1
Tactic:
simp [show a = 0 from by simpa using ltx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_one_iff_eq_zero_or_one
Proof 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 c : M
ltx : a < 1
⊢ a = 0
Tactic:
simpa using ltx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_one_iff_eq_zero_or_one
Proof 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 c : M
⊢ a = 0 ∨ a = 1 → a ≤ 1
Tactic:
rintro (rfl | rfl) <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof 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 c : M
⊢ a ≤ 2 → a = 0 ∨ a = 1 ∨ a = 2
Tactic:
intro h
Proof 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 c : M
h : a ≤ 2
⊢ a = 0 ∨ a = 1 ∨ a = 2
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof 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 c : M
h : a ≤ 2
⊢ a = 0 ∨ a = 1 ∨ a = 2
Tactic:
rcases h with (rfl | lt)
Proof 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 2 = 0 ∨ 2 = 1 ∨ 2 = 2

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt : a < 2
⊢ a = 0 ∨ a = 1 ∨ a = 2
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 2 = 0 ∨ 2 = 1 ∨ 2 = 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt : a < 2
⊢ a = 0 ∨ a = 1 ∨ a = 2
Tactic:
rcases lt_two_iff_le_one.mp lt with (rfl | lt)
Proof state after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
lt : 1 < 2
⊢ 1 = 0 ∨ 1 = 1 ∨ 1 = 2

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝ : a < 2
lt : a < 1
⊢ a = 0 ∨ a = 1 ∨ a = 2
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof state before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
lt : 1 < 2
⊢ 1 = 0 ∨ 1 = 1 ∨ 1 = 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof state before:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝ : a < 2
lt : a < 1
⊢ a = 0 ∨ a = 1 ∨ a = 2
Tactic:
simp [show a = 0 from by simpa using lt]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof 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 c : M
lt✝ : a < 2
lt : a < 1
⊢ a = 0
Tactic:
simpa using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_iff_eq_zero_or_one_or_two
Proof 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 c : M
⊢ a = 0 ∨ a = 1 ∨ a = 2 → a ≤ 2
Tactic:
rintro (rfl | rfl | rfl) <;> simp [one_le_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof 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 c : M
⊢ a ≤ 3 → a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Tactic:
intro h
Proof 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 c : M
h : a ≤ 3
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof 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 c : M
h : a ≤ 3
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Tactic:
rcases h with (rfl | lt)
Proof 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 3 = 0 ∨ 3 = 1 ∨ 3 = 2 ∨ 3 = 3

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt : a < 3
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 3 = 0 ∨ 3 = 1 ∨ 3 = 2 ∨ 3 = 3
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt : a < 3
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Tactic:
have : a ≤2 := by simpa [←le_iff_lt_succ, ←two_add_one_eq_three] using lt
Proof 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt : a < 3
this : a ≤ 2
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt : a < 3
this : a ≤ 2
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Tactic:
rcases this with (rfl| lt)
Proof state after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
lt : 2 < 3
⊢ 2 = 0 ∨ 2 = 1 ∨ 2 = 2 ∨ 2 = 3

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝ : a < 3
lt : a < 2
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof 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 c : M
lt : a < 3
⊢ a ≤ 2
Tactic:
simpa [←le_iff_lt_succ, ←two_add_one_eq_three] using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof state before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
lt : 2 < 3
⊢ 2 = 0 ∨ 2 = 1 ∨ 2 = 2 ∨ 2 = 3
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof state before:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝ : a < 3
lt : a < 2
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Tactic:
rcases lt_two_iff_le_one.mp lt with (rfl | lt)
Proof state after:
case inr.inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
lt✝ : 1 < 3
lt : 1 < 2
⊢ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 3

case inr.inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝¹ : a < 3
lt✝ : a < 2
lt : a < 1
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof state before:
case inr.inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
lt✝ : 1 < 3
lt : 1 < 2
⊢ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 3
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_three
Proof state before:
case inr.inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝¹ : a < 3
lt✝ : a < 2
lt : a < 1
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3
Tactic:
simp [show a = 0 from by simpa using lt]
Proof state after:
no goals