mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : List α
⊢ ¬Shortlex r s []

Tactic:
simp [shortlex_def]

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
⊢ Acc (Shortlex r) p

Tactic:
· cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ ([].reverse ++ a :: l) :: splitBy r [] = [a :: (l ++ [])]

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons.h
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ IsChain (fun x y ↦ r x y = true) ([].reverse ++ a :: l)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons.ha
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ ∀ (x : α), x ∈ [].head? → r ((a :: l).getLast ⋯) x = false

Tactic:
simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
i : m
j : n
⊢ a i j = 0 i j

Tactic:
replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
inhabited_h : Inhabited l
i : m
j : n
h : (mulRightLinearMap l R a) (Matrix.single default i 1) = 0 (Matrix.single default i 1)
⊢ a i j = 0 i j
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q w

Tactic:
convert_to take q (drop q w) = take q (drop q w ++ z)

Goal state after:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q w = take q (drop q w ++ z)

α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q (drop q w) = take q (drop q w ++ z)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ w = take q w ++ drop q w

Tactic:
take_append_drop q w

Goal state after:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ w = w
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ x ∈ s.toFinset, (count x s + 1 - 0) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
tsub_zero

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
m k : ℕ
hn_fac : IsUnit ↑(m + k)!
hmn : m ≤ m + k
⊢ IsUnit ↑m !

Tactic:
clear hmn

Goal state after:
A : Type u_1
inst✝ : Semiring A
m k : ℕ
hn_fac : IsUnit ↑(m + k)!
⊢ IsUnit ↑m !
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
zeckendorf_of_pos h,

Goal state after:
case inr
n a : ℕ
ha :
  a ∈
    ((n + 1 - fib (n + 1).greatestFib).greatestFib ::
          (n + 1 - fib (n + 1).greatestFib - fib (n + 1 - fib (n + 1).greatestFib).greatestFib).zeckendorf ++
        [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
h : p 0
⊢ nth p 0 = 0

Tactic:
by simp [nth_zero, h]

Goal state after:
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

pp: case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

Tactic:
swap

Goal state after:
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
dsimp [delta, ratio] at lr₁ mr₁

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m < ↑n ↔ m < n

Tactic:
rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (Num.ofNat' n).succ.toZNum = (Num.ofNat' n).toZNum + 1

Tactic:
Num.toZNum_succ,

Goal state after:
α : Type u_1
n : ℕ
⊢ (Num.ofNat' n).toZNum.succ = (Num.ofNat' n).toZNum + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n).succ.toZNum = ↑(n + 1)

Tactic:
Num.toZNum_succ,

Goal state after:
n : ℕ
⊢ (↑n).toZNum.succ = ↑(n + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : F.M
⊢ Agree' n x x

Tactic:
induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_

Goal state after:
case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x

case succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
x : F.M
⊢ Agree' (n✝ + 1) x x
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (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 (rs + size_1 + 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).dual =
    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 (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual

pp: case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)

Tactic:
swap

Goal state after:
case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)

case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (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 (rs + size_1 + 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).dual =
    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 (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x = y

Tactic:
apply ext'; intro i
  induction i with
  | zero => subsingleton
  | succ i i_ih =>
    apply ext_aux x y x
    · rw [← agree_iff_agree']
      apply x.consistent
    · rw [← agree_iff_agree', i_ih]
      apply y.consistent
    introv H'
    dsimp only [iselect] at H
    cases H'
    apply H ps

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

Goal state before:
pp: 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
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)

Tactic:
rw [M.dest_map]; congr
  apply eq_of_drop_last_eq (by simp)
  simp only [lastFun_appendFun]
  ext1; apply h

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ P.WPath (WType.mk a f) ⟹ α

Tactic:
by
  intro i x
  match x with
  | WPath.root _ _ i c => exact g' i c
  | WPath.child _ _ i j c => exact g j i c

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
⊢ Valid' o₁
      ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).2)
      o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).1
          (rl.findMin' rx, (Ordnode.node ?neg.s✝ rl rx rr).eraseMin).2).size =
      ls + rs

pp: case neg.s
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
⊢ ℕ

Tactic:
· obtain ⟨v, e⟩ := Valid'.eraseMin_aux hr
      suffices H : _ by
        refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩
        · refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil
          exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)
        · exact
            @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)
        · rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl
      refine Or.inr ⟨_, Or.inr e, ?_⟩
      rwa [hr.2.eq_node'] at bal

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

Goal state before:
pp: case right.right.right.left
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
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = x * ↑b' + 1

Tactic:
mul_coe,

Goal state after:
case right.right.right.left
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
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' = x * ↑b' + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.right.left
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
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(w * b') = y * ↑a' + 1

Tactic:
mul_coe,

Goal state after:
case right.right.right.right.left
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
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑w * ↑b' = y * ↑a' + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
⊢ All (fun y ↦ All (fun z ↦ y < z) t₂) t₁

Tactic:
refine h₁.mem_lt.imp fun y yx => ?_
  exact h₂.mem_gt.imp fun z xz => lt_trans yx xz

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

Goal state before:
pp: case sz
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Sized

pp: case node.bal
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Balanced

Tactic:
· constructor
      · rw [t_l_size, t_r_size]; exact h.sz.1
      · constructor
        · exact t_l_valid.sz
        · exact t_r_valid.sz

Goal state after:
case node.bal
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Balanced
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(Pi.P F) α), Pi.abs F (f <$$> p) = f <$$> Pi.abs F p

Tactic:
rintro α β f ⟨x, g⟩; simp only [Pi.abs, (· <$$> ·), ← abs_map]; rfl

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 : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (x : Fix F α), (recF g ∘ fixToW) x = rec g x

Tactic:
apply Quotient.ind

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (a : (P F).W α), (recF g ∘ fixToW) ⟦a⟧ = rec g ⟦a⟧
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h₀
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
i : Fin2 n
x : (α ::: ι).drop i
⊢ subtypeVal α.repeatEq i (diagSub i x) = prod.diag i x

Tactic:
induction i with
      | fz => rfl
      | fs _ ih =>
        apply ih

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
rw [i1, i2]

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_1
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝² : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : S s✝ t✝
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h✝ : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ s = flatten (Computation.pure s)

Tactic:
simp [h]

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝² : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : S s✝ t✝
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h✝ : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ t = flatten (Computation.pure t)

Tactic:
simp [h]

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

Goal state before:
pp: case refine_3
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝² : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : S s✝ t✝
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h✝ : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRel R) (Computation.pure s) (Computation.pure t)

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h

Goal state after:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
o : Option α
om : o ∈ ⟨g, al⟩
oe : Option.map f o = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b