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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
x y z : F.M
hx : Agree' (n + 1) z x
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
⊢ x.approx (n + 1 + 1) = y.approx (n + 1 + 1)

Tactic:
cases hx
    cases hy
    induction x using PFunctor.M.casesOn'
    induction y using PFunctor.M.casesOn'
    subst z
    iterate 3 (have := mk_inj ‹_›; cases this)
    rename_i n_ih a f₃ f₂ hAgree₂ _ _ h₂ _ _ f₁ h₁ hAgree₁ clr
    simp only [approx_mk]
    have := mk_inj h₁
    cases this; clear h₁
    have := mk_inj h₂
    cases this; clear h₂
    congr
    ext i
    apply n_ih
    · solve_by_elim
    · solve_by_elim
    introv h
    specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)
    simp only [iselect_cons] at hrec
    exact hrec

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match cmpLE x y with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

Tactic:
this,

Goal state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match cmpLE y x with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ α i

Tactic:
match x with
  | WPath.root _ _ i c => exact g' i c
  | WPath.child _ _ i j c => exact g j i c

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

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this : (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p
⊢ Multiset.pmap (fun a h ↦ ↑⟨↑a, h⟩) v h = v

Tactic:
this,

Goal state after:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this : (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p
⊢ Multiset.pmap (fun p x ↦ id p) v h = v
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size✝ l x r).Valid
⊢ (node size✝ l x r).eraseMin.Valid

Tactic:
h.2.eq_node'

Goal state after:
α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size✝ l x r).Valid
⊢ (l.node' x r).eraseMin.Valid
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
this,

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (u.prod ^ m).factorMultiset = m • u.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.left
m n : ℕ+
⊢ m ∣ m.lcm n

Tactic:
exact dvd_lcm_left m n

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

Goal state before:
pp: case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
this,

Goal state after:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ ↑u.w * ↑u.b + (↑u.w * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> x = g <$$> f <$$> x

Tactic:
by
  rw [← abs_repr x, ← abs_map, ← abs_map, ← abs_map]
  rfl

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

Goal state before:
pp: case mp.inl
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1

Tactic:
exact ⟨le_rfl, Nat.le_succ _⟩

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

Goal state before:
pp: n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ : TypeVec.{u} m
x✝ : Comp F G α✝
⊢ (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get)
      ((comp.mk ∘ repr ∘ (MvFunctor.map fun i ↦ repr) ∘ Comp.get) x✝) =
    x✝

Tactic:
simp +unfoldPartialApp only [Function.comp_def, comp.get_mk, abs_repr,
      map_map, TypeVec.comp, MvFunctor.id_map', Comp.mk_get]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid

Tactic:
exact insertWith.valid _ _ (fun _ => id) h

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

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ IsUniform → SuppPreservation

Tactic:
rintro h α ⟨a, f⟩
    ext
    rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]

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

Goal state before:
pp: case node.ord
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Bounded (Option.map f a₁) (Option.map f a₂)

pp: case sz
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Sized

pp: case node.bal
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Balanced

Tactic:
· exact And.intro t_l_valid.ord t_r_valid.ord

Goal state after:
case sz
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Sized

case node.bal
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Balanced
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
by
  have : recF g ∘ fixToW = Fix.rec g := by
    apply funext
    apply Quotient.ind
    intro x
    apply recF_eq_of_wEquiv
    apply wrepr_equiv
  conv =>
    lhs
    rw [Fix.rec, Fix.mk]
    dsimp
  rcases h : repr x with ⟨a, f⟩
  rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']
  rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]

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

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
this,

Goal state after:
case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem
  apply Ordnode.pos_size_of_mem t.property.sz h_mem

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Tactic:
this,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: _root_.id) <$$> x = TypeVec.id <$$> x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ⊚ TypeVec.id ::: mk ∘ fun i ↦ i.dest) <$$> x = x

Tactic:
this,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ⊚ TypeVec.id ::: _root_.id) <$$> x = x
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
⊢ (prod.fst ⊚ subtypeVal R) <$$> h <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, fst_prod_mk, comp_assoc, fst_diag]

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
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ sign 0 = 0

Tactic:
sign_zero

Goal state after:
case inr.inl
⊢ 0 = 0
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
exact liftRel_destruct h

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

Goal state before:
pp: α : Type u
c : Computation (WSeq α)
⊢ Seq.destruct (flatten c.think) = some (none, flatten c)

Tactic:
simp [flatten]

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨b, a, hji⟩ | ⟨b, a, hba⟩)

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hab : ⟨j✝, a⟩ < ⟨i✝, b⟩
⊢ False

case refine_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : ⟨i✝, a⟩ < ⟨i✝, b⟩
⊢ False
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
· rintro (⟨b, a, hji⟩ | ⟨b, a, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.inr.none
α : 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')
h' :
  corec parallel.aux1
      ((fun l' ↦
          match none with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = none
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

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:
· exact
        let ⟨d, o, ad⟩ := IH _ _ h'
        let ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (WSeq.notMem_nil _), ad⟩
        ⟨c, Or.inl cl, ac⟩

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')
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
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
⊢ False

Tactic:
let ⟨c, cs, _⟩ := exists_of_mem_parallel m

Goal state after:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
⊢ False
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
induction n with
  | zero => exact False.elim (Vector.notMem_zero a v.tail ha)
  | succ n _ => exact (mem_succ_iff a v).2 (Or.inr ha)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
s : σ₁
f₂ : α → β
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun x s ↦ f₁ (f₂ x) s) xs s

Tactic:
induction xs using Vector.revInductionOn generalizing s

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → β
s : σ₁
⊢ mapAccumr f₁ (map f₂ nil) s = mapAccumr (fun x s ↦ f₁ (f₂ x) s) nil s

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ xs✝) s = mapAccumr (fun x s ↦ f₁ (f₂ x) s) xs✝ s
s : σ₁
⊢ mapAccumr f₁ (map f₂ (xs✝.snoc x✝)) s = mapAccumr (fun x s ↦ f₁ (f₂ x) s) (xs✝.snoc x✝) s
Module: Mathlib.Data.Vector.MapLemmas

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

Tactic:
induction xs using Vector.revInductionOn generalizing s

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
s : σ₂
⊢ map f₁ (mapAccumr f₂ nil s).2 =
    (mapAccumr
        (fun x s ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        nil s).2

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s : σ₂},
    map f₁ (mapAccumr f₂ xs✝ s).2 =
      (mapAccumr
          (fun x s ↦
            let r := f₂ x s;
            (r.1, f₁ r.2))
          xs✝ s).2
s : σ₂
⊢ map f₁ (mapAccumr f₂ (xs✝.snoc x✝) s).2 =
    (mapAccumr
        (fun x s ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        (xs✝.snoc x✝) s).2
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: f : Natβ Natα.succ → WType Natβ
⊢ ofNat (mk Natα.succ f).toNat = mk Natα.succ f

Tactic:
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]

Goal state after:
f : Natβ Natα.succ → WType Natβ
⊢ (fun x ↦ f ()) = f
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: f : Natβ Natα.succ → WType Natβ
⊢ ofNat (mk Natα.succ f).toNat = mk Natα.succ f

Tactic:
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]
    rfl

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m

Tactic:
by
  simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_eq_iff_map_eq f.monotone (strictMono_id.add_const (m : ℝ)) hn

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

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
⊢ z < τ f

Tactic:
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
  refine lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_
  apply le_translationNumber_of_add_le
  simp only [← le_sub_iff_add_le']
  exact f.forall_map_sub_of_Icc _ hx

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

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

Tactic:
have hF₂ : ∀ g, ⇑(F₂ g) = f₂ g := fun _ => rfl

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : 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
⊢ Disjoint s (a • V)

Tactic:
simp_rw [s, disjoint_iUnion_left, disjoint_left]

Goal state after:
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
⊢ ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • V