internlm/Lean-Github huggingface dataset:
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + (a₂ + a₃)) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0
Tactic:
all_goals simp [RingHom.iterate_map_zero, mul_zero, AddMonoidAlgebra.single_zero]
Proof state after:
no goals
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)
Tactic:
intros n r1 r2
Proof state after:
case e_g.h.h.e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
n : ℕ
r1 r2 : R
⊢ single (a₁ + n) (b₁ * (↑φ)^[a₁] (r1 + r2)) = single (a₁ + n) (b₁ * (↑φ)^[a₁] r1) + single (a₁ + n) (b₁ * (↑φ)^[a₁] r2)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
n : ℕ
r1 r2 : R
⊢ single (a₁ + n) (b₁ * (↑φ)^[a₁] (r1 + r2)) = single (a₁ + n) (b₁ * (↑φ)^[a₁] r1) + single (a₁ + n) (b₁ * (↑φ)^[a₁] r2)
Tactic:
rw [RingHom.iterate_map_add, mul_add, AddMonoidAlgebra.single_add]
Proof state after:
no goals
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)
Tactic:
intros n r1 r2
Proof state after:
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
n : ℕ
r1 r2 : R
⊢ single (a₁ + n) (b₁ * (↑φ)^[a₁] (r1 + r2)) = single (a₁ + n) (b₁ * (↑φ)^[a₁] r1) + single (a₁ + n) (b₁ * (↑φ)^[a₁] r2)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
n : ℕ
r1 r2 : R
⊢ single (a₁ + n) (b₁ * (↑φ)^[a₁] (r1 + r2)) = single (a₁ + n) (b₁ * (↑φ)^[a₁] r1) + single (a₁ + n) (b₁ * (↑φ)^[a₁] r2)
Tactic:
rw [RingHom.iterate_map_add, mul_add, AddMonoidAlgebra.single_add]
Proof state after:
no goals
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
intros n r1 r2
Proof state after:
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
n : ℕ
r1 r2 : R
⊢ (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) ((r1 + r2) * (↑φ)^[n] b₂)) =
    (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r1 * (↑φ)^[n] b₂)) +
      sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r2 * (↑φ)^[n] b₂)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
n : ℕ
r1 r2 : R
⊢ (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) ((r1 + r2) * (↑φ)^[n] b₂)) =
    (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r1 * (↑φ)^[n] b₂)) +
      sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r2 * (↑φ)^[n] b₂)
Tactic:
simp_rw [add_mul, AddMonoidAlgebra.single_add, sum_add]
Proof state after:
no goals
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
intros n r1 r2
Proof state after:
case h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
n : ℕ
r1 r2 : R
⊢ (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) ((r1 + r2) * (↑φ)^[n] b₂)) =
    (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r1 * (↑φ)^[n] b₂)) +
      sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r2 * (↑φ)^[n] b₂)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
n : ℕ
r1 r2 : R
⊢ (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) ((r1 + r2) * (↑φ)^[n] b₂)) =
    (sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r1 * (↑φ)^[n] b₂)) +
      sum c.toFinsupp fun a₂ b₂ => single (n + a₂) (r2 * (↑φ)^[n] b₂)
Tactic:
simp_rw [add_mul, AddMonoidAlgebra.single_add, sum_add]
Proof state after:
no goals
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0
Tactic:
simp [RingHom.iterate_map_zero, mul_zero, AddMonoidAlgebra.single_zero]
Proof state after:
no goals
Theorem: HW3.problem_1
Proof state before:
U : Type
A B : Set U
⊢ A ∩ B ∪ A = A
Tactic:
sorry
Proof state after:
no goals
Theorem: HW3.problem_2
Proof state before:
U : Type
A B : Set U
⊢ (Aᶜ \ B)ᶜ = A ∪ B
Tactic:
sorry
Proof state after:
no goals
Theorem: BrownCs22.Set.inter_union_cancel_left
Proof state before:
α : Type u
s t : Set α
⊢ s ∩ t ∪ s = s
Tactic:
simp
Proof state after:
no goals
Theorem: BrownCs22.Set.inter_union_cancel_right
Proof state before:
α : Type u
s t : Set α
⊢ s ∩ t ∪ t = t
Tactic:
simp
Proof state after:
no goals
Theorem: example_1
Proof state before:
p : Prop
⊢ p → p → p
Tactic:
sorry
Proof state after:
no goals
Theorem: example_1'
Proof state before:
p : Prop
⊢ p → p → p
Tactic:
intro hp1
Proof state after:
p : Prop
hp1 : p
⊢ p → p
Theorem: example_1'
Proof state before:
p : Prop
hp1 : p
⊢ p → p
Tactic:
intro hp2
Proof state after:
p : Prop
hp1 hp2 : p
⊢ p
Theorem: example_1'
Proof state before:
p : Prop
hp1 hp2 : p
⊢ p
Tactic:
sorry
Proof state after:
no goals
Theorem: problem_1
Proof state before:
p q r s : Prop
⊢ p ∧ q ∧ r → p ∧ r
Tactic:
intro hpqr
Proof state after:
p q r s : Prop
hpqr : p ∧ q ∧ r
⊢ p ∧ r
Theorem: problem_1
Proof state before:
p q r s : Prop
hpqr : p ∧ q ∧ r
⊢ p ∧ r
Tactic:
eliminate hpqr with hp hqr
Proof state after:
case intro
p q r s : Prop
hp : p
hqr : q ∧ r
⊢ p ∧ r
Theorem: problem_1
Proof state before:
case intro
p q r s : Prop
hp : p
hqr : q ∧ r
⊢ p ∧ r
Tactic:
eliminate hqr with hq hr
Proof state after:
case intro.intro
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p ∧ r
Theorem: problem_1
Proof state before:
case intro.intro
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p ∧ r
Tactic:
split_goal
Proof state after:
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p

case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Theorem: problem_1
Proof state before:
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p

case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Tactic:
{ assumption }
Proof state after:
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Theorem: problem_1
Proof state before:
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Tactic:
{ assumption }
Proof state after:
no goals
Theorem: problem_1
Proof state before:
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p
Tactic:
assumption
Proof state after:
no goals
Theorem: problem_1
Proof state before:
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Tactic:
assumption
Proof state after:
no goals
Theorem: problem_2
Proof state before:
p q r s : Prop
⊢ (p → ¬q) → ¬(p ∧ q)
Tactic:
intro hpnq
Proof state after:
p q r s : Prop
hpnq : p → ¬q
⊢ ¬(p ∧ q)
Theorem: problem_2
Proof state before:
p q r s : Prop
hpnq : p → ¬q
⊢ ¬(p ∧ q)
Tactic:
intro hpq
Proof state after:
p q r s : Prop
hpnq : p → ¬q
hpq : p ∧ q
⊢ False
Theorem: problem_2
Proof state before:
p q r s : Prop
hpnq : p → ¬q
hpq : p ∧ q
⊢ False
Tactic:
eliminate hpq with hp hq
Proof state after:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
⊢ False
Theorem: problem_2
Proof state before:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
⊢ False
Tactic:
have hnq : ¬ q := hpnq hp
Proof state after:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
hnq : ¬q
⊢ False
Theorem: problem_2
Proof state before:
case intro
p q r s : Prop
hpnq : p → ¬q
hp : p
hq : q
hnq : ¬q
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: problem_3
Proof state before:
p q r s : Prop
⊢ (p ∨ q) ∧ (p → r) ∧ (q → s) → r ∨ s
Tactic:
intro h_long_and
Proof state after:
p q r s : Prop
h_long_and : (p ∨ q) ∧ (p → r) ∧ (q → s)
⊢ r ∨ s
Theorem: problem_3
Proof state before:
p q r s : Prop
h_long_and : (p ∨ q) ∧ (p → r) ∧ (q → s)
⊢ r ∨ s
Tactic:
eliminate h_long_and with hpq h_short_and
Proof state after:
case intro
p q r s : Prop
hpq : p ∨ q
h_short_and : (p → r) ∧ (q → s)
⊢ r ∨ s
Theorem: problem_3
Proof state before:
case intro
p q r s : Prop
hpq : p ∨ q
h_short_and : (p → r) ∧ (q → s)
⊢ r ∨ s
Tactic:
eliminate h_short_and with hpr hqs
Proof state after:
case intro.intro
p q r s : Prop
hpq : p ∨ q
hpr : p → r
hqs : q → s
⊢ r ∨ s
Theorem: problem_3
Proof state before:
case intro.intro
p q r s : Prop
hpq : p ∨ q
hpr : p → r
hqs : q → s
⊢ r ∨ s
Tactic:
eliminate hpq with hp hq
Proof state after:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s

case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Theorem: problem_3
Proof state before:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s

case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Tactic:
{ have hr : r := hpr hp 
  left 
  assumption }
Proof state after:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Theorem: problem_3
Proof state before:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Tactic:
{ have hs : s := hqs hq 
  right 
  assumption }
Proof state after:
no goals
Theorem: problem_3
Proof state before:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s
Tactic:
have hr : r := hpr hp
Proof state after:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r ∨ s
Theorem: problem_3
Proof state before:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r ∨ s
Tactic:
left
Proof state after:
case intro.intro.inl.h
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r
Theorem: problem_3
Proof state before:
case intro.intro.inl.h
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r
Tactic:
assumption
Proof state after:
no goals
Theorem: problem_3
Proof state before:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Tactic:
have hs : s := hqs hq
Proof state after:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ r ∨ s
Theorem: problem_3
Proof state before:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ r ∨ s
Tactic:
right
Proof state after:
case intro.intro.inr.h
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ s
Theorem: problem_3
Proof state before:
case intro.intro.inr.h
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ s
Tactic:
assumption
Proof state after:
no goals
Theorem: HW2.problem_1
Proof state before:
⊢ ∃ n, ∀ (x : ℕ), n ≤ x
Tactic:
sorry
Proof state after:
no goals
Theorem: HW2.problem_2
Proof state before:
⊢ 5 ∣ 15
Tactic:
sorry
Proof state after:
no goals
Theorem: HW2.problem_3
Proof state before:
⊢ ∀ (x : ℕ), x ∣ 10 → x ∣ 100
Tactic:
sorry
Proof state after:
no goals
Theorem: HW2.problem_4
Proof state before:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
⊢ a ≤ b
Tactic:
sorry
Proof state after:
no goals
Theorem: HW2.bonus_challenge
Proof state before:
p : Prop
⊢ ¬(p ↔ ¬p)
Tactic:
sorry
Proof state after:
no goals
Theorem: problem_1
Proof state before:
p q r s : Prop
⊢ p ∧ q ∧ r → p ∧ r
Tactic:
sorry
Proof state after:
no goals
Theorem: problem_2
Proof state before:
p q r s : Prop
⊢ (p → ¬q) → ¬(p ∧ q)
Tactic:
sorry
Proof state after:
no goals
Theorem: problem_3
Proof state before:
p q r s : Prop
⊢ (p ∨ q) ∧ (p → r) ∧ (q → s) → r ∨ s
Tactic:
sorry
Proof state after:
no goals
Theorem: Lecture04.these_are_contradictory
Proof state before:
p q r al_ac betty_beg carl_cac : Prop
h1 : al_ac ∧ (betty_beg ∨ carl_cac)
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
⊢ False
Tactic:
eliminate h1 with h4 h5
Proof state after:
case intro
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h5 : betty_beg ∨ carl_cac
⊢ False
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h5 : betty_beg ∨ carl_cac
⊢ False
Tactic:
eliminate h5 with h6 h7
Proof state after:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
⊢ False

case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
⊢ False

case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Tactic:
{ have h8 : ¬ al_ac := h2 h6 contradiction }
Proof state after:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Tactic:
{ have h9 : betty_beg := h3 h7 have h10 : ¬ al_ac := h2 h9  contradiction }
Proof state after:
no goals
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
⊢ False
Tactic:
have h8 : ¬ al_ac := h2 h6
Proof state after:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
h8 : ¬al_ac
⊢ False
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
h8 : ¬al_ac
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Tactic:
have h9 : betty_beg := h3 h7
Proof state after:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
⊢ False
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
⊢ False
Tactic:
have h10 : ¬ al_ac := h2 h9
Proof state after:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
h10 : ¬al_ac
⊢ False
Theorem: Lecture04.these_are_contradictory
Proof state before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
h10 : ¬al_ac
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: HW2.problem_1
Proof state before:
⊢ ∃ n, ∀ (x : ℕ), n ≤ x
Tactic:
existsi 0
Proof state after:
⊢ ∀ (x : ℕ), 0 ≤ x
Theorem: HW2.problem_1
Proof state before:
⊢ ∀ (x : ℕ), 0 ≤ x
Tactic:
intro x
Proof state after:
x : ℕ
⊢ 0 ≤ x
Theorem: HW2.problem_1
Proof state before:
x : ℕ
⊢ 0 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: HW2.problem_2
Proof state before:
⊢ 5 ∣ 15
Tactic:
existsi 3
Proof state after:
⊢ 15 = 5 * 3
Theorem: HW2.problem_2
Proof state before:
⊢ 15 = 5 * 3
Tactic:
numbers
Proof state after:
no goals
Theorem: HW2.problem_3
Proof state before:
⊢ ∀ (x : ℕ), x ∣ 10 → x ∣ 100
Tactic:
intro x
Proof state after:
x : ℕ
⊢ x ∣ 10 → x ∣ 100
Theorem: HW2.problem_3
Proof state before:
x : ℕ
⊢ x ∣ 10 → x ∣ 100
Tactic:
intro hxdvd
Proof state after:
x : ℕ
hxdvd : x ∣ 10
⊢ x ∣ 100
Theorem: HW2.problem_3
Proof state before:
x : ℕ
hxdvd : x ∣ 10
⊢ x ∣ 100
Tactic:
dsimp [dvd] at hxdvd
Proof state after:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ x ∣ 100
Theorem: HW2.problem_3
Proof state before:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ x ∣ 100
Tactic:
dsimp [dvd]
Proof state after:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ ∃ c, 100 = x * c
Theorem: HW2.problem_3
Proof state before:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ ∃ c, 100 = x * c
Tactic:
eliminate hxdvd with k hkx
Proof state after:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ ∃ c, 100 = x * c
Theorem: HW2.problem_3
Proof state before:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ ∃ c, 100 = x * c
Tactic:
existsi k*10
Proof state after:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ 100 = x * (k * 10)
Theorem: HW2.problem_3
Proof state before:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ 100 = x * (k * 10)
Tactic:
linarith
Proof state after:
no goals
Theorem: HW2.problem_4
Proof state before:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
⊢ a ≤ b
Tactic:
have hab2 : 2*a ≤ a + b ∨ a + b ≤ 2*b := h (a + b)
Proof state after:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
hab2 : 2 * a ≤ a + b ∨ a + b ≤ 2 * b
⊢ a ≤ b
Theorem: HW2.problem_4
Proof state before:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
hab2 : 2 * a ≤ a + b ∨ a + b ≤ 2 * b
⊢ a ≤ b
Tactic:
eliminate hab2 with h1 h2
Proof state after:
case inl
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h1 : 2 * a ≤ a + b
⊢ a ≤ b

