mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'
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₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax ↑(findMax' x l.dual) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this

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

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

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l

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

case node
α : Type u_1
inst✝ : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size r.size
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue r) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue r).size = (Ordnode.node ls ll lx lr).size + r.size
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mpr
m n : ℕ+
⊢ m ∣ n → m.factorMultiset ≤ n.factorMultiset

Tactic:
· intro h
    rw [← mul_div_exact h, factorMultiset_mul]
    exact le_self_add

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ PNat.find h = PNat.find h₂ + 1

Tactic:
by
  refine (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩
  induction n with
  | one => simp [h1]
  | succ m _ =>
    intro hm
    simp only [add_lt_add_iff_right, lt_find_iff] at hm
    exact hm _ le_rfl

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

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

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l

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

case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
⊢ All (fun y ↦ All (fun z ↦ y < z) t₂) t₁

Tactic:
refine h₁.mem_lt.imp fun y yx => ?_

Goal state after:
α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
y : α
yx : y < x
⊢ All (fun z ↦ y < z) t₂
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
g : α ⟹ β
⊢ ∀ (a b : (P F).M α), Mcongr a b → Quot.mk Mcongr (g <$$> a) = Quot.mk Mcongr (g <$$> b)

Tactic:
by
      rintro aa₁ aa₂ ⟨r, pr, ra₁a₂⟩; apply Quot.sound
      let r' b₁ b₂ := ∃ a₁ a₂ : q.P.M α, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
      use r'; constructor
      · show IsPrecongr r'
        rintro b₁ b₂ ⟨a₁, a₂, ra₁a₂, b₁eq, b₂eq⟩
        let u : Quot r → Quot r' :=
          Quot.lift (fun x : q.P.M α => Quot.mk r' (g <$$> x))
            (by
              intro a₁ a₂ ra₁a₂
              apply Quot.sound
              exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩)
        have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r := by
          ext x
          rfl
        rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]
        rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_comp]
        rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]
      show r' (g <$$> aa₁) (g <$$> aa₂); exact ⟨aa₁, aa₂, ra₁a₂, rfl, rfl⟩

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

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

Tactic:
simp only [map, size_nil, and_true]

Goal state after:
case nil
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) nil (Option.map f a₂)
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 ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
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.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hn]

Goal state after:
case inl
r : ℝ
hn : 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
α : TypeVec.{u} n
x : Cofix F α
⊢ Quot.mk Mcongr x.repr = x

Tactic:
let R := fun x y : Cofix F α => abs (repr y) = x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
⊢ Quot.mk Mcongr x.repr = x
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
⊢ c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
m

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
⊢ c.Terminates → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
l : List (Computation α)
S : WSeq (Computation α)
⊢ pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
m

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
⊢ s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
m

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
⊢ s.destruct = Computation.pure (some (a', s')) → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
m

Goal state after:
case h1
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
m : s.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s : WSeq α
⊢ s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
m

Goal state after:
case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s : WSeq α
m : s.destruct = c.think
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
s : WSeq α
⊢ a ∈ s.tail → some (some a) = (↑s.tail).get 0 → a ∈ s

Tactic:
m

Goal state after:
case zero
α : Type u
a : α
s : WSeq α
m : a ∈ s.tail
⊢ some (some a) = (↑s.tail).get 0 → a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s : WSeq α
⊢ a ∈ s.tail → some (some a) = (↑s.tail).get (n✝ + 1) → a ∈ s

Tactic:
m

Goal state after:
case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s : WSeq α
m : a ∈ s.tail
⊢ some (some a) = (↑s.tail).get (n✝ + 1) → a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero.cons
α : Type u
a x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get 0
⊢ a ∈ cons x✝ s✝

pp: case zero.think
α : Type u
a : α
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get 0
⊢ a ∈ s✝.think

pp: case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get (n✝ + 1)
⊢ a ∈ cons x✝ s✝

pp: case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think

Tactic:
case zero.cons | succ.cons => exact WSeq.mem_cons_iff .. |>.mpr <| Or.inr (by simpa using m)

Goal state after:
case zero.think
α : Type u
a : α
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get 0
⊢ a ∈ s✝.think

case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ (↑s).destruct.destruct = Sum.inl (Option.map (fun a ↦ (a, ↑s.tail)) s.head)

Tactic:
simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
      Seq.head]

Goal state after:
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' ↦ (a', (some <$> s).tail)) ((some <$> s).get? 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s ↦
            match Option.map (fun a' ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a ↦ (a, some <$> s.tail)) (s.get? 0))
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ico) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ ≤ ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩

Tactic:
by
    simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ←
      exists_prop]
    exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

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

Goal state before:
pp: case h1
α : 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 α
S : WSeq (WSeq α)
ej : s.append S.join = cons b ss
⊢ a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
m

Goal state after:
case h1
α : 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 α
S : WSeq (WSeq α)
ej : s.append S.join = cons b ss
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : 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 α
S : WSeq (WSeq α)
ej : s.append S.join = ss.think
⊢ a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
m

Goal state after:
case h2
α : 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 α
S : WSeq (WSeq α)
ej : s.append S.join = ss.think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
⊢ ∀ {S : WSeq (WSeq α)}, a ∈ S.join → ∃ s ∈ S, a ∈ s

Tactic:
by
  suffices
    ∀ ss : WSeq α,
      a ∈ ss → ∀ s S, append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
    from fun S h => (this _ h nil S (by simp) (by simp [h])).resolve_left (notMem_nil _)
  intro ss h
  apply mem_rec_on h
  · intro b ss o s S ej m
    induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip] <;>
      have := congr_arg Seq.destruct ej
    case nil.nil | nil.cons | nil.think | think => simp at this
    case cons =>
      simp only [cons_append, seq_destruct_cons, Option.some.injEq, Prod.mk.injEq] at this
      cases this with
      | intro b' s =>
        subst b' ss
        simp? at m ⊢ says simp only [cons_append, mem_cons_iff] at m ⊢
        rcases o with e | IH
        · simp [e]
        rcases m with e | m
        · simp [e]
        exact Or.imp_left Or.inr (IH _ _ rfl m)
  · intro ss IH s S ej m
    induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip] <;>
      have := congr_arg Seq.destruct ej
    case nil.cons | nil.think | think => simp at this; simp_all
    case nil.nil | cons => simp at this

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

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct

Tactic:
obtain ⟨s, h⟩ := h

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr.inl
α₁ : 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 : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)

Tactic:
exact mem_map_of_mem _ h

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr.inr
α₁ : 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 : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)

Tactic:
exact mem_map_of_mem _ h

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot

Tactic:
try rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot
Module: Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, ∀ x_1 ∈ Finset.range n, φ (f^[x_1] x) = ψ (f^[x_1] x)

Tactic:
apply ae_all_iff.mpr (fun i => ?_)

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n i : ℕ
⊢ ∀ᵐ (a : α) ∂μ, i ∈ Finset.range n → φ (f^[i] a) = ψ (f^[i] a)
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T
⊢ ENNReal.ofReal T * μ (s ∩ I j) = μ (I j) * ↑(n j) * volume (s ∩ closedBall d (T / (2 * ↑(n j))))

Tactic:
hI₂

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T
⊢ ENNReal.ofReal T * μ (s ∩ I j) = ENNReal.ofReal T * volume (s ∩ closedBall d (T / (2 * ↑(n j))))
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ν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
⊢ f ⁻¹' s =ᵐ[ν] s

Tactic:
suffices ν (f ⁻¹' s \ s) = 0 from (ae_le_set.mpr this).antisymm (ae_le_set.mpr <| hν_sdiff ▸ this)

Goal state after:
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ν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
⊢ ν (f ⁻¹' s \ s) = 0