awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Finsupp (goal)
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
f : α →₀ M₀
p : Sym2 α
hp : Ne.{u_2 + 1} (α := M₀) (mul (map (⇑f : (a : α) → M₀) p)) 0
⊢ p ∈ f.support.sym2
have mk : ∀ (a b : α) (hp : Ne.{u_2 + 1} (α := M₀) (mul (map (⇑f : (a : α) → M₀) (Quot.mk (Rel α) (a, b)))) 0),
  Quot.mk (Rel α) (a, b) ∈ f.support.sym2
Tactic: obtain ⟨a, b⟩ := p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : Lattice α
s : Sym2 α
⊢ s.inf ≤ s.sup
have h : ∀ (x y : α), s(x, y).inf ≤ s(x, y).sup
Tactic: cases s using Sym2.ind
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (↑((fun (s : Sym2 α) ↦ (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (s.inf, s.sup) ⋯ : { p : α × α // p.1 ≤ p.2 }))
                s(a, b)) :
            α × α).1 =
        a ∧
      (↑((fun (s : Sym2 α) ↦
                  (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (s.inf, s.sup) ⋯ : { p : α × α // p.1 ≤ p.2 }))
                s(a, b)) :
            α × α).2 =
        b ∨
    (↑((fun (s : Sym2 α) ↦
                  (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (s.inf, s.sup) ⋯ : { p : α × α // p.1 ≤ p.2 }))
                s(a, b)) :
            α × α).1 =
        b ∧
      (↑((fun (s : Sym2 α) ↦
                  (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (s.inf, s.sup) ⋯ : { p : α × α // p.1 ≤ p.2 }))
                s(a, b)) :
            α × α).2 =
        a
have x : a ≤ b ∨ b ≤ a
Tactic: cases le_total a b with
    | inl h => simp [h]
    | inr h => simp [h]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s t : Sym2 α
⊢ s.inf = t.inf ∧ s.sup = t.sup ↔ s = t
have h : ∀ (a b : α), s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t
Tactic: induction s with | _ a b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
t : Sym2 α
a b : α
⊢ s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t
have h : ∀ (c d : α), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: induction t with | _ c d
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
have h : ∀ (hab : a ≤ b), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h : ∀ (hab : a ≤ b), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
have h₁ : ∀ (hba : b ≤ a), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a ≤ b
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
have h : ∀ (hcd : c ≤ d), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: obtain hcd | hdc := le_total c d
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a ≤ b
h : ∀ (hcd : c ≤ d), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
have h₁ : ∀ (hdc : d ≤ c), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: obtain hcd | hdc := le_total c d
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hba : b ≤ a
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
have h : ∀ (hcd : c ≤ d), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: obtain hcd | hdc := le_total c d
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Order (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hba : b ≤ a
h : ∀ (hcd : c ≤ d), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
have h₁ : ∀ (hdc : d ≤ c), s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Tactic: obtain hcd | hdc := le_total c d
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Tree α) (map id nil) nil
have nil : Eq.{u + 1} (α := Tree α) nil nil
Tactic: rw [map]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
v : α
l r : Tree α
hl : map id l = l
hr : map id r = r
⊢ map id (node v l r) = node v l r
have node : node (id v) (map id l) (map id r) = node v l r
Tactic: rw [map, hl, hr, id_eq]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
v : α
l r : Tree α
hl : map id l = l
hr : map id r = r
node : Tree.node (id v) (map id l) (map id r) = Tree.node v l r
⊢ map id (Tree.node v l r) = Tree.node v l r
have node₁ : Tree.node (id v) l (map id r) = Tree.node v l r
Tactic: rw [map, hl, hr, id_eq]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
v : α
l r : Tree α
hl : map id l = l
hr : map id r = r
node : Tree.node (id v) (map id l) (map id r) = Tree.node v l r
node₁ : Tree.node (id v) l (map id r) = Tree.node v l r
⊢ map id (Tree.node v l r) = Tree.node v l r
have node₂ : Tree.node (id v) l r = Tree.node v l r
Tactic: rw [map, hl, hr, id_eq]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
v : α
l r : Tree α
hl : map id l = l
hr : map id r = r
node : Tree.node (id v) (map id l) (map id r) = Tree.node v l r
node₁ : Tree.node (id v) l (map id r) = Tree.node v l r
node₂ : Tree.node (id v) l r = Tree.node v l r
⊢ map id (Tree.node v l r) = Tree.node v l r
have node₃ : Tree.node v l r = Tree.node v l r
Tactic: rw [map, hl, hr, id_eq]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
t : Tree α
⊢ map id t = t
have nil : Eq.{u + 1} (α := Tree α) (map id nil) nil
Tactic: induction t with
  | nil => rw [map]
  | node v l r hl hr => rw [map, hl, hr, id_eq]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
t : Tree α
nil : Eq.{u + 1} (α := Tree α) (map id Tree.nil) Tree.nil
⊢ map id t = t
have node : ∀ (v : α) (l r : Tree α) (hl : map id l = l) (hr : map id r = r), map id (node v l r) = node v l r
Tactic: induction t with
  | nil => rw [map]
  | node v l r hl hr => rw [map, hl, hr, id_eq]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
⊢ map (g ∘ f) nil = map g (map f nil)
have nil : nil = map g (map f nil)
Tactic: rw [map, map, map]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
nil : Tree.nil = map g (map f Tree.nil)
⊢ map (g ∘ f) Tree.nil = map g (map f Tree.nil)
have nil₁ : Tree.nil = map g Tree.nil
Tactic: rw [map, map, map]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
nil : Tree.nil = map g (map f Tree.nil)
nil₁ : Tree.nil = map g Tree.nil
⊢ map (g ∘ f) Tree.nil = map g (map f Tree.nil)
have nil₂ : Eq.{u_2 + 1} (α := Tree γ) Tree.nil Tree.nil
Tactic: rw [map, map, map]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
⊢ map (g ∘ f) (node v l r) = map g (map f (node v l r))
have node : node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (map f (node v l r))
Tactic: rw [map, map, map, hl, hr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
node : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (map f (Tree.node v l r))
⊢ map (g ∘ f) (Tree.node v l r) = map g (map f (Tree.node v l r))
have node₁ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (Tree.node (f v) (map f l) (map f r))
Tactic: rw [map, map, map, hl, hr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
node : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (map f (Tree.node v l r))
node₁ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (Tree.node (f v) (map f l) (map f r))
⊢ map (g ∘ f) (Tree.node v l r) = map g (map f (Tree.node v l r))
have node₂ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
Tactic: rw [map, map, map, hl, hr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
node : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (map f (Tree.node v l r))
node₁ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (Tree.node (f v) (map f l) (map f r))
node₂ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
⊢ map (g ∘ f) (Tree.node v l r) = map g (map f (Tree.node v l r))
have node₃ : Tree.node ((g ∘ f) v) (map g (map f l)) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
Tactic: rw [map, map, map, hl, hr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
node : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (map f (Tree.node v l r))
node₁ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (Tree.node (f v) (map f l) (map f r))
node₂ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
node₃ :
  Tree.node ((g ∘ f) v) (map g (map f l)) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
⊢ map (g ∘ f) (Tree.node v l r) = map g (map f (Tree.node v l r))
have node₄ : Tree.node ((g ∘ f) v) (map g (map f l)) (map g (map f r)) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
Tactic: rw [map, map, map, hl, hr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : Tree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
node : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (map f (Tree.node v l r))
node₁ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = map g (Tree.node (f v) (map f l) (map f r))
node₂ : Tree.node ((g ∘ f) v) (map (g ∘ f) l) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
node₃ :
  Tree.node ((g ∘ f) v) (map g (map f l)) (map (g ∘ f) r) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
node₄ :
  Tree.node ((g ∘ f) v) (map g (map f l)) (map g (map f r)) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
⊢ map (g ∘ f) (Tree.node v l r) = map g (map f (Tree.node v l r))
have node₅ : Tree.node (g (f v)) (map g (map f l)) (map g (map f r)) = Tree.node (g (f v)) (map g (map f l)) (map g (map f r))
Tactic: rw [map, map, map, hl, hr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
t : Tree α
⊢ map (g ∘ f) t = map g (map f t)
have nil : map (g ∘ f) nil = map g (map f nil)
Tactic: induction t with
  | nil => rw [map, map, map]
  | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
t : Tree α
nil : map (g ∘ f) Tree.nil = map g (map f Tree.nil)
⊢ map (g ∘ f) t = map g (map f t)
have node : ∀ (v : α) (l r : Tree α) (hl : map (g ∘ f) l = map g (map f l)) (hr : map (g ∘ f) r = map g (map f r)),
  map (g ∘ f) (node v l r) = map g (map f (node v l r))
Tactic: induction t with
  | nil => rw [map, map, map]
  | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure nil) (pure nil)
have nil : Eq.{u_1 + 1} (α := m (Tree α)) (pure nil) (pure nil)
Tactic: rw [traverse]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (node v l r)) (pure (node v l r))
have node : Eq.{u_1 + 1} (α := m (Tree α)) (node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₂ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> pure r) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
node₂ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> pure r) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₃ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v) <*> pure l <*> pure r) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
node₂ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> pure r) (pure (Tree.node v l r))
node₃ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v) <*> pure l <*> pure r) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₄ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node v <$> pure l <*> pure r) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
node₂ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> pure r) (pure (Tree.node v l r))
node₃ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v) <*> pure l <*> pure r) (pure (Tree.node v l r))
node₄ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node v <$> pure l <*> pure r) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₅ : Eq.{u_1 + 1} (α := m (Tree α)) ((fun (h : Tree α → Tree α) ↦ h r) <$> Tree.node v <$> pure l) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
node₂ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> pure r) (pure (Tree.node v l r))
node₃ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v) <*> pure l <*> pure r) (pure (Tree.node v l r))
node₄ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node v <$> pure l <*> pure r) (pure (Tree.node v l r))
node₅ :
  Eq.{u_1 + 1} (α := m (Tree α)) ((fun (h : Tree α → Tree α) ↦ h r) <$> Tree.node v <$> pure l) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₆ : Eq.{u_1 + 1} (α := m (Tree α)) ((fun (h : Tree α → Tree α) ↦ h r) <$> pure (Tree.node v l)) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
v : α
l r : Tree α
hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l)
hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)
node :
  Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> traverse pure l <*> traverse pure r) (pure (Tree.node v l r))
node₁ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> traverse pure r) (pure (Tree.node v l r))
node₂ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node <$> pure v <*> pure l <*> pure r) (pure (Tree.node v l r))
node₃ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v) <*> pure l <*> pure r) (pure (Tree.node v l r))
node₄ : Eq.{u_1 + 1} (α := m (Tree α)) (Tree.node v <$> pure l <*> pure r) (pure (Tree.node v l r))
node₅ :
  Eq.{u_1 + 1} (α := m (Tree α)) ((fun (h : Tree α → Tree α) ↦ h r) <$> Tree.node v <$> pure l) (pure (Tree.node v l r))
node₆ :
  Eq.{u_1 + 1} (α := m (Tree α)) ((fun (h : Tree α → Tree α) ↦ h r) <$> pure (Tree.node v l)) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (Tree.node v l r)) (pure (Tree.node v l r))
have node₇ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v l r)) (pure (Tree.node v l r))
Tactic: rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
t : Tree α
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure t) (pure t)
have nil : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure nil) (pure nil)
Tactic: induction t with
  | nil => rw [traverse]
  | node v l r hl hr =>
    rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
t : Tree α
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
nil : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure Tree.nil) (pure Tree.nil)
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure t) (pure t)
have node : ∀ (v : α) (l r : Tree α) (hl : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure l) (pure l))
  (hr : Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure r) (pure r)),
  Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure (node v l r)) (pure (node v l r))
Tactic: induction t with
  | nil => rw [traverse]
  | node v l r hl hr =>
    rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
x : Tree α
⊢ x.numLeaves = x.numNodes + 1
have nil : numLeaves.{u} (α := α) nil = numNodes.{u} (α := α) nil + 1
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
x : Tree α
nil : numLeaves.{u} (α := α) Tree.nil = numNodes.{u} (α := α) Tree.nil + 1
⊢ x.numLeaves = x.numNodes + 1
have node : ∀ (value : α) (left right : Tree α),
  left.numLeaves = left.numNodes + 1 →
    right.numLeaves = right.numNodes + 1 → (node value left right).numLeaves = (node value left right).numNodes + 1
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Tree.Basic (goal)
Goal:
α : Type u
x : Tree α
⊢ 0 < x.numLeaves
have rw : 0 < x.numNodes + 1
Tactic: rw [numLeaves_eq_numNodes_succ]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) nil)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g nil))
have nil : Eq.{w + 1} (α := Functor.Comp G F (Tree γ)) (pure nil) (Functor.Comp.mk (pure (pure nil)))
Tactic: rw [traverse, traverse, map_pure, traverse]