mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case pos.h
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ False

Tactic:
apply h

Goal state after:
case pos.h
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
rw [M.dest_eq_dest' _ e₁'] at e₁

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
e₁ : dest' P e₁' f₁ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ (casesOn (id (node rs rl rx rr))
        (casesOn (id l) (Ordnode.singleton x) fun ls ll lx lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 l x nil) fun size l lrx r ↦ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
              else node (ls + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs_1 l_1 x_1 r ↦
        casesOn (id l) (node (rs_1 + 1) nil x (node rs rl rx rr)) fun ls ll lx lr ↦
          if ls > delta * rs_1 then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls + rs_1 + 1) ll lx (node (rs_1 + lrs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs_1 + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx
                    (node (lrr.size + rs_1 + 1) lrr x (node rs rl rx rr))
          else node (ls + rs_1 + 1) l x (node rs rl rx rr)).dual =
    casesOn (id (node rs rl rx rr).dual)
      (casesOn (id l.dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x l.dual) fun size l rlx r ↦ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun ls l_1 x_1 r ↦
      casesOn (id l.dual) (node (ls + 1) (node rs rl rx rr).dual x nil) fun rs_1 rl_1 rx_1 rr_1 ↦
        if rs_1 > delta * ls then
          casesOn (id rr_1) nil fun rrs l x_2 r ↦
            casesOn (id rl_1) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then
                node (ls + rs_1 + 1) (node (ls + rls + 1) (node rs rl rx rr).dual x rl_1) rx_1 rr_1
              else
                node (ls + rs_1 + 1) (node (ls + rll.size + 1) (node rs rl rx rr).dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx_1 rr_1)
        else node (ls + rs_1 + 1) (node rs rl rx rr).dual x l.dual

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l; · rfl
    dsimp only [dual, id]
    split_ifs; swap; · simp [add_comm]
    obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> try rfl
    dsimp only [dual, id]
    split_ifs with h <;> simp [add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x

Tactic:
exact h

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x✝ : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ (match ll.splitMax' lx lr with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x✝ l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))

Tactic:
splitMax_eq ls ll lx lr,

Goal state after:
α : Type u_1
x✝ : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ (match ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x✝ l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
x✝ : (α ::: P.M α).last
⊢ lastFun g x✝ = dropFun g <$$> x✝

Tactic:
apply h

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

Tactic:
replace h₀ := congr_arg Sigma.fst h₀

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : (M.mk ⟨a, f⟩).dest.fst = ⟨a'', g⟩.fst
⊢ a = a'
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ f = M.corec g

Tactic:
by
  ext x
  apply bisim' (fun _ => True) _ _ _ _ trivial
  clear x
  intro x _
  rcases gxeq : g x with ⟨a, f'⟩
  have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
  have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
  refine ⟨_, _, _, h₀, h₁, ?_⟩
  intro i
  exact ⟨f' i, trivial, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n < PNat.find h ↔ ∀ (m : ℕ+), m ≤ n → ¬p m

Tactic:
by
  simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v ↔ m ∣ v.prod
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
exact h

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n ↔ u ≤ n.factorMultiset
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
exact h

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

Tactic:
exact (lt_irrefl a₁ hlt₂).elim

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ (if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
    else
      if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
      else (node ls ll lx lr).node' x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
              if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
              else
                node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        rec nil
          (fun size l x_1 r l_ih r_ih ↦
            rec nil
              (fun size_1 l x_2 r l_ih r_ih ↦
                if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

Tactic:
split_ifs with h h_1
        · have rd : delta ≤ size rl + size rr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
            rwa [sr.1, Nat.lt_succ_iff] at this
          obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
          · rw [size, zero_add] at rd
            exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)
          obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
          · exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)
          dsimp [rotateL]; split_ifs
          · simp [node3L, node', sr.1]; abel
          · simp [node4L, node', sr.1, sr.2.1.1]; abel
        · have ld : delta ≤ size ll + size lr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
            rwa [sl.1, Nat.lt_succ_iff] at this
          obtain - | ⟨lls, lll, llx, llr⟩ := ll
          · rw [size, zero_add] at ld
            exact absurd (le_trans ld (balancedSz_zero.1 hl.1.symm)) (by decide)
          obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
          · exact absurd (le_trans ld (balancedSz_zero.1 hl.1)) (by decide)
          dsimp [rotateR]; split_ifs
          · simp [node3R, node', sl.1]; abel
          · simp [node4R, node', sl.1, sl.2.2.1]; abel
        · simp [node']

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑z * ↑a' = x * ↑b' + 1

Tactic:
rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ x * y + 1 + ↑z * x = x * y + x * ↑z + 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

Tactic:
simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
      image_univ, mem_range, exists_imp]

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' a₁ (erase x nil) a₂ ∧ Raised (erase x nil).size nil.size

Tactic:
simpa [erase, Raised]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type v
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ QPF.abs ⟨a✝¹, f✝¹⟩ = QPF.abs ⟨a✝, f✝⟩

Tactic:
apply h

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ g₁ (mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩))

Tactic:
apply h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ (TypeVec.id ::: g₁) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    (TypeVec.id ::: g₂) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))

Tactic:
apply h

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩ = g₂ <$> abs ⟨a, fun x ↦ ⟦f x⟧⟩
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest

Tactic:
apply h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ r x✝ y✝
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ p (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))

Tactic:
apply h

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ Liftp p (abs ⟨a, fun x ↦ ⟦f x⟧⟩)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ p (mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩))

Tactic:
apply h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ LiftP (α.PredLast p) (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hz]

Goal state after:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ 0⁻¹ = 0
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
⊢ closure (range fun x ↦ x ^ n) = ⊤

Tactic:
by
  refine (eq_top_iff' _).2 fun x ↦ ?_
  suffices x = (x.num * x.den ^ (n - 1)) • (x.den : ℚ≥0)⁻¹ ^ n by
    rw [this]
    exact nsmul_mem (subset_closure <| mem_range_self _) _
  rw [nsmul_eq_mul]
  push_cast
  rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel₀, one_pow, one_mul,
    ← div_eq_mul_inv, num_div_den]
  all_goals simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop (n + 1)).destruct (t.drop (n + 1)).destruct

Tactic:
simp only [drop, destruct_tail]
    apply liftRel_bind
    · apply liftRel_dropn_destruct H n
    exact fun {a b} o =>
      match a, b, o with
      | none, none, _ => by simp
      | some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : (a', s').1 = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
dsimp at i

Goal state after:
case some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s.get? (n + 1) ~ t.get? (n + 1)

Tactic:
apply h

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) (some b))

Tactic:
· obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        exact ⟨h2 r, s, rfl, t, rfl, h⟩

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case intro.inl
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
e : a = x✝
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

pp: case intro.inr
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

Tactic:
· simp [e]

Goal state after:
case intro.inr
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case intro.inr.inl
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
e : a = x✝
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

pp: case intro.inr.inr
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
m : a ∈ s✝.append S.join
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

Tactic:
· simp [e]

Goal state after:
case intro.inr.inr
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
m : a ∈ s✝.append S.join
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i

Tactic:
subst h
    simp

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ ∀ {b : Option (β × WSeq β)},
    b ∈ T.join.destruct →
      ∃ a ∈ S.join.destruct,
        LiftRelO R
          (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
          a b

Tactic:
· intro b mb
          rw [← LiftRelO.swap]
          apply liftRel_join.lem (swap R)
          · rw [← LiftRel.swap R, ← LiftRel.swap]
            apply ST
          · rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
            exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
          · exact mb

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T

Tactic:
rw [← aa] at h

Goal state after:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T