mathlib-initiative/mathlib-tactics huggingface dataset:
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.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs

Tactic:
splitMin_eq

Goal state after:
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

case neg.s
α : 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
⊢ ℕ
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.finish.v.2 = u.v.2

Tactic:
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b

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.a + ↑u.z * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm

Goal state after:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.refl
α : Type u_1
x : α
rs : ℕ
rx : α
rr : Ordnode α
sl : nil.Sized
sr : (node rs nil rx rr).Sized
H1 : nil.size = 0 → (node rs nil rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx rr).size → (node rs nil rx rr).size ≤ delta * nil.size
this : nil.size = 0 ∧ rr.size = 0
⊢ nil.balanceL x (node rs nil rx rr) = nil.balance x (node rs nil rx rr)

Tactic:
cases sr.2.2.size_eq_zero.1 this.2

Goal state after:
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : nil.Sized
sr : (node rs nil rx nil).Sized
H1 : nil.size = 0 → (node rs nil rx nil).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * nil.size
this : nil.size = 0 ∧ nil.size = 0
⊢ nil.balanceL x (node rs nil rx nil) = nil.balance x (node rs nil rx nil)
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
h₇ : ↑(a.gcd b) ∣ ↑(a.gcdZ b) * ↑a
h₈ : ↑(a.gcd b) ∣ a.gcdX b * ↑b
⊢ a.gcd b ∣ a.gcdD b

Tactic:
h₅

Goal state after:
case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
h₇ : ↑(a.gcd b) ∣ a.gcdX b * ↑b + ↑(a.gcdD b)
h₈ : ↑(a.gcd b) ∣ a.gcdX b * ↑b
⊢ a.gcd b ∣ a.gcdD b
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : Preorder α
h : nil.Bounded ⊥ ⊤
⊢ nil.dual.Bounded ⊤ ⊥

Tactic:
trivial

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

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
h : nil.Bounded ⊥ ↑a✝
⊢ nil.dual.Bounded ↑a✝ ⊥

Tactic:
trivial

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

Goal state before:
pp: case coe.top
α : Type u_1
inst✝ : Preorder α
a✝ : α
h : nil.Bounded ↑a✝ ⊤
⊢ nil.dual.Bounded ⊤ ↑a✝

Tactic:
trivial

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

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : Preorder α
a✝¹ a✝ : α
h : nil.Bounded ↑a✝¹ ↑a✝
⊢ nil.dual.Bounded ↑a✝ ↑a✝¹

Tactic:
trivial

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

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

Tactic:
trivial

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
a✝ : α
h : nil.Bounded o₁ ↑a✝
⊢ nil.Bounded ⊥ ↑a✝

Tactic:
trivial

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

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

Tactic:
trivial

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
a✝ : α
h : nil.Bounded (↑a✝) o₂
⊢ nil.Bounded ↑a✝ ⊤

Tactic:
trivial

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

Goal state before:
pp: case nil.bot
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
h : Valid' ⊥ nil a₂
⊢ nil.Bounded (Option.map f ⊥) (Option.map f a₂)

Tactic:
trivial

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

Goal state before:
pp: case nil.coe.top
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a✝ : α
h : Valid' (↑a✝) nil ⊤
⊢ nil.Bounded (Option.map f ↑a✝) (Option.map f ⊤)

Tactic:
trivial

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)

pp: case refine_2
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (a₀ : (P F).A) (f'₀ : (P F).drop.B a₀ ⟹ α) (f₀ : (P F).last.B a₀ → (P F).W α) (a₁ : (P F).A)
    (f'₁ : (P F).drop.B a₁ ⟹ α) (f₁ : (P F).last.B a₁ → (P F).W α),
    abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ →
      recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)

pp: case refine_3
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (u_1 v w : (P F).W α),
    WEquiv u_1 v → WEquiv v w → recF u u_1 = recF u v → recF u v = recF u w → recF u u_1 = recF u w

Tactic:
· intro a f' f₀ f₁ _h ih; simp only [recF_eq]
        congr 4; funext; apply ih

Goal state after:
case refine_2
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (a₀ : (P F).A) (f'₀ : (P F).drop.B a₀ ⟹ α) (f₀ : (P F).last.B a₀ → (P F).W α) (a₁ : (P F).A)
    (f'₁ : (P F).drop.B a₁ ⟹ α) (f₁ : (P F).last.B a₁ → (P F).W α),
    abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ →
      recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)

case refine_3
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (u_1 v w : (P F).W α),
    WEquiv u_1 v → WEquiv v w → recF u u_1 = recF u v → recF u v = recF u w → recF u u_1 = recF u w
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (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), p (Quot.mk (⇑(wSetoid α)) (f i))
a✝ : Fin2 n
j : (P F).B a a✝.fs
⊢ α.PredLast p ((P F).appendContents f' (fun x ↦ ⟦f x⟧) a✝.fs j)

Tactic:
trivial

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ LiftR' R (f <$$> x) (g <$$> x)

Tactic:
LiftR_def

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> x
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 (LiftRel R)) s.destruct t.destruct

Tactic:
obtain h | h := h

Goal state after:
case inl
α : 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 : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

case inr
α : 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 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
rw [← LiftRelO.swap, Computation.LiftRel.swap]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none none

Tactic:
trivial

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

Goal state before:
pp: case some
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ C (Seq.cons (some b) s')

Tactic:
· apply h1
    apply Or.imp_left _ h
    intro h
    injection h

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

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

Tactic:
trivial

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

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

Tactic:
trivial

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

Goal state before:
pp: case ind
α : 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.join.destruct.Results a n
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
simp only [destruct_join] at ra

Goal state after:
case ind
α : 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
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b
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
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ LiftRelO R U none none

Tactic:
trivial

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.inr.some
α : Type u
S✝ : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a✝ ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a✝ ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
a : Seq1 (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' ↦
          match some a with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a✝ ∈ c

Tactic:
obtain ⟨o, S'⟩ := a

Goal state after:
case h2.inr.some
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
o : Option (Computation α)
S' : Stream'.Seq (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' ↦
          match some (o, S') with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some (o, S')
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.String.Basic

Goal state before:
pp: a b c : String
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
simp only [le_iff_toList_le]

Goal state after:
a b c : String
⊢ a.toList ≤ b.toList → b.toList ≤ c.toList → a.toList ≤ c.toList
Module: Mathlib.Data.String.Basic

Goal state before:
pp: a b : String
⊢ a ≤ b ∨ b ≤ a

Tactic:
simp only [le_iff_toList_le]

Goal state after:
a b : String
⊢ a.toList ≤ b.toList ∨ b.toList ≤ a.toList
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α} ↦ η.app α) (node <$> f v <*> traverse f l <*> traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r

Tactic:
η.preserves_seq,

Goal state after:
case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α} ↦ η.app α) (node <$> f v <*> traverse f l) <*> (fun {α} ↦ η.app α) (traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α} ↦ η.app α) (node <$> f v <*> traverse f l) <*> (fun {α} ↦ η.app α) (traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r

Tactic:
η.preserves_seq,

Goal state after:
case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α} ↦ η.app α) (node <$> f v) <*> (fun {α} ↦ η.app α) (traverse f l) <*> (fun {α} ↦ η.app α) (traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
    c ∈ sumLift₂ f g a b

Tactic:
rintro (⟨a, b, c, rfl, rfl, rfl, h⟩ | ⟨a, b, c, rfl, rfl, rfl, h⟩) <;> exact mem_map_of_mem _ h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᵐ[μ] f ⁻¹' s
h_fin : μ s ≠ ∞
⊢ s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ

Tactic:
by
  replace h_fin : μ (f ⁻¹' s) ≠ ∞ := by rwa [hf.measure_preimage hs]
  refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_
  exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ⇑f fun x ↦ x - ↑n

Tactic:
by
  simpa only [sub_eq_add_neg] using!
    (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

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

Goal state before:
pp: case e'_3
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ |((f ^ 2 ^ n) 0 - x (2 ^ n)) / 2 ^ n| = dist ((f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n

Tactic:
abs_div,

Goal state after:
case e'_3
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ |(f ^ 2 ^ n) 0 - x (2 ^ n)| / |2 ^ n| = dist ((f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n