mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → ↑X.toLightCondSet.toTopCat :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ ⇑(OnePoint.continuousMapMkNat f p h)
x : X.toLightCondSet.obj.obj (Opposite.op ℕ∪{∞}) := OnePoint.continuousMapMkNat f p h
⊢ Continuous g

Tactic:
exact continuous_coinducingCoprod X.toLightCondSet x

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : Profinite
inst✝¹ : Nonempty ↑S.toTop
inst✝ : Finite ↑S.toTop
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
this : ∀ (T : Profinite) [Nonempty ↑T.toTop], IsSplitEpi (CompHausLike.isTerminalPUnit.from T)
⊢ ∃ h, f ≫ h = g

Tactic:
obtain ⟨k, _, h2⟩ := exists_lift_of_finite_of_mono_of_epi f
        (CompHausLike.isTerminalPUnit.from S) g (CompHausLike.isTerminalPUnit.from Y)
      (CompHausLike.isTerminalPUnit.hom_ext _ _)

Goal state after:
S : Profinite
inst✝¹ : Nonempty ↑S.toTop
inst✝ : Finite ↑S.toTop
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
this : ∀ (T : Profinite) [Nonempty ↑T.toTop], IsSplitEpi (CompHausLike.isTerminalPUnit.from T)
k : Y ⟶ S
left✝ : k ≫ CompHausLike.isTerminalPUnit.from S = CompHausLike.isTerminalPUnit.from Y
h2 : f ≫ k = g
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))

Tactic:
continuous_coinduced_dom

Goal state after:
X Y : CondensedSet
f : X ⟶ Y
⊢ Continuous (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ CondensedSet.coinducingCoprod✝ X)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
⊢ Continuous fun x ↦ x.toFun PUnit.unit

Tactic:
continuous_coinduced_dom

Goal state after:
X✝ : CondensedSet
X : TopCat
⊢ Continuous ((fun x ↦ x.toFun PUnit.unit) ∘ CondensedSet.coinducingCoprod✝ X.toCondensedSet)
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x

Tactic:
refine (comp_traverse (pure ∘ f) g x).symm.trans ?_

Goal state after:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)

Tactic:
suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val by
      rw [this]
      exact (measure _).wf
    ext ⟨a, ha⟩ ⟨b, _⟩
    dsimp [InvImage, Upto.GT]
    rw [tsub_lt_tsub_iff_left_of_le (le_of_not_gt fun h' => ha _ h' h)]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
⊢ ∀ (x y : FreeMonoid α),
    flip (List.foldrM f) (FreeMonoid.toList (x * y)) =
      flip (List.foldrM f) (FreeMonoid.toList x) * flip (List.foldrM f) (FreeMonoid.toList y)

Tactic:
by intros; funext; apply List.foldrM_append

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ toSubtype p ⊚ ofSubtype p ⊚ f = f

Tactic:
by
  rw [← comp_assoc, toSubtype_of_subtype]; simp

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

Goal state before:
pp: case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
⊢ ⨅ i, ∑ a ∈ Finset.cons a s ha, f i a = ∑ a ∈ Finset.cons a s ha, ⨅ i, f i a

Tactic:
| cons a s ha ih =>

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
⊢ ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ e

Tactic:
intro X Y p hp S f

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₀ l₁ : List (Sigma β)
nd₀ : l₀.NodupKeys
nd₁ : l₁.NodupKeys
h : ∀ (x : α) (y : β x), y ∈ dlookup x l₀ ↔ y ∈ dlookup x l₁
⊢ l₀ ~ l₁

Tactic:
grind [_=_ mem_dlookup_iff, mem_ext]

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π' = 𝟙 (S' ⊗ ℕ∪{∞})

Tactic:
by ext x; all_goals exact h.elim x

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

Goal state before:
pp: α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ sizeOf (a :: l) ≤ sizeOf (a :: r)

