internlm/Lean-Github huggingface dataset:
Theorem: ValidModel.small_char_div_12
Proof state before:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp 2
Tactic:
rw [←p2]
Proof state after:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp p
Theorem: ValidModel.small_char_div_12
Proof state before:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp p
Tactic:
exact le_of_eq (valp.v_uniformizer).symm
Proof state after:
no goals
Theorem: ValidModel.small_char_div_12
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 12 = 2 * 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: ValidModel.small_char_div_12
Proof state before:
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp 12 ≥ 1
Tactic:
rw [(show (12 : R) = 3 * 4 by norm_num)]
Proof state after:
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp (3 * 4) ≥ 1
Theorem: ValidModel.small_char_div_12
Proof state before:
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp (3 * 4) ≥ 1
Tactic:
apply val_mul_ge_of_left_ge
Proof state after:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp 3
Theorem: ValidModel.small_char_div_12
Proof state before:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp 3
Tactic:
rw [←p3]
Proof state after:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp p
Theorem: ValidModel.small_char_div_12
Proof state before:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp p
Tactic:
exact le_of_eq (valp.v_uniformizer).symm
Proof state after:
no goals
Theorem: ValidModel.small_char_div_12
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 12 = 3 * 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: ValidModel.v_rst_b2_of_small_char
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 (rst_iso r s t e).toModel) ≥ 1
Tactic:
simp only [rst_iso]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 (Model.rst_iso r s t e.toModel)) ≥ 1
Theorem: ValidModel.v_rst_b2_of_small_char
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 (Model.rst_iso r s t e.toModel)) ≥ 1
Tactic:
rw [Model.rst_b2]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 e.toModel + 12 * r) ≥ 1
Theorem: ValidModel.v_rst_b2_of_small_char
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 e.toModel + 12 * r) ≥ 1
Tactic:
apply val_add_ge_of_ge valp h_b2
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ 1 ≤ v valp (12 * r)
Theorem: ValidModel.v_rst_b2_of_small_char
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ 1 ≤ v valp (12 * r)
Tactic:
exact val_mul_ge_of_left_ge valp h_p
Proof state after:
no goals
Theorem: ENat.mul_infty
Proof state before:
case top
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ⊤ * ⊤ = if ⊤ = 0 then 0 else ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.mul_infty
Proof state before:
case nat
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n : ℕ
⊢ ↑n * ⊤ = if ↑n = 0 then 0 else ⊤
Tactic:
cases n
Proof state after:
case nat.zero
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ↑Nat.zero * ⊤ = if ↑Nat.zero = 0 then 0 else ⊤

case nat.succ
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n✝ : ℕ
⊢ ↑(Nat.succ n✝) * ⊤ = if ↑(Nat.succ n✝) = 0 then 0 else ⊤
Theorem: ENat.mul_infty
Proof state before:
case nat.zero
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ↑Nat.zero * ⊤ = if ↑Nat.zero = 0 then 0 else ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.mul_infty
Proof state before:
case nat.succ
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n✝ : ℕ
⊢ ↑(Nat.succ n✝) * ⊤ = if ↑(Nat.succ n✝) = 0 then 0 else ⊤
Tactic:
simp [add_mul]
Proof state after:
no goals
Theorem: ENat.infty_mul
Proof state before:
case top
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ⊤ * ⊤ = if ⊤ = 0 then 0 else ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.infty_mul
Proof state before:
case nat
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n : ℕ
⊢ ⊤ * ↑n = if ↑n = 0 then 0 else ⊤
Tactic:
cases n
Proof state after:
case nat.zero
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ⊤ * ↑Nat.zero = if ↑Nat.zero = 0 then 0 else ⊤

case nat.succ
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n✝ : ℕ
⊢ ⊤ * ↑(Nat.succ n✝) = if ↑(Nat.succ n✝) = 0 then 0 else ⊤
Theorem: ENat.infty_mul
Proof state before:
case nat.zero
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ⊤ * ↑Nat.zero = if ↑Nat.zero = 0 then 0 else ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ENat.infty_mul
Proof state before:
case nat.succ
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n✝ : ℕ
⊢ ⊤ * ↑(Nat.succ n✝) = if ↑(Nat.succ n✝) = 0 then 0 else ⊤
Tactic:
simp [mul_add]
Proof state after:
no goals
Theorem: usize_size_eq
Proof state before:
⊢ Eq (hPow 2 32) 4294967296
Tactic:
decide
Proof state after:
no goals
Theorem: usize_size_eq
Proof state before:
⊢ Eq (hPow 2 64) 18446744073709551616
Tactic:
decide
Proof state after:
no goals
Theorem: isValidChar_UInt32
Proof state before:
n : Nat
h✝ : Nat.isValidChar n
h : LT.lt n 55296
⊢ LT.lt 55296 UInt32.size
Tactic:
decide
Proof state after:
no goals
Theorem: isValidChar_UInt32
Proof state before:
n : Nat
h✝ : Nat.isValidChar n
left✝ : LT.lt 57343 n
h : LT.lt n 1114112
⊢ LT.lt 1114112 UInt32.size
Tactic:
decide
Proof state after:
no goals
Theorem: add_comm
Proof state before:
n m : Nat
⊢ n + (m + 1) = m + 1 + n
Tactic:
have : Nat.succ (n + m) = Nat.succ (m + n) :=
  by apply congrArg; apply Nat.add_comm
Proof state after:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = m + 1 + n
Theorem: add_comm
Proof state before:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = m + 1 + n
Tactic:
rw [Nat.succ_add m n]
Proof state after:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = Nat.succ (m + n)
Theorem: add_comm
Proof state before:
n m : Nat
this : Nat.succ (n + m) = Nat.succ (m + n)
⊢ n + (m + 1) = Nat.succ (m + n)
Tactic:
apply this
Proof state after:
no goals
Theorem: add_comm
Proof state before:
n m : Nat
⊢ Nat.succ (n + m) = Nat.succ (m + n)
Tactic:
apply congrArg
Proof state after:
case h
n m : Nat
⊢ n + m = m + n
Theorem: add_comm
Proof state before:
case h
n m : Nat
⊢ n + m = m + n
Tactic:
apply Nat.add_comm
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f : Form
h₁ : s ≤ t
g : Form
h₂ : s⊨~g
⊢ t⊨~g
Tactic:
intros p h₃ h₄
Proof state after:
α : Type
inst : Model α
s t : α
f : Form
h₁ : s ≤ t
g : Form
h₂ : s⊨~g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑(p*)⊨g
⊢ False
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f : Form
h₁ : s ≤ t
g : Form
h₂ : s⊨~g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑(p*)⊨g
⊢ False
Tactic:
exact h₂ (le_trans h₁ h₃) h₄
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f&g
Tactic:
apply And.intro
Proof state after:
case left
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f

case right
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f
Tactic:
case left => exact upwardsClosure h₁ h₂.left
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g
Tactic:
case right => exact upwardsClosure h₁ h₂.right
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f
Tactic:
exact upwardsClosure h₁ h₂.left
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g
Tactic:
exact upwardsClosure h₁ h₂.right
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
⊢ t⊨f¦g
Tactic:
intros p h₃
Proof state after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
apply Or.elim (h₂ (le_trans' h₃ h₁))
Proof state after:
case left
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f → ↑p⊨f ∨ ↑p⊨g

case right
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨g → ↑p⊨f ∨ ↑p⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f → ↑p⊨f ∨ ↑p⊨g
Tactic:
case left => intro h₄; exact Or.inl h₄
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨g → ↑p⊨f ∨ ↑p⊨g
Tactic:
case right => intro h₄; exact Or.inr h₄
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f → ↑p⊨f ∨ ↑p⊨g
Tactic:
intro h₄
Proof state after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inl h₄
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨g → ↑p⊨f ∨ ↑p⊨g
Tactic:
intro h₄
Proof state after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inr h₄
Proof state after:
no goals
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
⊢ t⊨f⊃g
Tactic:
intros u h₃
Proof state after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
⊢ t∙u⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
⊢ t∙u⊨g
Tactic:
have l₁ : s ∙ u ≤ t ∙ u := inst.appMonotoneRight u h₁
Proof state after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
⊢ t∙u⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
⊢ t∙u⊨g
Tactic:
have l₂ : (s ∙ u) ⊨ g := h₂ h₃
Proof state after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
l₂ : s∙u⊨g
⊢ t∙u⊨g
Theorem: upwardsClosure
Proof state before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
l₂ : s∙u⊨g
⊢ t∙u⊨g
Tactic:
exact upwardsClosure l₁ l₂
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
⊢ t⊨~f
Tactic:
intros p h₂ h₃
Proof state after:
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Tactic:
exact h₁ p h₂ (le_refl p.val) h₃
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f&g
Tactic:
apply And.intro
Proof state after:
case left
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f

case right
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨g
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f
Tactic:
case left => 
  have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ f := by
    intros p h₂
    exact (h₁ p h₂).left
  exact primeDetermination l₁
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨g
Tactic:
case right =>
  have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ g := by
    intros p h₂
    exact (h₁ p h₂).right
  exact primeDetermination l₁
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f
Tactic:
have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ f := by
  intros p h₂
  exact (h₁ p h₂).left
Proof state after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f
⊢ t⊨f
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f
⊢ t⊨f
Tactic:
exact primeDetermination l₁
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ ∀ (p : Model.primes), t ≤ ↑p → p⊨f
Tactic:
intros p h₂
Proof state after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨f
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨f
Tactic:
exact (h₁ p h₂).left
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨g
Tactic:
have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ g := by
  intros p h₂
  exact (h₁ p h₂).right
Proof state after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨g
⊢ t⊨g
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨g
⊢ t⊨g
Tactic:
exact primeDetermination l₁
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ ∀ (p : Model.primes), t ≤ ↑p → p⊨g
Tactic:
intros p h₂
Proof state after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨g
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨g
Tactic:
exact (h₁ p h₂).right
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
⊢ t⊨f¦g
Tactic:
intros p h₂
Proof state after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
cases h₁ p h₂ (le_refl p.val)
Proof state after:
case inl
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g

case inr
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inl => apply Or.inl; assumption
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inr => apply Or.inr; assumption
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
apply Or.inl
Proof state after:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f
Theorem: primeDetermination
Proof state before:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f
Tactic:
assumption
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
apply Or.inr
Proof state after:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨g
Theorem: primeDetermination
Proof state before:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨g
Tactic:
assumption
Proof state after:
no goals
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
⊢ t⊨f⊃g
Tactic:
intros u h₂
Proof state after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ t∙u⊨g
Theorem: primeDetermination
Proof state before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ t∙u⊨g
Tactic:
apply primeDetermination
Proof state after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ ∀ (p : Model.primes), t∙u ≤ ↑p → p⊨g
Theorem: primeDetermination
Proof state before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ ∀ (p : Model.primes), t∙u ≤ ↑p → p⊨g
Tactic:
intros p h₃
Proof state after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
⊢ p⊨g
Theorem: primeDetermination
Proof state before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
⊢ p⊨g
Tactic:
have ⟨q, _, l₃,_,l₄,_⟩ : ∃q r : inst.primes, t ≤ q ∧ u ≤ r ∧ (↑q ∙ u) ≤ p ∧ (t ∙ r) ≤ p.val := inst.appBounding t u p h₃
Proof state after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
⊢ p⊨g
Theorem: primeDetermination
Proof state before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
⊢ p⊨g
Tactic:
have l₅ : (↑q ∙ u) ⊨ g  := h₁ q l₃ h₂
Proof state after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
l₅ : ↑q∙u⊨g
⊢ p⊨g
Theorem: primeDetermination
Proof state before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
l₅ : ↑q∙u⊨g
⊢ p⊨g
Tactic:
exact upwardsClosure l₄ l₅
Proof state after:
no goals
Theorem: starCompatRight
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
⊢ p*⊨f → ¬p⊨~f
Tactic:
intro h₁ h₂
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : p⊨~f
⊢ False
Theorem: starCompatRight
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : p⊨~f
⊢ False
Tactic:
unfold psatisfies at h₂
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ↑p⊨~f
⊢ False
Theorem: starCompatRight
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ↑p⊨~f
⊢ False
Tactic:
unfold satisfies at h₂
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ∀ {p_1 : Model.primes}, ↑p ≤ ↑p_1 → ¬↑(p_1*)⊨f
⊢ False
Theorem: starCompatRight
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ∀ {p_1 : Model.primes}, ↑p ≤ ↑p_1 → ¬↑(p_1*)⊨f
⊢ False
Tactic:
exact h₂ (le_refl p.val) h₁
Proof state after:
no goals
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g ↔ ∀ (x : α), x⊨f → x⊨g
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g

case mpr
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g
Tactic:
case mp => 
  intros h₁ x h₂
  rw [←inst.appLeftIdent x]
  exact h₁ h₂
Proof state after:
no goals
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g
Tactic:
case mpr =>
  intro h₁ u h₂
  rw [inst.appLeftIdent u]
  exact h₁ u h₂
Proof state after:
no goals
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g
Tactic:
intros h₁ x h₂
Proof state after:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ x⊨g