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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (l.balance' x r).size = l.size + r.size + 1

Tactic:
size_balance' sl sr

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ l.size + r.size + 1 = l.size + r.size + 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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
⊢ ∀ (a b : (P F).M α), r a b → Quot.mk r' (g <$$> a) = Quot.mk r' (g <$$> b)

Tactic:
intro a₁ a₂ ra₁a₂
              apply Quot.sound
              exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩

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

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

Tactic:
simp only [Option.map, Bounded]

Goal state after:
case nil.coe.coe
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a✝¹ a✝ : α
h : Valid' (↑a✝¹) nil ↑a✝
⊢ f a✝¹ < f a✝
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

Tactic:
hz

Goal state after:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ 0⁻¹ = 0
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
x✝ : α
⊢ x✝ ∈ supp x ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}

Tactic:
apply mem_supp

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

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl i) =
    i

Tactic:
mv_bisim i with R a b x Ha Hb
    rw [Ha, Hb, Cofix.dest_corec]
    dsimp [Function.comp_def]
    repeat rw [MvFunctor.map_map, ← appendFun_comp_id]
    apply liftR_map_last'
    dsimp [Function.comp_def]
    intros
    exact ⟨_, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.tail.get? n → a ∈ s.tail
⊢ a ∈ s

Tactic:
get?_tail

Goal state after:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.get? (n + 1) → a ∈ s.tail
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: 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 : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s.get? (n + 1) ~ t.tail.get? n

Tactic:
get?_tail

Goal state after:
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 : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s.get? (n + 1) ~ t.get? (n + 1)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr.some.none
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
e : S.get? 0 = some none
D : S.destruct = some (none, S.tail)
⊢ (corec parallel.aux1
      (match some (none, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates

Tactic:
simp [TT]

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

Goal state before:
pp: case inr.inr.some.some
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
val✝ : Computation α
e : S.get? 0 = some (some val✝)
D : S.destruct = some (some val✝, S.tail)
⊢ (corec parallel.aux1
      (match some (some val✝, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates

Tactic:
simp [TT]

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

Goal state before:
pp: case inr.inr.inl
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ d
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).toList.destruct = Sum.inr (List.cons a <$> s.toList)

Tactic:
unfold toList

Goal state after:
α : Type u
a : α
s : WSeq α
⊢ (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        ([], cons a s)).destruct =
    Sum.inr
      (List.cons a <$>
        Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          ([], s))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Tactic:
ext ⟨⟩

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
a✝ : γ
⊢ Option.map (g ∘ f) none = some a✝ ↔ (Option.map g ∘ Option.map f) none = some a✝

case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
val✝ : α
a✝ : γ
⊢ Option.map (g ∘ f) (some val✝) = some a✝ ↔ (Option.map g ∘ Option.map f) (some val✝) = some a✝
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 (some b))

Tactic:
· obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        simpa using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩

Goal state after:
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:
by
      simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2
      exact
        let ⟨k1, rs3, ek⟩ := of_results_think rs2
        let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
        let ⟨p', mt, rop'⟩ := Computation.exists_of_liftRel_left (liftRel_destruct st) rs4.mem
        match o', p', rop', rs4, rs5, mt with
        | none, none, _, _, rs5', mt => by
          have : n1 < n := by
            rw [en, ek, ek1]
            apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
            apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
          let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
          refine ⟨ob, ?_, rob⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            exact mb
        | some (a, s'), some (b, t'), ⟨ab, st'⟩, _, rs5, mt => by
          simp only [destruct_append.aux] at rs5
          refine ⟨some (b, append t' (join T')), ?_, ?_⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            apply ret_mem
          rw [eq_of_pure_mem rs5.mem]
          exact ⟨ab, HU _ _ ⟨s', t', S', T', rfl, rfl, st', ST'⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map (ret ∘ f) s).join ~ʷ map f s

Tactic:
map_comp

Goal state after:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map ret (map f s)).join ~ʷ map f s
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y s ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y s ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y s ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 xs s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 ↦
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 ↦
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 ↦
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 ↦
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

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

Goal state before:
pp: α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
⊢ (s.tail.get? n).Terminates

Tactic:
get?_tail

Goal state after:
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
⊢ (s.get? (n + 1)).Terminates
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this : some val✝ ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none

Tactic:
have := mem_unique h' (@Computation.mem_of_get_eq _ _ _ _ h)

Goal state after:
case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this✝ : some val✝ ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
this : some a' = none
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ x + ↑-[n+1]

Tactic:
simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
⊢ z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ → {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 z

Tactic:
hz

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ
⊢ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 z
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
t : Set (Set X)
htc : t.Countable
ht_sub : ∀ s ∈ t, s ∈ range Ioi
ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ s ∈ compl '' t, s ∈ range Iic

Tactic:
by simpa [← compl_inj_iff (x := Ioi _)] using ht_sub

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s)

Tactic:
omegaLimit_eq_biInter_inter _ _ _ hv

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ u ∈ f, closure[inst✝] (image2 ϕ (u ∩ v) s) = ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Tactic:
rw [haveLebesgueDecomposition_add μ ν]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity fun x ↦ (μ.rnDeriv ν x)⁻¹) = ν

Tactic:
rw [withDensity_inv_same (measurable_rnDeriv _ _)
    (by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne')
    (rnDeriv_ne_top _ _)]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG x) = T (φ ↑x)

Tactic:
hG.val_restrict_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ φ (S ↑x) = T (φ ↑x)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG a) = T (φ ↑a)

Tactic:
hG.val_restrict_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ φ (S ↑a) = T (φ ↑a)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
⊢ Group.IsSolvable s.prod.Gal

Tactic:
by
  apply Multiset.induction_on' s
  · exact gal_one_isSolvable
  · intro p t hps _ ht
    rw [Multiset.insert_eq_cons, Multiset.prod_cons]
    exact gal_mul_isSolvable (hs p hps) ht

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n).Gal

Tactic:
exact gal_X_pow_isSolvable n

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]
  rw [lintegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf]
  simp only [Pi.mul_apply]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ (map i (X ^ n - 1)).Splits

Tactic:
have hn'' : (X ^ n - C a).degree ≠ 0 :=
    ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt WithBot.coe_eq_coe.mp hn)

Goal state after:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n).Gal

Tactic:
exact gal_X_pow_isSolvable n

Goal state after: