mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_3
α : 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
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).eraseMax.size + (Ordnode.node rs rl rx rr).size + 1 = ls + rs

Tactic:
add_right_comm,

Goal state after:
case refine_3
α : 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
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).eraseMax.size + 1 + (Ordnode.node rs rl rx rr).size = ls + rs
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balanceL rx rr).size = ls + rs

Tactic:
· rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel

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

Goal state before:
pp: case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.1 = u.v.1

pp: case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.2 = u.v.2

Tactic:
· change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
    have : u.wp + 1 = u.w := rfl
    rw [this, ← ha, u.qp_eq hr]
    ring

Goal state after:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.2 = u.v.2
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
a✝¹ : 1 ≤ t.size
a✝ : 1 ≤ rr.size
⊢ rr.size ≤ delta * (ll.size + lr.size + 1 + rl.size)

Tactic:
unfold delta at hr₂ ⊢

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ 3 * rl.size
a✝¹ : 1 ≤ t.size
a✝ : 1 ≤ rr.size
⊢ rr.size ≤ 3 * (ll.size + lr.size + 1 + rl.size)
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:
by
    unfold Ordnode.insert insertWith; cases cmpLE x y <;> simp [insert_eq_insertWith]

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 y : (P F).W α
h : WEquiv x y
⊢ WEquiv y x

Tactic:
induction h with
  | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
  | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ 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
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
conv =>
    lhs
    rw [Fix.rec, Fix.mk]
    dsimp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ recF g ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr 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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
| abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
| abs ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
⊢ Wequiv x y

Tactic:
cases x
  cases y
  apply Wequiv.abs
  apply h

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
conv =>
    lhs
    rw [Fix.rec, Fix.mk]
    dsimp

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (repr x))) = g (rec g <$> x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : Cofix F α
h : x.dest = y.dest
⊢ x = y

Tactic:
by
  rw [← Cofix.mk_dest x, h, Cofix.mk_dest]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hp]

Goal state after:
case inr.inr
r : ℝ
hp : r.sign = 1
⊢ 1⁻¹ = 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x ↦ ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ b =
    ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag

Tactic:
dsimp [b]
    apply eq_of_drop_last_eq
    · dsimp
      simp only [prod_map_id, TypeVec.id_comp]
      erw [toSubtype_of_subtype_assoc, TypeVec.id_comp]
      clear liftR_map_last q lawful F x R f g hh h b c
      ext (i x) : 2
      induction i with
      | fz => rfl
      | fs _ ih =>
        apply ih
    simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun,
      lastFun_subtypeVal, Function.id_comp, lastFun_comp, lastFun_prod]
    ext1
    rfl

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) →
    ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Tactic:
intro h
    have : Liftp (· ∈ supp x) x := by rw [h]; intro u; exact id
    rw [liftp_iff] at this
    rcases this with ⟨a, f, xeq, h'⟩
    refine ⟨a, f, xeq.symm, ?_⟩
    intro a' f' h''
    rintro u ⟨i, _, hfi⟩
    have : u ∈ supp x := by rw [← hfi]; apply h'
    exact (mem_supp x u).mp this _ _ h''

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s : WSeq α
⊢ LiftRel R s s

Tactic:
refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 ↦ x1 = x2) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.nil.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : nil.append nil.join = cons b ss
m : a ∈ nil.append nil.join
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h1.nil.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : nil.append nil.join = cons b ss
m : a ∈ nil.append nil.join
this : Seq.destruct (nil.append nil.join) = Seq.destruct (cons b ss)
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.nil.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = cons b ss
m : a ∈ nil.append (cons x✝ s✝).join
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h1.nil.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = cons b ss
m : a ∈ nil.append (cons x✝ s✝).join
this : Seq.destruct (nil.append (cons x✝ s✝).join) = Seq.destruct (cons b ss)
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.nil.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = cons b ss
m : a ∈ nil.append s✝.think.join
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h1.nil.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = cons b ss
m : a ∈ nil.append s✝.think.join
this : Seq.destruct (nil.append s✝.think.join) = Seq.destruct (cons b ss)
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons b ss
m : a ∈ (cons x✝ s✝).append S.join
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h1.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons b ss
m : a ∈ (cons x✝ s✝).append S.join
this : Seq.destruct ((cons x✝ s✝).append S.join) = Seq.destruct (cons b ss)
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = cons b ss
m : a ∈ s✝.think.append S.join
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h1.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = cons b ss
m : a ∈ s✝.think.append S.join
this : Seq.destruct (s✝.think.append S.join) = Seq.destruct (cons b ss)
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝ : S.destruct.Results (some (s, S')) m
rs2 : (destruct_join.aux (some (s, S'))).Results a k
mT : some (t, T') ∈ T.destruct
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝ : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.nil.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : nil.append nil.join = ss.think
m : a ∈ nil.append nil.join
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h2.nil.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : nil.append nil.join = ss.think
m : a ∈ nil.append nil.join
this : Seq.destruct (nil.append nil.join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.nil.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = ss.think
m : a ∈ nil.append (cons x✝ s✝).join
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h2.nil.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = ss.think
m : a ∈ nil.append (cons x✝ s✝).join
this : Seq.destruct (nil.append (cons x✝ s✝).join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.nil.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = ss.think
m : a ∈ nil.append s✝.think.join
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h2.nil.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = ss.think
m : a ∈ nil.append s✝.think.join
this : Seq.destruct (nil.append s✝.think.join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = ss.think
m : a ∈ (cons x✝ s✝).append S.join
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h2.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = ss.think
m : a ∈ (cons x✝ s✝).append S.join
this : Seq.destruct ((cons x✝ s✝).append S.join) = Seq.destruct ss.think
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = ss.think
m : a ∈ s✝.think.append S.join
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
have := congr_arg Seq.destruct ej

Goal state after:
case h2.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = ss.think
m : a ∈ s✝.think.append S.join
this : Seq.destruct (s✝.think.append S.join) = Seq.destruct ss.think
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
v : Vector α 0
f : α → β
⊢ ¬b ∈ (map f v).toList

Tactic:
simpa only [Vector.eq_nil v, Vector.map_nil, Vector.toList_nil] using List.not_mem_nil

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: case inr
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
h : s =ᵐ[μ] univ
⊢ g ∈ aestabilizer G μ s

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + (g 0 - 1) < f 0 + ↑⌊g 0⌋

Tactic:
by gcongr; exact sub_one_lt_floor _

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ f b
⊢ Continuous fun x ↦ x + τ f

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ ContinuousAt (fun x ↦ id x + 1) (⨆ g, (f₂ g⁻¹) ((f₁ g) x))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : (range fun x ↦ g ^ x)ᶜ ∈ 𝓝 a
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun x ↦
    match x with
    | (x, y) => a * x / y

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: case inr
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h✝ : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x ↦ g * x) ⁻¹' s = s
h : μ sᶜ = 0
⊢ False

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν

Tactic:
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ Measurable (μ.rnDeriv ν)

Tactic:
fun_prop

Goal state after: