mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
⊢ p f

Tactic:
induction hs : univ.sigma f using Finset.strongInductionOn generalizing f with | _ s ihs

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
s : Finset ((i : ι) × α i)
ihs : ∀ t ⊂ s, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
f : (i : ι) → Finset (α i)
hs : univ.sigma f = s
⊢ p f
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ (lookup a l).getD 0 = x ↔ x ∈ lookup a l

Tactic:
rcases lookup a l with - | m <;> simp [hx.symm]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).take = ↑(take ⟨is, h⟩).take

Tactic:
by
      simp [assocRight, take, cast_type, List.take_take, Nat.le_add_right]

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

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

Tactic:
by_cases h : f false false <;> simp [h]

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

Goal state before:
pp: case nil
α : Type u_1
x : α
hx : ¬x ∈ []
n : ℕ
hn : n ∈ {n | n ≤ [].length}
m : ℕ
hm : m ∈ {n | n ≤ [].length}
h : (fun k ↦ [].insertIdx k x) n = (fun k ↦ [].insertIdx k x) m
⊢ n = m

Tactic:
simp_all [Set.mem_singleton_iff, Set.ofPred_eq_eq_singleton, length]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ l.length ≤ tail.length

Tactic:
exact Nat.le_of_lt_succ ll

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)
⊢ splitBy r (a :: l) = [a :: l]

Tactic:
rw [splitBy, ← append_nil l, splitByLoop_append]

Goal state after:
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 ++ [])]

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)

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
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case inr.inr
α : 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 ≠ []
⊢ l ++ m = (splitBy r l ++ splitBy r m).flatten ∧
    ¬[] ∈ splitBy r l ++ splitBy r m ∧
      (∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1) ∧
        IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)

Tactic:
refine ⟨by simp, by simp, ?_, ?_⟩

Goal state after:
case inr.inr.refine_1
α : 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 ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1

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 ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
m : List α
ha : ∀ (x : α), x ∈ l.getLast? → r x a = false
⊢ splitBy r (l ++ a :: m) = splitBy r l ++ splitBy r (a :: m)

Tactic:
by
  apply splitBy_append
  simpa

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
zify

Goal state after:
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = ↑q₁.num * ↑q₂.num / ↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den))
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
zify

Goal state after:
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num * ↑q₂.num = ↑(q₁ * q₂).num * ↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den))
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k.factorization = f

Tactic:
exact h ▸ factorization_prod_pow_eq_self_of_le_factorization hlt.le

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a b n : ℕ
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  obtain rfl | ha := eq_or_ne a 0
  · simp [hn]
  rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

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

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

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 node 3 (ι x) rx rr

Goal state after:
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 α
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact node 3 (ι x) rx rr

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

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i ↦ p (i + m)) n = nth (fun i ↦ p (i + m)) n + m - m

Tactic:
Nat.add_sub_cancel

Goal state after:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i ↦ p (i + m)) n = nth (fun i ↦ p (i + m)) n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
this : nth p k < nth p (k + 1)
⊢ a < nth p (k + 1) ∧ p a
Module: Mathlib.Data.Num.ZNum

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

Tactic:
by
  cases n <;> try { rfl }; rw [succ, Num.zneg_toZNumNeg]; rfl

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

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

Tactic:
exact Set.Finite.toFinset_subset.mpr this

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

Goal state before:
pp: m n : Num
⊢ ↑(ofZNum (m.sub' n)) = ↑m - ↑n

Tactic:
ofZNum_toNat,

Goal state after:
m n : Num
⊢ (↑(m.sub' n)).toNat = ↑m - ↑n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ofInt' ↑0 = 0

Tactic:
by
    dsimp [ofInt', cast_zero]
    simp only [Num.ofNat'_zero, Num.toZNum]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (x n.succ) = head' (x m.succ)

Tactic:
suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]

Goal state after:
F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ ∀ (n : ℕ), head' (x n.succ) = head' (x 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro x_a fun j ↦ (x_f j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))

Tactic:
have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›

Goal state after:
case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
h_a_1 : ⟨x_a, x_f⟩ = ⟨a, x'⟩
⊢ Agree (CofixA.intro x_a fun j ↦ (x_f j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
          | nil => 0
          | node sz l x r => sz) +
          ((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
        1 +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
← add_assoc

Goal state after:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ l.toList ++ (x :: r.toList ++ r') = (node size✝ l x r).toList ++ r'

Tactic:
← List.append_assoc,

Goal state after:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ l.toList ++ x :: r.toList ++ r' = (node size✝ l x r).toList ++ r'
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m ∣ n

Tactic:
← prod_factorMultiset m,

Goal state after:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod ∣ n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : rls < ratio * rrs
⊢ nil.node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)

Tactic:
simp [node3L, node']; abel

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

Goal state before:
pp: case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p

Tactic:
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h

Goal state after:
case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m

Tactic:
← PNat.factorMultiset_lcm n m,

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.lcm m).factorMultiset.prod = n.lcm m
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : lls ≤ 1
⊢ lll.size = 0 ∧ llr.size = 0

Tactic:
sl.2.1.1,

Goal state after:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : lll.size + llr.size + 1 ≤ 1
⊢ lll.size = 0 ∧ llr.size = 0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
hr : nil.Balanced
sr : nil.Sized
⊢ (node ls ll lx lr).balance x nil = (node ls ll lx lr).balance' x nil

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
⊢ (node ls ll lx lr).balance x (node rs rl rx rr) = (node ls ll lx lr).balance' x (node rs rl rx rr)

Tactic:
· rw [sl.eq_node'] at hl ⊢
      obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;>
        dsimp [balance, balance']
      · rfl
      · have : size lrl = 0 ∧ size lrr = 0 := by
          have := balancedSz_zero.1 hl.1.symm
          rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
        cases sl.2.2.2.1.size_eq_zero.1 this.1
        cases sl.2.2.2.2.size_eq_zero.1 this.2
        obtain rfl : lrs = 1 := sl.2.2.1
        rw [if_neg, rotateR_node, if_neg]; · rfl
        all_goals (try dsimp only [size]); decide
      · have : size lll = 0 ∧ size llr = 0 := by
          have := balancedSz_zero.1 hl.1
          rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
        cases sl.2.1.2.1.size_eq_zero.1 this.1
        cases sl.2.1.2.2.size_eq_zero.1 this.2
        obtain rfl : lls = 1 := sl.2.1.1
        rw [if_neg, rotateR_node, if_pos]; · rfl
        all_goals (try dsimp only [size]); decide
      · symm; rw [if_neg, rotateR]
        · dsimp only [size_node]; split_ifs
          · simp [node3R, node']; abel
          · simp [node4R, node', sl.2.2.1]; abel
        · exact not_le_of_gt (Nat.succ_lt_succ (add_pos sl.2.1.pos sl.2.2.pos))

Goal state after:
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
⊢ (node ls ll lx lr).balance x (node rs rl rx rr) = (node ls ll lx lr).balance' x (node rs rl rx rr)
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.finish.IsReduced

Tactic:
by
  dsimp [IsReduced]
  rfl

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

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
rw [← xeq, ← abs_repr u, h, ← abs_map]; rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ supp x a'

Tactic:
← hfi

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ f a' j ∈ supp x a'
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
hh : u ∈ supp x a'
⊢ u ∈ h'' a' '' univ

Tactic:
exact (mem_supp x _ u).mp hh _ _ hu

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H :
  (∃ l', Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ r', Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H :
  (∃ l', Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ r', Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Raised (node sz l y r).size ((insertWith f x l).size + r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Ordnode.insert x (node size✝ l y r) = insertWith (fun x_1 ↦ x) x (node size✝ l y r)

Tactic:
unfold Ordnode.insert insertWith

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: 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)

Tactic:
apply Wequiv.trans (v := PFunctor.W.mk (q.P.map Wrepr ⟨a, f⟩))

Goal state after:
case mk.a
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)) (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩))

case mk.a
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 (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)) (WType.mk a f)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: 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), p x

Tactic:
rintro ⟨x⟩
  induction x with | _ a f ih
  change p ⟦⟨a, f⟩⟧
  rw [← Fix.ind_aux a f]
  apply h
  rw [liftp_iff]
  refine ⟨_, _, rfl, ?_⟩
  convert! ih

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
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Tactic:
have : Fix.mk ∘ Fix.dest (F := F) (α := α) = _root_.id := by
    ext (x : Fix F α)
    apply Fix.mk_dest

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
u : α
i : (P F).B a
left✝ : i ∈ univ
hfi : f i = u
⊢ u ∈ supp x

Tactic:
← hfi

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
u : α
i : (P F).B a
left✝ : i ∈ univ
hfi : f i = u
⊢ f i ∈ supp x
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro l S e

Goal state after:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ a, parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates