mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
f : α✝ → Finset β✝
g : β✝ → Finset γ✝
⊢ s >>= f >>= g = s >>= fun x ↦ f x >>= g

Tactic:
simp only [bind, sup_eq_biUnion, biUnion_biUnion]

Goal state after:
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ image (fun p ↦ p.1 * p.2) (image Subtype.val (m.divisors ×ˢ n.divisors).attach) =
    map { toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ } (m.divisors ×ˢ n.divisors).attach

Tactic:
rw [Finset.map_eq_image, Finset.image_image]

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ image ((fun p ↦ p.1 * p.2) ∘ Subtype.val) (m.divisors ×ˢ n.divisors).attach =
    image (⇑{ toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ }) (m.divisors ×ˢ n.divisors).attach
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = f (h ▸ ⟨k, i⟩.snd)

Tactic:
subst h
    simp only [embSigma, Embedding.sigmaMk]
    apply embDomain_apply_self

Goal state after:
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2

Tactic:
← natAbs_eq_iff_sq_eq

Goal state after:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a.natAbs = b.natAbs
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ 0 ^^^ a = a

Tactic:
LawfulXor.xor_comm,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ a ^^^ 0 = a
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(#({x ∈ Ico a b | x ≡ v [MOD r]})) = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0

Tactic:
simp_rw [← Ico_filter_modEq_cast _ _ ▸ card_map _,
    Int.Ico_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]

Goal state after:
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
rw [dropWhile]

Goal state after:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p q : α → Bool
l : List α
⊢ takeWhile p (takeWhile q l) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) l

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl IH => by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]

Goal state after:
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l

Tactic:
induction p

Goal state after:
case nil
α : Type u_1
l : List α
⊢ [].reverse = []

case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : List α
h : s.length = t.length
⊢ Shortlex r s t ↔ Lex r s t

Tactic:
by
  simp [shortlex_def, h]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ TransGen OneStep = IsDershowitzMannaLT

Tactic:
ext M N

Goal state after:
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ TransGen OneStep M N ↔ M.IsDershowitzMannaLT N
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit0

pp: case refine_2
n : PosNum
⊢ ↑n.bit0 = (↑n.bit0).minFac ↔ n = 1

Tactic:
· exact add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))

Goal state after:
case refine_2
n : PosNum
⊢ ↑n.bit0 = (↑n.bit0).minFac ↔ n = 1
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
refine if rs > delta * ls then ?_ else node (ls + rs + 1) l x r
      rcases id rr with _ | rrs
      · exact nil
      --should not happen
      rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · exact nil
      --should not happen
      exact
        if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
        else
          node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
            (node (size rlr + rrs + 1) rlr rx rr)

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
⊢ a ∈ {n ∈ range (nth p (k + 1)) | p n} → a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
ha

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ {n ∈ range (nth p (k + 1)) | p n}
⊢ a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ (n + if p (nth p n) then 1 else 0) = n + 1

Tactic:
if_pos (nth_mem _ hn)

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ n + 1 = n + 1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
rcases h with ⟨a', f', heq, h'⟩
    cases heq
    assumption

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit0) = ↑a.bit0 - ↑b.bit0

Tactic:
sub',

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bit0 = ↑a.bit0 - ↑b.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit1) = ↑a.bit0 - ↑b.bit1

Tactic:
sub',

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bitm1 = ↑a.bit0 - ↑b.bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit1.sub' b.bit0) = ↑a.bit1 - ↑b.bit0

Tactic:
sub',

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bit1 = ↑a.bit1 - ↑b.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit1.sub' b.bit1) = ↑a.bit1 - ↑b.bit1

Tactic:
sub',

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bit0 = ↑a.bit1 - ↑b.bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ZNum.ofInt' (-[0+1] + 1) = ZNum.ofInt' -[0+1] + 1

Tactic:
change ZNum.ofInt' 0 = ZNum.ofInt' (-[0+1]) + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [ofNat'_succ, ofNat'_zero]; rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
x y : F.M
h : Agree' (n✝ + 1) x y
⊢ Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
obtain - | @⟨_, a, x', y'⟩ := h

Goal state after:
case mpr.succ.step
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
x y : F.M
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : x = M.mk ⟨a, x'⟩
a✝ : y = M.mk ⟨a, y'⟩
⊢ Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).Sized

Tactic:
· exact hl.node4L hr.2.1 hr.2.2

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

Goal state before:
pp: α : Type u_1
P : α → Prop
⊢ ∀ (x : α), Emem x nil → P x

Tactic:
by rintro _ ⟨⟩

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

Goal state before:
pp: α : Type u_1
P : α → Prop
⊢ Any P nil → ∃ x, Emem x nil ∧ P x

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
by
  cases m <;> simp [node4L, all_node', All, all_node3L, and_assoc]

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
⊢ MvFunctor P.W

Tactic:
by delta MvPFunctor.W; infer_instance

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ PNat.find h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n

Tactic:
constructor
  · rintro rfl
    exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩
  · rintro ⟨hm, hlt⟩
    exact le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : lrs ≤ 1
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
sl.2.2.1,

Goal state after:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : lrl.size + lrr.size + 1 ≤ 1
⊢ lrl.size = 0 ∧ lrr.size = 0
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
b : α ⊥
⊢ ⟨⊥, ⊥⟩ ≤ ⟨⊥, b⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, b⟩

Tactic:
· exact Lex.right _ bot_le

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, 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
x : F α
⊢ TypeVec.id <$$> x = x

Tactic:
← abs_repr x,

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ TypeVec.id <$$> abs (repr x) = abs (repr x)
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:
← abs_repr x,

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> abs (repr x) = g <$$> f <$$> abs (repr x)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inr
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))

Tactic:
exact Or.inr rfl

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

Goal state before:
pp: case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)

Tactic:
exact Or.inr rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
⊢ t.Bounded o₁ o₂

Tactic:
by
    have := Bounded.dual h; rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

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

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(Sigma.P F) α), Sigma.abs F (f <$$> p) = f <$$> Sigma.abs F p

Tactic:
by rintro α β f ⟨x, g⟩; simp only [Sigma.abs, MvPFunctor.map_eq]
                simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable : ?m.286
⊢ Valid' a₁
      (match Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match Ordering.gt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      (t_l.size + t_r.size + 1)

Tactic:
constructor
        · exact Valid'.balanceL h.left t_r_valid h_balanceable
        · rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
          apply Raised.add_right
          apply Raised.add_left
          exact t_r_size

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

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
rw [← xeq, ← abs_repr u, h, ← abs_map]
      rfl

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x ↦ ⟦f x⟧⟩)))).dest = abs (Wrepr (WType.mk a f)).dest

Tactic:
rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq]

Goal state after:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x ↦ ⟦f x⟧⟩ = abs (Wrepr (WType.mk a f)).dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ih
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 α
a✝ : ∀ (i : (P F).last.B a✝¹), p (Quot.mk (⇑(wSetoid α)) (f✝ i))
⊢ p (Quot.mk (⇑(wSetoid α)) ((P F).wMk a✝¹ f'✝ f✝))

Tactic:
case ih a f' f ih =>
    change p ⟦q.P.wMk a f' f⟧
    rw [← Fix.ind_aux a f' f]
    apply h
    rw [MvQPF.liftP_iff]
    refine ⟨_, _, rfl, ?_⟩
    intro i j
    cases i
    · apply ih
    · trivial

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

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x ↦ ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal α.repeatEq ⊚ (toSubtype fun i ↦ α.RelLast' R i.fs) ⊚ dropFun c ⊚ diagSub = prod.diag

Tactic:
toSubtype_of_subtype_assoc,

Goal state after:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x ↦ ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i ↦ { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) s.destruct t.destruct

Tactic:
← LiftRelO.swap,

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (swap (LiftRelO R (LiftRel R))) s.destruct t.destruct
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case zero.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ 0 = 0 + (m + 1)

Tactic:
have : a ∈ s \ {a} := enumerate_mem sel h_sel h'

Goal state after:
case zero.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ 0 = 0 + (m + 1)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO S fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) (map f1 s).destruct
    (map f2 t).destruct

Tactic:
simp only [exists_and_left, destruct_map]
      apply Computation.liftRel_map _ _ (liftRel_destruct h)
      intro o p h
      rcases o with - | a <;> rcases p with - | b
      · simp
      · cases b; cases h
      · cases a; cases h
      · obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        exact ⟨h2 r, s, rfl, t, rfl, h⟩

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

pp: case inr.inr.inr
α : 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
dl : d ∈ val✝
⊢ ∃ 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:
case inr.inr.inr
α : 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
dl : d ∈ val✝
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
b : α ⊤
⊢ ⟨⊤, b⟩ ≤ ⟨⊤, ⊤⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
· exact Lex.right _ _ le_top

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : 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)) μ ν
⊢ μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3 → μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε

Tactic:
ha

Goal state after:
α : 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
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ n * f) = ↑(n + 1) * τ f

Tactic:
translationNumber_mul_of_commute (Commute.pow_self f n),

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ n) + τ f = ↑(n + 1) * τ f