internlm/Lean-Github huggingface dataset:
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { toByte := u.val.toUInt8, valid := ⋯ } = c
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u
Tactic:
cases h
Proof state after:
case mpr.refl
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mpr.refl
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Tactic:
simp [_root_.Char.isASCII, _root_.Char.toNat] at hu
Proof state after:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Tactic:
have hlt : u.val.toNat < 256 := by apply Nat.lt_trans hu; decide
Proof state after:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Tactic:
ext
Proof state after:
case mpr.refl.a.a
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ }.val.toNat = u.val.toNat
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
case mpr.refl.a.a
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ }.val.toNat = u.val.toNat
Tactic:
simp [Nat.mod_eq_of_lt hlt]
Proof state after:
no goals
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ u.val.toNat < 256
Tactic:
apply Nat.lt_trans hu
Proof state after:
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ 128 < 256
Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq
Proof state before:
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ 128 < 256
Tactic:
decide
Proof state after:
no goals
Theorem: ASCII.Char.toUnicode_ofUnicode
Proof state before:
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ↑(ofUnicode u hu) = u
Tactic:
rw [toUnicode_eq_iff_ofUnicode_eq]
Proof state after:
no goals
Theorem: ASCII.Char.ofUnicode_toUnicode
Proof state before:
c : ASCII.Char
⊢ ofUnicode ↑c ⋯ = c
Tactic:
rw [← toUnicode_eq_iff_ofUnicode_eq]
Proof state after:
no goals
Theorem: ASCII.Char.ofUnicode?_eq_ofUnicode
Proof state before:
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ofUnicode? u = some (ofUnicode u hu)
Tactic:
simp [ofUnicode?, dif_pos hu]
Proof state after:
no goals
Theorem: ASCII.Char.ofUnicode!_eq_ofUnicode
Proof state before:
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ofUnicode! u = ofUnicode u hu
Tactic:
simp [ofUnicode!, dif_pos hu]
Proof state after:
no goals
Theorem: ASCII.Char.isLower_iff
Proof state before:
c : ASCII.Char
⊢ c.isLower = true ↔ 97 ≤ c.toNat ∧ c.toNat ≤ 122
Tactic:
simp [isLower]
Proof state after:
c : ASCII.Char
⊢ 97 ≤ c.toByte ∧ c.toByte ≤ 122 ↔ 97 ≤ c.toNat ∧ c.toNat ≤ 122
Theorem: ASCII.Char.isLower_iff
Proof state before:
c : ASCII.Char
⊢ 97 ≤ c.toByte ∧ c.toByte ≤ 122 ↔ 97 ≤ c.toNat ∧ c.toNat ≤ 122
Tactic:
rfl
Proof state after:
no goals
Theorem: ASCII.Char.isUpper_iff
Proof state before:
c : ASCII.Char
⊢ c.isUpper = true ↔ 65 ≤ c.toNat ∧ c.toNat ≤ 90
Tactic:
simp [isUpper]
Proof state after:
c : ASCII.Char
⊢ 65 ≤ c.toByte ∧ c.toByte ≤ 90 ↔ 65 ≤ c.toNat ∧ c.toNat ≤ 90
Theorem: ASCII.Char.isUpper_iff
Proof state before:
c : ASCII.Char
⊢ 65 ≤ c.toByte ∧ c.toByte ≤ 90 ↔ 65 ≤ c.toNat ∧ c.toNat ≤ 90
Tactic:
rfl
Proof state after:
no goals
Theorem: ASCII.Char.not_isUpper_of_isLower
Proof state before:
c : ASCII.Char
⊢ c.isLower = true → ¬c.isUpper = true
Tactic:
simp only [isLower_iff, isUpper_iff]
Proof state after:
c : ASCII.Char
⊢ 97 ≤ c.toNat ∧ c.toNat ≤ 122 → ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
Theorem: ASCII.Char.not_isUpper_of_isLower
Proof state before:
c : ASCII.Char
⊢ 97 ≤ c.toNat ∧ c.toNat ≤ 122 → ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
Tactic:
intro ⟨hl, _⟩ ⟨_, hu⟩
Proof state after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ False
Theorem: ASCII.Char.not_isUpper_of_isLower
Proof state before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ False
Tactic:
apply Nat.lt_irrefl c.toNat
Proof state after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ c.toNat < c.toNat
Theorem: ASCII.Char.not_isUpper_of_isLower
Proof state before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ c.toNat < c.toNat
Tactic:
apply Nat.lt_of_le_of_lt hu
Proof state after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < c.toNat
Theorem: ASCII.Char.not_isUpper_of_isLower
Proof state before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < c.toNat
Tactic:
apply Nat.lt_of_lt_of_le _ hl
Proof state after:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < 97
Theorem: ASCII.Char.not_isUpper_of_isLower
Proof state before:
c : ASCII.Char
hl : 97 ≤ c.toNat
right✝ : c.toNat ≤ 122
left✝ : 65 ≤ c.toNat
hu : c.toNat ≤ 90
⊢ 90 < 97
Tactic:
decide
Proof state after:
no goals
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
⊢ ¬c.toLower.isUpper = true
Tactic:
simp [-not_and, toLower, isUpper_iff]
Proof state after:
c : ASCII.Char
⊢ ¬(65 ≤ (if h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 then ofNatAux (c.toNat + 32) ⋯ else c).toNat ∧
      (if h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 then ofNatAux (c.toNat + 32) ⋯ else c).toNat ≤ 90)
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
⊢ ¬(65 ≤ (if h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 then ofNatAux (c.toNat + 32) ⋯ else c).toNat ∧
      (if h : 65 ≤ c.toNat ∧ c.toNat ≤ 90 then ofNatAux (c.toNat + 32) ⋯ else c).toNat ≤ 90)
Tactic:
split
Proof state after:
case isTrue
c : ASCII.Char
h✝ : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(65 ≤ (ofNatAux (c.toNat + 32) ⋯).toNat ∧ (ofNatAux (c.toNat + 32) ⋯).toNat ≤ 90)

case isFalse
c : ASCII.Char
h✝ : ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
⊢ ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
case isTrue
c : ASCII.Char
h✝ : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(65 ≤ (ofNatAux (c.toNat + 32) ⋯).toNat ∧ (ofNatAux (c.toNat + 32) ⋯).toNat ≤ 90)
Tactic:
next h =>
simp [-not_and, toNat_ofNatAux]
intro h'
absurd h'.2
apply Nat.not_le_of_gt
apply Nat.lt_of_lt_of_le _ h.1
decide
Proof state after:
no goals
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(65 ≤ (ofNatAux (c.toNat + 32) ⋯).toNat ∧ (ofNatAux (c.toNat + 32) ⋯).toNat ≤ 90)
Tactic:
simp [-not_and, toNat_ofNatAux]
Proof state after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(33 ≤ c.toNat ∧ c.toNat ≤ 58)
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
⊢ ¬(33 ≤ c.toNat ∧ c.toNat ≤ 58)
Tactic:
intro h'
Proof state after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ False
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ False
Tactic:
absurd h'.2
Proof state after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ ¬c.toNat ≤ 58
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ ¬c.toNat ≤ 58
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ c.toNat > 58
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
case h
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ c.toNat > 58
Tactic:
apply Nat.lt_of_lt_of_le _ h.1
Proof state after:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ 58 < 65
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
c : ASCII.Char
h : 65 ≤ c.toNat ∧ c.toNat ≤ 90
h' : 33 ≤ c.toNat ∧ c.toNat ≤ 58
⊢ 58 < 65
Tactic:
decide
Proof state after:
no goals
Theorem: ASCII.Char.not_isUpper_toLower
Proof state before:
case isFalse
c : ASCII.Char
h✝ : ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
⊢ ¬(65 ≤ c.toNat ∧ c.toNat ≤ 90)
Tactic:
assumption
Proof state after:
no goals
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
c : ASCII.Char
⊢ ¬c.toUpper.isLower = true
Tactic:
simp [-not_and, toUpper, isLower_iff]
Proof state after:
c : ASCII.Char
⊢ ¬(97 ≤ (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ∧
      (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ≤ 122)
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
c : ASCII.Char
⊢ ¬(97 ≤ (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ∧
      (if h : 97 ≤ c.toNat ∧ c.toNat ≤ 122 then ofNatAux (c.toNat - 32) ⋯ else c).toNat ≤ 122)
Tactic:
split
Proof state after:
case isTrue
c : ASCII.Char
h✝ : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ (ofNatAux (c.toNat - 32) ⋯).toNat ∧ (ofNatAux (c.toNat - 32) ⋯).toNat ≤ 122)

case isFalse
c : ASCII.Char
h✝ : ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
⊢ ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
case isTrue
c : ASCII.Char
h✝ : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ (ofNatAux (c.toNat - 32) ⋯).toNat ∧ (ofNatAux (c.toNat - 32) ⋯).toNat ≤ 122)
Tactic:
next h =>
simp [-not_and, toNat_ofNatAux]
intro h'
absurd h'.1
apply Nat.not_le_of_gt
apply Nat.lt_of_le_of_lt (Nat.sub_le_sub_right h.2 32)
decide
Proof state after:
no goals
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ (ofNatAux (c.toNat - 32) ⋯).toNat ∧ (ofNatAux (c.toNat - 32) ⋯).toNat ≤ 122)
Tactic:
simp [-not_and, toNat_ofNatAux]
Proof state after:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122)
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
⊢ ¬(97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122)
Tactic:
intro h'
Proof state after:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ False
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ False
Tactic:
absurd h'.1
Proof state after:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ ¬97 ≤ c.toNat - 32
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ ¬97 ≤ c.toNat - 32
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 97 > c.toNat - 32
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 97 > c.toNat - 32
Tactic:
apply Nat.lt_of_le_of_lt (Nat.sub_le_sub_right h.2 32)
Proof state after:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 122 - 32 < 97
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
case h
c : ASCII.Char
h : 97 ≤ c.toNat ∧ c.toNat ≤ 122
h' : 97 ≤ c.toNat - 32 ∧ c.toNat - 32 ≤ 122
⊢ 122 - 32 < 97
Tactic:
decide
Proof state after:
no goals
Theorem: ASCII.Char.not_isLower_toUpper
Proof state before:
case isFalse
c : ASCII.Char
h✝ : ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
⊢ ¬(97 ≤ c.toNat ∧ c.toNat ≤ 122)
Tactic:
assumption
Proof state after:
no goals
Theorem: ASCII.Char.toUpper_eq_self_of_not_isLower
Proof state before:
c : ASCII.Char
h : ¬c.isLower = true
⊢ c.toUpper = c
Tactic:
simp [toUpper]
Proof state after:
c : ASCII.Char
h : ¬c.isLower = true
⊢ ∀ (h : c.isLower = true), ofNatAux (c.toNat - 32) ⋯ = c
Theorem: ASCII.Char.toUpper_eq_self_of_not_isLower
Proof state before:
c : ASCII.Char
h : ¬c.isLower = true
⊢ ∀ (h : c.isLower = true), ofNatAux (c.toNat - 32) ⋯ = c
Tactic:
intro
Proof state after:
c : ASCII.Char
h : ¬c.isLower = true
h✝ : c.isLower = true
⊢ ofNatAux (c.toNat - 32) ⋯ = c
Theorem: ASCII.Char.toUpper_eq_self_of_not_isLower
Proof state before:
c : ASCII.Char
h : ¬c.isLower = true
h✝ : c.isLower = true
⊢ ofNatAux (c.toNat - 32) ⋯ = c
Tactic:
contradiction
Proof state after:
no goals
Theorem: ASCII.Char.toLower_eq_self_of_not_isUpper
Proof state before:
c : ASCII.Char
h : ¬c.isUpper = true
⊢ c.toLower = c
Tactic:
simp [toLower]
Proof state after:
c : ASCII.Char
h : ¬c.isUpper = true
⊢ ∀ (h : c.isUpper = true), ofNatAux (c.toNat + 32) ⋯ = c
Theorem: ASCII.Char.toLower_eq_self_of_not_isUpper
Proof state before:
c : ASCII.Char
h : ¬c.isUpper = true
⊢ ∀ (h : c.isUpper = true), ofNatAux (c.toNat + 32) ⋯ = c
Tactic:
intro
Proof state after:
c : ASCII.Char
h : ¬c.isUpper = true
h✝ : c.isUpper = true
⊢ ofNatAux (c.toNat + 32) ⋯ = c
Theorem: ASCII.Char.toLower_eq_self_of_not_isUpper
Proof state before:
c : ASCII.Char
h : ¬c.isUpper = true
h✝ : c.isUpper = true
⊢ ofNatAux (c.toNat + 32) ⋯ = c
Tactic:
contradiction
Proof state after:
no goals
Theorem: ASCII.String.length_push
Proof state before:
s : ASCII.String
c : ASCII.Char
⊢ (s.push c).length = s.length + 1
Tactic:
simp [length]
Proof state after:
no goals
Theorem: ASCII.String.length_append
Proof state before:
s t : ASCII.String
⊢ (s ++ t).length = s.length + t.length
Tactic:
simp [length, ByteArray.size_append]
Proof state after:
no goals
Theorem: ASCII.String.length_extract
Proof state before:
s : ASCII.String
start stop : Nat
⊢ (s.extract start stop).length = min stop s.length - start
Tactic:
simp [length, ByteArray.size_extract]
Proof state after:
no goals
Theorem: ASCII.String.append_nil
Proof state before:
s : ASCII.String
⊢ s ++ "".toASCII ⋯ = s
Tactic:
ext
Proof state after:
case a.a
s : ASCII.String
⊢ (s ++ "".toASCII ⋯).toByteArray.data = s.toByteArray.data
Theorem: ASCII.String.append_nil
Proof state before:
case a.a
s : ASCII.String
⊢ (s ++ "".toASCII ⋯).toByteArray.data = s.toByteArray.data
Tactic:
simp
Proof state after:
no goals
Theorem: ASCII.String.nil_append
Proof state before:
t : ASCII.String
⊢ "".toASCII ⋯ ++ t = t
Tactic:
ext
Proof state after:
case a.a
t : ASCII.String
⊢ ("".toASCII ⋯ ++ t).toByteArray.data = t.toByteArray.data
Theorem: ASCII.String.nil_append
Proof state before:
case a.a
t : ASCII.String
⊢ ("".toASCII ⋯ ++ t).toByteArray.data = t.toByteArray.data
Tactic:
simp
Proof state after:
no goals
Theorem: ASCII.String.append_assoc
Proof state before:
s t u : ASCII.String
⊢ s ++ t ++ u = s ++ (t ++ u)
Tactic:
ext
Proof state after:
case a.a
s t u : ASCII.String
⊢ (s ++ t ++ u).toByteArray.data = (s ++ (t ++ u)).toByteArray.data
Theorem: ASCII.String.append_assoc
Proof state before:
case a.a
s t u : ASCII.String
⊢ (s ++ t ++ u).toByteArray.data = (s ++ (t ++ u)).toByteArray.data
Tactic:
simp [Array.append_assoc]
Proof state after:
no goals
Theorem: ASCII.String.append_push
Proof state before:
s t : ASCII.String
c : ASCII.Char
⊢ s ++ t.push c = (s ++ t).push c
Tactic:
ext
Proof state after:
case a.a
s t : ASCII.String
c : ASCII.Char
⊢ (s ++ t.push c).toByteArray.data = ((s ++ t).push c).toByteArray.data
Theorem: ASCII.String.append_push
Proof state before:
case a.a
s t : ASCII.String
c : ASCII.Char
⊢ (s ++ t.push c).toByteArray.data = ((s ++ t).push c).toByteArray.data
Tactic:
simp [Array.push_eq_append_singleton, Array.append_assoc]
Proof state after:
no goals
Theorem: ASCII.String.get_push_lt
Proof state before:
s : ASCII.String
c : ASCII.Char
i : Nat
h : i < s.length
h' : optParam (i < (s.push c).length) ⋯
⊢ (s.push c)[i] = s[i]
Tactic:
ext
Proof state after:
case a.a
s : ASCII.String
c : ASCII.Char
i : Nat
h : i < s.length
h' : optParam (i < (s.push c).length) ⋯
⊢ (s.push c)[i].toByte.toNat = s[i].toByte.toNat
Theorem: ASCII.String.get_push_lt
Proof state before:
case a.a
s : ASCII.String
c : ASCII.Char
i : Nat
h : i < s.length
h' : optParam (i < (s.push c).length) ⋯
⊢ (s.push c)[i].toByte.toNat = s[i].toByte.toNat
Tactic:
simp [ByteArray.get_push_lt, h]
Proof state after:
no goals
Theorem: ASCII.String.get_push_eq
Proof state before:
s : ASCII.String
c : ASCII.Char
⊢ (s.push c)[s.length] = c
Tactic:
ext
Proof state after:
case a.a
s : ASCII.String
c : ASCII.Char
⊢ (s.push c)[s.length].toByte.toNat = c.toByte.toNat
Theorem: ASCII.String.get_push_eq
Proof state before:
case a.a
s : ASCII.String
c : ASCII.Char
⊢ (s.push c)[s.length].toByte.toNat = c.toByte.toNat
Tactic:
simp
Proof state after:
no goals
Theorem: ASCII.String.get_append_left
Proof state before:
s t : ASCII.String
i : Nat
hlt : i < s.length
h : optParam (i < (s ++ t).length) ⋯
⊢ (s ++ t)[i] = s[i]
Tactic:
ext
Proof state after:
case a.a
s t : ASCII.String
i : Nat
hlt : i < s.length
h : optParam (i < (s ++ t).length) ⋯
⊢ (s ++ t)[i].toByte.toNat = s[i].toByte.toNat
Theorem: ASCII.String.get_append_left
Proof state before:
case a.a
s t : ASCII.String
i : Nat
hlt : i < s.length
h : optParam (i < (s ++ t).length) ⋯
⊢ (s ++ t)[i].toByte.toNat = s[i].toByte.toNat
Tactic:
simp [ByteArray.get_append_left hlt]
Proof state after:
no goals
Theorem: ASCII.String.get_append_right
Proof state before:
s t : ASCII.String
i : Nat
hle : s.length ≤ i
h : i < (s ++ t).length
h' : optParam (i - s.length < t.length) ⋯
⊢ (s ++ t)[i] = t[i - s.length]
Tactic:
ext
Proof state after:
case a.a
s t : ASCII.String
i : Nat
hle : s.length ≤ i
h : i < (s ++ t).length
h' : optParam (i - s.length < t.length) ⋯
⊢ (s ++ t)[i].toByte.toNat = t[i - s.length].toByte.toNat
Theorem: ASCII.String.get_append_right
Proof state before:
case a.a
s t : ASCII.String
i : Nat
hle : s.length ≤ i
h : i < (s ++ t).length
h' : optParam (i - s.length < t.length) ⋯
⊢ (s ++ t)[i].toByte.toNat = t[i - s.length].toByte.toNat
Tactic:
simp [length, ByteArray.get_append_right hle]
Proof state after:
no goals
Theorem: ASCII.String.get_extract
Proof state before:
i : Nat
s : ASCII.String
start stop : Nat
h : i < (s.extract start stop).length
h' : optParam (start + i < s.length) ⋯
⊢ (s.extract start stop)[i] = s[start + i]
Tactic:
ext
Proof state after:
case a.a
i : Nat
s : ASCII.String
start stop : Nat
h : i < (s.extract start stop).length
h' : optParam (start + i < s.length) ⋯
⊢ (s.extract start stop)[i].toByte.toNat = s[start + i].toByte.toNat
Theorem: ASCII.String.get_extract
Proof state before:
case a.a
i : Nat
s : ASCII.String
start stop : Nat
h : i < (s.extract start stop).length
h' : optParam (start + i < s.length) ⋯
⊢ (s.extract start stop)[i].toByte.toNat = s[start + i].toByte.toNat
Tactic:
simp
Proof state after:
no goals
Theorem: ASCII.Char.toUnicode_isASCII
Proof state before:
c : ASCII.Char
⊢ Char.isASCII ↑c = true
Tactic:
simp [Char.toUnicode, Char.isASCII, _root_.Char.toNat]
Proof state after:
c : ASCII.Char
⊢ c.toByte.toNat < 128
Theorem: ASCII.Char.toUnicode_isASCII
Proof state before:
c : ASCII.Char
⊢ c.toByte.toNat < 128
Tactic:
exact c.valid
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
rstu : r / s = t / u
⊢ proportion r s t u
Tactic:
refine' ⟨hr, hs, ht, hu, _⟩
Proof state after:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
rstu : r / s = t / u
⊢ ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
rstu : r / s = t / u
⊢ ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Tactic:
intro n m
Proof state after:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
rstu : r / s = t / u
n m : ℕ
⊢ (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
rstu : r / s = t / u
n m : ℕ
⊢ (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Tactic:
field_simp at rstu
Proof state after:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Tactic:
constructor
Proof state after:
case left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ ↑n * r = ↑m * s → ↑n * t = ↑m * u

case right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Theorem: proportion_of_eq_ratio
Proof state before:
case left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ ↑n * r = ↑m * s → ↑n * t = ↑m * u
Tactic:
intro h
Proof state after:
case left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * t = ↑m * u
Theorem: proportion_of_eq_ratio
Proof state before:
case left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * t = ↑m * u
Tactic:
suffices hh : (n : ℝ) * t * s = m * u * s
Proof state after:
case left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑n * t = ↑m * u

case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * t * s = ↑m * u * s
Theorem: proportion_of_eq_ratio
Proof state before:
case left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑n * t = ↑m * u
Tactic:
convert (congr_arg (fun x => x / s) hh) using 1
Proof state after:
case h.e'_2
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑n * t = ↑n * t * s / s

case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑m * u = ↑m * u * s / s