internlm/Lean-Github huggingface dataset:
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inr
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
cases Classical.em (num a' = 0) with
| inl ha'0 =>
  simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
| inr ha'0 =>
  simp [Setoid_Iff, ha0, ha'0] at *
  linarith
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inr.inl
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
ha'0 : a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inr.inr
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
ha'0 : ¬a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [Setoid_Iff, ha0, ha'0] at *
Proof state after:
case inr.inr
a a' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
ha0 ha'0 : True
⊢ a.denom * a'.num = a'.denom * a.num
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inr.inr
a a' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
ha0 ha'0 : True
⊢ a.denom * a'.num = a'.denom * a.num
Tactic:
linarith
Proof state after:
no goals
Theorem: LoVe.id_Not_CauchySeq
Proof state before:
⊢ ¬IsCauchySeq fun n => ↑n
Tactic:
rw [IsCauchySeq]
Proof state after:
⊢ ¬∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
Theorem: LoVe.id_Not_CauchySeq
Proof state before:
⊢ ¬∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
Tactic:
intro h
Proof state after:
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
⊢ False
Theorem: LoVe.id_Not_CauchySeq
Proof state before:
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
⊢ False
Tactic:
cases h 1 zero_lt_one with
| intro i hi =>
  have hi_succi :=
    hi (i + 1) (by simp)
  simp [←sub_sub] at hi_succi
Proof state after:
no goals
Theorem: LoVe.id_Not_CauchySeq
Proof state before:
case intro
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
⊢ False
Tactic:
have hi_succi :=
  hi (i + 1) (by simp)
Proof state after:
case intro
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
hi_succi : |↑i - ↑(i + 1)| < 1
⊢ False
Theorem: LoVe.id_Not_CauchySeq
Proof state before:
case intro
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
hi_succi : |↑i - ↑(i + 1)| < 1
⊢ False
Tactic:
simp [←sub_sub] at hi_succi
Proof state after:
no goals
Theorem: LoVe.id_Not_CauchySeq
Proof state before:
h : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |↑N - ↑m| < ε
i : ℕ
hi : ∀ (m : ℕ), m ≥ i → |↑i - ↑m| < 1
⊢ i + 1 ≥ i
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_iff
Proof state before:
f g : CauchySeq
⊢ f ≈ g ↔ ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf f m - seqOf g m| < ε
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
⊢ f + g ≈ f' + g'
Tactic:
intro ε₀ hε₀
Proof state after:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
simp [Setoid_iff]
Proof state after:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
cases hf (ε₀ / 2) (half_pos hε₀) with
| intro Nf hNf =>
  cases hg (ε₀ / 2) (half_pos hε₀) with
  | intro Ng hNg =>
    apply Exists.intro (max Nf Ng)
    intro m hm
    calc
      abs (seqOf (f + g) m - seqOf (f' + g') m)
      = abs ((seqOf f m + seqOf g m)
        - (seqOf f' m + seqOf g' m)) :=
        by rfl
      _ = abs ((seqOf f m - seqOf f' m)
          + (seqOf g m - seqOf g' m)) :=
        by
          have arg_eq :
            seqOf f m + seqOf g m
              - (seqOf f' m + seqOf g' m) =
            seqOf f m - seqOf f' m
              + (seqOf g m - seqOf g' m) :=
            by linarith
          rw [arg_eq]
      _ ≤ abs (seqOf f m - seqOf f' m)
          + abs (seqOf g m - seqOf g' m) :=
        by apply abs_add
      _ < ε₀ / 2 + ε₀ / 2 :=
        add_lt_add (hNf m (le_of_max_le_left hm))
          (hNg m (le_of_max_le_right hm))
      _ = ε₀ :=
        by simp
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
case intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
cases hg (ε₀ / 2) (half_pos hε₀) with
| intro Ng hNg =>
  apply Exists.intro (max Nf Ng)
  intro m hm
  calc
    abs (seqOf (f + g) m - seqOf (f' + g') m)
    = abs ((seqOf f m + seqOf g m)
      - (seqOf f' m + seqOf g' m)) :=
      by rfl
    _ = abs ((seqOf f m - seqOf f' m)
        + (seqOf g m - seqOf g' m)) :=
      by
        have arg_eq :
          seqOf f m + seqOf g m
            - (seqOf f' m + seqOf g' m) =
          seqOf f m - seqOf f' m
            + (seqOf g m - seqOf g' m) :=
          by linarith
        rw [arg_eq]
    _ ≤ abs (seqOf f m - seqOf f' m)
        + abs (seqOf g m - seqOf g' m) :=
      by apply abs_add
    _ < ε₀ / 2 + ε₀ / 2 :=
      add_lt_add (hNf m (le_of_max_le_left hm))
        (hNg m (le_of_max_le_right hm))
    _ = ε₀ :=
      by simp
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
apply Exists.intro (max Nf Ng)
Proof state after:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
⊢ ∀ (m : ℕ), max Nf Ng ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
⊢ ∀ (m : ℕ), max Nf Ng ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
intro m hm
Proof state after:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
calc
  abs (seqOf (f + g) m - seqOf (f' + g') m)
  = abs ((seqOf f m + seqOf g m)
    - (seqOf f' m + seqOf g' m)) :=
    by rfl
  _ = abs ((seqOf f m - seqOf f' m)
      + (seqOf g m - seqOf g' m)) :=
    by
      have arg_eq :
        seqOf f m + seqOf g m
          - (seqOf f' m + seqOf g' m) =
        seqOf f m - seqOf f' m
          + (seqOf g m - seqOf g' m) :=
        by linarith
      rw [arg_eq]
  _ ≤ abs (seqOf f m - seqOf f' m)
      + abs (seqOf g m - seqOf g' m) :=
    by apply abs_add
  _ < ε₀ / 2 + ε₀ / 2 :=
    add_lt_add (hNf m (le_of_max_le_left hm))
      (hNg m (le_of_max_le_right hm))
  _ = ε₀ :=
    by simp
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| = |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)|
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)| = |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)|
Tactic:
have arg_eq :
  seqOf f m + seqOf g m
    - (seqOf f' m + seqOf g' m) =
  seqOf f m - seqOf f' m
    + (seqOf g m - seqOf g' m) :=
  by linarith
Proof state after:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
arg_eq : seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
⊢ |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)| = |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)|
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
arg_eq : seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
⊢ |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)| = |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)|
Tactic:
rw [arg_eq]
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
Tactic:
linarith
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)| ≤ |seqOf f m - seqOf f' m| + |seqOf g m - seqOf g' m|
Tactic:
apply abs_add
Proof state after:
no goals
Theorem: LoVe.CauchySeq.Setoid_add
Proof state before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ ε₀ / 2 + ε₀ / 2 = ε₀
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.BTree.graft_assoc
Proof state before:
α : Type
t u v : BTree α
⊢ graft (graft t u) v = graft t (graft u v)
Tactic:
induction t with
| empty                => rfl
| node a l r ih_l ih_r => simp [BTree.graft, ih_l, ih_r]
Proof state after:
no goals
Theorem: LoVe.BTree.graft_assoc
Proof state before:
case empty
α : Type
u v : BTree α
⊢ graft (graft empty u) v = graft empty (graft u v)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BTree.graft_assoc
Proof state before:
case node
α : Type
u v : BTree α
a : α
l r : BTree α
ih_l : graft (graft l u) v = graft l (graft u v)
ih_r : graft (graft r u) v = graft r (graft u v)
⊢ graft (graft (node a l r) u) v = graft (node a l r) (graft u v)
Tactic:
simp [BTree.graft, ih_l, ih_r]
Proof state after:
no goals
Theorem: LoVe.BTree.graft_empty
Proof state before:
α : Type
t : BTree α
⊢ graft t empty = t
Tactic:
induction t with
| empty                => rfl
| node a l r ih_l ih_r => simp [BTree.graft, ih_l, ih_r]
Proof state after:
no goals
Theorem: LoVe.BTree.graft_empty
Proof state before:
case empty
α : Type
⊢ graft empty empty = empty
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BTree.graft_empty
Proof state before:
case node
α : Type
a : α
l r : BTree α
ih_l : graft l empty = l
ih_r : graft r empty = r
⊢ graft (node a l r) empty = node a l r
Tactic:
simp [BTree.graft, ih_l, ih_r]
Proof state after:
no goals
Theorem: LoVe.BTree.add_left_neg_counterexample
Proof state before:
⊢ ∃ x, ∀ (y : BTree ℕ), graft y x ≠ empty
Tactic:
apply Exists.intro (BTree.node 0 BTree.empty BTree.empty)
Proof state after:
⊢ ∀ (y : BTree ℕ), graft y (node 0 empty empty) ≠ empty
Theorem: LoVe.BTree.add_left_neg_counterexample
Proof state before:
⊢ ∀ (y : BTree ℕ), graft y (node 0 empty empty) ≠ empty
Tactic:
intro y hy
Proof state after:
y : BTree ℕ
hy : graft y (node 0 empty empty) = empty
⊢ False
Theorem: LoVe.BTree.add_left_neg_counterexample
Proof state before:
y : BTree ℕ
hy : graft y (node 0 empty empty) = empty
⊢ False
Tactic:
cases y with
| empty      => cases hy
| node a l r => cases' hy
Proof state after:
no goals
Theorem: LoVe.BTree.add_left_neg_counterexample
Proof state before:
case empty
hy : graft empty (node 0 empty empty) = empty
⊢ False
Tactic:
cases hy
Proof state after:
no goals
Theorem: LoVe.BTree.add_left_neg_counterexample
Proof state before:
case node
a : ℕ
l r : BTree ℕ
hy : graft (node a l r) (node 0 empty empty) = empty
⊢ False
Tactic:
cases' hy
Proof state after:
no goals
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
t : BTree ℕ
⊢ elems (mirror t) = elems t
Tactic:
induction t with
| empty =>
  rfl
| node a l r ih_l ih_r =>
  rw [Multiset.elems]
  rw [mirror]
  rw [←ih_l]
  rw [←ih_r]
  rw [Multiset.elems]
  rw [Multiset.union_assoc,
      Multiset.union_comm (elems (mirror r)),
      ←Multiset.union_assoc]
Proof state after:
no goals
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case empty

⊢ elems (mirror BTree.empty) = elems BTree.empty
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = elems (BTree.node a l r)
Tactic:
rw [Multiset.elems]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = {a} ∪ elems l ∪ elems r
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = {a} ∪ elems l ∪ elems r
Tactic:
rw [mirror]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems l ∪ elems r
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems l ∪ elems r
Tactic:
rw [←ih_l]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems r
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems r
Tactic:
rw [←ih_r]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Tactic:
rw [Multiset.elems]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ {a} ∪ elems (mirror r) ∪ elems (mirror l) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Theorem: LoVe.Multiset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ {a} ∪ elems (mirror r) ∪ elems (mirror l) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Tactic:
rw [Multiset.union_assoc,
    Multiset.union_comm (elems (mirror r)),
    ←Multiset.union_assoc]
Proof state after:
no goals
Theorem: LoVe.Finset.elems_mirror
Proof state before:
t : BTree ℕ
⊢ elems (mirror t) = elems t
Tactic:
induction t with
| empty =>
  rfl
| node a l r ih_l ih_r =>
  rw [Finset.elems]
  rw [mirror]
  rw [←ih_l]
  rw [←ih_r]
  rw [Finset.elems]
  ac_rfl
Proof state after:
no goals
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case empty

⊢ elems (mirror BTree.empty) = elems BTree.empty
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = elems (BTree.node a l r)
Tactic:
rw [Finset.elems]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = {a} ∪ elems l ∪ elems r
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = {a} ∪ elems l ∪ elems r
Tactic:
rw [mirror]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems l ∪ elems r
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems l ∪ elems r
Tactic:
rw [←ih_l]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems r
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems r
Tactic:
rw [←ih_r]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (BTree.node a (mirror r) (mirror l)) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Tactic:
rw [Finset.elems]
Proof state after:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ {a} ∪ elems (mirror r) ∪ elems (mirror l) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Theorem: LoVe.Finset.elems_mirror
Proof state before:
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ {a} ∪ elems (mirror r) ∪ elems (mirror l) = {a} ∪ elems (mirror l) ∪ elems (mirror r)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.List.elems_mirror_counterexample
Proof state before:
⊢ ∃ t, elems t ≠ elems (mirror t)
Tactic:
apply Exists.intro badTree
Proof state after:
⊢ elems badTree ≠ elems (mirror badTree)
Theorem: LoVe.List.elems_mirror_counterexample
Proof state before:
⊢ elems badTree ≠ elems (mirror badTree)
Tactic:
simp [List.elems]
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.add_comm_zero_left_by_exact
Proof state before:
n : ℕ
⊢ add 0 n = add n 0
Tactic:
exact add_comm 0 n
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.nat_exists_double_iden
Proof state before:
⊢ double 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.nat_exists_double_iden_no_show
Proof state before:
⊢ double 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.Forall.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hall : ∀ (x : α), x = t → P x
⊢ P t
Tactic:
apply hall t
Proof state after:
α : Type
t : α
P : α → Prop
hall : ∀ (x : α), x = t → P x
⊢ t = t
Theorem: LoVe.ForwardProofs.Forall.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hall : ∀ (x : α), x = t → P x
⊢ t = t
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.Forall.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hp : P t
x : α
heq : x = t
⊢ P x
Tactic:
rw [heq]
Proof state after:
α : Type
t : α
P : α → Prop
hp : P t
x : α
heq : x = t
⊢ P t
Theorem: LoVe.ForwardProofs.Forall.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hp : P t
x : α
heq : x = t
⊢ P t
Tactic:
exact hp
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.Exists.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P t
Tactic:
rw [←hxt]
Proof state after:
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P x
Theorem: LoVe.ForwardProofs.Exists.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P x
Tactic:
exact hpx
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.Exists.one_point
Proof state before:
α : Type
t : α
P : α → Prop
hp : P t
⊢ t = t
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.two_mul_example
Proof state before:
m n : ℕ
⊢ 2 * m + n = m + m + n
Tactic:
rw [Nat.two_mul]
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.two_mul_example
Proof state before:
m n : ℕ
⊢ m + m + n = m + n + m
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.two_mul_example_have
Proof state before:
m n : ℕ
⊢ 2 * m + n = m + m + n
Tactic:
rw [Nat.two_mul]
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.two_mul_example_have
Proof state before:
m n : ℕ
hmul : 2 * m + n = m + m + n
⊢ m + m + n = m + n + m
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.prop_comp_tactical
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
⊢ a → c
Tactic:
intro ha
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c
Theorem: LoVe.ForwardProofs.prop_comp_tactical
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c
Tactic:
have hb : b :=
  hab ha
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
⊢ c
Theorem: LoVe.ForwardProofs.prop_comp_tactical
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
⊢ c
Tactic:
let c' := c
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
⊢ c
Theorem: LoVe.ForwardProofs.prop_comp_tactical
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
⊢ c
Tactic:
have hc : c' :=
  hbc hb
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
hc : c'
⊢ c
Theorem: LoVe.ForwardProofs.prop_comp_tactical
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
hc : c'
⊢ c
Tactic:
exact hc
Proof state after:
no goals
Theorem: LoVe.ForwardProofs.And_swap_tactical
Proof state before:
a b : Prop
⊢ a ∧ b → b ∧ a
Tactic:
intro hab
Proof state after:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Theorem: LoVe.ForwardProofs.And_swap_tactical
Proof state before:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Tactic:
apply And.intro
Proof state after:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.ForwardProofs.And_swap_tactical
Proof state before:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
apply And.right
Proof state after:
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a