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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : ¬decide (a = a') = true
⊢ False

pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none

Tactic:
· simp_all

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none

Tactic:
· simp_all

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case mp
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
g : β✝ → γ✝
hg : g ∈ u
f : α✝ → β✝
hf : f ∈ t
a : α✝
ha : a ∈ s
⊢ ∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = g (f a)

Tactic:
exact ⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l_hd : Sigma β
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
⊢ dlookup a (l_hd :: tail✝).dedupKeys = dlookup a (l_hd :: tail✝)

Tactic:
obtain ⟨a', b⟩ := l_hd

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit m.succ = -[n+1].testBit m

Tactic:
by
    dsimp only [testBit]
    simp only [bit_negSucc]
    cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
⊢ CPRankMax (d :: ds).prod x

Tactic:
have h_summands :
      ∀ i : { x // x ∈ Finset.range d },
        CPRankMax ds.prod (unitVec d i.1 ⊗ slice x i.1 (mem_range.1 i.2)) :=
      fun i => cprankMax_mul _ _ _ (cprankMax_upper_bound (slice x i.1 (mem_range.1 i.2)))

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod x
Module: Mathlib.Data.List.ChainOfFn

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i : ℕ) (_hi : i + 1 < (ofFn f).length), r (f ⟨i, ⋯⟩) (f ⟨i + 1, ⋯⟩)) ↔
    ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
length_ofFn

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

Goal state before:
pp: case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?

Tactic:
have phh' : ¬(p head = true) := by simp [phh.symm]
      rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]
      · exact hi
      · simpa using phh

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

Goal state before:
pp: n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ Ico n m ++ Ico m l = Ico n l

Tactic:
dsimp only [Ico]

Goal state after:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case succ
α : 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 α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]

Tactic:
simp only [getElem_cons_succ, tail_ih]

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
h : l.length ≤ [].sum
⊢ ([].splitLengths l).flatten = l

pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), l.length ≤ tail✝.sum → (tail✝.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head✝ :: tail✝).sum
⊢ ((head✝ :: tail✝).splitLengths l).flatten = l

Tactic:
· simp_all

Goal state after:
case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), l.length ≤ tail✝.sum → (tail✝.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head✝ :: tail✝).sum
⊢ ((head✝ :: tail✝).splitLengths l).flatten = l
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
w : List α
len : n ≤ w.length
dvd : 0 ∣ n
per : w.HasPeriod 0
⊢ (take n w ++ w).HasPeriod 0

Tactic:
simp_all [HasPeriod]

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

Goal state before:
pp: case inr.inl
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
p_pos : p > 0
dvd : p ∣ 0
len : 0 ≤ w.length
⊢ (take 0 w ++ w).HasPeriod p

pp: case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ (take n w ++ w).HasPeriod p

Tactic:
· simp_all

Goal state after:
case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ (take n w ++ w).HasPeriod p
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:
classical
    replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
    simpa using Matrix.ext_iff.2 h default j

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

Goal state before:
pp: case inl
α : Type u_1
w : List α
q : ℕ
per_q : w.HasPeriod q
per_p : w.HasPeriod 0
len : 0 + q - Nat.gcd 0 q ≤ w.length
⊢ w.HasPeriod (Nat.gcd 0 q)

Tactic:
simp_all [HasPeriod]

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

Goal state before:
pp: case inr.inl
α : Type u_1
w : List α
p : ℕ
per_p : w.HasPeriod p
p_pos : p > 0
per_q : w.HasPeriod 0
len : p + 0 - p.gcd 0 ≤ w.length
⊢ w.HasPeriod (p.gcd 0)

pp: case inr.inr
α : 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
⊢ w.HasPeriod (p.gcd q)

Tactic:
· simp_all

Goal state after:
case inr.inr
α : 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
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌈r⌉₊ m

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ IsNat ⌈↑m⌉₊ m
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsInt r (Int.negOfNat m) → IsNat ⌈r⌉₊ 0

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ IsNat ⌈↑(Int.negOfNat m)⌉₊ 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ nth p n = 0

Tactic:
nth,

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b ↦ a ≤ b).getD n 0
    else ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)) =
    0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
n : ℕ
⊢ nth p n = ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)

Tactic:
nth,

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Infinite
n : ℕ
⊢ (if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b ↦ a ≤ b).getD n 0
    else ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)) =
    ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ nth p n ≤ f n

Tactic:
nth,

Goal state after:
case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ (if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b ↦ a ≤ b).getD n 0
    else ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)) ≤
    f n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p).bit0 = ↑(neg p) + ↑(neg p)

Tactic:
rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.succ = ↑n + 1

Tactic:
← add_one,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(n + 1) = ↑n + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < s

Tactic:
rw [h.1]; apply Nat.le_add_left

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

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

Tactic:
by rw [← of_to_int n, e]; simp

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

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

Tactic:
dsimp only [dual, id]

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

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

Tactic:
dsimp only [dual, id]

Goal state after:
case nil.node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lrx (Ordnode.singleton lx).dual =
    node 3 (Ordnode.singleton x) lrx (Ordnode.singleton lx)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
x y : F.M
h : Agree' (n✝ + 1) x y
⊢ Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]

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

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ (casesOn (id nil)
        (casesOn (id (node ls (node lls lll llx llr) lx nil)) (Ordnode.singleton x) fun ls_1 ll lx_1 lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 (node ls (node lls lll llx llr) lx nil) x nil) fun size l lrx r ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx_1 (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr x nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs l x_1 r ↦
        casesOn (id (node ls (node lls lll llx llr) lx nil)) (node (rs + 1) nil x nil) fun ls_1 ll lx_1 lr ↦
          if ls_1 > delta * rs 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_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr x nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + rs + 1) lrr x nil)
          else node (ls_1 + rs + 1) (node ls (node lls lll llx llr) lx nil) x nil).dual =
    casesOn (id nil.dual)
      (casesOn (id (node ls (node lls lll llx llr) lx nil).dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x (node ls (node lls lll llx llr) lx nil).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_1 l x_1 r ↦
      casesOn (id (node ls (node lls lll llx llr) lx nil).dual) (node (ls_1 + 1) nil.dual x nil) fun rs rl rx rr ↦
        if rs > delta * ls_1 then
          casesOn (id rr) nil fun rrs l x_2 r ↦
            casesOn (id rl) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) nil.dual x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) nil.dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) nil.dual x (node ls (node lls lll llx llr) lx nil).dual

Tactic:
dsimp only [dual, id]

Goal state after:
case nil.node.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lx (node lls llr.dual llx lll.dual) =
    node 3 (Ordnode.singleton x) lx (node lls llr.dual llx lll.dual)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
⊢ IsPath (⟨a', i⟩ :: xs) (M.mk ⟨a, f⟩) → a = a'

Tactic:
by
  generalize h : M.mk ⟨a, f⟩ = x
  rintro (_ | ⟨_, _, _, _, rfl, _⟩)
  cases mk_inj h
  rfl

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

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

Tactic:
dsimp only [dual, id]

Goal state after:
case pos.node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then
        node (ls + rs + 1) (node lls lll llx llr) lx (node (rs + lrs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
      else
        node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))).dual =
    if lrs < ratio * lls then
      node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
        (node lls llr.dual llx lll.dual)
    else
      node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual

Tactic:
← dual_dual (balanceL _ _ _),

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (r.dual.balanceL x l.dual).dual.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
hm : nil.Sized
⊢ (l.node4L x nil y r).Sized

Tactic:
exact (hl.node' hm).node' hr

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| dest P ⟨a, g ⊚ f⟩ = (g ::: fun x ↦ g <$$> x) <$$> dest P ⟨a, f⟩

Tactic:
rhs

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| (g ::: fun x ↦ g <$$> x) <$$> dest P ⟨a, f⟩