awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : β
⊢ map₂ f a (some b) = Option.map (fun (a : α) ↦ f a b) a

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : γ
⊢ c ∈ map₂ f a b ↔ ∃ (a' : α), ∃ (b' : β), a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : γ
⊢ map₂ f a b = some c ↔ ∃ (a' : α), ∃ (b' : β), a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = none ↔ a = none ∨ b = none

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = map₂ (fun (a : β) (b : α) ↦ f b a) b a

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f a b) = map₂ (fun (a : α) (b : β) ↦ g (f a b)) a b

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : γ → β → δ
g : α → γ
⊢ map₂ f (Option.map g a) b = map₂ (fun (a : α) (b : β) ↦ f (g a) b) a b

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → γ → δ
g : β → γ
⊢ map₂ f a (Option.map g b) = map₂ (fun (a : α) (b : β) ↦ f a (g b)) a b

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
a : Option α
b : Option β
⊢ map₂ (curry f) a b = Option.map f (map₂ Prod.mk a b)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x : Option (α × β)
⊢ Option.map (uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
ε : Type u_8
ε' : Type u_9
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f a b = map₂ g b a

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ a) (Option.map g₂ b)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' a) b

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ Option.map g (map₂ f a b) = map₂ f' a (Option.map g' b)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' a b)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' a b)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ b) (Option.map g₂ a)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' b) a

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f a b) = map₂ f' b (Option.map g' a)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' b a)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' b a)

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
o : Option β
⊢ map₂ f (some a) o = o

Tactic:
grind
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
o : Option α
⊢ map₂ f o (some b) = o

Tactic:
grind
-- Module: Mathlib.Data.Ordering.Basic
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ lt.Compares a b = (a < b)

Tactic:
rfl

Premises used: Ordering.Compares, rfl
-- Module: Mathlib.Data.Ordering.Basic
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ eq.Compares a b = (a = b)

Tactic:
rfl

Premises used: Ordering.Compares, rfl
-- Module: Mathlib.Data.Ordering.Basic
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ gt.Compares a b = (a > b)

Tactic:
rfl

Premises used: Ordering.Compares, rfl
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
pos : c → ((if c then a else b) = lt) = if c then a = lt else b = lt
neg : ¬c → ((if c then a else b) = lt) = if c then a = lt else b = lt
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
by_cases c
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
simp [*]
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
simp [*]
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
pos : c → ((if c then a else b) = eq) = if c then a = eq else b = eq
neg : ¬c → ((if c then a else b) = eq) = if c then a = eq else b = eq
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
by_cases c
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
simp [*]
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
simp [*]
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
pos : c → ((if c then a else b) = gt) = if c then a = gt else b = gt
neg : ¬c → ((if c then a else b) = gt) = if c then a = gt else b = gt
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
by_cases c
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
simp [*]
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
c : Prop
inst : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
simp [*]
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
o₁ o₂ : Ordering
lt : (Ordering.lt.dthen fun (x : Ordering.lt = Ordering.eq) ↦ o₂) = Ordering.lt.then o₂
eq : (Ordering.eq.dthen fun (x : Ordering.eq = Ordering.eq) ↦ o₂) = Ordering.eq.then o₂
gt : (Ordering.gt.dthen fun (x : Ordering.gt = Ordering.eq) ↦ o₂) = Ordering.gt.then o₂
⊢ (o₁.dthen fun (x : o₁ = Ordering.eq) ↦ o₂) = o₁.then o₂

Tactic:
cases o₁
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
o₂ : Ordering
⊢ (lt.dthen fun (x : lt = eq) ↦ o₂) = lt.then o₂

Tactic:
rfl
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
o₂ : Ordering
⊢ (eq.dthen fun (x : eq = eq) ↦ o₂) = eq.then o₂

Tactic:
rfl
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
o₂ : Ordering
⊢ (gt.dthen fun (x : gt = eq) ↦ o₂) = gt.then o₂

Tactic:
rfl
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
α : Type u
lt : α → α → Prop
inst : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.lt) = lt a b

Tactic:
simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right, and_true, reduceCtorEq]

Premises used: reduceCtorEq, and_true, ite_self, cmpUsing, if_false_right, Ordering.ite_eq_lt_distrib
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
α : Type u
lt : α → α → Prop
inst : DecidableRel lt
inst_1 : IsStrictOrder α lt
a b : α
simp : lt b a → ¬lt a b
⊢ cmpUsing lt a b = Ordering.gt ↔ lt b a

Tactic:
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left,
    and_iff_right_iff_imp, reduceCtorEq]

Premises used: reduceCtorEq, and_true, cmpUsing, Ordering.ite_eq_gt_distrib, and_iff_right_iff_imp, if_false_left, if_false_right
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
α : Type u
lt : α → α → Prop
inst : DecidableRel lt
inst_1 : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b

Tactic:
fun hba hab ↦ (irrefl a) (_root_.trans hab hba)

Premises used: trans, irrefl, Not
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
α : Type u
lt : α → α → Prop
inst : DecidableRel lt
inst_1 : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b

