awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Tactic:
and_iff_right ⟨a, mem_univ _, ha⟩

Premises used: Finset.mem_univ, and_iff_right, And.intro, Exists.intro
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Tactic:
exact and_iff_right ⟨a, mem_univ _, ha⟩

Premises used: and_iff_right
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Fintype.card.{u_1} (↑diagSetᶜ : Type u_1) = (Fintype.card α).choose 2

Tactic:
card_subtype_not_diag

Premises used: Sym2.card_subtype_not_diag, Set.Mem, setOf, Sym2.diagSet, Set.decidableCompl._aux_1, Not, Sym2.IsDiag
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_2
inst : Fintype α
⊢ Fintype.card.{u_2} (Sym2 α) = (Fintype.card α + 1).choose 2

Tactic:
Finset.card_sym2 _

Premises used: Finset.univ, Finset.card_sym2, Fintype.card, Finset.sym2
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
f : α →₀ M₀
h :
  ∀ (x : Sym2 α) (a b : α),
    Quot.mk (Rel α) (a, b) ∈ (↑f.support.sym2 : Set (Sym2 α)) ↔
      Membership.mem (γ := Set (Sym2 α))
        (Set.preimage.{u_1, u_2} (β := Sym2 M₀) (map (⇑f : (a : α) → M₀)) (Function.support mul))
        (Quot.mk (Rel α) (a, b))
⊢ (↑f.support.sym2 : Set (Sym2 α)) =
    Set.preimage.{u_1, u_2} (β := Sym2 M₀) (map (⇑f : (a : α) → M₀)) (Function.support mul)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
f : α →₀ M₀
x : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ (↑f.support.sym2 : Set (Sym2 α)) ↔
    Membership.mem (γ := Set (Sym2 α))
      (Set.preimage.{u_1, u_2} (β := Sym2 M₀) (map (⇑f : (a : α) → M₀)) (Function.support mul)) (Quot.mk (Rel α) (a, b))

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
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
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
⊢ p ∈ f.support.sym2

Tactic:
obtain ⟨a, b⟩ := p
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
f : α →₀ M₀
p : Sym2 α
a b : α
hp : ¬HMul.hMul (α := M₀) (β := M₀) ((f : (a : α) → M₀) a : M₀) ((f : (a : α) → M₀) b : M₀) = 0
⊢ Quot.mk (Rel α) (a, b) ∈ f.support.sym2

Tactic:
simpa using .intro (left_ne_zero_of_mul hp) (right_ne_zero_of_mul hp)
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
f : α →₀ M₀
⊢ f.sym2Mul.support ⊆ f.support.sym2

Tactic:
support_onFinset_subset

Premises used: Set.Mem, setOf, Finsupp.support_onFinset_subset
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
f : α →₀ M₀
⊢ Eq (α := (a : Sym2 α) → M₀) (⇑f.sym2Mul : (a : Sym2 α) → M₀) (mul ∘ map (⇑f : (a : α) → M₀))

Tactic:
rfl

Premises used: Sym2.mul, rfl
-- Module: Mathlib.Data.Sym.Sym2.Finsupp
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
f : α →₀ M₀
a b : α
⊢ (f.sym2Mul : (a : Sym2 α) → M₀) s(a, b) =
    HMul.hMul (α := M₀) (β := M₀) ((f : (a : α) → M₀) a : M₀) ((f : (a : α) → M₀) b : M₀)

Tactic:
rfl

Premises used: Sym2.mul, rfl
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : SemilatticeSup α
a b : α
⊢ s(a, b).sup = a ⊔ b

Tactic:
rfl

Premises used: Sym2.sup, rfl
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
⊢ s(a, b).inf = a ⊓ b

Tactic:
rfl

Premises used: Sym2.inf, rfl
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : Lattice α
s : Sym2 α
h : ∀ (x y : α), s(x, y).inf ≤ s(x, y).sup
⊢ s.inf ≤ s.sup

Tactic:
cases s using Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : Lattice α
x y : α
⊢ s(x, y).inf ≤ s(x, y).sup

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : 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

Tactic:
simp [h]
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ 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)) :
            α × α).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

Tactic:
simp [h]
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a ≤ b ∨ b ≤ a

Tactic:
cases le_total a b with
    | inl h => simp [h]
    | inr h => simp [h]

Premises used: le_total
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
hxy : (x, y).1 ≤ (x, y).2
⊢ (↑((fun (s : Sym2 α) ↦ (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (s.inf, s.sup) ⋯ : { p : α × α // p.1 ≤ p.2 }))
            ((fun (p : { p : α × α // p.1 ≤ p.2 }) ↦ s((↑p : α × α).1, (↑p : α × α).2))
              (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (x, y) hxy))) :
        α × α).1 =
    (↑(Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (x, y) hxy) : α × α).1

Tactic:
simp [hxy]
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
hxy : (x, y).1 ≤ (x, y).2
⊢ (↑((fun (s : Sym2 α) ↦ (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (s.inf, s.sup) ⋯ : { p : α × α // p.1 ≤ p.2 }))
            ((fun (p : { p : α × α // p.1 ≤ p.2 }) ↦ s((↑p : α × α).1, (↑p : α × α).2))
              (Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (x, y) hxy))) :
        α × α).2 =
    (↑(Subtype.mk (p := fun (p : α × α) ↦ p.1 ≤ p.2) (x, y) hxy) : α × α).2

Tactic:
simp [hxy]
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
s t : Sym2 α
h : ∀ (a b : α), s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t
⊢ s.inf = t.inf ∧ s.sup = t.sup ↔ s = t

Tactic:
induction s with | _ a b
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
t : Sym2 α
a b : α
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)
⊢ s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t

Tactic:
induction t with | _ c d
-- Module: Mathlib.Data.Sym.Sym2.Order
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)
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)
⊢ 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

Premises used: le_total
-- Module: Mathlib.Data.Sym.Sym2.Order
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)
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)
⊢ 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

Premises used: le_total
-- Module: Mathlib.Data.Sym.Sym2.Order
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)
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)
⊢ 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

Premises used: le_total
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a ≤ b
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:
aesop (add unsafe le_antisymm)

Premises used: le_antisymm
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a ≤ b
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:
aesop (add unsafe le_antisymm)

Premises used: le_antisymm
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hba : b ≤ a
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:
aesop (add unsafe le_antisymm)

Premises used: le_antisymm
-- Module: Mathlib.Data.Sym.Sym2.Order
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hba : b ≤ a
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:
aesop (add unsafe le_antisymm)

Premises used: le_antisymm
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
nil nil₁ : Eq.{u + 1} (α := Tree α) Tree.nil Tree.nil
⊢ Eq.{u + 1} (α := Tree α) (map id Tree.nil) Tree.nil

Tactic:
rw [map]

Premises used: Tree.map
-- Module: Mathlib.Data.Tree.Basic
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
node₃ node₄ : Tree.node v l r = Tree.node v l r
⊢ map id (Tree.node v l r) = Tree.node v l r

Tactic:
rw [map, hl, hr, id_eq]

Premises used: Tree.map, id_eq
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
t : Tree α
nil : Eq.{u + 1} (α := Tree α) (map id Tree.nil) Tree.nil
node : ∀ (v : α) (l r : Tree α) (hl : map id l = l) (hr : map id r = r), map id (Tree.node v l r) = Tree.node v l r
⊢ map id t = t

Tactic:
induction t with
  | nil => rw [map]
  | node v l r hl hr => rw [map, hl, hr, id_eq]

Premises used: Tree.node, Tree.nil, Tree.map, id_eq
-- Module: Mathlib.Data.Tree.Basic
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
nil₂ nil₃ : Eq.{u_2 + 1} (α := Tree γ) Tree.nil Tree.nil
⊢ map (g ∘ f) Tree.nil = map g (map f Tree.nil)

Tactic:
rw [map, map, map]

Premises used: Tree.map
-- Module: Mathlib.Data.Tree.Basic
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))
node₅ 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))

Tactic:
rw [map, map, map, hl, hr, Function.comp_apply]

Premises used: Tree.map, Function.comp_apply
-- Module: Mathlib.Data.Tree.Basic
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)
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) (Tree.node v l r) = map g (map f (Tree.node v l r))
⊢ map (g ∘ f) t = map g (map f t)

Tactic:
induction t with
  | nil => rw [map, map, map]
  | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]

Premises used: Tree.node, Tree.nil, Tree.map, Function.comp_apply
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
m : Type u → Type u_1
inst : Applicative m
inst_1 : LawfulApplicative m
nil nil₁ : Eq.{u_1 + 1} (α := m (Tree α)) (pure Tree.nil) (pure Tree.nil)
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure Tree.nil) (pure Tree.nil)

Tactic:
rw [traverse]

Premises used: Tree.traverse
-- Module: Mathlib.Data.Tree.Basic
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))
node₇ node₈ : Eq.{u_1 + 1} (α := m (Tree α)) (pure (Tree.node v l 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))

Tactic:
rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

Premises used: LawfulApplicative.seq_pure, LawfulApplicative.pure_seq, LawfulApplicative.map_pure, Tree.traverse
-- Module: Mathlib.Data.Tree.Basic
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)
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 (Tree.node v l r)) (pure (Tree.node v l r))
⊢ Eq.{u_1 + 1} (α := m (Tree α)) (traverse pure t) (pure t)

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]

Premises used: Tree.node, Tree.nil, LawfulApplicative.seq_pure, LawfulApplicative.pure_seq, LawfulApplicative.map_pure, Tree.traverse
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
x : Tree α
nil : numLeaves.{u} (α := α) Tree.nil = numNodes.{u} (α := α) Tree.nil + 1
node :
  ∀ (value : α) (left right : Tree α),
    left.numLeaves = left.numNodes + 1 →
      right.numLeaves = right.numNodes + 1 →
        (Tree.node value left right).numLeaves = (Tree.node value left right).numNodes + 1
⊢ x.numLeaves = x.numNodes + 1

Tactic:
induction x
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
⊢ numLeaves.{u} (α := α) nil = numNodes.{u} (α := α) nil + 1

Tactic:
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Premises used: Nat.add_left_comm, Nat.add_assoc, Nat.add_comm
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
value : α
left right : Tree α
left_ih : left.numLeaves = left.numNodes + 1
right_ih : right.numLeaves = right.numNodes + 1
⊢ (node value left right).numLeaves = (node value left right).numNodes + 1

Tactic:
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Premises used: Nat.add_left_comm, Nat.add_assoc, Nat.add_comm
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
x : Tree α
rw : 0 < x.numNodes + 1
⊢ 0 < x.numLeaves

Tactic:
rw [numLeaves_eq_numNodes_succ]

Premises used: Tree.numLeaves_eq_numNodes_succ
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
x : Tree α
⊢ 0 < x.numNodes + 1

Tactic:
x.numNodes.zero_lt_succ

Premises used: Tree.numNodes, Nat.zero_lt_succ
-- Module: Mathlib.Data.Tree.Basic
Goal:
α : Type u
x : Tree α
⊢ 0 < x.numNodes + 1

Tactic:
exact x.numNodes.zero_lt_succ

Premises used: Tree.numNodes, Nat.zero_lt_succ
-- Module: Mathlib.Data.Tree.Basic
Goal:
h : Ne (α := Tree Unit) nil nil
⊢ node () (left nil) (right nil) = nil

Tactic:
trivial
-- Module: Mathlib.Data.Tree.Traversable
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 β
nil : Eq.{w + 1} (α := Functor.Comp G F (Tree γ)) (pure Tree.nil) (Functor.Comp.mk (pure (pure Tree.nil)))
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) Tree.nil)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g Tree.nil))

Tactic:
rw [traverse, traverse, map_pure, traverse]

Premises used: LawfulApplicative.map_pure, Tree.traverse
-- Module: Mathlib.Data.Tree.Traversable
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.{w + 1} (α := Functor.Comp G F (Tree γ)) (pure nil) (Functor.Comp.mk (pure (pure nil)))

Tactic:
rfl
-- Module: Mathlib.Data.Tree.Traversable
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 β
v : α
l r : Tree α
hl :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l))
hr :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
node :
  Eq (α := Functor.Comp G F (Tree γ))
    (Tree.node <$> (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) v <*>
        Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> (Tree.node <$> g v <*> traverse g l <*> traverse g r)))
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (Tree.node v l r))
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g (Tree.node v l r)))

Tactic:
rw [traverse, hl, hr, traverse]

Premises used: Tree.traverse
-- Module: Mathlib.Data.Tree.Traversable
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 β
v : α
l r : Tree α
hl :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l))
hr :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
node :
  Eq (α := Functor.Comp G F (Tree γ))
    (Functor.Comp.mk
      ((fun (a : β) (x x_1 : Tree β) ↦ Tree.node <$> f a <*> traverse f x <*> traverse f x_1) <$> g v <*>
          traverse g l <*>
        traverse g r))
    (Functor.Comp.mk
      ((fun (a : β) (x x_1 : Tree β) ↦ traverse f (Tree.node a x x_1)) <$> g v <*> traverse g l <*> traverse g r))
⊢ Eq (α := Functor.Comp G F (Tree γ))
    (Tree.node <$> (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) v <*>
        Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> (Tree.node <$> g v <*> traverse g l <*> traverse g r)))

Tactic:
simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]

Premises used: Function.comp_def, Function.comp_apply, Functor.map_map, Comp.seq_mk, seq_map_assoc, Functor.Comp.map_mk, map_seq
-- Module: Mathlib.Data.Tree.Traversable
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 β
v : α
l r : Tree α
hl :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l))
hr :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
⊢ Eq (α := Functor.Comp G F (Tree γ))
    (Functor.Comp.mk
      ((fun (a : β) (x x_1 : Tree β) ↦ node <$> f a <*> traverse f x <*> traverse f x_1) <$> g v <*> traverse g l <*>
        traverse g r))
    (Functor.Comp.mk
      ((fun (a : β) (x x_1 : Tree β) ↦ traverse f (node a x x_1)) <$> g v <*> traverse g l <*> traverse g r))

Tactic:
rfl
-- Module: Mathlib.Data.Tree.Traversable
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 β
t : Tree α
nil :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) Tree.nil)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g Tree.nil))
node :
  ∀ (v : α) (l r : Tree α)
    (hl :
      Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
        (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l)))
    (hr :
      Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
        (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))),
    Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (Tree.node v l r))
      (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g (Tree.node v l r)))
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) t)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g t))

Tactic:
induction t with
  | nil => rw [traverse, traverse, map_pure, traverse]; rfl
  | node v l r hl hr =>
    rw [traverse, hl, hr, traverse]
    simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]
    rfl

Premises used: Tree.node, Tree.nil, Function.comp_def, Function.comp_apply, LawfulApplicative.map_pure, Functor.map_map, Tree.traverse, Comp.seq_mk, seq_map_assoc, Functor.Comp.map_mk, map_seq
-- Module: Mathlib.Data.Tree.Traversable
Goal:
α : Type u_1
β : Type u_2
f : α → β
nil : Eq (α := Id (Tree β)) (pure Tree.nil) (pure (map f Tree.nil))
nil₁ nil₂ : Eq.{u_2 + 1} (α := Id (Tree β)) (pure Tree.nil) (pure Tree.nil)
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) Tree.nil) (pure (map f Tree.nil))

Tactic:
rw [traverse, map]

Premises used: Tree.map, Tree.traverse