internlm/Lean-Github huggingface dataset:
Theorem: GaussInt.norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm / 2 < y.norm
Tactic:
apply Int.ediv_lt_of_lt_mul
Proof state after:
case H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ 0 < 2

case H'
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm < y.norm * 2
Theorem: GaussInt.norm_mod_lt
Proof state before:
case H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: GaussInt.norm_mod_lt
Proof state before:
case H'
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm < y.norm * 2
Tactic:
linarith
Proof state after:
no goals
Theorem: GaussInt.natAbs_norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm.natAbs < y.norm.natAbs
Tactic:
apply Int.ofNat_lt.1
Proof state after:
x y : GaussInt
hy : y ≠ 0
⊢ ↑(x % y).norm.natAbs < ↑y.norm.natAbs
Theorem: GaussInt.natAbs_norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
⊢ ↑(x % y).norm.natAbs < ↑y.norm.natAbs
Tactic:
simp only [Int.coe_natAbs, abs_of_nonneg, norm_nonneg]
Proof state after:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm < y.norm
Theorem: GaussInt.natAbs_norm_mod_lt
Proof state before:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm < y.norm
Tactic:
apply norm_mod_lt x hy
Proof state after:
no goals
Theorem: GaussInt.not_norm_mul_left_lt_norm
Proof state before:
x y : GaussInt
hy : y ≠ 0
⊢ ¬(x * y).norm.natAbs < x.norm.natAbs
Tactic:
apply not_lt_of_ge
Proof state after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ (x * y).norm.natAbs ≥ x.norm.natAbs
Theorem: GaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ (x * y).norm.natAbs ≥ x.norm.natAbs
Tactic:
rw [norm_mul, Int.natAbs_mul]
Proof state after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ x.norm.natAbs * y.norm.natAbs ≥ x.norm.natAbs
Theorem: GaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ x.norm.natAbs * y.norm.natAbs ≥ x.norm.natAbs
Tactic:
apply le_mul_of_one_le_right (Nat.zero_le _)
Proof state after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ 1 ≤ y.norm.natAbs
Theorem: GaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ 1 ≤ y.norm.natAbs
Tactic:
apply Int.ofNat_le.1
Proof state after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ ↑y.norm.natAbs
Theorem: GaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ ↑y.norm.natAbs
Tactic:
rw [coe_natAbs_norm]
Proof state after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ y.norm
Theorem: GaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ y.norm
Tactic:
exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
n : ℕ
⊢ 0 < fac n
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ 0 < fac 0

case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < fac (n + 1)
Theorem: fac_pos
Proof state before:
case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < fac (n + 1)
Tactic:
rw [fac]
Proof state after:
case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < (n + 1) * fac n
Theorem: fac_pos
Proof state before:
case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < (n + 1) * fac n
Tactic:
exact mul_pos n.succ_pos ih
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
case zero

⊢ 0 < fac 0
Tactic:
rw [fac]
Proof state after:
case zero

⊢ 0 < 1
Theorem: fac_pos
Proof state before:
case zero

⊢ 0 < 1
Tactic:
exact zero_lt_one
Proof state after:
no goals
Theorem: dvd_fac
Proof state before:
i n : ℕ
ipos : 0 < i
ile : i ≤ n
⊢ i ∣ fac n
Tactic:
induction' n with n ih
Proof state after:
case zero
i : ℕ
ipos : 0 < i
ile : i ≤ 0
⊢ i ∣ fac 0

case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ fac (n + 1)
Theorem: dvd_fac
Proof state before:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ fac (n + 1)
Tactic:
rw [fac]
Proof state after:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ (n + 1) * fac n
Theorem: dvd_fac
Proof state before:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ (n + 1) * fac n
Tactic:
rcases Nat.of_le_succ ile with h | h
Proof state after:
case succ.inl
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i ≤ n
⊢ i ∣ (n + 1) * fac n

case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ i ∣ (n + 1) * fac n
Theorem: dvd_fac
Proof state before:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ i ∣ (n + 1) * fac n
Tactic:
rw [h]
Proof state after:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ n.succ ∣ (n + 1) * fac n
Theorem: dvd_fac
Proof state before:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ n.succ ∣ (n + 1) * fac n
Tactic:
apply dvd_mul_right
Proof state after:
no goals
Theorem: dvd_fac
Proof state before:
case zero
i : ℕ
ipos : 0 < i
ile : i ≤ 0
⊢ i ∣ fac 0
Tactic:
exact absurd ipos (not_lt_of_ge ile)
Proof state after:
no goals
Theorem: dvd_fac
Proof state before:
case succ.inl
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i ≤ n
⊢ i ∣ (n + 1) * fac n
Tactic:
apply dvd_mul_of_dvd_right (ih h)
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
n : ℕ
⊢ 2 ^ (n - 1) ≤ fac n
Tactic:
rcases n with _ | n
Proof state after:
case zero

⊢ 2 ^ (0 - 1) ≤ fac 0

case succ
n : ℕ
⊢ 2 ^ (n + 1 - 1) ≤ fac (n + 1)
Theorem: pow_two_le_fac
Proof state before:
case succ
n : ℕ
⊢ 2 ^ (n + 1 - 1) ≤ fac (n + 1)
Tactic:
induction' n with n ih
Proof state after:
case succ.zero

⊢ 2 ^ (0 + 1 - 1) ≤ fac (0 + 1)

case succ.succ
n : ℕ
ih : 2 ^ (n + 1 - 1) ≤ fac (n + 1)
⊢ 2 ^ (n + 1 + 1 - 1) ≤ fac (n + 1 + 1)
Theorem: pow_two_le_fac
Proof state before:
case succ.succ
n : ℕ
ih : 2 ^ (n + 1 - 1) ≤ fac (n + 1)
⊢ 2 ^ (n + 1 + 1 - 1) ≤ fac (n + 1 + 1)
Tactic:
simp at *
Proof state after:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ^ (n + 1) ≤ fac (n + 1 + 1)
Theorem: pow_two_le_fac
Proof state before:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ^ (n + 1) ≤ fac (n + 1 + 1)
Tactic:
rw [pow_succ', fac]
Proof state after:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 * 2 ^ n ≤ (n + 1 + 1) * fac (n + 1)
Theorem: pow_two_le_fac
Proof state before:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 * 2 ^ n ≤ (n + 1 + 1) * fac (n + 1)
Tactic:
apply Nat.mul_le_mul _ ih
Proof state after:
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ≤ n + 1 + 1
Theorem: pow_two_le_fac
Proof state before:
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ≤ n + 1 + 1
Tactic:
repeat' apply Nat.succ_le_succ
Proof state after:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 0 ≤ n
Theorem: pow_two_le_fac
Proof state before:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 0 ≤ n
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case zero

⊢ 2 ^ (0 - 1) ≤ fac 0
Tactic:
simp [fac]
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case succ.zero

⊢ 2 ^ (0 + 1 - 1) ≤ fac (0 + 1)
Tactic:
simp [fac]
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 1 ≤ n + 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 0 ≤ n
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i ∈ range (n + 1), i = n * (n + 1) / 2
Tactic:
symm
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i ∈ range (n + 1), i
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i ∈ range (n + 1), i
Tactic:
apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i
Tactic:
induction' n with n ih
Proof state after:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) = 2 * ∑ i ∈ range (0 + 1), i

case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = 2 * ∑ i ∈ range (n + 1 + 1), i
Theorem: sum_id
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = 2 * ∑ i ∈ range (n + 1 + 1), i
Tactic:
rw [Finset.sum_range_succ, mul_add 2, ← ih]
Proof state after:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = n * (n + 1) + 2 * (n + 1)
Theorem: sum_id
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = n * (n + 1) + 2 * (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: sum_id
Proof state before:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) = 2 * ∑ i ∈ range (0 + 1), i
Tactic:
simp
Proof state after:
no goals
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i ∈ range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6
Tactic:
symm
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) / 6 = ∑ i ∈ range (n + 1), i ^ 2
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) / 6 = ∑ i ∈ range (n + 1), i ^ 2
Tactic:
apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 6)
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
Tactic:
induction' n with n ih
Proof state after:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) * (2 * 0 + 1) = 6 * ∑ i ∈ range (0 + 1), i ^ 2

case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * ∑ i ∈ range (n + 1 + 1), i ^ 2
Theorem: sum_sqr
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * ∑ i ∈ range (n + 1 + 1), i ^ 2
Tactic:
rw [Finset.sum_range_succ, mul_add 6, ← ih]
Proof state after:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2
Theorem: sum_sqr
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) * (2 * n + 1) = 6 * ∑ i ∈ range (n + 1), i ^ 2
⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ 0 < 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: sum_sqr
Proof state before:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) * (2 * 0 + 1) = 6 * ∑ i ∈ range (0 + 1), i ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
n : MyNat
⊢ zero.add n = n
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ zero.add zero = zero

case succ
n : MyNat
ih : zero.add n = n
⊢ zero.add n.succ = n.succ
Theorem: MyNat.zero_add
Proof state before:
case succ
n : MyNat
ih : zero.add n = n
⊢ zero.add n.succ = n.succ
Tactic:
rw [add, ih]
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ zero.add zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
m n : MyNat
⊢ m.succ.add n = (m.add n).succ
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ m.succ.add zero = (m.add zero).succ

case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ m.succ.add n.succ = (m.add n.succ).succ
Theorem: MyNat.succ_add
Proof state before:
case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ m.succ.add n.succ = (m.add n.succ).succ
Tactic:
rw [add, ih]
Proof state after:
case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ (m.add n).succ.succ = (m.add n.succ).succ
Theorem: MyNat.succ_add
Proof state before:
case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ (m.add n).succ.succ = (m.add n.succ).succ
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
case zero
m : MyNat
⊢ m.succ.add zero = (m.add zero).succ
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
m n : MyNat
⊢ m.add n = n.add m
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ m.add zero = zero.add m

case succ
m n : MyNat
ih : m.add n = n.add m
⊢ m.add n.succ = n.succ.add m
Theorem: MyNat.add_comm
Proof state before:
case succ
m n : MyNat
ih : m.add n = n.add m
⊢ m.add n.succ = n.succ.add m
Tactic:
rw [add, succ_add, ih]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case zero
m : MyNat
⊢ m.add zero = zero.add m
Tactic:
rw [zero_add]
Proof state after:
case zero
m : MyNat
⊢ m.add zero = m
Theorem: MyNat.add_comm
Proof state before:
case zero
m : MyNat
⊢ m.add zero = m
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
m n k : MyNat
⊢ (m.add n).add k = m.add (n.add k)
Tactic:
induction' k with k ih
Proof state after:
case zero
m n : MyNat
⊢ (m.add n).add zero = m.add (n.add zero)

case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add n).add k.succ = m.add (n.add k.succ)
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add n).add k.succ = m.add (n.add k.succ)
Tactic:
rw [add, ih]
Proof state after:
case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add (n.add k)).succ = m.add (n.add k.succ)
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add (n.add k)).succ = m.add (n.add k.succ)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case zero
m n : MyNat
⊢ (m.add n).add zero = m.add (n.add zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
m n k : MyNat
⊢ m.mul (n.add k) = (m.mul n).add (m.mul k)
Tactic:
induction' k with k ih
Proof state after:
case zero
m n : MyNat
⊢ m.mul (n.add zero) = (m.mul n).add (m.mul zero)

case succ
m n k : MyNat
ih : m.mul (n.add k) = (m.mul n).add (m.mul k)
⊢ m.mul (n.add k.succ) = (m.mul n).add (m.mul k.succ)
Theorem: MyNat.mul_add
Proof state before:
case succ
m n k : MyNat
ih : m.mul (n.add k) = (m.mul n).add (m.mul k)
⊢ m.mul (n.add k.succ) = (m.mul n).add (m.mul k.succ)
Tactic:
rw [add, mul, mul, ih, add_assoc]
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
case zero
m n : MyNat
⊢ m.mul (n.add zero) = (m.mul n).add (m.mul zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
n : MyNat
⊢ zero.mul n = zero
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ zero.mul zero = zero

case succ
n : MyNat
ih : zero.mul n = zero
⊢ zero.mul n.succ = zero
Theorem: MyNat.zero_mul
Proof state before:
case succ
n : MyNat
ih : zero.mul n = zero
⊢ zero.mul n.succ = zero
Tactic:
rw [mul, ih]
Proof state after:
case succ
n : MyNat
ih : zero.mul n = zero
⊢ zero.add zero = zero
Theorem: MyNat.zero_mul
Proof state before:
case succ
n : MyNat
ih : zero.mul n = zero
⊢ zero.add zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
case zero

⊢ zero.mul zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
m n : MyNat
⊢ m.succ.mul n = (m.mul n).add n
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ m.succ.mul zero = (m.mul zero).add zero

case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ m.succ.mul n.succ = (m.mul n.succ).add n.succ
Theorem: MyNat.succ_mul
Proof state before:
case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ m.succ.mul n.succ = (m.mul n.succ).add n.succ
Tactic:
rw [mul, mul, ih, add_assoc, add_assoc, add_comm n, succ_add]
Proof state after:
case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ (m.mul n).add (m.add n).succ = (m.mul n).add (m.add n.succ)
Theorem: MyNat.succ_mul
Proof state before:
case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ (m.mul n).add (m.add n).succ = (m.mul n).add (m.add n.succ)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
case zero
m : MyNat
⊢ m.succ.mul zero = (m.mul zero).add zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
m n : MyNat
⊢ m.mul n = n.mul m
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ m.mul zero = zero.mul m

case succ
m n : MyNat
ih : m.mul n = n.mul m
⊢ m.mul n.succ = n.succ.mul m
Theorem: MyNat.mul_comm
Proof state before:
case succ
m n : MyNat
ih : m.mul n = n.mul m
⊢ m.mul n.succ = n.succ.mul m
Tactic:
rw [mul, ih, succ_mul]
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
case zero
m : MyNat
⊢ m.mul zero = zero.mul m
Tactic:
rw [zero_mul]
Proof state after:
case zero
m : MyNat
⊢ m.mul zero = zero
Theorem: MyNat.mul_comm
Proof state before:
case zero
m : MyNat
⊢ m.mul zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: fact1
Proof state before:
a b c d e : ℝ
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Tactic:
have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
Proof state after:
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 - 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Theorem: fact1
Proof state before:
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 - 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Tactic:
calc
  a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
  _ ≥ 0 := by apply pow_two_nonneg
Proof state after:
a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Theorem: fact1
Proof state before:
a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: fact1
Proof state before:
a b c d e : ℝ
⊢ a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: fact1
Proof state before:
a b c d e : ℝ
⊢ (a - b) ^ 2 ≥ 0
Tactic:
apply pow_two_nonneg
Proof state after:
no goals
Theorem: fact2
Proof state before:
a b c d e : ℝ
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2
Tactic:
have h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
Proof state after:
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 + 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2
Theorem: fact2
Proof state before:
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 + 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2
Tactic:
calc
  a ^ 2 + 2 * a * b + b ^ 2 = (a + b) ^ 2 := by ring
  _ ≥ 0 := by apply pow_two_nonneg
Proof state after:
a b c d e : ℝ
h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2
Theorem: fact2
Proof state before:
a b c d e : ℝ
h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
⊢ -(a * b) * 2 ≤ a ^ 2 + b ^ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: fact2
Proof state before:
a b c d e : ℝ
⊢ a ^ 2 + 2 * a * b + b ^ 2 = (a + b) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: fact2
Proof state before:
a b c d e : ℝ
⊢ (a + b) ^ 2 ≥ 0
Tactic:
apply pow_two_nonneg
Proof state after:
no goals
Theorem: map_inv_of_inv
Proof state before:
M N F : Type
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass₂ F M N
f : F
m m' : M
h : m * m' = 1
⊢ ↑f m * ↑f m' = 1
Tactic:
rw [← MonoidHomClass₂.map_mul, h, MonoidHomClass₂.map_one]
Proof state after:
no goals
Theorem: absorb1
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) = x
Tactic:
sorry
Proof state after:
no goals
Theorem: absorb2
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y = x
Tactic:
sorry
Proof state after:
no goals
Theorem: absorb1αα
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) = x
Tactic:
apply le_antisymm
Proof state after:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) ≤ x

case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊓ (x ⊔ y)
Theorem: absorb1αα
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊓ (x ⊔ y)
Tactic:
apply le_inf
Proof state after:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x

case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ y
Theorem: absorb1αα
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ y
Tactic:
apply le_sup_left
Proof state after:
no goals
Theorem: absorb1αα
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) ≤ x
Tactic:
apply inf_le_left
Proof state after:
no goals
Theorem: absorb1αα
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: absorb2αα
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y = x
Tactic:
apply le_antisymm
Proof state after:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y ≤ x

case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ x ⊓ y
Theorem: absorb2αα
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ x ⊓ y
Tactic:
apply le_sup_left
Proof state after:
no goals
Theorem: absorb2αα
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y ≤ x
Tactic:
apply sup_le
Proof state after:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x

case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ y ≤ x
Theorem: absorb2αα
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ y ≤ x
Tactic:
apply inf_le_left
Proof state after:
no goals
Theorem: absorb2αα
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: aux1
Proof state before:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : a ≤ b
⊢ 0 ≤ b - a
Tactic:
rw [← sub_self a, sub_eq_add_neg, sub_eq_add_neg, add_comm, add_comm b]
Proof state after:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : a ≤ b
⊢ -a + a ≤ -a + b
Theorem: aux1
Proof state before:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : a ≤ b
⊢ -a + a ≤ -a + b
Tactic:
apply add_le_add_left h
Proof state after:
no goals
Theorem: aux2
Proof state before:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : 0 ≤ b - a
⊢ a ≤ b
Tactic:
rw [← add_zero a, ← sub_add_cancel b a, add_comm (b - a)]
Proof state after:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : 0 ≤ b - a
⊢ a + 0 ≤ a + (b - a)
Theorem: aux2
Proof state before:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : 0 ≤ b - a
⊢ a + 0 ≤ a + (b - a)
Tactic:
apply add_le_add_left h
Proof state after:
no goals
Theorem: aux
Proof state before:
X✝ : Type u_1
Y✝ : Type u_2
X : Type u_3
Y : Type u_4
A : Type u_5
inst✝ : TopologicalSpace X
c : A → X
f : A → Y
x : X
F : Filter Y
h : Tendsto f (comap c (𝓝 x)) F
V' : Set Y
V'_in : V' ∈ F
⊢ ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V'
Tactic:
simpa [and_assoc] using ((nhds_basis_opens' x).comap c).tendsto_left_iff.mp h V' V'_in
Proof state after:
no goals