mathlib-initiative/mathlib-tactics huggingface dataset:
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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := ⋯
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x =
        (TypeVec.id ::: _root_.id) <$$> x →
      (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) (mk x)).fst = _root_.id (mk x)

Tactic:
intro x' ih

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) (mk x')).fst = _root_.id (mk x')
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (TypeVec.id ::: ((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) =
    (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest)

Tactic:
apply congrArg

Goal state after:
case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) = Quot.mk fun x y ↦ x = mk y.dest
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Tactic:
sign_of_pos (Int.cast_pos.mpr hp),

Goal state after:
case inr.inr
z : ℤ
hp : 0 < z
⊢ 1 = ↑z.sign
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x

Tactic:
have := liftR_map_last R x f id hh

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this : LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: _root_.id) <$$> x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x
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 α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest

Tactic:
apply liftR_map_last'

Goal state after:
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 α
R : Cofix F α → Cofix F α → Prop := ⋯
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ ∀ (x : Cofix F α),
    R
      ((((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl)
        x)
      x
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.tail.destruct = s.destruct >>= tail.aux

Tactic:
simp only [tail, destruct_flatten]; rw [← bind_pure_comp, LawfulMonad.bind_assoc]
  apply congr_arg; ext1 (_ | ⟨a, s⟩) <;> apply (@pure_bind Computation _ _ _ _ _ _).trans _ <;> simp

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

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ (s.drop (n + 1)).destruct = s.destruct >>= drop.aux (n + 1)

Tactic:
by
    rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]
    rfl

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

Goal state before:
pp: case inr
α : 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
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think.Terminates

Tactic:
refine @Computation.think_terminates _ _ ?_

Goal state after:
case inr
α : 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
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates
Module: Mathlib.Data.Seq.Parallel

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

Tactic:
refine @Computation.think_terminates _ _ ?_

Goal state after:
case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
      (match some (some c, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : 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
⊢ (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think.Terminates

Tactic:
refine @Computation.think_terminates _ _ ?_

Goal state after:
case inr.inr
α : 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
⊢ (corec parallel.aux1
      (match S.destruct with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates
Module: Mathlib.Data.Sum.Interval

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

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mp.inl.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 : γ₁
hc : c ∈ f a b
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Module: Mathlib.Data.Sum.Interval

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

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mp.inr.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 : γ₂
hc : c ∈ g a b
⊢ (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ Embedding.inr c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ Embedding.inr c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.inl.inl
α₁ : 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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ (∃ a_1 ∈ f₁ a b, Embedding.inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mp.inl.inl
α₁ : 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 : β₁
c : γ₁
hc : c ∈ f₁ a b
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.inl.inr.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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ a_1 ∈ g₁ a b, inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mp.inl.inr.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 : β₂
c : γ₁
hc : c ∈ g₁ a b
h : inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ inl c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inl c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.inl.inr.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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ b_1 ∈ g₂ a b, inr b_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mp.inl.inr.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 : β₂
c : γ₂
hc : c ∈ g₂ a b
h : inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ inr c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inr c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inr c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ inr c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.inr.inr
α₁ : 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 γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ (∃ a_1 ∈ f₂ a b, { toFun := inr, inj' := ⋯ } a_1 = c) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Goal state after:
case mp.inr.inr
α₁ : 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 : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ { toFun := inr, inj' := ⋯ } c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Module: Mathlib.Data.Vector3

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

Tactic:
exact a

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ'
⊢ Semiconj (⇑e.symm) (⇑e ∘ f ∘ ⇑e.symm) f

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic f μ
⊢ Semiconj (⇑e) f (⇑e ∘ f ∘ ⇑e.symm)

Tactic:
· simp [Semiconj]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic f μ
⊢ Semiconj (⇑e) f (⇑e ∘ f ∘ ⇑e.symm)
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic f μ
⊢ Semiconj (⇑e) f (⇑e ∘ f ∘ ⇑e.symm)

Tactic:
· simp [Semiconj]

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Prufer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ g • s = s

Tactic:
by
  suffices ∀ {g' : G} (_ : g' ^ n ^ j = 1), g' • s ⊆ s by
    refine le_antisymm (this hg) ?_
    conv_lhs => rw [← smul_inv_smul g s]
    replace hg : g⁻¹ ^ n ^ j = 1 := by rw [inv_zpow, hg, inv_one]
    simp only [smul_set_subset_smul_set_iff, this hg]
  rw [(IsFixedPt.preimage_iterate hs j : (zpowGroupHom n)^[j] ⁻¹' s = s).symm]
  rintro g' hg' - ⟨y, hy, rfl⟩
  change (zpowGroupHom n)^[j] (g' * y) ∈ s
  replace hg' : (zpowGroupHom n)^[j] g' = 1 := by simpa [zpowGroupHom]
  rwa [iterate_map_mul, hg', one_mul]

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f (x - ↑⌊x⌋) - (x - ↑⌊x⌋) = f x - x

Tactic:
f.map_sub_int,

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ f x - ↑⌊x⌋ - (x - ↑⌊x⌋) = f x - x
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case h₂
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ (⇑g ⁻¹' U ∆ s) ≤ ε / 3

Tactic:
hg.measure_preimage (hmU.symmDiff hs)

Goal state after:
case h₂
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ ν (U ∆ s) ≤ ε / 3
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
H : ∀ (x : ℝ), f x < x + τ f
⊢ False

Tactic:
exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)

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
hz : z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ
⊢ μ ((⇑(f z) ⁻¹' t) ∆ s) ≠ 0

Tactic:
ne_eq,

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}ᶜ
⊢ ¬μ ((⇑(f z) ⁻¹' t) ∆ s) = 0
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mpr
a b : ℝ
hb : b ≠ 0
⊢ Irrational (a / b) → Dense ↑(AddSubgroup.closure {a, b})

Tactic:
intro h
    contrapose h
    rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩
    have : {a, b} ⊆ range (· • c : ℤ → ℝ) := by
      rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
      apply AddSubgroup.subset_closure
    rcases pair_subset_iff.1 this with ⟨⟨m, rfl⟩, n, rfl⟩
    simp_all [mul_div_mul_right]

Goal state after: