awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
ne0 : p.length (r := r) ≠ 0
len : p.eraseLast (r := r).length (r := r) = d
h : p = p.eraseLast (r := r).snoc (r := r) (p.last (r := r)) ⋯
⊢ motive p

Tactic:
convert! snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)

Premises used: RelSeries.last, RelSeries.eraseLast, RelSeries.eraseLast_last_rel_last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
ne0 : p.length (r := r) ≠ 0
len : p.eraseLast (r := r).length (r := r) = d
⊢ p = p.eraseLast (r := r).snoc (r := r) (p.last (r := r)) ⋯

Tactic:
(p.snoc_self_eraseLast ne0).symm

Premises used: Eq.symm, RelSeries.snoc_self_eraseLast
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
d : ℕ
hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p
p : RelSeries r
heq : p.length (r := r) = d + 1
ne0 : p.length (r := r) ≠ 0
len : p.eraseLast (r := r).length (r := r) = d
⊢ p = p.eraseLast (r := r).snoc (r := r) (p.last (r := r)) ⋯

Tactic:
exact (p.snoc_self_eraseLast ne0).symm

Premises used: Eq.symm, RelSeries.snoc_self_eraseLast
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
n : ℕ
heq : p.length (r := r) = n
zero : (p : RelSeries r) → (heq : p.length (r := r) = 0) → motive p
succ :
  (d : ℕ) →
    (hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p) →
      (p : RelSeries r) → (heq : p.length (r := r) = d + 1) → motive p
⊢ motive p

Tactic:
induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      · simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have ne0 : p.length ≠ 0 := by simp [heq]
      have len : p.eraseLast.length = d := by simp [heq]
      convert! snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)
      exact (p.snoc_self_eraseLast ne0).symm

Premises used: RelSeries.apply_zero, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
let : motive p
⊢ motive p

Tactic:
let this {n : ℕ} (heq : p.length = n) : motive p := by
    induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      · simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have ne0 : p.length ≠ 0 := by simp [heq]
      have len : p.eraseLast.length = d := by simp [heq]
      convert! snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)
      exact (p.snoc_self_eraseLast ne0).symm
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last (r := r), x) ∈ r) → (hp : motive p) → motive (p.snoc (r := r) x hx)
p : RelSeries r
this : {n : ℕ} → (heq : p.length (r := r) = n) → motive p :=
  fun {n : ℕ} (heq : p.length (r := r) = n) ↦
    Nat.recAux (motive := fun {n : ℕ} ↦ (p : RelSeries r) → (heq : p.length (r := r) = n) → motive p)
      (fun (p : RelSeries r) (heq : p.length (r := r) = 0) ↦
        Eq.mpr (β := motive (RelSeries.singleton r (p.head (r := r)))) ⋯ (singleton (p.head (r := r))))
      (fun (d : ℕ) (hd : (p : RelSeries r) → (heq : p.length (r := r) = d) → motive p) (p : RelSeries r)
          (heq : p.length (r := r) = d + 1) ↦
        have ne0 : p.length (r := r) ≠ 0 := ⋯;
        have len : p.eraseLast (r := r).length (r := r) = d := ⋯;
        Eq.mpr ⋯ (snoc (p.eraseLast (r := r)) (p.last (r := r)) ⋯ (hd (p.eraseLast (r := r)) len)))
      n p heq
⊢ motive p

Tactic:
exact this rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
left :
  ∀ (i : Fin (p.length (r := r))),
    Membership.mem (α := α × α) r
      ((Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
            (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castSucc (Fin.castAdd (q.length (r := r)) i)),
          Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
            (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.succ (Fin.castAdd (q.length (r := r)) i))) :
        α × α)
right :
  ∀ (i : Fin (q.length (r := r))),
    Membership.mem (α := α × α) r
      ((Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
            (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castSucc (Fin.natAdd (p.length (r := r)) i)),
          Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
            (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.succ (Fin.natAdd (p.length (r := r)) i))) :
        α × α)
⊢ ∀ (i : Fin (p.length (r := r) + q.length (r := r))),
    Membership.mem (α := α × α) r
      ((Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
            (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) i.castSucc,
          Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
            (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) i.succ) :
        α × α)

Tactic:
apply Fin.addCases
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
left :
  Membership.mem (α := α × α) r
    (((p.toFun (r := r) ∘ Fin.castSucc) i,
        Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
          (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
          (if h : i.succ = Fin.last (p.length (r := r)) then Fin.natAdd (p.length (r := r)) 0
          else Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ) + 1, ⋯⟩)) :
      α × α)
⊢ Membership.mem (α := α × α) r
    ((Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
          (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castSucc (Fin.castAdd (q.length (r := r)) i)),
        Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
          (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.succ (Fin.castAdd (q.length (r := r)) i))) :
      α × α)

Tactic:
simp_rw [Fin.castSucc_castAdd, Fin.addCases_left, Fin.succ_castAdd]

Premises used: Fin.addCases_left, Fin.castSucc_castAdd, Fin.succ_castAdd
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
⊢ (p.toFun (r := r) i.castSucc, p.toFun (r := r) i.succ) ∈ r

Tactic:
p.step i

Premises used: RelSeries.step
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
h :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
      (if h : i.succ = Fin.last (p.length (r := r)) then Fin.natAdd (p.length (r := r)) 0
      else Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ) + 1, ⋯⟩) =
    p.toFun (r := r) i.succ
⊢ Membership.mem (α := α × α) r
    (((p.toFun (r := r) ∘ Fin.castSucc) i,
        Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
          (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
          (if h : i.succ = Fin.last (p.length (r := r)) then Fin.natAdd (p.length (r := r)) 0
          else Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ) + 1, ⋯⟩)) :
      α × α)

Tactic:
convert! p.step i

Premises used: RelSeries.step
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
pos :
  ∀ (h : i.succ = Fin.last (p.length (r := r))),
    Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
        (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r)) 0) =
      p.toFun (r := r) i.succ
neg :
  ∀ (h : ¬i.succ = Fin.last (p.length (r := r))),
    Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
        (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ) + 1, ⋯⟩) =
      p.toFun (r := r) i.succ
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
      (if h : i.succ = Fin.last (p.length (r := r)) then Fin.natAdd (p.length (r := r)) 0
      else Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ) + 1, ⋯⟩) =
    p.toFun (r := r) i.succ

Tactic:
split_ifs with h
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
h : i.succ = Fin.last (p.length (r := r))
pos : q.toFun (r := r) 0 = p.toFun (r := r) i.succ
pos₁ : q.toFun (r := r) 0 = p.toFun (r := r) (Fin.last (p.length (r := r)))
pos₂ : q.toFun (r := r) 0 = p.last (r := r)
pos₃ : q.toFun (r := r) 0 = q.head (r := r)
pos₄ pos₅ : q.toFun (r := r) 0 = q.toFun (r := r) 0
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r)) 0) =
    p.toFun (r := r) i.succ

Tactic:
rw [Fin.addCases_right, h, ← last, connect, head]

Premises used: RelSeries.last, Fin.addCases_right, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
h : ¬i.succ = Fin.last (p.length (r := r))
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castAdd (q.length (r := r) + 1) ⟨(↑i : ℕ) + 1, ⋯⟩) =
    p.toFun (r := r) i.succ

Tactic:
apply Fin.addCases_left

Premises used: Fin.addCases_left
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last (r := r) = q.head (r := r)
i : Fin (q.length (r := r))
⊢ Membership.mem (α := α × α) r
    ((Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
          (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castSucc (Fin.natAdd (p.length (r := r)) i)),
        Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
          (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.succ (Fin.natAdd (p.length (r := r)) i))) :
      α × α)

Tactic:
simpa only [Fin.castSucc_natAdd, Fin.succ_natAdd, Fin.addCases_right] using q.step i

Premises used: Fin.succ_natAdd, Fin.addCases_right, RelSeries.step, Fin.castSucc_natAdd
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r) + 1)
⊢ p.length (r := r) + 1 ≤ (p.smash (r := r) q h).length (r := r) + 1

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r) + 1)
x : Fin (p.length (r := r))
dsimp :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castLE ⋯ x.castSucc) =
    p.toFun (r := r) x.castSucc
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.castLE ⋯ x.castSucc) = p.toFun (r := r) x.castSucc

Tactic:
dsimp only [smash]

Premises used: RelSeries.smash
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r) + 1)
x : Fin (p.length (r := r))
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.castLE ⋯ x.castSucc) =
    p.toFun (r := r) x.castSucc

Tactic:
apply Fin.addCases_left

Premises used: Fin.addCases_left
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r) + 1)
refine :
  (p.smash (r := r) q h).toFun (r := r) (Fin.castLE ⋯ (Fin.last (p.length (r := r)))) =
    p.toFun (r := r) (Fin.last (p.length (r := r)))
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.castLE ⋯ i) = p.toFun (r := r) i

Tactic:
refine i.lastCases ?_ fun _ ↦ by dsimp only [smash]; apply Fin.addCases_left
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r) + 1)
change :
  (p.smash (r := r) q h).toFun (r := r) (Fin.natAdd (p.length (r := r)) 0) =
    p.toFun (r := r) (Fin.last (p.length (r := r)))
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.castLE ⋯ (Fin.last (p.length (r := r)))) =
    p.toFun (r := r) (Fin.last (p.length (r := r)))

Tactic:
change p.smash q h (Fin.natAdd p.length (0 : Fin (q.length + 1))) = _

Premises used: Fin.natAdd, RelSeries.length, RelSeries.smash, RelSeries.toFun, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r) + 1)
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.natAdd (p.length (r := r)) 0) =
    p.toFun (r := r) (Fin.last (p.length (r := r)))

Tactic:
simpa only [smash, Fin.addCases_right] using h.symm

Premises used: RelSeries.smash, Fin.addCases_right, Eq.symm
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.castSucc (Fin.castAdd (q.length (r := r)) i)) = p.toFun (r := r) i.castSucc

Tactic:
smash_castLE h i.castSucc

Premises used: RelSeries.smash_castLE, Fin.castSucc
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (p.length (r := r))
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.succ (Fin.castAdd (q.length (r := r)) i)) = p.toFun (r := r) i.succ

Tactic:
smash_castLE h i.succ

Premises used: Fin.succ, RelSeries.smash_castLE
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (q.length (r := r))
dsimp :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r)) i.castSucc) =
    q.toFun (r := r) i.castSucc
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.castSucc (Fin.natAdd (p.length (r := r)) i)) = q.toFun (r := r) i.castSucc

Tactic:
dsimp only [smash, Fin.castSucc_natAdd]

Premises used: RelSeries.smash, Fin.castSucc_natAdd
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (q.length (r := r))
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r)) i.castSucc) =
    q.toFun (r := r) i.castSucc

Tactic:
apply Fin.addCases_right

Premises used: Fin.addCases_right
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (q.length (r := r))
dsimp :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r)) i.succ) =
    q.toFun (r := r) i.succ
⊢ (p.smash (r := r) q h).toFun (r := r) (Fin.succ (Fin.natAdd (p.length (r := r)) i)) = q.toFun (r := r) i.succ

Tactic:
dsimp only [smash, Fin.succ_natAdd]

Premises used: Fin.succ_natAdd, RelSeries.smash
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
i : Fin (q.length (r := r))
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.natAdd (p.length (r := r)) i.succ) =
    q.toFun (r := r) i.succ

Tactic:
apply Fin.addCases_right

Premises used: Fin.addCases_right
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
zero :
  ∀ (toFun : Fin (HAdd.hAdd (α := ℕ) 0 1) → α) (step : ∀ (i : Fin 0), (toFun i.castSucc, toFun i.succ) ∈ r)
    (h : (mk (r := r) 0 toFun step).last (r := r) = q.head (r := r)),
    ((mk (r := r) 0 toFun step).smash (r := r) q h).head (r := r) = (mk (r := r) 0 toFun step).head (r := r)
succ :
  ∀ (n : ℕ) (toFun : Fin (n + 1 + 1) → α) (step : ∀ (i : Fin (n + 1)), (toFun i.castSucc, toFun i.succ) ∈ r)
    (h : (mk (r := r) (n + 1) toFun step).last (r := r) = q.head (r := r)),
    ((mk (r := r) (n + 1) toFun step).smash (r := r) q h).head (r := r) = (mk (r := r) (n + 1) toFun step).head (r := r)
⊢ (p.smash (r := r) q h).head (r := r) = p.head (r := r)

Tactic:
obtain ⟨_ | _, _⟩ := p
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
q : RelSeries r
toFun : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
step : ∀ (i : Fin 0), (toFun i.castSucc, toFun i.succ) ∈ r
h : (mk (r := r) 0 toFun step).last (r := r) = q.head (r := r)
⊢ ((mk (r := r) 0 toFun step).smash (r := r) q h).head (r := r) = (mk (r := r) 0 toFun step).head (r := r)

Tactic:
simpa [Fin.addCases] using h.symm

Premises used: Eq.symm
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
q : RelSeries r
n : ℕ
toFun : Fin (n + 1 + 1) → α
step : ∀ (i : Fin (n + 1)), (toFun i.castSucc, toFun i.succ) ∈ r
h : (mk (r := r) (n + 1) toFun step).last (r := r) = q.head (r := r)
succ :
  Fin.addCases (motive := fun (x : Fin (n + 1 + (q.length (r := r) + 1))) ↦ α) (toFun ∘ Fin.castSucc) (q.toFun (r := r))
      0 =
    toFun 0
⊢ ((mk (r := r) (n + 1) toFun step).smash (r := r) q h).head (r := r) = (mk (r := r) (n + 1) toFun step).head (r := r)

Tactic:
dsimp only [smash, head]

Premises used: RelSeries.smash, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
q : RelSeries r
n : ℕ
toFun : Fin (n + 1 + 1) → α
step : ∀ (i : Fin (n + 1)), (toFun i.castSucc, toFun i.succ) ∈ r
h : (mk (r := r) (n + 1) toFun step).last (r := r) = q.head (r := r)
⊢ Fin.addCases (motive := fun (x : Fin (n + 1 + (q.length (r := r) + 1))) ↦ α) (toFun ∘ Fin.castSucc) (q.toFun (r := r))
      0 =
    toFun 0

Tactic:
Fin.addCases_left 0

Premises used: Fin.addCases_left, Fin.ofNat, Nat.mod, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
q : RelSeries r
n : ℕ
toFun : Fin (n + 1 + 1) → α
step : ∀ (i : Fin (n + 1)), (toFun i.castSucc, toFun i.succ) ∈ r
h : (mk (r := r) (n + 1) toFun step).last (r := r) = q.head (r := r)
⊢ Fin.addCases (motive := fun (x : Fin (n + 1 + (q.length (r := r) + 1))) ↦ α) (toFun ∘ Fin.castSucc) (q.toFun (r := r))
      0 =
    toFun 0

Tactic:
exact Fin.addCases_left 0

Premises used: Fin.addCases_left, OfNat.ofNat
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
dsimp :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.last (p.length (r := r) + q.length (r := r))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))
⊢ (p.smash (r := r) q h).last (r := r) = q.last (r := r)

Tactic:
dsimp only [smash, last]

Premises used: RelSeries.last, RelSeries.smash
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last (r := r) = q.head (r := r)
rw :
  Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r))
      (Fin.natAdd (p.length (r := r)) (Fin.last (q.length (r := r)))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))
rw₁ rw₂ : q.toFun (r := r) (Fin.last (q.length (r := r))) = q.toFun (r := r) (Fin.last (q.length (r := r)))
⊢ Fin.addCases (motive := fun (x : Fin (p.length (r := r) + (q.length (r := r) + 1))) ↦ α)
      (p.toFun (r := r) ∘ Fin.castSucc) (q.toFun (r := r)) (Fin.last (p.length (r := r) + q.length (r := r))) =
    q.toFun (r := r) (Fin.last (q.length (r := r)))

Tactic:
rw [← Fin.natAdd_last, Fin.addCases_right]

Premises used: Fin.addCases_right, Fin.natAdd_last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r_1 : SetRel α α
β : Type u_2
s : SetRel β β
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
x : Fin ((↑i : ℕ) + 1)
j : ℕ
h : j < (↑i : ℕ) + 1
⊢ j < p.length (r := r) + 1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r_1 : SetRel α α
β : Type u_2
s : SetRel β β
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
x : Fin (↑i : ℕ)
j : ℕ
h : j < (↑i : ℕ)
⊢ j < p.length (r := r)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ (p.take (r := r) i).head (r := r) = p.head (r := r)

Tactic:
simp [take, head]

Premises used: RelSeries.take, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length (r := r) + 1)
⊢ (p.take (r := r) i).last (r := r) = p.toFun (r := r) i

Tactic:
simp [take, last, Fin.last]

Premises used: RelSeries.last, RelSeries.take, Fin.last
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r) + 1)
x : Fin (p.length (r := r) - (↑i : ℕ) + 1)
j : ℕ
h : j < p.length (r := r) - (↑i : ℕ) + 1
⊢ j + (↑i : ℕ) < p.length (r := r) + 1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin (p.length (r := r) + 1)
x : Fin (p.length (r := r) - (↑i : ℕ))
j : ℕ
h : j < p.length (r := r) - (↑i : ℕ)
⊢ j + (↑i : ℕ) < p.length (r := r)

Tactic:
lia