internlm/Lean-Github huggingface dataset:
Theorem: QPF.M.bisim
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }
Tactic:
rw [Container.Obj.snd_equals_iff]
Proof state after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ (fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst) = fun x =>
    Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd
Theorem: QPF.M.bisim
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ (fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst) = fun x =>
    Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd
Tactic:
funext a
Proof state after:
case mk.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).fst = Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).snd
Theorem: QPF.M.bisim
Proof state before:
case mk.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).fst = Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).snd
Tactic:
apply Quot.sound
Proof state after:
case mk.h.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ (↑(kz a)).fst = (↑(kz a)).snd ∨ r (↑(kz a)).fst (↑(kz a)).snd
Theorem: QPF.M.bisim
Proof state before:
case mk.h.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ (↑(kz a)).fst = (↑(kz a)).snd ∨ r (↑(kz a)).fst (↑(kz a)).snd
Tactic:
right
Proof state after:
case mk.h.a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ r (↑(kz a)).fst (↑(kz a)).snd
Theorem: QPF.M.bisim
Proof state before:
case mk.h.a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ r (↑(kz a)).fst (↑(kz a)).snd
Tactic:
apply (kz a).2
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof state before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y
Tactic:
right
Proof state after:
case a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ r x y
Theorem: QPF.M.bisim
Proof state before:
case a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ r x y
Tactic:
assumption
Proof state after:
no goals
Theorem: eq_I_Nat
Proof state before:
m n : Nat
⊢ m = n ↔ I m = I n
Tactic:
apply Iff.intro
Proof state after:
case mp
m n : Nat
⊢ m = n → I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n
Theorem: eq_I_Nat
Proof state before:
case mp
m n : Nat
⊢ m = n → I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n
Tactic:
intro h
Proof state after:
case mp
m n : Nat
h : m = n
⊢ I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n
Theorem: eq_I_Nat
Proof state before:
case mp
m n : Nat
h : m = n
⊢ I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n
Tactic:
exact congrArg I h
Proof state after:
case mpr
m n : Nat
⊢ I m = I n → m = n
Theorem: eq_I_Nat
Proof state before:
case mpr
m n : Nat
⊢ I m = I n → m = n
Tactic:
intro h
Proof state after:
case mpr
m n : Nat
h : I m = I n
⊢ m = n
Theorem: eq_I_Nat
Proof state before:
case mpr
m n : Nat
h : I m = I n
⊢ m = n
Tactic:
cases h
Proof state after:
case mpr.refl
m : Nat
⊢ m = m
Theorem: eq_I_Nat
Proof state before:
case mpr.refl
m : Nat
⊢ m = m
Tactic:
rfl
Proof state after:
no goals
Theorem: eq_Is_Nat
Proof state before:
m n : Nat
⊢ m = n ↔ Is m = Is n
Tactic:
apply Iff.intro
Proof state after:
case mp
m n : Nat
⊢ m = n → Is m = Is n

case mpr
m n : Nat
⊢ Is m = Is n → m = n
Theorem: eq_Is_Nat
Proof state before:
case mp
m n : Nat
⊢ m = n → Is m = Is n

case mpr
m n : Nat
⊢ Is m = Is n → m = n
Tactic:
intro h
Proof state after:
case mp
m n : Nat
h : m = n
⊢ Is m = Is n

case mpr
m n : Nat
⊢ Is m = Is n → m = n
Theorem: eq_Is_Nat
Proof state before:
case mp
m n : Nat
h : m = n
⊢ Is m = Is n

