mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ -[↑n.pred' / ↑d+1] = -[↑n.pred' / (↑d.pred' + 1)+1]

Tactic:
rw [d.to_nat_eq_succ_pred]

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

Goal state before:
pp: n d : PosNum
⊢ ↑(↑n.pred' / ↑d).succ = ↑(↑n.pred' / (↑d.pred' + 1)).succ

Tactic:
rw [d.to_nat_eq_succ_pred]

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

Goal state before:
pp: case pos.h
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ ¬IsPath ps_tail (x_f (cast ⋯ i))

Tactic:
intro h'

Goal state after:
case pos.h
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ False
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n

Tactic:
rcases n with - | n

Goal state after:
case zero
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ sCorec f x₀ 0 = Approx.sMk (F.map (M.corec f) (f x₀)) 0

case succ
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ (n + 1) = Approx.sMk (F.map (M.corec f) (f x₀)) (n + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).size = l.size + m.size + r.size + 2

Tactic:
dsimp [node3R, node', size]; rw [← add_assoc, ← add_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1

Tactic:
have := H.2.eq_node'

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this : Ordnode.node s l x r = l.node' x r
⊢ Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil.node.refl.refl.hc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ nil.size < ratio * (node 1 nil rrx nil).size

pp: case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rrx : α
this : nil.size = 0 ∧ nil.size = 0
hr : (nil.node' rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ ¬0 + (0 + 1 + 1) ≤ 1

Tactic:
all_goals (try dsimp only [size]); decide

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

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

Tactic:
rw [if_neg, rotateL_node, if_neg]

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

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

case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬0 + (1 + 1) ≤ 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬(node 1 nil rlx nil).size < ratio * nil.size

pp: case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬0 + (1 + 1) ≤ 1

Tactic:
all_goals (try dsimp only [size]); decide

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

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

pp: 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

Tactic:
all_goals (try dsimp only [size]); decide

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

Goal state before:
pp: case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ nil.size < ratio * (node 1 nil llx nil).size

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

Tactic:
all_goals (try dsimp only [size]); decide

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

Goal state before:
pp: case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * ↑u.a + ↑u.z * ↑u.b

Tactic:
rw [← ha, u.qp_eq hr]

Goal state after:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * (↑u.b * (u.qp + 1)) + ↑u.z * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
⊢ x✝.reduce.IsReduced

Tactic:
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h, flip_isReduced]
      apply reduce_isReduced

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

Goal state before:
pp: case mpr.mpr
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
⊢ (∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u) → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)

Tactic:
intro h'

Goal state after:
case mpr.mpr
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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : nil.Bounded o₁ o₂
⊢ nil.Bounded o₁ ⊤

Tactic:
by cases o₁ <;> trivial

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

Goal state before:
pp: case mp
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 ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) → u ∈ f i✝ '' univ

Tactic:
intro h'

Goal state after:
case mp
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 ⟹ α
i✝ : Fin2 n
u : α i✝
h' : ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ
⊢ u ∈ f i✝ '' univ
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 ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ f i✝ '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 ⟹ α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ

Tactic:
intro h'

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 ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
⊢ ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ
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
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u) →
    ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_2 i), p i (f_1 i j)

Tactic:
intro h'

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
⊢ ∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj

Goal state before:
pp: n : ℕ
i : Fin2 n
α β : TypeVec.{?u.11} n
f : α ⟹ β
⊢ ∀ (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p

Tactic:
P

Goal state after:
n : ℕ
i : Fin2 n
α β : TypeVec.{?u.11} n
f : α ⟹ β
P : ↑(Prj.P i) α
⊢ abs i (f <$$> P) = f <$$> abs i P
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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₀⟩ = (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
dyeq,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₀⟩ = (TypeVec.id ::: Quot.mk r) <$$> MvQPF.abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Quot.mk r <$> abs ⟨a, f₀⟩ = Quot.mk r <$> y.dest

Tactic:
dyeq,

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Quot.mk r <$> abs ⟨a, f₀⟩ = Quot.mk r <$> abs ⟨a, f₁⟩
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n

pp: case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))

Tactic:
· have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩
    simp [subset_antisymm_iff, range_subset_iff, this]

Goal state after:
case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr.mpr
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
⊢ (∀ u ∈ supp x, p u) → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
intro h'

Goal state after:
case mpr.mpr
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
h' : ∀ u ∈ supp x, p u
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) → u ∈ f '' univ

Tactic:
intro h'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ
⊢ u ∈ f '' univ
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 → α
u : α
⊢ u ∈ f '' univ → ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 → α), abs ⟨a_2, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ

Tactic:
intro h'

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 → α
u : α
h' : u ∈ f '' univ
⊢ ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∀ u ∈ supp (abs ⟨a, f⟩), p u) → ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : (P F).B a_2), p (f_1 i)

Tactic:
intro h'

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
⊢ ∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op

Tactic:
· apply op_injective

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop → x✝ ∈ {unop x}

pp: case mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop

Tactic:
· apply op_injective

Goal state after:
case mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}

pp: case mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop

Tactic:
· apply op_injective

Goal state after:
case mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op

Tactic:
· apply op_injective

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

Goal state before:
pp: α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
⊢ Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b

Tactic:
rcases a with - | a <;> rcases b with - | b

Goal state after:
case none.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none none
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd none

case none.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)

case some.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.tail ~ʷ t.tail

Tactic:
apply flatten_congr
  dsimp only [(· <$> ·)]; rw [← Computation.bind_pure, ← Computation.bind_pure]
  apply liftRel_bind _ _ (destruct_congr h)
  intro a b h; simp only [comp_apply, liftRel_pure]
  rcases a with - | a <;> rcases b with - | b
  · trivial
  · cases h
  · cases a
    cases h
  · obtain ⟨a, s'⟩ := a
    obtain ⟨b, t'⟩ := b
    exact h.right

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

Goal state before:
pp: case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a b : Option (α × WSeq α)
ma : a ∈ s.destruct
mb : b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
rcases a with - | a <;> rcases b with - | b

Goal state after:
case refine_2.none.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none none

case refine_2.none.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
ma : none ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)

case refine_2.some.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) none

case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case intro
α : 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
b' : x✝ = b
s : s✝.append S.join = ss
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
| intro b' s =>

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

Goal state before:
pp: α : Type u
β : Type v
s : WSeq α
f : α → WSeq β
b : β
h : b ∈ s.bind f
t : WSeq β
tm : t ∈ map f s
bt : b ∈ t
a : α
as : a ∈ s
e : f a = t
⊢ b ∈ f a

Tactic:
by rwa [e]

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

Goal state before:
pp: α : Type u
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    S.join.destruct.destruct (S.destruct.bind destruct_join.aux).destruct

Tactic:
induction S using WSeq.recOn
      case nil | cons => simp
      case think S => exact Or.inr ⟨S, by simp⟩

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

Goal state before:
pp: case nil.nil
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (nil.append (nil.append T).join).destruct.destruct (nil.append (nil.join.append T.join)).destruct.destruct

Tactic:
simp only [nil_append, join_nil]
      induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ ⇑↑(translate (Multiplicative.ofAdd x) ^ n) = ⇑↑(translate (Multiplicative.ofAdd (↑n * x)))

Tactic:
translate_pow

Goal state after:
x : ℝ
n : ℕ
⊢ ⇑↑(translate (Multiplicative.ofAdd (↑n * x))) = ⇑↑(translate (Multiplicative.ofAdd (↑n * x)))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
⊢ Tendsto (fun x ↦ x - 1) atTop atTop

Tactic:
by
      simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n

Tactic:
by
  have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
  rw [div_div, ← pow_succ', ← abs_of_pos this]
  calc
    _ = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| := by
      simp_rw [transnumAuxSeq, Real.dist_eq]
      rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
    _ < _ := by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

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

Goal state before:
pp: case h₂
f : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f

Tactic:
apply floor_le

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
⊢ a • V ⊆ sᶜ

Tactic:
rwa [disjoint_right] at hd

Goal state after: