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

Goal state before:
pp: m n k : ℕ
⊢ (∃ k₁ k₂, k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k) ∧ m ≠ 0 ∧ n ≠ 0 ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k

Tactic:
← exists_and_right

Goal state after:
m n k : ℕ
⊢ (∃ x x_1, (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup

Tactic:
by
    convert! List.support_sum_eq a this
    simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃

Tactic:
rw [append_assoc]

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(count (fun x ↦ x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
rw [count_eq_card_filter_range, ← Ico_zero_eq_range, Ico_filter_modEq_card _ _ hr,
    max_eq_left (sub_nonneg.mpr <| by gcongr; positivity)]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rtake n = (take n l.reverse).reverse

Tactic:
by
  rw [rtake]
  induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · exact drop_length
    · simp [drop_append, IH]

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

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
minus : i - p < w.length - p
per' : w[i - p]? = w[i - p + p]?
⊢ w[i % p]? = w[i]?

Tactic:
simp only [large, Nat.sub_add_cancel] at per'

Goal state after:
case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
minus : i - p < w.length - p
per' : w[i - p]? = w[i]?
⊢ w[i % p]? = w[i]?
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k : ℕ
⊢ 1 = mulLeftLinearMap n R 1

Tactic:
mulLeftLinearMap_one,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k : ℕ
⊢ 1 = LinearMap.id
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : X₁ + Z₁ = X₂ + Y₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Tactic:
add_comm X₁,

Goal state after:
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = X₂ + Y₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N

Tactic:
rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  refine .tail (b := X + Y' + Z) (ih (X + Y') (Y - Y') hZ ?_ rfl fun y hy ↦ ?_) <|
    ⟨X + Z, Y', z, add_right_comm .., by simp [hN, add_comm (_ + _)], by simp [Y']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ IsNat ⌈r⌉₊ res

Tactic:
constructor
  rw [← hres, h.to_eq rfl rfl, ← @NNRat.ceil_cast R]
  simp

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

Goal state before:
pp: p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.choose a)

Tactic:
Nat.choose_eq_descFactorial_div_factorial

Goal state after:
p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.descFactorial a / a !)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ ∀ x ∈ ((Icc 1 (n - 1)).gcd n.choose).primeFactors, x = n.minFac

Tactic:
intro p

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
⊢ p ∈ ((Icc 1 (n - 1)).gcd n.choose).primeFactors → p = n.minFac
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

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

Goal state before:
pp: case node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

Goal state after:
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
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
by
  refine (filter_range_nth_subset_insert p k).antisymm fun a ha => ?_
  simp only [mem_insert, mem_filter, mem_range] at ha ⊢
  have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
  rcases ha with (rfl | ⟨hlt, hpa⟩)
  · exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩
  · exact ⟨hlt.trans this, hpa⟩

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
r : F.M → Sort w
f : (x : ↑F F.M) → r (M.mk x)
x : F.M
this : r (M.mk x.dest)
⊢ r (M.mk x.dest)

Tactic:
exact this

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

Goal state before:
pp: α : Type u_1
t : Ordnode α
x : α
⊢ findMax' x t.dual = t.findMin' x

Tactic:
by
  rw [← findMin'_dual, dual_dual]

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

Goal state before:
pp: l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = l.prod
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
exact this

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

Goal state before:
pp: l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l) h).prod = l.prod
⊢ (ofPNatList l h).prod = l.prod

Tactic:
exact this

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n ≤ PNat.find h ↔ ∀ (m : ℕ+), m < n → ¬p m

Tactic:
simp only [← not_lt, find_lt_iff, not_exists, not_and]

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

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

Tactic:
← prod_factorMultiset m

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

Goal state before:
pp: case a.hn
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
exact le_sup_right

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

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

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll

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

case node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
⊢ ((node lls lll llx llr).node' lx lr).balance x nil = ((node lls lll llx llr).node' lx lr).balance' x nil
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + 1 + 1 ≤ 1 then (nil.node' lx (node 1 nil lrx nil)).node' x nil
    else (nil.node' lx (node 1 nil lrx nil)).rotateR x nil

Tactic:
rw [if_neg, rotateR_node, if_neg]

Goal state after:
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = nil.node4R lx (node 1 nil lrx nil) x nil

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ ¬(node 1 nil lrx nil).size < ratio * nil.size

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ ¬0 + 1 + 1 ≤ 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.IsSpecial ↔ u.IsSpecial'

Tactic:
dsimp [IsSpecial, IsSpecial']

Goal state after:
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ u.w * u.z = (u.x * u.y).succPNat
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

Tactic:
· exact (lt_irrefl a₁ hlt₂).elim

Goal state after:
case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : 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
h : ¬delta * ls < rs
h_1 : delta * rs < ls
ld : delta ≤ ll.size + lr.size
⊢ (node ls ll lx lr).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2 (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      ll

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll

Goal state after:
case pos.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : (node ls nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
ld : delta ≤ nil.size + lr.size
⊢ (node ls nil lx lr).rotateR x (node rs rl rx rr) =
    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) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      nil

case pos.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
ld : delta ≤ (node lls lll llx llr).size + lr.size
⊢ (node ls (node lls lll llx llr) lx lr).rotateR x (node rs rl rx rr) =
    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 (size_1 + rs + 1) lr 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)))
          lr)
      (node lls lll llx llr)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
⊢ Raised n m ↔ n ≤ m ∧ m ≤ n + 1

Tactic:
constructor
  · rintro (rfl | rfl)
    · exact ⟨le_rfl, Nat.le_succ _⟩
    · exact ⟨Nat.le_succ _, le_rfl⟩
  · rintro ⟨h₁, h₂⟩
    rcases eq_or_lt_of_le h₁ with (rfl | h₁)
    · exact Or.inl rfl
    · exact Or.inr (le_antisymm h₂ h₁)

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

Goal state before:
pp: case H2.inl.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
l' : ℕ
e : Raised l' l.size
H : l' + r.size ≤ 1
⊢ r.size ≤ delta * l.size

Tactic:
exact le_trans (le_trans (Nat.le_add_left _ _) H) (mul_pos (by decide) l1 : (0 : ℕ) < _)

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

Goal state before:
pp: case mpr.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
i✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : (P F).B a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ u

Tactic:
rw [← f'ieq]

Goal state after:
case mpr.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
i✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : (P F).B a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ (f' i✝ i)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)

Tactic:
← q.P.comp_map,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs (((TypeVec.id ::: Quot.mk r') ⊚ (g ::: fun x ↦ g <$$> x)) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt.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_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : 0 < 0
⊢ t_l.size + (0 - 1) + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

Tactic:
cases h_pos_t_r_size

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

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ ↑((P F₂).comp (P F₁)) α → F₂ (F₁ α)

Tactic:
intro p

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
p : ↑((P F₂).comp (P F₁)) α
⊢ F₂ (F₁ α)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
⊢ ∀
    (p :
      ↑{ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
            B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }
        α),
    abs
        ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                    B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                f p).fst.fst,
          fun x ↦
          abs
            ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                          B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                      f p).fst.snd
                x,
              fun y ↦
              ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                        B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                    f p).snd
                ⟨x, y⟩⟩⟩ =
      f <$> abs ⟨p.fst.fst, fun x ↦ abs ⟨p.fst.snd x, fun y ↦ p.snd ⟨x, y⟩⟩⟩

Tactic:
intro p

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
p :
  ↑{ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }
    α
⊢ abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f p).fst.fst,
        fun x ↦
        abs
          ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                        B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                    f p).fst.snd
              x,
            fun y ↦
            ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                      B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                  f p).snd
              ⟨x, y⟩⟩⟩ =
    f <$> abs ⟨p.fst.fst, fun x ↦ abs ⟨p.fst.snd x, fun y ↦ p.snd ⟨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 : Cofix F α
⊢ Quot.mk Mcongr x.repr = x

Tactic:
by
  let R := fun x y : Cofix F α => abs (repr y) = x
  refine Cofix.bisim₂ R ?_ _ _ rfl
  clear x
  rintro x y h
  subst h
  dsimp [Cofix.dest, Cofix.abs]
  induction y using Quot.ind
  simp only [Cofix.repr, M.dest_corec, abs_map, MvQPF.abs_repr, Function.comp]
  conv => congr; rfl; rw [Cofix.dest]
  rw [MvFunctor.map_map, MvFunctor.map_map, ← appendFun_comp_id, ← appendFun_comp_id]
  apply liftR_map_last
  intros
  rfl

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

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

Tactic:
rw [← f'ieq]

Goal state after:
case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
a' : (P F).A
f' : (P F).B a' → α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : (P F).B a'), p (f' i)
u : α
usuppx : u ∈ supp x
i : (P F).B a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p (f' i)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
s : WSeq α
t : WSeq β
h : (fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s.destruct
    t.destruct

Tactic:
have h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t) := by
        obtain h | h := h
        · exact liftRel_destruct h
        · assumption
      apply Computation.LiftRel.imp _ _ _ h
      apply LiftRelO.imp_right
      intro s t
      apply Or.inl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Symm R
s1 s2 : WSeq α
h : Function.swap (LiftRel R) s2 s1
⊢ LiftRel R s2 s1

Tactic:
rwa [LiftRel.swap, Std.Symm.swap_eq] at h

Goal state after: