mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F✝ : TypeVec.{u} n → Type u_1
q✝ : MvQPF F✝
F : TypeVec.{u} n → Type u_2
F' : TypeVec.{u} n → Type u_3
q : MvQPF F'
inst✝ : MvFunctor F
eqv : (α : TypeVec.{u} n) → F α ≃ F' α
map_eq : ∀ (α β : TypeVec.{u} n) (f : α ⟹ β) (a : F α), f <$$> a = (eqv β).symm (f <$$> (eqv α) a)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F') α), (eqv β).symm (abs (f <$$> p)) = f <$$> (eqv α).symm (abs p)

Tactic:
simp [q.abs_map, map_eq]

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

Goal state before:
pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x

Tactic:
use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Subtype.val <$> abs ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x

Tactic:
use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Subtype.val <$> abs ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk.mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
this : IsPrecongr r'
⊢ Mcongr x y

Tactic:
exact ⟨r', this, rxy⟩

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
have : recF g ∘ fixToW = Fix.rec g := by
    ext ⟨x⟩
    apply recF_eq_of_Wequiv
    rw [fixToW]
    apply Wrepr_equiv

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g (rec g <$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| (corec g x).dest

Tactic:
rw [Cofix.dest, Cofix.corec]

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| Quot.lift (fun x ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x))
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
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))
⊢ LiftP (α.PredLast p) (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)

Tactic:
rw [MvQPF.liftP_iff]

Goal state after:
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_1 f_1,
    abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ = abs ⟨a_1, f_1⟩ ∧
      ∀ (i : Fin2 (n + 1)) (j : (P F).B a_1 i), α.PredLast p (f_1 i j)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
this : IsPrecongr r'
⊢ Mcongr x y

Tactic:
exact ⟨r', this, rxy⟩

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

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

Tactic:
apply Computation.memRecOn h <;> [skip; intro c IH] <;> intro s m <;>
    induction s using WSeq.recOn <;>
    have := congr_arg Computation.destruct m

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

case h1.cons
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
this : (cons x✝ s✝).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

case h1.think
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
this : s✝.think.destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

case h2.nil
α : 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')
m : nil.destruct = c.think
this : nil.destruct.destruct = c.think.destruct
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

case h2.cons
α : 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')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
this : (cons x✝ s✝).destruct.destruct = c.think.destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

case h2.think
α : 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✝.think.destruct = c.think
this : s✝.think.destruct.destruct = c.think.destruct
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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'
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inr ?m.247

Tactic:
simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h]

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

Goal state before:
pp: case inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S
l : List (Computation α)
a : α
⊢ Prop

Tactic:
exact ∃ c ∈ l, a ∈ c

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹ → x✝¹ < x✝

Tactic:
· rintro ⟨⟨i, a, b, hab⟩, h⟩
        rw [mk_le_mk_iff] at h
        exact mk_lt_mk_iff.2 (hab.lt_of_not_ge h)

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

Goal state before:
pp: case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    ltb s₁.next s₂.next

Tactic:
if_pos (by simpa using h₁),

Goal state after:
case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
    else true) =
    ltb s₁.next s₂.next
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    decide (s₁.curr < s₂.curr)

Tactic:
if_pos (by simpa using h₁),

Goal state after:
case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
    else true) =
    decide (s₁.curr < s₂.curr)
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    true

Tactic:
if_pos (by simpa using h₁),

Goal state after:
case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
    else true) =
    true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []

Tactic:
rename_i c₁ cs₁ ih; apply iff_of_false
    · unfold ltb
      simp [Legacy.Iterator.hasNext]
    · apply not_lt_of_gt; apply List.nil_lt_cons

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

Goal state before:
pp: case h2.inr.some.some.inl.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
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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ c
dc : d = c
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
refine ⟨c, Or.inr ?_, ad⟩

Goal state after:
case h2.inr.some.some.inl.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
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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ c
dc : d = c
⊢ c ∈ S
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    s1.destruct s2.destruct

Tactic:
rw [h1, h2]; rw [destruct_append, destruct_append]
    apply Computation.liftRel_bind _ _ (liftRel_destruct st)
    exact fun {o p} h =>
      match o, p, h with
      | some (a, s), some (b, t), ⟨h1, h2⟩ => by
        simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
      | none, none, _ => by
        -- We do not `dsimp` with `LiftRelO` since `liftRel_join.lem` uses `LiftRelO`.
        dsimp only [destruct_append.aux, Computation.LiftRel]; constructor
        · intro
          apply liftRel_join.lem _ ST fun _ _ => id
        · intro b mb
          rw [← LiftRelO.swap]
          apply liftRel_join.lem (swap R)
          · rw [← LiftRel.swap R, ← LiftRel.swap]
            apply ST
          · rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
            exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
          · exact mb

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

Goal state before:
pp: case refine_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅

Tactic:
rintro a b rfl rfl

Goal state after:
case refine_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLift₂ f g (inl a) (inl b) = ∅
⊢ f a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅

Tactic:
rintro a b rfl rfl

Goal state after:
case refine_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅

Tactic:
rintro a b rfl rfl

Goal state after:
case refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) = ∅
⊢ f₁ a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅

Tactic:
rintro a b rfl rfl

Goal state after:
case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = ∅
⊢ g₁ a b = ∅ ∧ g₂ a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_3
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅

Tactic:
rintro a b rfl rfl

Goal state after:
case refine_3
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) = ∅
⊢ f₂ a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_4
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅

Tactic:
rintro a b rfl rfl

Goal state after:
case refine_4
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
⊢ α

Tactic:
refine i.cases' ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
⊢ α

case refine_2
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
⊢ Fin2 n → α
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)

Tactic:
refine i.cases' ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)

case refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_1 : Fin2 n), p ((a :: v) n_1.fs)
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - 1 - x) = -1 * ↑(x + 1)

Tactic:
← tsub_add_eq_tsub_tsub_swap,

Goal state after:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - (x + 1)) = -1 * ↑(x + 1)
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hs : MeasurableSet s
hfs : f ⁻¹' s = s
⊢ s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ

Tactic:
by
  simpa only [eventuallyConst_set'] using hf.aeconst_set hs hfs

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

Goal state before:
pp: f : CircleDeg1Lift
⊢ f.transnumAuxSeq 0 = f 0

Tactic:
simp [transnumAuxSeq]

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
c : M
s : Set X
hsm : MeasurableSet s
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
by
    simpa only [smul_one_smul] using SMulInvariantMeasure.measure_preimage_smul (c • 1 : N) hsm

Goal state after: