mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y

Tactic:
rintro ⟨b, m⟩ hb ⟨c, n⟩ hc (rfl : b = c)

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ f.graph.toList
n : M
hc : (b, n) ∈ f.graph.toList
⊢ (b, m) = (b, n)
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ a ∈ (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset ↔ (lookup a l).getD 0 ≠ 0

Tactic:
mem_toFinset,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ a ∈ (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys ↔ (lookup a l).getD 0 ≠ 0
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g ↦ F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a✝ ∈ g₁.neLocus g₂

Tactic:
simpa only [mem_neLocus] using! (hF _).ne_iff

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f ↦ F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a✝ ∈ f₁.neLocus f₂

Tactic:
simpa only [mem_neLocus] using! (hF _).ne_iff

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]

Tactic:
by
    refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)
    dsimp [bodd]; cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]
    · change -[2 * Nat.div2 n+1] = _
      rw [zero_add]
    · rw [zero_add, add_comm]
      rfl

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑m >>> ↑i >>> ↑1

Tactic:
← shiftRight_add',

Goal state after:
m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑m >>> (↑i + ↑1)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ l₁ ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k

Tactic:
← rdrop_eq_reverse_drop_reverse

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ l₁ ++ l₂.rdrop k = l₁ ++ l₂.rdrop k
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ map f l.reverse = map f l

Tactic:
p.reverse_eq

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ map f l = map f l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α) {i : ℕ} {hi : i < (tail✝.splitLengths l).length}, (tail✝.splitLengths l)[i].length ≤ tail✝[i]
l : List α
i : ℕ
hi : i < ((head✝ :: tail✝).splitLengths l).length
⊢ ((head✝ :: tail✝).splitLengths l)[i].length ≤ (head✝ :: tail✝)[i]

Tactic:
case cons head tail tail_ih =>
    simp only [splitLengths_cons]
    cases i
    · simp
    · simp only [getElem_cons_succ, tail_ih]

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔ ∀ i < w.length, w[i]? = w[i % p]?

Tactic:
by
  constructor
  · intro per i len
    exact Eq.symm (per.getElem?_mod p i w len)
  · intro mod
    rw [hasPeriod_iff_getElem?]
    intro i less
    rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l✝ : List α
h✝ : m ∈ splitBy r l✝
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
apply isChain_of_mem_splitByLoop _ _ h <;> simp

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

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ ∃ ha hb, r (x.getLast ha) (y.head hb) = false

Tactic:
use ne_nil_of_mem_splitBy (mem_of_mem_getLast? hx), ne_nil_of_mem_splitBy (mem_of_mem_head? hy)

Goal state after:
case h
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ r (x.getLast ⋯) (y.head ⋯) = false
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ ∃ M', X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ ↑n.divisors
⊢ k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
have hdvd := dvd_of_mem_divisors h
    have hk := ne_zero_of_dvd_ne_zero hn hdvd
    exact ⟨_, factorization_le_iff_dvd hk hn |>.mpr hdvd, prod_factorization_pow_eq_self hk⟩

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: k n m : ℕ
⊢ (k * n).dist (k * m) = k * n.dist m

Tactic:
rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]

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

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

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

Tactic:
· simp [← two_mul]

Goal state after:
case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: n : ZNum
⊢ -n.succ = (-n).pred

Tactic:
cases n <;> try { rfl }

Goal state after:
case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ count p (nth p (k + 1)) = k + 1

Tactic:
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]

Goal state after:
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ nth p k ∉ {n ∈ range (nth p k) | p n}
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : 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
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)

Goal state after:
case node.inl
α : 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 : l.size = 0
m1 : (Ordnode.node s ml z mr).size = 1
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

case node.inr
α : 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 ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n

Tactic:
refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)
    exact Set.Finite.toFinset_subset.mpr this

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

Goal state before:
pp: m n : ZNum
x✝ : m ∣ n
k : ZNum
e : n = m * k
⊢ ↑n = ↑m * ↑k

Tactic:
simp [e]

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

Goal state before:
pp: case cons.f
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 → iselect ps_tail x = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ iselect (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩) = default.head

Tactic:
| _ x_a x_f
     => 

Goal state after:
case cons.f
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 → iselect ps_tail x = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ iselect (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩) = default.head
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
introv Hr

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : R x y
⊢ ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateR x r).dual.Sized

Tactic:
rw [dual_rotateR]; exact hr.dual.rotateL hl.dual

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ Valid' o₁ (l.rotateL x r) o₂

Tactic:
exact hl.rotateL hr h h_1 H₁

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

Goal state before:
pp: case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
introv Hr

Goal state after:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList

Tactic:
induction t <;> simp [Any, *]

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

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
simp [h.1]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂

Tactic:
introv Hr

Goal state after:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
⊢ s₁ = s₂
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: ⊢ Repr PrimeMultiset

Tactic:
delta PrimeMultiset; infer_instance

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

Goal state before:
pp: case a.left
m n : ℕ+
⊢ m.gcd n ∣ m

Tactic:
exact gcd_dvd_left m n

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

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ x✝.reduce.IsReduced

Tactic:
reduce_a h

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ u.finish.IsReduced
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ x✝.reduce.IsSpecial

Tactic:
reduce_a h

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ u.finish.IsSpecial
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
by
  rcases H with (rfl | rfl)
  · exact Or.inl rfl
  · exact Or.inr rfl

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

Goal state before:
pp: n : ℕ
i : Fin2 n
α : TypeVec.{?u.11} n
⊢ ∀ {β : TypeVec.{?u.11} n} (f : α ⟹ β) (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p

Tactic:
β

Goal state after:
n : ℕ
i : Fin2 n
α β : TypeVec.{?u.11} n
⊢ ∀ (f : α ⟹ β) (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p
Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ∀ {α β : TypeVec.{?u.11} n} (f : α ⟹ β) (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p

Tactic:
intro α β f P; cases P; rfl

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv (Wrepr x) x

Tactic:
induction x with | _ a f ih
   =>  _ 

Goal state after:
case mk
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (WType.mk a f)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt.zero
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
h_pos_t_l_size : 0 < 0
⊢ 0 - 1 + t_r.size + 1 = (node (0 + t_r.size + 1) t_l t_x t_r).size - 1

pp: case node.lt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size✝ : Raised (erase x t_l).size t_l.size
t_l_size : ℕ
h_pos_t_l_size : 0 < t_l_size + 1
⊢ t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
· cases h_pos_t_l_size

Goal state after:
case node.lt.succ
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size✝ : Raised (erase x t_l).size t_l.size
t_l_size : ℕ
h_pos_t_l_size : 0 < t_l_size + 1
⊢ t_l_size + 1 - 1 + t_r.size + 1 = (node (t_l_size + 1 + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case 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
x : (P F).W
⊢ g₁ (Quot.mk (⇑Wsetoid) x) = g₂ (Quot.mk (⇑Wsetoid) x)

Tactic:
induction x with | _ a f ih
   =>  _ 

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₁ (Quot.mk (⇑Wsetoid) (WType.mk a f)) = g₂ (Quot.mk (⇑Wsetoid) (WType.mk a f))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → mk (mk x).dest = mk x

Tactic:
Fix.dest,

Goal state after:
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ rec (Functor.map mk)) <$> x = id <$> x → mk (rec (Functor.map mk) (mk x)) = mk x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case 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
x : (P F).W
⊢ p (Quot.mk (⇑Wsetoid) x)

Tactic:
induction x with | _ a f ih
   =>  _ 

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))
⊢ p (Quot.mk (⇑Wsetoid) (WType.mk a f))
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
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x → mk (mk x).dest = mk x

Tactic:
Fix.dest,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x →
    mk (rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x)) = mk 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
⊢ ∀ {β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p

Tactic:
β

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
⊢ ∀ (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p
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
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ x = y

Tactic:
← Cofix.dest_mk x,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ (mk x).dest = y
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
hn : Even n
x : ℚ
⊢ ↑(nnabs x) ^ n = x ^ n

Tactic:
by simp [hn.pow_abs]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t1 : LiftRelO R (LiftRel R) a b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) a c

Tactic:
have t2 := Computation.rel_of_liftRel h2 hb hc

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t1 : LiftRelO R (LiftRel R) a b
t2 : LiftRelO R (LiftRel R) b c
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
⊢ ∀ (b : Option α) (s' : Seq (Option α)), some a = b ∨ C s' → C (Seq.cons b s')

Tactic:
intro o

Goal state after:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
⊢ ∀ (s' : Seq (Option α)), some a = o ∨ C s' → C (Seq.cons o s')
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inr ?m.407

Tactic:
simp only [parallel.aux1, rmap, corec_eq]
        rw [h]

Goal state after: