mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: case refine_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ p ⟨↑n, ⋯⟩

pp: case refine_3
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
m : ℕ+
hm : m < ⟨↑n, ⋯⟩
pm : p m
⊢ False

Tactic:
· obtain ⟨n', hn', pn'⟩ := n.prop.1
    simpa [hn', Subtype.coe_eta] using! pn'

Goal state after:
case refine_3
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
m : ℕ+
hm : m < ⟨↑n, ⋯⟩
pm : p m
⊢ False
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ #(Ioc a b) = #(Ioc ↑a ↑b)

Tactic:
← map_subtype_embedding_Ioc,

Goal state after:
a b : ℕ+
⊢ #(Ioc a b) = #(map (Embedding.subtype fun n ↦ 0 < n) (Ioc a b))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
    ls + rs

Tactic:
rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.2.1]

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).size + (Ordnode.node rs rl rx rr).size = ll.size + lr.size + 1 + rs
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos.node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
rd : delta ≤ (node rls rll rlx rlr).size + nil.size
⊢ (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx nil) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx nil
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx nil))
          nil)
      (node rls rll rlx rlr)

Tactic:
exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)

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

Goal state before:
pp: case H2.inl.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
l' : ℕ
e : Raised l' l.size
H : l' + r.size ≤ 1
⊢ r.size ≤ delta * l.size

pp: case H2.inl.inr
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
l' : ℕ
e : Raised l' l.size
left✝ : l' ≤ delta * r.size
H₂ : r.size ≤ delta * l'
⊢ r.size ≤ delta * l.size

pp: case H2.inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
⊢ r.size ≤ delta * l.size

pp: case H2.inr.inr
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
left✝ : l.size ≤ delta * r'
H₂ : r' ≤ delta * l.size
⊢ r.size ≤ delta * l.size

Tactic:
· exact le_trans (le_trans (Nat.le_add_left _ _) H) (mul_pos (by decide) l1 : (0 : ℕ) < _)

Goal state after:
case H2.inl.inr
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
l' : ℕ
e : Raised l' l.size
left✝ : l' ≤ delta * r.size
H₂ : r.size ≤ delta * l'
⊢ r.size ≤ delta * l.size

case H2.inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
⊢ r.size ≤ delta * l.size

case H2.inr.inr
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
left✝ : l.size ≤ delta * r'
H₂ : r' ≤ delta * l.size
⊢ r.size ≤ delta * l.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
⊢ (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r

Tactic:
ext x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
x : (P F).M α
⊢ (Quot.mk r' ∘ fun x ↦ g <$$> x) x = (u ∘ Quot.mk r) x
Module: Mathlib.Data.QPF.Multivariate.Basic

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

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

Tactic:
· intro h α a a' f f' h' i
    rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ IsUniform → SuppPreservation
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

Tactic:
constructor <;> intros <;> subst_vars

Goal state after:
case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)

case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
⊢ Wequiv x y

Tactic:
by
  cases x
  cases y
  apply Wequiv.abs
  apply h

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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (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), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ (g₁ ∘ fun x ↦ ⟦f x⟧) = g₂ ∘ fun x ↦ ⟦f x⟧

Tactic:
ext x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (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), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
x : (P F).last.B a
⊢ (g₁ ∘ fun x ↦ ⟦f x⟧) x = (g₂ ∘ fun x ↦ ⟦f x⟧) x
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
ext x

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h 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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
⊢ rec g = h

Tactic:
ext x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
⊢ (fun x ↦ f <$> abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩) = fun x ↦
    abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                    B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                f ⟨⟨b, h⟩, g⟩).fst.snd
          x,
        fun y ↦
        ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨⟨b, h⟩, g⟩).snd
          ⟨x, y⟩⟩

Tactic:
ext x

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
x : (P F₂).B b
⊢ f <$> abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩ =
    abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                    B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                f ⟨⟨b, h⟩, g⟩).fst.snd
          x,
        fun y ↦
        ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨⟨b, h⟩, g⟩).snd
          ⟨x, y⟩⟩
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ a, parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
obtain ⟨a, e⟩ := e

Goal state after:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Set.Finite.Monad

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(f.seq s)

Tactic:
rw [seq_def]
  infer_instance

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

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

Tactic:
intro s m

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

Goal state before:
pp: case h2
α : 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 α}, s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
intro s m

Goal state after:
case h2
α : 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.destruct = c.think
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.inr
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (cons a' s').get? (n + 1)

Tactic:
simpa [get?]

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : ?m.31
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Tactic:
rw [finsum_def, dif_pos hs']

Goal state after:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ s.ncard = ∑ i ∈ Set.Finite.toFinset hs', (s ∩ ↑i).ncard
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b

Tactic:
obtain ⟨i, a⟩ := a
    obtain ⟨j, b⟩ := b
    rintro ⟨rfl : i = j, h⟩
    exact LT.fiber _ _ _ h

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

Goal state before:
pp: l : List Char
h : ofList [] ≠ ""
⊢ (ofList []).toList = Legacy.front (ofList []) :: (Legacy.drop (ofList []) 1).toList

Tactic:
simp at h

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (node v l r) =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g (node v l r))

Tactic:
| node v l r hl hr =>

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ traverse (pure ∘ f) (node v l r) = pure (map f (node v l r))

Tactic:
| node v l r hl hr =>

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α} ↦ η.app α) (traverse f (node v l r)) = traverse (η.app β ∘ f) (node v l r)

Tactic:
| node v l r hl hr =>

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g) (map f s)).join.join ~ʷ (map ((fun y ↦ (map g y).join) ∘ f) s).join

Tactic:
← map_comp f (map g),

Goal state after:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map ((fun y ↦ (map g y).join) ∘ f) s).join
Module: Mathlib.Data.Sum.Interval

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

Tactic:
obtain a | a := a <;> obtain b | b := b

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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) →
    (∃ 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₂

case mp.inl.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 : β₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) →
    (∃ 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₂

case mp.inr.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 : β₁
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inl b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

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 : β₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) →
    (∃ 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₂
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
x✝ : ∃ i h, v.toList.get ⟨i, h⟩ = a
i : ℕ
hi : i < v.toList.length
h : v.toList.get ⟨i, hi⟩ = a
⊢ i < n

Tactic:
rwa [toList_length] at hi

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: f : Natβ Natα.zero → WType Natβ
⊢ Empty.elim = f

Tactic:
ext x

Goal state after:
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ x.elim = f x
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f

Tactic:
ext x

Goal state after:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty.{u + 1}
⊢ x.elim = f x
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ Dense
      (⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) ⁻¹'
        ↑(AddSubgroup.zmultiples ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) a))) ↔
    Dense ↑(AddSubgroup.closure {a, p})

Tactic:
← AddSubgroup.coe_comap,

Goal state after:
a p : ℝ
⊢ Dense
      ↑(AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
          (AddSubgroup.zmultiples ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) a))) ↔
    Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense (⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) ⁻¹' ↑s)
⊢ ∃ a, s = AddSubgroup.zmultiples a

Tactic:
← AddSubgroup.coe_comap,

Goal state after:
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense ↑(AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s)
⊢ ∃ a, s = AddSubgroup.zmultiples a
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
⊢ ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0

Tactic:
rw [Nat.frequently_atTop_iff_infinite, not_infinite] at H

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
⊢ ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
j : ℕ
⊢ addOrderOf (u j) = n.natAbs ^ j

Tactic:
convert!
          addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)

Goal state after:
case e'_4
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
j : ℕ
⊢ 1 = ↑1