mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) = f

Tactic:
funext r

Goal state after:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) r = f r
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)

Tactic:
simp [Equiv.map, Function.comp_def]

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : t' α
⊢ (fun {α} ↦ η.app α) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
simp only [Equiv.traverse, functor_norm]

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: case succ
w : ℕ
x : BitVec w
n : ℕ
ih : (x ^ n).toFin = x.toFin ^ n
⊢ (x ^ (n + 1)).toFin = x.toFin ^ (n + 1)

Tactic:
simp [ih, BitVec.pow_succ]

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
a b : τ
x : α
h : x ∈ f (E.symm a) ∩ f (E.symm b)
⊢ x ∈ f (E.symm (E (I (E.symm a) (E.symm b) x h)))

Tactic:
simpa using h₂ (E.symm a) (E.symm b) x h

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
rintro ⟨s, t, h⟩
        apply mem_inf_of_inter _ _ h
        · use s
        · use t

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => F.F.f s ∩ G.F.f t,
        pt := (F.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (F.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g

Tactic:
cases F; cases G; subst f g; simp only [CFilter.toFilter, Prod.exists]; ext
      constructor
      · rintro ⟨s, t, h⟩
        apply mem_inf_of_inter _ _ h
        · use s
        · use t
      · rintro ⟨_, ⟨a, ha⟩, _, ⟨b, hb⟩, rfl⟩
        exact ⟨a, b, inter_subset_inter ha hb⟩

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0

Tactic:
exact zero_mem_zero

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s

Tactic:
by
  refine ⟨congr_arg _, fun h => ?_⟩
  obtain ⟨_, v₁⟩ := q₁; obtain ⟨_, v₂⟩ := q₂; congr
  exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂

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

Goal state before:
pp: α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ (s :: l).NodupKeys ↔ ¬s.fst ∈ l.keys ∧ l.NodupKeys

Tactic:
simp [keys, NodupKeys]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: tl = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
rw [h₂]; rfl

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ l ↔ ∃ f ∈ l, x ∈ f.support

Tactic:
by
  simp only [Finset.sup_eq_union, Finsupp.mem_support_iff]
  induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
      mem_cons, exists_eq_or_imp]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
⊢ f.embSigma.support = Finset.map (Embedding.sigmaMk k) f.support

Tactic:
by
  simp [embSigma]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
⊢ embSigma 0 = 0

Tactic:
by
  simp [embSigma]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
⊢ f.embSigma = 0 ↔ f = 0

Tactic:
by
  simp [embSigma]

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

Goal state before:
pp: x a : ℤ
⊢ fib (x + a) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))

Tactic:
rw [add_comm x]
      simp only [two_mul, fib_add, fib_one, mul_one, reduceAdd, fib_two, ← add_sub, sub_add_cancel]
      ring

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)

Tactic:
by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Tactic:
by_cases hp : p x <;> simp [hp]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]

Tactic:
← nil_append [x],

Goal state after:
α : Type u_1
p : α → Bool
x : α
⊢ rdropWhile p ([] ++ [x]) = if p x = true then [] else [] ++ [x]
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]

Tactic:
rwa [← succ_singleton, append_consecutive]

Goal state after:
case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inl
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h1 : p.length < (xa :: xb).length
⊢ Acc (Shortlex r) p

pp: case intro.intro.inr
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
⊢ Acc (Shortlex r) p

Tactic:
· exact ih _ h1

Goal state after:
case intro.intro.inr
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
⊢ Acc (Shortlex r) p
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ v[j]? = v[j + p]?

Tactic:
have shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]? := by
    rw [getElem?_append_right, Nat.add_sub_cancel, getElem?_append_left]
    all_goals lia

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
⊢ v[j]? = v[j + p]?
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 x2 : Matrix m₁ n R
y1 y2 : Matrix m₂ n R
⊢ x1.fromRows y1 = x2.fromRows y2 → x1 = x2 ∧ y1 = y2

Tactic:
simp [← Matrix.ext_iff]

Goal state after:
Module: Mathlib.Data.NNRat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, cast_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ∑ i ∈ s, f i = ∑ a ∈ s, ↑(f a).toNNRat
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ n = 0 → n.greatestFib = 0

Tactic:
rintro rfl; rfl

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
· simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

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

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun x ↦ id x + m
⊢ False

Tactic:
id_eq,

Goal state after:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun x ↦ x + m
⊢ False
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (ofNat' n + 1).toZNum = (ofNat' n).toZNum + 1

Tactic:
Num.add_one,

Goal state after:
n : ℕ
⊢ (ofNat' n).succ.toZNum = (ofNat' n).toZNum + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1

Tactic:
Num.add_one,

Goal state after:
n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (ofNat' n + 1).toZNumNeg = (ofNat' n + 1).toZNumNeg.pred + 1

Tactic:
Num.add_one,

Goal state after:
n : ℕ
⊢ (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg.pred + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n + 1).toZNum = ZNum.ofInt' ↑(n + 1)

Tactic:
Num.add_one,

Goal state after:
n : ℕ
⊢ (↑n).succ.toZNum = ZNum.ofInt' ↑(n + 1)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
A : Type u
α : TypeVec.{u} n
x : ↑(const n A) α
⊢ mk n (get x) = x

Tactic:
by
  cases x
  dsimp [const.get, const.mk]
  congr with (_⟨⟩)

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

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (Num.ofNat' n + 1).toZNum = (Num.ofNat' n).toZNum + 1

Tactic:
Num.add_one,

Goal state after:
α : Type u_1
n : ℕ
⊢ (Num.ofNat' n).succ.toZNum = (Num.ofNat' n).toZNum + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ -(↑n + 1).toZNumNeg = ↑(n + 1)

Tactic:
Num.add_one,

Goal state after:
n : ℕ
⊢ -(↑n).succ.toZNumNeg = ↑(n + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ foldr List.cons l (x :: foldr List.cons r r') = (node size✝ l x r).toList ++ r'

Tactic:
foldr_cons_eq_toList l,

Goal state after:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ l.toList ++ x :: foldr List.cons r r' = (node size✝ l x r).toList ++ r'
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
⊢ a = a'

Tactic:
rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
⊢ R (f i) (f' i)

Tactic:
rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩

Goal state after:
case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)
Module: Mathlib.Data.PNat.Factors

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

Tactic:
Multiset.map_id

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

Goal state before:
pp: case pos
α : 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
⊢ (∃ 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'

Tactic:
refine Or.inl ⟨_, Or.inr e, ?_⟩

Goal state after:
case pos
α : 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
⊢ BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hba : b ≤ a
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∨ ⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
· exact Or.inr (Lex.right _ hba)

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

Goal state before:
pp: u : XgcdType
⊢ u.finish.IsReduced

Tactic:
dsimp [IsReduced]

Goal state after:
u : XgcdType
⊢ u.finish.ap = u.finish.bp
Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp

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

Tactic:
intros
    simp only [(· ∘ ·)]
    rw [← abs_map]
    simp +unfoldPartialApp only [comp.get_map, map_map, TypeVec.comp,
      abs_map, map_mk]

Goal state after:
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₂
⊢ ∀ (a b : (P F).M α), r a b → Quot.mk r' (g <$$> a) = Quot.mk r' (g <$$> b)

Tactic:
intro a₁ a₂ ra₁a₂

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₂✝
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
⊢ Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
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 := ⋯
⊢ IsPrecongr r'

Tactic:
show IsPrecongr r'
        rintro b₁ b₂ ⟨a₁, a₂, ra₁a₂, b₁eq, b₂eq⟩
        let u : Quot r → Quot r' :=
          Quot.lift (fun x : q.P.M α => Quot.mk r' (g <$$> x))
            (by
              intro a₁ a₂ ra₁a₂
              apply Quot.sound
              exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩)
        have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r := by
          ext x
          rfl
        rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]
        rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_comp]
        rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]

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 : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : (P F).W α
⊢ (recF g ∘ fixToW) ⟦x⟧ = rec g ⟦x⟧

Tactic:
apply recF_eq_of_wEquiv

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : (P F).W α
⊢ WEquiv (fixToW ⟦x⟧) x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → mk (mk x).dest = id (mk x)

Tactic:
id_eq,

Goal state after:
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → mk (mk x).dest = mk x
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n

Tactic:
rw [nsmul_eq_mul]

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑(x.num * x.den ^ (n - 1)) * (↑x.den)⁻¹ ^ n
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ aux n none = Computation.pure none

Tactic:
drop.aux_none n

Goal state after:
α : Type u
n : ℕ
⊢ Computation.pure none = Computation.pure none
Module: Mathlib.Data.Set.Finite.List

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite

Tactic:
by
  convert! (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i; ext; simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : swap (LiftRel fun x y ↦ R y x) s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b

Tactic:
exact exists_of_liftRel_left H h

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

Goal state before:
pp: α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ cons a s ~ʷ cons a t

Tactic:
unfold Equiv

Goal state after:
α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ LiftRel Eq (cons a s) (cons a t)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think ~ʷ s

Tactic:
unfold Equiv

Goal state after:
α : Type u
s : WSeq α
⊢ LiftRel Eq s.think s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.think ~ʷ t.think

Tactic:
unfold Equiv

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ LiftRel Eq s.think t.think
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get 0 → a ∈ s

Tactic:
intro s m e

Goal state after:
case zero
α : Type u
a : α
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail).get 0
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get (n✝ + 1) → a ∈ s

Tactic:
intro s m e

Goal state after:
case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail).get (n✝ + 1)
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s

Tactic:
rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
    rcases o with - | o
    · injection h2
    injection h2 with h'
    obtain ⟨a', s'⟩ := o
    exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)

Goal state after: