internlm/Lean-Github huggingface dataset:
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ |s N - b| < ε
Tactic:
apply hNb
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb
Theorem: C03S06.convergesTo_unique
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb
Tactic:
apply le_max_right
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| = |-(s N - a) + (s N - b)|
Tactic:
congr
Proof state after:
case e_a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ a - b = -(s N - a) + (s N - b)
Theorem: C03S06.convergesTo_unique
Proof state before:
case e_a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ a - b = -(s N - a) + (s N - b)
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |(-(s N - a))| + |s N - b| = |s N - a| + |s N - b|
Tactic:
rw [abs_neg]
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ ε + ε = |a - b|
Tactic:
norm_num
Proof state after:
no goals
Theorem: C03S01.my_lemma4
Proof state before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
Tactic:
calc
  |x * y| = |x| * |y| := sorry
  _ ≤ |x| * ε := sorry
  _ < 1 * ε := sorry
  _ = ε := sorry
Proof state after:
no goals
Theorem: C03S04.aux
Proof state before:
x y : ℝ
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 = 0
Tactic:
linarith [pow_two_nonneg x, pow_two_nonneg y]
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:
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_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:
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.zero_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 0 * a = 0
Tactic:
have h : 0 * a + 0 * a = 0 * a + 0 := by rw [← add_mul, add_zero, add_zero]
Proof state after:
R : Type u_1
inst✝ : Ring R
a : R
h : 0 * a + 0 * a = 0 * a + 0
⊢ 0 * a = 0
Theorem: MyRing.zero_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
h : 0 * a + 0 * a = 0 * a + 0
⊢ 0 * a = 0
Tactic:
rw [add_left_cancel h]
Proof state after:
no goals
Theorem: MyRing.zero_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 0 * a + 0 * a = 0 * a + 0
Tactic:
rw [← add_mul, add_zero, add_zero]
Proof state after:
no goals
Theorem: MyRing.neg_eq_of_add_eq_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -a = b
Tactic:
rw [← neg_add_cancel_left a b, h, add_zero]
Proof state after:
no goals
Theorem: MyRing.eq_neg_of_add_eq_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ a = -b
Tactic:
symm
Proof state after:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -b = a
Theorem: MyRing.eq_neg_of_add_eq_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -b = a
Tactic:
apply neg_eq_of_add_eq_zero
Proof state after:
case h
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ b + a = 0
Theorem: MyRing.eq_neg_of_add_eq_zero
Proof state before:
case h
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ b + a = 0
Tactic:
rw [add_comm, h]
Proof state after:
no goals
Theorem: MyRing.neg_neg
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ - -a = a
Tactic:
apply neg_eq_of_add_eq_zero
Proof state after:
case h
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a + a = 0
Theorem: MyRing.neg_neg
Proof state before:
case h
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a + a = 0
Tactic:
rw [add_left_neg]
Proof state after:
no goals
Theorem: MyRing.self_sub
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a - a = 0
Tactic:
rw [sub_eq_add_neg, add_right_neg]
Proof state after:
no goals
Theorem: MyRing.two_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 2 * a = a + a
Tactic:
rw [← one_add_one_eq_two, add_mul, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_right_inv
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Tactic:
have h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1 := by
  rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
Proof state after:
G : Type u_1
inst✝ : Group G
a : G
h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
⊢ a * a⁻¹ = 1
Theorem: MyGroup.mul_right_inv
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
⊢ a * a⁻¹ = 1
Tactic:
rw [← h, ← mul_assoc, mul_left_inv, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_right_inv
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
Tactic:
rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
Proof state after:
no goals
Theorem: MyGroup.mul_one
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * 1 = a
Tactic:
rw [← mul_left_inv a, ← mul_assoc, mul_right_inv, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_inv_rev
Proof state before:
G : Type u_1
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
rw [← one_mul (b⁻¹ * a⁻¹), ← mul_left_inv (a * b), mul_assoc, mul_assoc, ← mul_assoc b b⁻¹,
  mul_right_inv, one_mul, mul_right_inv, mul_one]
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₁ = x₂
Tactic:
have x₂A : x₂ ∈ A := by
  apply not_imp_self.mp
  intro (x₂nA : x₂ ∉ A)
  rw [if_pos x₁A, if_neg x₂nA] at hxeq
  rw [A_def, sbSet, mem_iUnion] at x₁A
  have x₂eq : x₂ = g (f x₁) := by
    rw [hxeq, sb_right_inv f g x₂nA]
  rcases x₁A with ⟨n, hn⟩
  rw [A_def, sbSet, mem_iUnion]
  use n + 1
  simp [sbAux]
  exact ⟨x₁, hn, x₂eq.symm⟩
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂
Theorem: inverse_spec
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (inverse f y) = y
Tactic:
rw [inverse, dif_pos h]
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y
Theorem: inverse_spec
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y
Tactic:
exact Classical.choose_spec h
Proof state after:
no goals
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
α : Type u_3
⊢ ∀ (f : α → Set α), ¬Surjective f
Tactic:
intro f surjf
Proof state after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Theorem: Cantor
Proof state before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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 α✝
α : 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: Equiv.fwd_rev
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
x : β
⊢ e.fwd (e.rev x) = x
Tactic:
rw [Equiv.fwd_eq_iff_rev_eq]
Proof state after:
no goals