case mpr
m n : Nat
⊢ Is m = Is n → m = n
Tactic:
exact congrArg Is h
Proof state after:
case mpr
m n : Nat
⊢ Is m = Is n → m = n
Theorem: eq_Is_Nat
Proof state before:
case mpr
m n : Nat
⊢ Is m = Is n → m = n
Tactic:
intro h
Proof state after:
case mpr
m n : Nat
h : Is m = Is n
⊢ m = n
Theorem: eq_Is_Nat
Proof state before:
case mpr
m n : Nat
h : Is m = Is n
⊢ m = n
Tactic:
cases h
Proof state after:
case mpr.refl
m : Nat
⊢ m = m
Theorem: eq_Is_Nat
Proof state before:
case mpr.refl
m : Nat
⊢ m = m
Tactic:
rfl
Proof state after:
no goals
Theorem: mod_mod
Proof state before:
K : Type u_1
a b : K
inst✝ : EuclideanDomain K
⊢ a % b % b = a % b
Tactic:
sorry
Proof state after:
no goals
Theorem: SurjVal.p_non_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬p = 0
Tactic:
rw [←nav.v_eq_top_iff_zero, nav.v_uniformizer]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬1 = ⊤
Theorem: SurjVal.p_non_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬1 = ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: SurjVal.val_mul_ge_right
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (a * b)
Tactic:
rw [mul_comm]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (b * a)
Theorem: SurjVal.val_mul_ge_right
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (b * a)
Tactic:
exact val_mul_ge_left nav b a
Proof state after:
no goals
Theorem: SurjVal.val_mul_ge_of_both_ge
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : m ≤ v nav a
hb : n ≤ v nav b
⊢ m + n ≤ v nav (a * b)
Tactic:
rw [nav.v_mul_eq_add_v]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : m ≤ v nav a
hb : n ≤ v nav b
⊢ m + n ≤ v nav a + v nav b
Theorem: SurjVal.val_mul_ge_of_both_ge
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : m ≤ v nav a
hb : n ≤ v nav b
⊢ m + n ≤ v nav a + v nav b
Tactic:
exact add_le_add ha hb
Proof state after:
no goals
Theorem: SurjVal.val_of_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ (fun x => x + v nav p) (v nav 1) = (fun x => x + v nav p) 0
Tactic:
dsimp
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 + v nav p = 0 + v nav p
Theorem: SurjVal.val_of_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 + v nav p = 0 + v nav p
Tactic:
rw [← v_mul_eq_add_v]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (1 * p) = 0 + v nav p
Theorem: SurjVal.val_of_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (1 * p) = 0 + v nav p
Tactic:
simp
Proof state after:
no goals
Theorem: SurjVal.val_of_one
Proof state before:
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ Function.Injective fun x => x + v nav p
Tactic:
intro x y h
Proof state after:
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x y : ℕ∞
h : (fun x => x + v nav p) x = (fun x => x + v nav p) y
⊢ x = y
Theorem: SurjVal.val_of_one
Proof state before:
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x y : ℕ∞
h : (fun x => x + v nav p) x = (fun x => x + v nav p) y
⊢ x = y
Tactic:
induction x using ENat.recTopCoe <;>
induction y using ENat.recTopCoe <;>
simp at * <;>
sorry
Proof state after:
no goals
Theorem: SurjVal.val_pow_ge_of_ge
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
k : ℕ
ha : m ≤ v nav a
⊢ k • m ≤ v nav (a ^ k)
Tactic:
induction k with
| zero => simp [zero_nsmul]
| succ k ih =>
  simp only [succ_nsmul, pow_succ]
  apply val_mul_ge_of_both_ge _ ha ih
Proof state after:
no goals
Theorem: SurjVal.val_pow_ge_of_ge
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
⊢ Nat.zero • m ≤ v nav (a ^ Nat.zero)
Tactic:
simp [zero_nsmul]
Proof state after:
no goals
Theorem: SurjVal.val_pow_ge_of_ge
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ Nat.succ k • m ≤ v nav (a ^ Nat.succ k)
Tactic:
simp only [succ_nsmul, pow_succ]
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ m + k • m ≤ v nav (a * a ^ k)
Theorem: SurjVal.val_pow_ge_of_ge
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ m + k • m ≤ v nav (a * a ^ k)
Tactic:
apply val_mul_ge_of_both_ge _ ha ih
Proof state after:
no goals
Theorem: SurjVal.val_pow_eq_of_eq
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
k : ℕ
ha : v nav a = m
⊢ v nav (a ^ k) = ↑k * m
Tactic:
induction k with
| zero => simp
| succ k ih =>
  simp only [pow_succ, Nat.cast_succ, add_mul, one_mul, add_comm]
  rw [nav.v_mul_eq_add_v, ha, ih]
Proof state after:
no goals
Theorem: SurjVal.val_pow_eq_of_eq
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
⊢ v nav (a ^ Nat.zero) = ↑Nat.zero * m
Tactic:
simp
Proof state after:
no goals
Theorem: SurjVal.val_pow_eq_of_eq
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a ^ Nat.succ k) = ↑(Nat.succ k) * m
Tactic:
simp only [pow_succ, Nat.cast_succ, add_mul, one_mul, add_comm]
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a * a ^ k) = m + ↑k * m
Theorem: SurjVal.val_pow_eq_of_eq
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a * a ^ k) = m + ↑k * m
Tactic:
rw [nav.v_mul_eq_add_v, ha, ih]
Proof state after:
no goals
Theorem: SurjVal.val_of_minus_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (-1) = 0
Tactic:
by_contra
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ False
Theorem: SurjVal.val_of_minus_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ False
Tactic:
have contradiction : nav 1 > 0 := by
  rw [←neg_neg 1, ←one_mul 1, neg_mul_eq_neg_mul, neg_mul_eq_mul_neg, nav.v_mul_eq_add_v]
  simpa [pos_iff_ne_zero]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : v nav 1 > 0