Tactic:
rw [cons.sizeOf_spec, cons.sizeOf_spec]
  exact Nat.add_le_add_iff_left.mpr h

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
⊢ Finset α

Tactic:
by
    haveI := Classical.decEq α; haveI := Classical.decEq M
    exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
a✝ : b ∈ (Finset.range d).attach
⊢ b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Tactic:
(hbi : b ≠ ⟨i, _⟩)

Goal state after:
case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
a✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ (bif !false then 1 else 0) + 2 * -[n+1].div2 = -[false.toNat + 2 * n.div2+1]

Tactic:
dsimp [cond, not, div2, Int.mul]

Goal state after:
case false
n : ℕ
⊢ 1 + 2 * -[n.div2+1] = -[0 + 2 * n.div2+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case true
n : ℕ
⊢ (bif !true then 1 else 0) + 2 * -[n+1].div2 = -[true.toNat + 2 * n.div2+1]

Tactic:
dsimp [cond, not, div2, Int.mul]

Goal state after:
case true
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ ↑|a|.toNat ≤ sqrt ↑b.toNat ↔ ↑|a|.toNat * ↑|a|.toNat ≤ ↑b.toNat

Tactic:
Int.sqrt_natCast,

Goal state after:
a b : ℤ
hn : 0 ≤ b
⊢ ↑|a|.toNat ≤ ↑b.toNat.sqrt ↔ ↑|a|.toNat * ↑|a|.toNat ≤ ↑b.toNat
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true

Tactic:
by
  rw [rtakeWhile, mem_reverse] at hx
  exact mem_takeWhile_imp hx

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

Goal state before:
pp: n : ℕ
⊢ range' 0 (n - 0) = range n

Tactic:
Nat.sub_zero,

Goal state after:
n : ℕ
⊢ range' 0 n = range n
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
by
  rw [List.getElem_take' (hj := i.lt_add_one)]
  simp only [take_splitLength]
  conv_rhs =>
    rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
match l, h with
  | a::l, h => apply isChain_of_mem_splitByLoop _ _ h <;> simp

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)

Tactic:
by
  let z := chineseRemainderOfList a s l' (co.perm hl coprime_comm.mpr)
  have hlp : (l.map s).prod = (l'.map s).prod := List.Perm.prod_eq (List.Perm.map s hl)
  exact (chineseRemainderOfList_modEq_unique a s l co (z := z)
    (fun i hi => z.prop i (hl.symm.mem_iff.mpr hi))).symm.eq_of_lt_of_lt
      (chineseRemainderOfList_lt_prod _ _ _ _ hs)
      (by rw [hlp]
          exact chineseRemainderOfList_lt_prod _ _ _ _
            (by simpa [List.Perm.mem_iff hl.symm] using hs))

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ↑(k - multiplicity n.minFac (n.minFac ^ (k - 1))) < ↑2

Tactic:
multiplicity_pow_self_of_prime (prime_iff.mp isPrime)

Goal state after:
case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ↑(k - (k - 1)) < ↑2
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
hf : (Set.ofPred p).Finite
ha : #⋯.toFinset ≤ a
⊢ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b

Tactic:
exact ⟨hf, ha.trans hab⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(neg p) = ↑(neg p)

Tactic:
by rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]

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

Goal state before:
pp: P : PFunctor.{uA, uB}
p : ↑P P.W
⊢ (mk p).dest = p

Tactic:
cases p; rfl

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

Goal state before:
pp: P : PFunctor.{uA, uB}
p : P.W
⊢ mk p.dest = p

Tactic:
cases p; rfl

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

Goal state before:
pp: case neg.inr.refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ l.size ≤ delta * ml.size

Tactic:
refine (mul_le_mul_iff_right₀ (by decide)).1 (le_trans this ?_)

Goal state after:
case neg.inr.refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ ml.size + mr.size + 1 ≤ 2 * (delta * ml.size)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit1).2 + ↑d * ↑(d.divModAux q r.bit1).1 = ↑n.bit1 ∧ ↑(d.divModAux q r.bit1).2 < ↑d

Tactic:
apply divMod_to_nat_aux

Goal state after:
case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit1 + ↑d * (↑q + ↑q) = ↑n.bit1

case bit1.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit1 < 2 * ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit0).2 + ↑d * ↑(d.divModAux q r.bit0).1 = ↑n.bit0 ∧ ↑(d.divModAux q r.bit0).2 < ↑d

Tactic:
apply divMod_to_nat_aux

Goal state after:
case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 + ↑d * (↑q + ↑q) = ↑n.bit0

case bit0.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 < 2 * ↑d
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
simp [node4L, all_node', All, all_node3L, and_assoc]

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

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

Tactic:
simp [node4L, all_node', All, all_node3L, and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

Tactic:
cases cmpLE x y <;>
      simp [Ordering.swap, dual_balanceL, dual_balanceR, dual_insert]

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
rcases gxeq : g x with ⟨a, f'⟩

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
hs : u.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
dsimp [IsSpecial, finish] at hs ⊢

Goal state after:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
hs : u.IsSpecial
⊢ u.step.IsSpecial

Tactic:
by
  dsimp [IsSpecial, step] at hs ⊢
  rw [mul_add, mul_comm u.y u.x, ← hs]
  ring

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ l', Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ r', Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ l', Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ r', Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Raised (l.size + r.size + 1) (l.size + (insertWith f x r).size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_h : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_r_h

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
⊢ ∀ (a b : (P F).M), Mcongr a b → Quot.mk Mcongr <$> abs a.dest = Quot.mk Mcongr <$> abs b.dest

Tactic:
rintro x y ⟨r, pr, rxy⟩
      have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, h⟩
      rw [← Quot.factor_mk_eq _ _ this]
      conv =>
        lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]

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
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
| LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) (MvQPF.repr ∘ dest)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
congr; rfl; rw [Cofix.dest]

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
| (TypeVec.id ::: Quot.mk Mcongr) <$$>
    (TypeVec.id :::
        M.corec (P F)
          (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) <$$>
      Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝)

case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ : (P F).M α
| (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')

Tactic:
apply ret_mem

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

Goal state before:
pp: case 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✝)
a : α
h : c.destruct = Sum.inl a
⊢ a ∈ pure a

Tactic:
apply ret_mem

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

Goal state before:
pp: case 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✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (Sum.inl a)

Tactic:
refine ⟨c, List.mem_cons_self, ?_⟩
          rw [destruct_eq_pure h]
          apply ret_mem

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
    · obtain ⟨k, hi, hj⟩ := exists_between h
      obtain ⟨c⟩ : Nonempty (α k) := inferInstance
      exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

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

Goal state before:
pp: n : ℕ
c : Char
x✝ : String
s : String := x✝
⊢ x✝.IsSuffix (leftpad n c x✝)

Tactic:
by simp [leftpad, IsSuffix]

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

Goal state before:
pp: case cons
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
x✝ : α
s✝ : WSeq α
h : c1 = ((cons x✝ s✝).append t).destruct ∧ c2 = (cons x✝ s✝).destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x✝ s✝).append t).destruct.destruct ((cons x✝ s✝).destruct.bind (destruct_append.aux t)).destruct

pp: case think
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s✝ : WSeq α
h : c1 = (s✝.think.append t).destruct ∧ c2 = s✝.think.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s✝.think.append t).destruct.destruct (s✝.think.destruct.bind (destruct_append.aux t)).destruct

Tactic:
case cons => simp

Goal state after:
case think
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s✝ : WSeq α
h : c1 = (s✝.think.append t).destruct ∧ c2 = s✝.think.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s✝.think.append t).destruct.destruct (s✝.think.destruct.bind (destruct_append.aux t)).destruct