Tactic:
exact fun hba hab ↦ (irrefl a) (_root_.trans hab hba)

Premises used: trans, irrefl
-- Module: Mathlib.Data.Ordering.Lemmas
Goal:
α : Type u
lt : α → α → Prop
inst : DecidableRel lt
a b : α
⊢ cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a

Tactic:
simp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
s : ℕ
H : 1 ≤ s
⊢ ¬s ≤ delta * 0

Tactic:
not_le_of_gt H

Premises used: not_le_of_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 0 < delta

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 1 ≤ delta * delta

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)

Tactic:
simpa [mul_assoc] using Nat.mul_le_mul_right a (by decide : 1 ≤ delta * delta)

Premises used: Nat.mul_le_mul_right, mul_assoc
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.node' x r).Sized

Tactic:
⟨rfl, hl, hr⟩

Premises used: Ordnode.Sized, And.intro, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
rw rw₁ : node (l.size + r.size + 1) l x r = l.node' x r
⊢ node s l x r = l.node' x r

Tactic:
rw [h.1]

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
H : (node s l x r).Sized
⊢ (node s l x r).size = l.size + r.size + 1

Tactic:
H.1

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
hl : Sized.{u_1} (α := α) nil
⊢ C nil

Tactic:
H0
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
hl : Sized.{u_1} (α := α) nil
⊢ C nil

Tactic:
exact H0
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
t_ih_l : ∀ (hl : l.Sized), C l
t_ih_r : ∀ (hl : r.Sized), C r
hl : (Ordnode.node size l x r).Sized
node : C (l.node' x r)
⊢ C (Ordnode.node size l x r)

Tactic:
rw [hl.eq_node']

Premises used: Ordnode.Sized.eq_node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
t_ih_l : ∀ (hl : l.Sized), C l
t_ih_r : ∀ (hl : r.Sized), C r
hl : (node size l x r).Sized
⊢ C (l.node' x r)

Tactic:
H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
t_ih_l : ∀ (hl : l.Sized), C l
t_ih_r : ∀ (hl : r.Sized), C r
hl : (node size l x r).Sized
⊢ C (l.node' x r)

Tactic:
exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
hl : t.Sized
C : Ordnode α → Prop
H0 : C Ordnode.nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
nil : ∀ (hl : Sized.{u_1} (α := α) Ordnode.nil), C Ordnode.nil
node :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (t_ih_l : ∀ (hl : l.Sized), C l) (t_ih_r : ∀ (hl : r.Sized), C r)
    (hl : (Ordnode.node size l x r).Sized), C (Ordnode.node size l x r)
⊢ C t

Tactic:
induction t with
  | nil => exact H0
  | node _ _ _ _ t_ih_l t_ih_r =>
    rw [hl.eq_node']
    exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

Premises used: Ordnode.node, Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
rw : l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize
⊢ (node s l x r).size = (node s l x r).realSize

Tactic:
rw [size, h₁, size_eq_realSize h₂, size_eq_realSize h₃]

Premises used: Ordnode.size
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
ht : t.Sized
nil :
  ∀ (ht : Sized.{u_1} (α := α) Ordnode.nil),
    size.{u_1} (α := α) Ordnode.nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) Ordnode.nil Ordnode.nil
node :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (ht : (Ordnode.node size l x r).Sized),
    (Ordnode.node size l x r).size = 0 ↔ Ordnode.node size l x r = Ordnode.nil
⊢ t.size = 0 ↔ t = Ordnode.nil

Tactic:
cases t
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
ht : Sized.{u_1} (α := α) nil
⊢ size.{u_1} (α := α) nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) nil nil

Tactic:
simp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
ht : (node size l x r).Sized
⊢ (node size l x r).size = 0 ↔ node size l x r = nil

Tactic:
simp [ht.1]

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
ht : t.Sized
nil :
  ∀ (ht : Sized.{u_1} (α := α) Ordnode.nil),
    size.{u_1} (α := α) Ordnode.nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) Ordnode.nil Ordnode.nil
node :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (ht : (Ordnode.node size l x r).Sized),
    (Ordnode.node size l x r).size = 0 ↔ Ordnode.node size l x r = Ordnode.nil
nil₁ :
  ∀ (ht : Sized.{u_1} (α := α) Ordnode.nil),
    size.{u_1} (α := α) Ordnode.nil = 0 ↔ Eq.{u_1 + 1} (α := Ordnode α) Ordnode.nil Ordnode.nil
node₁ :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (ht : (Ordnode.node size l x r).Sized),
    (Ordnode.node size l x r).size = 0 ↔ Ordnode.node size l x r = Ordnode.nil
⊢ t.size = 0 ↔ t = Ordnode.nil

Tactic:
cases t <;> [simp; simp [ht.1]]
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
rw : 0 < l.size + r.size + 1
⊢ 0 < s

Tactic:
rw [h.1]

Premises used: And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < l.size + r.size + 1

Tactic:
apply Nat.le_add_left

Premises used: Nat.le_add_left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
rw : (node s r.dual x l.dual).dual = node s l x r
rw₁ : node s l.dual.dual x r.dual.dual = node s l x r
rw₂ : node s l x r.dual.dual = node s l x r
rw₃ rw₄ : node s l x r = node s l x r
⊢ (node s l x r).dual.dual = node s l x r

Tactic:
rw [dual, dual, dual_dual l, dual_dual r]

Premises used: Ordnode.dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
nil : size.{u_1} (α := α) (dual Ordnode.nil) = size.{u_1} (α := α) Ordnode.nil
node :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α),
    (Ordnode.node size l x r).dual.size = (Ordnode.node size l x r).size
⊢ t.dual.size = t.size

Tactic:
cases t
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
⊢ size.{u_1} (α := α) (dual nil) = size.{u_1} (α := α) nil

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node size l x r).dual.size = (node size l x r).size

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r : ℕ
rw : r + l ≤ 1 → r + l ≤ 1
⊢ l + r ≤ 1 → r + l ≤ 1

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r : ℕ
⊢ r + l ≤ 1 → r + l ≤ 1

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r : ℕ
⊢ r + l ≤ 1 → r + l ≤ 1

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l : ℕ
⊢ BalancedSz l 0 ↔ l ≤ 1

Tactic:
simp +contextual [BalancedSz]

Premises used: Ordnode.BalancedSz
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂

Tactic:
or_iff_not_imp_left.2 fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left, Ordnode.BalancedSz
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
refine : ∀ (h : ¬l + r₂ ≤ 1), l ≤ delta * r₂ ∧ r₂ ≤ delta * l
⊢ BalancedSz l r₂

Tactic:
refine or_iff_not_imp_left.2 fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l

Tactic:
⟨?_, h₂.resolve_left h⟩

Premises used: Or.resolve_left, And.intro
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
refine : l ≤ delta * r₂
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l

Tactic:
refine ⟨?_, h₂.resolve_left h⟩
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l + r₁ ≤ 1
inl : ∀ (h₁ : r₁ ≤ 0) (h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l) (h : ¬l + 0 ≤ 1), l ≤ delta * 0
inl₁ :
  ∀ (n : ℕ) (h₁ : r₁ ≤ n + 1) (h₂ : l + (n + 1) ≤ 1 ∨ n + 1 ≤ delta * l) (h : ¬l + (n + 1) ≤ 1), l ≤ delta * (n + 1)
⊢ l ≤ delta * r₂

Tactic:
cases r₂
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ : ℕ
H : l + r₁ ≤ 1
h₁ : r₁ ≤ 0
h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l
h : ¬l + 0 ≤ 1
⊢ l ≤ delta * 0

Tactic:
cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)

Premises used: Nat.zero_le, Nat.add_le_add_left, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ : ℕ
H : l + r₁ ≤ 1
n : ℕ
h₁ : r₁ ≤ n + 1
h₂ : l + (n + 1) ≤ 1 ∨ n + 1 ≤ delta * l
h : ¬l + (n + 1) ≤ 1
⊢ l ≤ delta * (n + 1)

Tactic:
le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)

Premises used: Nat.le_add_right, Nat.le_add_left, OfNat.ofNat, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ : ℕ
H : l + r₁ ≤ 1
n : ℕ
h₁ : r₁ ≤ n + 1
h₂ : l + (n + 1) ≤ 1 ∨ n + 1 ≤ delta * l
h : ¬l + (n + 1) ≤ 1
⊢ l ≤ delta * (n + 1)

Tactic:
exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)

Premises used: Nat.le_add_right, Nat.le_add_left, OfNat.ofNat, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l
⊢ l ≤ delta * r₂

Tactic:
le_trans H.1 (Nat.mul_le_mul_left _ h₁)

Premises used: Nat.mul_le_mul_left, And.left, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l
⊢ l ≤ delta * r₂

Tactic:
exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

Premises used: Nat.mul_le_mul_left, And.left, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
inl : ∀ (H : l + r₁ ≤ 1), l ≤ delta * r₂
inr : ∀ (H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l), l ≤ delta * r₂
⊢ l ≤ delta * r₂

Tactic:
cases H with
  | inl H =>
    cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
  | inr H =>
    exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

Premises used: Nat.zero_le, Nat.le_add_right, Nat.le_add_left, OfNat.ofNat, Nat.add_le_add_left, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ l ≤ delta * r₁
H : BalancedSz l r₂
⊢ BalancedSz l r₁

Tactic:
have : l + r₂ ≤ 1 → BalancedSz l r₁ := fun H => Or.inl (le_trans (Nat.add_le_add_left h₁ _) H)
  Or.casesOn H this fun H => Or.casesOn h₂ this fun h₂ => Or.inr ⟨h₂, le_trans h₁ H.2⟩

Premises used: Or.casesOn, Or.inl, Nat.add_le_add_left, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
rw : BalancedSz r.size l.size
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
rw [size_dual, size_dual]

Premises used: Ordnode.size_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size

Tactic:
b.symm

Premises used: Ordnode.BalancedSz.symm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size

Tactic:
exact b.symm

Premises used: Ordnode.BalancedSz.symm