⊢ False
Theorem: SurjVal.val_of_minus_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : v nav 1 > 0
⊢ False
Tactic:
rw [val_of_one] at contradiction
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : 0 > 0
⊢ False
Theorem: SurjVal.val_of_minus_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : 0 > 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: SurjVal.val_of_minus_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav 1 > 0
Tactic:
rw [←neg_neg 1, ←one_mul 1, neg_mul_eq_neg_mul, neg_mul_eq_mul_neg, nav.v_mul_eq_add_v]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav (-1) + v nav (-1) > 0
Theorem: SurjVal.val_of_minus_one
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav (-1) + v nav (-1) > 0
Tactic:
simpa [pos_iff_ne_zero]
Proof state after:
no goals
Theorem: SurjVal.val_neg
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x p : R
nav : SurjVal p
⊢ v nav (-x) = v nav x
Tactic:
rw [←one_mul x, neg_mul_eq_neg_mul, nav.v_mul_eq_add_v, val_of_minus_one, one_mul, zero_add]
Proof state after:
no goals
Theorem: SurjVal.v_sub_ge_min_v
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a - b)
Tactic:
rw [sub_eq_add_neg]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a + -b)
Theorem: SurjVal.v_sub_ge_min_v
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a + -b)
Tactic:
convert nav.v_add_ge_min_v a (-b) using 2
Proof state after:
case h.e'_3.h.e'_4
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b = v nav (-b)
Theorem: SurjVal.v_sub_ge_min_v
Proof state before:
case h.e'_3.h.e'_4
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b = v nav (-b)
Tactic:
simp
Proof state after:
no goals
Theorem: SurjVal.val_sub_ge_of_ge
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (a - b)
Tactic:
rw [sub_eq_add_neg]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (a + -b)
Theorem: SurjVal.val_sub_ge_of_ge
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (a + -b)
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav a

case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)
Theorem: SurjVal.val_sub_ge_of_ge
Proof state before:
case ha
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav a

case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)
Tactic:
assumption
Proof state after:
case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)
Theorem: SurjVal.val_sub_ge_of_ge
Proof state before:
case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)
Tactic:
simpa
Proof state after:
no goals
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) = v nav a
Tactic:
apply le_antisymm
Proof state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Tactic:
. apply le_of_not_lt
  intro h'
  have hm : nav a < nav (-b) := by rwa [val_neg]
  apply lt_irrefl (nav a)
  apply lt_of_lt_of_le (lt_min h' hm)
  convert nav.v_add_ge_min_v (a + b) (-b)
  simp
Proof state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Tactic:
. exact le_trans (le_min (le_of_eq rfl) (le_of_lt h)) (SurjVal.v_add_ge_min_v nav a b)
Proof state after:
no goals
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a
Tactic:
apply le_of_not_lt
Proof state after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ ¬v nav a < v nav (a + b)
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ ¬v nav a < v nav (a + b)
Tactic:
intro h'
Proof state after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
⊢ False
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
⊢ False
Tactic:
have hm : nav a < nav (-b) := by rwa [val_neg]
Proof state after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ False
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ False
Tactic:
apply lt_irrefl (nav a)
Proof state after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ v nav a < v nav a
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ v nav a < v nav a
Tactic:
apply lt_of_lt_of_le (lt_min h' hm)
Proof state after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ min (v nav (a + b)) (v nav (-b)) ≤ v nav a
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ min (v nav (a + b)) (v nav (-b)) ≤ v nav a
Tactic:
convert nav.v_add_ge_min_v (a + b) (-b)
Proof state after:
case h.e'_4.h.e'_6
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ a = a + b + -b
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case h.e'_4.h.e'_6
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ a = a + b + -b
Tactic:
simp
Proof state after:
no goals
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
⊢ v nav a < v nav (-b)
Tactic:
rwa [val_neg]
Proof state after:
no goals
Theorem: SurjVal.v_add_eq_min_v
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Tactic:
exact le_trans (le_min (le_of_eq rfl) (le_of_lt h)) (SurjVal.v_add_ge_min_v nav a b)
Proof state after:
no goals
Theorem: SurjVal.val_of_pow_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
⊢ v nav (p ^ n) = ↑n
Tactic:
induction n with
| zero      =>
  rw [pow_zero]
  exact val_of_one nav
| succ n ih =>
  rw [pow_succ, SurjVal.v_mul_eq_add_v nav, ih, SurjVal.v_uniformizer nav]
  simp [Nat.succ_eq_add_one, add_comm]
Proof state after:
no goals
Theorem: SurjVal.val_of_pow_uniformizer
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (p ^ Nat.zero) = ↑Nat.zero
Tactic:
rw [pow_zero]
Proof state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 = ↑Nat.zero
Theorem: SurjVal.val_of_pow_uniformizer
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 = ↑Nat.zero
Tactic:
exact val_of_one nav
Proof state after:
no goals
Theorem: SurjVal.val_of_pow_uniformizer
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ v nav (p ^ Nat.succ n) = ↑(Nat.succ n)
Tactic:
rw [pow_succ, SurjVal.v_mul_eq_add_v nav, ih, SurjVal.v_uniformizer nav]
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ 1 + ↑n = ↑(Nat.succ n)
Theorem: SurjVal.val_of_pow_uniformizer
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ 1 + ↑n = ↑(Nat.succ n)
Tactic:
simp [Nat.succ_eq_add_one, add_comm]
Proof state after:
no goals