mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ traverse (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)

Tactic:
rw [h₂, Equiv.comp_traverse, h₂]; congr; rw [h₂]

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
F : CFilter α σ
a : τ
⊢ (ofEquiv E F).f a = F.f (E.symm a)

Tactic:
cases F

Goal state after:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }).f a =
    { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }.f (E.symm a)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
a : Set α
⊢ a ∈ f ↔ ∃ b, F.F.f b ⊆ a

Tactic:
cases F

Goal state after:
case mk
α : Type u_1
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ a ∈ f ↔ ∃ b, { σ := σ✝, F := F✝, eq := eq✝ }.F.f b ⊆ a
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : f.Realizer
x✝ : Set α
⊢ x✝ ∈ { f := fun s ↦ m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets

Tactic:
cases F

Goal state after:
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
x✝ : Set α
σ✝ : Type ?u.50
F✝ : CFilter (Set β) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      { f := fun s ↦ m ⁻¹' { σ := σ✝, F := F✝, eq := eq✝ }.F.f s, pt := { σ := σ✝, F := F✝, eq := eq✝ }.F.pt,
            inf := { σ := σ✝, F := F✝, eq := eq✝ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m f).sets
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
x✝ : Set α
σ✝ : Type ?u.50
F✝ : CFilter (Set β) σ✝
⊢ x✝ ∈
      { f := fun s ↦ m ⁻¹' { σ := σ✝, F := F✝, eq := ⋯ }.F.f s, pt := { σ := σ✝, F := F✝, eq := ⋯ }.F.pt,
            inf := { σ := σ✝, F := F✝, eq := ⋯ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (comap m F✝.toFilter).sets

Tactic:
exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩,
        fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
x✝ : Set α
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => F.F.f s ∪ G.F.f t,
            pt := (F.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (F.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
cases F

Goal state after:
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
x✝ : Set α
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∪ G.F.f t,
            pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
F : Ctop α σ
a : τ
⊢ (ofEquiv E F).f a = F.f (E.symm a)

Tactic:
cases F

Goal state after:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
a : τ
f✝ : σ → Set α
top✝ : α → σ
top_mem✝ : ∀ (x : α), x ∈ f✝ (top✝ x)
inter✝ : (a b : σ) → (x : α) → x ∈ f✝ a ∩ f✝ b → σ
inter_mem✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), x ∈ f✝ (inter✝ a b x h)
inter_sub✝ : ∀ (a b : σ) (x : α) (h : x ∈ f✝ a ∩ f✝ b), f✝ (inter✝ a b x h) ⊆ f✝ a ∩ f✝ b
⊢ (ofEquiv E
          { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝,
            inter_sub := inter_sub✝ }).f
      a =
    { f := f✝, top := top✝, top_mem := top_mem✝, inter := inter✝, inter_mem := inter_mem✝, inter_sub := inter_sub✝ }.f
      (E.symm a)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => F.F.f s ∩ G.F.f t,
        pt := (F.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (F.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g

Tactic:
cases F

Goal state after:
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∩ G.F.f t,
        pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax

Tactic:
rw [← sub_nonneg] at *

Goal state after:
C : FloatCfg
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)
Module: Mathlib.Data.Fin.Tuple.Curry

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
induction n with
  | zero => rfl
  | succ n ih => exact funext (ih <| f ·)

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α

Tactic:
simp only [toList, List.mem_map, List.mem_finRange, true_and]; exists equiv x; simp

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
by simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by
  induction l with
  | nil => simp
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

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

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ ¬[] ∈ splitBy.loop r l b (a :: g) []

Tactic:
exact IH

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?
⊢ ∀ i < u.length + (v.length + w.length) - p, (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]?

Tactic:
simp_all [hasPeriod_iff_getElem?]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded IsDershowitzMannaLT

Tactic:
by
  rw [← transGen_oneStep_eq_isDershowitzMannaLT]
  exact isDershowitzMannaLT_singleton_wf.transGen

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

Goal state before:
pp: case inr
q : ℚ
hq : 0 ≤ q
⊢ (↑q.toNNRat)⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
rw [← coe_inv, toNNRat_coe]

Goal state after:
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
  convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂ <;> norm_cast

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ { k // ∀ i ∈ t, k ≡ a i [MOD s i] }

Tactic:
simpa using chineseRemainderOfMultiset a s t.nodup (by simpa using hs) (by simpa using pp)

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

Goal state before:
pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ a.factorization ⌊/⌋ n ≤ a.factorization

Tactic:
exact le_self_nsmul (by simp) (by lia) |>.trans <| smul_floorDiv_le (by lia)

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ ((x₁, x₂).1 + p * (x₁, x₂).2) % p = x₁ ∧ ((x₁, x₂).1 + p * (x₁, x₂).2) / p = x₂

Tactic:
add_mul_mod_self_left,

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ (x₁, x₂).1 % p = x₁ ∧ ((x₁, x₂).1 + p * (x₁, x₂).2) / p = x₂
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ IsChain (fun a b ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))

Tactic:
refine (isZeckendorfRep_zeckendorf _).cons (fun a ha ↦ ?_)

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ f n ≤ nth p n

Tactic:
induction n with
  | zero =>
    rw [Nat.nth_zero]
    refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_
    rcases hsurj hb with ⟨k, hk, rfl⟩
    exact hmono hn hk (Nat.zero_le _)
  | succ n ih =>
    rw [nth_eq_sInf]
    refine le_csInf ?_ ?_
    · use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn
    rintro b ⟨hb, h⟩
    rcases hsurj hb with ⟨m, hm, rfl⟩
    apply hmono hn hm
    rw [Nat.succ_le_iff]
    apply hmono.reflect_lt <;> grind

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : ↑P α
f : α → β
i : P.Idx
h : i.fst = x.fst
⊢ (P.map f x).iget i = f (x.iget i)

Tactic:
simp only [Obj.iget, fst_map, *, dif_pos]

Goal state after:
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : ↑P α
f : α → β
i : P.Idx
h : i.fst = x.fst
⊢ (P.map f x).snd (cast ⋯ i.snd) = f (x.snd (cast ⋯ i.snd))
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑n.pred' + 1

Tactic:
rw [← Num.succ'_to_nat, n.succ'_pred']

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

Goal state before:
pp: m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]; exact not_congr lt_to_int

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

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ s = (node s l x r).realSize

Tactic:
h₁,

Goal state after:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.size + r.size + 1 = (node (l.size + r.size + 1) l x r).realSize
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
⊢ (u + v).prod = u.prod * v.prod

Tactic:
change (coePNatMonoidHom (u + v)).prod = _
  rw [coePNatMonoidHom.map_add]
  exact Multiset.prod_add _ _

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
hl : Valid' o₁ nil o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) nil
bal : BalancedSz nil.size r.size
⊢ Valid' o₁ (nil.glue r) o₂ ∧ (nil.glue r).size = nil.size + r.size

Tactic:
exact ⟨hr, (zero_add _).symm⟩

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

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.PSigma.Order

Goal state before:
pp: case refine_2.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hab : b₁✝ ≤ b₂✝
hba : ¬⟨i, b₂✝⟩ ≤ ⟨i, b₁✝⟩
⊢ ⟨i, b₁✝⟩ < ⟨i, b₂✝⟩

Tactic:
· exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

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

Goal state before:
pp: u : XgcdType
hr : u.r ≠ 0
⊢ u.r - 1 < u.bp

Tactic:
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)

Goal state after:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
⊢ u.r - 1 < u.bp
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ nil o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) nil
⊢ Valid' o₁ (nil.merge r) o₂ ∧ (nil.merge r).size = nil.size + r.size

Tactic:
exact ⟨hr, (zero_add _).symm⟩

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

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ supp (abs ⟨a, f⟩) x✝¹ ↔ x✝ ∈ supp ⟨a, f⟩ x✝¹

Tactic:
supp_eq_of_isUniform,

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ f x✝¹ '' univ ↔ x✝ ∈ supp ⟨a, f⟩ x✝¹

case mpr.h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ IsUniform
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} (x : Sigma F α), Sigma.abs F (Sigma.repr F x) = x

Tactic:
rintro α ⟨x, f⟩

Goal state after:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec.{u} n
x : A
f : F x α
⊢ Sigma.abs F (Sigma.repr F ⟨x, f⟩) = ⟨x, 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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ ((TypeVec.id ::: g₁) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧) =
    (TypeVec.id ::: g₂) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧

Tactic:
rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ rec g (mk x) = g (h <$> x)

Tactic:
← hyp',

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ rec g (mk x) = g (rec g <$> 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ rec g (mk x) = g ((TypeVec.id ::: h) <$$> x)

Tactic:
← hyp',

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> 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
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:
rw [Fix.dest, Fix.rec_eq, ← comp_map, ← appendFun_comp, id_comp]

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 ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Mcongr x y

Tactic:
have : IsPrecongr r' := by
    intro a b r'ab
    have h₀ :
      Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) =
        Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) :=
      h _ _ r'ab
    have h₁ : ∀ u v : q.P.M, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      simp only [r']
      rw [Quot.sound cuv]
      apply h'
    let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁) <| by
        rintro ⟨c⟩ ⟨d⟩ rcd
        exact Quot.sound rcd
    have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
    rw [← this, ← PFunctor.map_map _ _ f, ← PFunctor.map_map _ _ (Quot.mk r), abs_map, abs_map,
      abs_map, h₀]
    rw [← PFunctor.map_map _ _ f, ← PFunctor.map_map _ _ (Quot.mk r), abs_map, abs_map, abs_map]

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
this : IsPrecongr r'
⊢ Mcongr x y
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✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$>
      (TypeVec.id ::: corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
        (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
rw [← comp_map, ← appendFun_comp, id_comp]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: (Quot.mk fun x y ↦ x = mk y.dest) ∘ corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$>
      (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * (↑x.den ^ n * (↑x.den)⁻¹ * (↑x.den)⁻¹ ^ n)

pp: case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

pp: case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Tactic:
mul_right_comm,

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * (↑x.den ^ n * (↑x.den)⁻¹ ^ n * (↑x.den)⁻¹)

case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
supp_eq_of_isUniform,

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ f '' univ = supp ⟨a, f⟩

case mpr.h
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ IsUniform
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ (Pure.pure a).Terminates

Tactic:
exact ret_terminates a

Goal state after: