internlm/Lean-Github huggingface dataset:
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False
Tactic:
have h₁ : j ∉ f j := by
  intro h'
  have : j ∉ f j := by rwa [h] at h'
  contradiction
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Tactic:
have h₂ : j ∈ S
Proof state after:
case h₂
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ j ∈ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Theorem: Cantor
Proof state before:
case h₂
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ j ∈ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Tactic:
sorry
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Tactic:
have h₃ : j ∉ S
Proof state after:
case h₃
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ j ∉ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Theorem: Cantor
Proof state before:
case h₃
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ j ∉ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Tactic:
sorry
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Theorem: Cantor
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ j ∉ f j
Tactic:
intro h'
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False
Tactic:
have : j ∉ f j := by rwa [h] at h'
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ j ∉ f j
Tactic:
rwa [h] at h'
Proof state after:
no goals
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
⊢ ∀ (f : α → Set α), ¬Surjective f
Tactic:
intro f surjf
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Tactic:
let S := { i | i ∉ f i }
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False
Tactic:
rcases surjf S with ⟨j, h⟩
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False
Theorem: Cantorαα
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False
Tactic:
have h₁ : j ∉ f j := by
  intro h'
  have : j ∉ f j := by rwa [h] at h'
  contradiction
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Theorem: Cantorαα
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Tactic:
have h₂ : j ∈ S := h₁
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Theorem: Cantorαα
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Tactic:
have h₃ : j ∉ S := by rwa [h] at h₁
Proof state after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Theorem: Cantorαα
Proof state before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ j ∉ f j
Tactic:
intro h'
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False
Tactic:
have : j ∉ f j := by rwa [h] at h'
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ j ∉ f j
Tactic:
rwa [h] at h'
Proof state after:
no goals
Theorem: Cantorαα
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ j ∉ S
Tactic:
rwa [h] at h₁
Proof state after:
no goals
Theorem: C03S05.MyAbs.le_abs_self
Proof state before:
x✝ y x : ℝ
⊢ x ≤ |x|
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S05.MyAbs.neg_le_abs_self
Proof state before:
x✝ y x : ℝ
⊢ -x ≤ |x|
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_add
Proof state before:
x✝ y✝ x y : ℝ
⊢ |x + y| ≤ |x| + |y|
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S05.MyAbs.le_abs_selfαα
Proof state before:
x✝ y x : ℝ
⊢ x ≤ |x|
Tactic:
rcases le_or_gt 0 x with h | h
Proof state after:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ x ≤ |x|

case inr
x✝ y x : ℝ
h : 0 > x
⊢ x ≤ |x|
Theorem: C03S05.MyAbs.le_abs_selfαα
Proof state before:
case inr
x✝ y x : ℝ
h : 0 > x
⊢ x ≤ |x|
Tactic:
. rw [abs_of_neg h]
  linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.le_abs_selfαα
Proof state before:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ x ≤ |x|
Tactic:
rw [abs_of_nonneg h]
Proof state after:
no goals
Theorem: C03S05.MyAbs.le_abs_selfαα
Proof state before:
case inr
x✝ y x : ℝ
h : 0 > x
⊢ x ≤ |x|
Tactic:
rw [abs_of_neg h]
Proof state after:
case inr
x✝ y x : ℝ
h : 0 > x
⊢ x ≤ -x
Theorem: C03S05.MyAbs.le_abs_selfαα
Proof state before:
case inr
x✝ y x : ℝ
h : 0 > x
⊢ x ≤ -x
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.neg_le_abs_selfαα
Proof state before:
x✝ y x : ℝ
⊢ -x ≤ |x|
Tactic:
rcases le_or_gt 0 x with h | h
Proof state after:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ -x ≤ |x|

case inr
x✝ y x : ℝ
h : 0 > x
⊢ -x ≤ |x|
Theorem: C03S05.MyAbs.neg_le_abs_selfαα
Proof state before:
case inr
x✝ y x : ℝ
h : 0 > x
⊢ -x ≤ |x|
Tactic:
. rw [abs_of_neg h]
Proof state after:
no goals
Theorem: C03S05.MyAbs.neg_le_abs_selfαα
Proof state before:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ -x ≤ |x|
Tactic:
rw [abs_of_nonneg h]
Proof state after:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ -x ≤ x
Theorem: C03S05.MyAbs.neg_le_abs_selfαα
Proof state before:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ -x ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.neg_le_abs_selfαα
Proof state before:
case inr
x✝ y x : ℝ
h : 0 > x
⊢ -x ≤ |x|
Tactic:
rw [abs_of_neg h]
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_addαα
Proof state before:
x✝ y✝ x y : ℝ
⊢ |x + y| ≤ |x| + |y|
Tactic:
rcases le_or_gt 0 (x + y) with h | h
Proof state after:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ |x + y| ≤ |x| + |y|

case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ |x + y| ≤ |x| + |y|
Theorem: C03S05.MyAbs.abs_addαα
Proof state before:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ |x + y| ≤ |x| + |y|
Tactic:
. rw [abs_of_neg h]
  linarith [neg_le_abs_self x, neg_le_abs_self y]
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_addαα
Proof state before:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ |x + y| ≤ |x| + |y|
Tactic:
rw [abs_of_nonneg h]
Proof state after:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ x + y ≤ |x| + |y|
Theorem: C03S05.MyAbs.abs_addαα
Proof state before:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ x + y ≤ |x| + |y|
Tactic:
linarith [le_abs_self x, le_abs_self y]
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_addαα
Proof state before:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ |x + y| ≤ |x| + |y|
Tactic:
rw [abs_of_neg h]
Proof state after:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ -(x + y) ≤ |x| + |y|
Theorem: C03S05.MyAbs.abs_addαα
Proof state before:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ -(x + y) ≤ |x| + |y|
Tactic:
linarith [neg_le_abs_self x, neg_le_abs_self y]
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_abs
Proof state before:
x y : ℝ
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_lt
Proof state before:
x y : ℝ
⊢ |x| < y ↔ -y < x ∧ x < y
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
x y : ℝ
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
rcases le_or_gt 0 y with h | h
Proof state after:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < |y| ↔ x < y ∨ x < -y

case inr
x y : ℝ
h : 0 > y
⊢ x < |y| ↔ x < y ∨ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr
x y : ℝ
h : 0 > y
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
rw [abs_of_neg h]
Proof state after:
case inr
x y : ℝ
h : 0 > y
⊢ x < -y ↔ x < y ∨ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr
x y : ℝ
h : 0 > y
⊢ x < -y ↔ x < y ∨ x < -y
Tactic:
constructor
Proof state after:
case inr.mp
x y : ℝ
h : 0 > y
⊢ x < -y → x < y ∨ x < -y

case inr.mpr
x y : ℝ
h : 0 > y
⊢ x < y ∨ x < -y → x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < |y| ↔ x < y ∨ x < -y
Tactic:
rw [abs_of_nonneg h]
Proof state after:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < y ↔ x < y ∨ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl
x y : ℝ
h : 0 ≤ y
⊢ x < y ↔ x < y ∨ x < -y
Tactic:
constructor
Proof state after:
case inl.mp
x y : ℝ
h : 0 ≤ y
⊢ x < y → x < y ∨ x < -y

case inl.mpr
x y : ℝ
h : 0 ≤ y
⊢ x < y ∨ x < -y → x < y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mp
x y : ℝ
h : 0 ≤ y
⊢ x < y → x < y ∨ x < -y
Tactic:
intro h'
Proof state after:
case inl.mp
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y ∨ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mp
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y ∨ x < -y
Tactic:
left
Proof state after:
case inl.mp.h
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mp.h
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y
Tactic:
exact h'
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mpr
x y : ℝ
h : 0 ≤ y
⊢ x < y ∨ x < -y → x < y
Tactic:
intro h'
Proof state after:
case inl.mpr
x y : ℝ
h : 0 ≤ y
h' : x < y ∨ x < -y
⊢ x < y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mpr
x y : ℝ
h : 0 ≤ y
h' : x < y ∨ x < -y
⊢ x < y
Tactic:
rcases h' with h' | h'
Proof state after:
case inl.mpr.inl
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y

case inl.mpr.inr
x y : ℝ
h : 0 ≤ y
h' : x < -y
⊢ x < y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mpr.inr
x y : ℝ
h : 0 ≤ y
h' : x < -y
⊢ x < y
Tactic:
. linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mpr.inl
x y : ℝ
h : 0 ≤ y
h' : x < y
⊢ x < y
Tactic:
exact h'
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inl.mpr.inr
x y : ℝ
h : 0 ≤ y
h' : x < -y
⊢ x < y
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mp
x y : ℝ
h : 0 > y
⊢ x < -y → x < y ∨ x < -y
Tactic:
intro h'
Proof state after:
case inr.mp
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < y ∨ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mp
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < y ∨ x < -y
Tactic:
right
Proof state after:
case inr.mp.h
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mp.h
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Tactic:
exact h'
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mpr
x y : ℝ
h : 0 > y
⊢ x < y ∨ x < -y → x < -y
Tactic:
intro h'
Proof state after:
case inr.mpr
x y : ℝ
h : 0 > y
h' : x < y ∨ x < -y
⊢ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mpr
x y : ℝ
h : 0 > y
h' : x < y ∨ x < -y
⊢ x < -y
Tactic:
rcases h' with h' | h'
Proof state after:
case inr.mpr.inl
x y : ℝ
h : 0 > y
h' : x < y
⊢ x < -y

case inr.mpr.inr
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mpr.inr
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Tactic:
. exact h'
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mpr.inl
x y : ℝ
h : 0 > y
h' : x < y
⊢ x < -y
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.lt_absαα
Proof state before:
case inr.mpr.inr
x y : ℝ
h : 0 > y
h' : x < -y
⊢ x < -y
Tactic:
exact h'
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
x y : ℝ
⊢ |x| < y ↔ -y < x ∧ x < y
Tactic:
rcases le_or_gt 0 x with h | h
Proof state after:
case inl
x y : ℝ
h : 0 ≤ x
⊢ |x| < y ↔ -y < x ∧ x < y

case inr
x y : ℝ
h : 0 > x
⊢ |x| < y ↔ -y < x ∧ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl
x y : ℝ
h : 0 ≤ x
⊢ |x| < y ↔ -y < x ∧ x < y
Tactic:
rw [abs_of_nonneg h]
Proof state after:
case inl
x y : ℝ
h : 0 ≤ x
⊢ x < y ↔ -y < x ∧ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl
x y : ℝ
h : 0 ≤ x
⊢ x < y ↔ -y < x ∧ x < y
Tactic:
constructor
Proof state after:
case inl.mp
x y : ℝ
h : 0 ≤ x
⊢ x < y → -y < x ∧ x < y

case inl.mpr
x y : ℝ
h : 0 ≤ x
⊢ -y < x ∧ x < y → x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mpr
x y : ℝ
h : 0 ≤ x
⊢ -y < x ∧ x < y → x < y
Tactic:
. intro h'
  rcases h' with ⟨h1, h2⟩
  exact h2
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mp
x y : ℝ
h : 0 ≤ x
⊢ x < y → -y < x ∧ x < y
Tactic:
intro h'
Proof state after:
case inl.mp
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ -y < x ∧ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mp
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ -y < x ∧ x < y
Tactic:
constructor
Proof state after:
case inl.mp.left
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ -y < x

case inl.mp.right
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mp.right
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ x < y
Tactic:
exact h'
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mp.left
x y : ℝ
h : 0 ≤ x
h' : x < y
⊢ -y < x
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mpr
x y : ℝ
h : 0 ≤ x
⊢ -y < x ∧ x < y → x < y
Tactic:
intro h'
Proof state after:
case inl.mpr
x y : ℝ
h : 0 ≤ x
h' : -y < x ∧ x < y
⊢ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mpr
x y : ℝ
h : 0 ≤ x
h' : -y < x ∧ x < y
⊢ x < y
Tactic:
rcases h' with ⟨h1, h2⟩
Proof state after:
case inl.mpr.intro
x y : ℝ
h : 0 ≤ x
h1 : -y < x
h2 : x < y
⊢ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inl.mpr.intro
x y : ℝ
h : 0 ≤ x
h1 : -y < x
h2 : x < y
⊢ x < y
Tactic:
exact h2
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr
x y : ℝ
h : 0 > x
⊢ |x| < y ↔ -y < x ∧ x < y
Tactic:
rw [abs_of_neg h]
Proof state after:
case inr
x y : ℝ
h : 0 > x
⊢ -x < y ↔ -y < x ∧ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr
x y : ℝ
h : 0 > x
⊢ -x < y ↔ -y < x ∧ x < y
Tactic:
constructor
Proof state after:
case inr.mp
x y : ℝ
h : 0 > x
⊢ -x < y → -y < x ∧ x < y

case inr.mpr
x y : ℝ
h : 0 > x
⊢ -y < x ∧ x < y → -x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mpr
x y : ℝ
h : 0 > x
⊢ -y < x ∧ x < y → -x < y
Tactic:
. intro h'
  linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mp
x y : ℝ
h : 0 > x
⊢ -x < y → -y < x ∧ x < y
Tactic:
intro h'
Proof state after:
case inr.mp
x y : ℝ
h : 0 > x
h' : -x < y
⊢ -y < x ∧ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mp
x y : ℝ
h : 0 > x
h' : -x < y
⊢ -y < x ∧ x < y
Tactic:
constructor
Proof state after:
case inr.mp.left
x y : ℝ
h : 0 > x
h' : -x < y
⊢ -y < x

case inr.mp.right
x y : ℝ
h : 0 > x
h' : -x < y
⊢ x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mp.right
x y : ℝ
h : 0 > x
h' : -x < y
⊢ x < y
Tactic:
. linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mp.left
x y : ℝ
h : 0 > x
h' : -x < y
⊢ -y < x
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mp.right
x y : ℝ
h : 0 > x
h' : -x < y
⊢ x < y
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mpr
x y : ℝ
h : 0 > x
⊢ -y < x ∧ x < y → -x < y
Tactic:
intro h'
Proof state after:
case inr.mpr
x y : ℝ
h : 0 > x
h' : -y < x ∧ x < y
⊢ -x < y
Theorem: C03S05.MyAbs.abs_ltαα
Proof state before:
case inr.mpr
x y : ℝ
h : 0 > x
h' : -y < x ∧ x < y
⊢ -x < y
Tactic:
linarith
Proof state after:
no goals
Theorem: MyRing.add_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a + 0 = a
Tactic:
rw [add_comm, zero_add]
Proof state after:
no goals
Theorem: MyRing.add_right_neg
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a + -a = 0
Tactic:
rw [add_comm, add_left_neg]
Proof state after:
no goals
Theorem: MyRing.neg_add_cancel_left
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
⊢ -a + (a + b) = b
Tactic:
rw [← add_assoc, add_left_neg, zero_add]
Proof state after:
no goals
Theorem: MyRing.add_neg_cancel_right
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
⊢ a + b + -b = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.add_neg_cancel_rightαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
⊢ a + b + -b = a
Tactic:
rw [add_assoc, add_right_neg, add_zero]
Proof state after:
no goals
Theorem: MyRing.add_left_cancel
Proof state before:
R : Type u_1
inst✝ : Ring R
a b c : R
h : a + b = a + c
⊢ b = c
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.add_right_cancel
Proof state before:
R : Type u_1
inst✝ : Ring R
a b c : R
h : a + b = c + b
⊢ a = c
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.add_left_cancelαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a b c : R
h : a + b = a + c
⊢ b = c
Tactic:
rw [← neg_add_cancel_left a b, h, neg_add_cancel_left]
Proof state after:
no goals
Theorem: MyRing.add_right_cancelαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a b c : R
h : a + b = c + b
⊢ a = c
Tactic:
rw [← add_neg_cancel_right a b, h, add_neg_cancel_right]
Proof state after:
no goals
Theorem: MyRing.mul_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a * 0 = 0
Tactic:
have h : a * 0 + a * 0 = a * 0 + 0 := by
  rw [← mul_add, add_zero, add_zero]
Proof state after:
R : Type u_1
inst✝ : Ring R
a : R
h : a * 0 + a * 0 = a * 0 + 0
⊢ a * 0 = 0
Theorem: MyRing.mul_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
h : a * 0 + a * 0 = a * 0 + 0
⊢ a * 0 = 0
Tactic:
rw [add_left_cancel h]
Proof state after:
no goals
Theorem: MyRing.mul_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a * 0 + a * 0 = a * 0 + 0
Tactic:
rw [← mul_add, add_zero, add_zero]
Proof state after:
no goals
Theorem: MyRing.zero_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 0 * a = 0
Tactic:
sorry
Proof state after:
no goals