case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
Theorem: HW2.problem_4
Proof state before:
case inl
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h1 : 2 * a ≤ a + b
⊢ a ≤ b

case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
Tactic:
linarith
Proof state after:
case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
Theorem: HW2.problem_4
Proof state before:
case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
Tactic:
linarith
Proof state after:
no goals
Theorem: HW2.bonus_challenge
Proof state before:
p : Prop
⊢ ¬(p ↔ ¬p)
Tactic:
intro hiff
Proof state after:
p : Prop
hiff : p ↔ ¬p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
p : Prop
hiff : p ↔ ¬p
⊢ False
Tactic:
eliminate hiff with h_left h_right
Proof state after:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ False
Tactic:
have hnp : ¬ p
Proof state after:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p

case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p

case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
Tactic:
{ intro hp 
  have hnp : ¬ p := h_left hp
  contradiction }
Proof state after:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
Tactic:
have hp : p := h_right hnp
Proof state after:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
hp : p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
hp : p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: HW2.bonus_challenge
Proof state before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p
Tactic:
intro hp
Proof state after:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
⊢ False
Tactic:
have hnp : ¬ p := h_left hp
Proof state after:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
hnp : ¬p
⊢ False
Theorem: HW2.bonus_challenge
Proof state before:
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hp : p
hnp : ¬p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Complexity.CostFunction.flatmap_bind
Proof state before:
θ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Zero θ
x : CostFunction α θ
f : β → Option α
g : γ → Option β
c : γ
⊢ flatMap (flip Option.bind f ∘ g) x c = flatMap g (flatMap f x) c
Tactic:
cases hg:g c <;> simp [flatMap, flip, Option.bind, hg]
Proof state after:
no goals
Theorem: List.split'_isSome
Proof state before:
α : Type u_1
head✝¹ head✝ : α
tl : List α
⊢ Option.isSome (split' (head✝¹ :: head✝ :: tl)).1 = decide (length (head✝¹ :: head✝ :: tl) % 2 = 1)
Tactic:
simpa using List.split'_isSome tl
Proof state after:
no goals
Theorem: List.split'_length_left
Proof state before:
α : Type u_1
head✝¹ head✝ : α
tl : List α
⊢ length (split' (head✝¹ :: head✝ :: tl)).2.1 = length (head✝¹ :: head✝ :: tl) / 2
Tactic:
simpa using List.split'_length_left tl
Proof state after:
no goals
Theorem: List.split'_length_right
Proof state before:
α : Type u_1
head✝¹ head✝ : α
tl : List α
⊢ length (split' (head✝¹ :: head✝ :: tl)).2.2 = length (head✝¹ :: head✝ :: tl) / 2
Tactic:
simpa using List.split'_length_right tl
Proof state after:
no goals
Theorem: HMem.Complexity.Karatsuba.eq_decide
Proof state before:
P : Prop
b : Bool
inst✝ : Decidable P
⊢ (b = decide P) = (decide (b = true) = true ↔ P)
Tactic:
cases b <;> simp
Proof state after:
no goals