mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
f₁ : F.B a₀ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)
h' : f' i = M.mk ⟨a₀, f₁⟩
⊢ IsPath ps (M.mk ⟨a₀, f₀⟩) ∨ IsPath ps (M.mk ⟨a₀, f₁⟩)

Tactic:
← h,

Goal state after:
case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
f₁ : F.B a₀ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)
h' : f' i = M.mk ⟨a₀, f₁⟩
⊢ IsPath ps (f i) ∨ IsPath ps (M.mk ⟨a₀, f₁⟩)
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
⊢ Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
    ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs

pp: case neg
α : 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
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs

Tactic:
· rw [splitMax_eq]
    · obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl
      suffices H : _ by
        refine ⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩
        · refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)
          exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)
        · exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2
        · rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.2.1]; rfl
      refine Or.inl ⟨_, Or.inr e, ?_⟩
      rwa [hl.2.eq_node'] at bal

Goal state after:
case neg
α : 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
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.gcd m).factorMultiset.prod = n.gcd m

Tactic:
PNat.prod_factorMultiset

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ n.gcd m = n.gcd m
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.lcm m).factorMultiset.prod = n.lcm m

Tactic:
PNat.prod_factorMultiset

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ n.lcm m = n.lcm m
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
· rintro ⟨⟨j, b, hij⟩ | ⟨i, hab⟩, hba⟩
        · exact Lex.left _ _ hij
        · exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

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

Goal state before:
pp: u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + u.y * u.x

Tactic:
mul_comm u.y u.x,

Goal state after:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + u.x * u.y
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]; rfl

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

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t ↦ (↑t).2) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = y

Tactic:
rw [yeq, ← abs_map]

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp ⟨a, f⟩ i = supp ⟨a', f'⟩ i

Tactic:
← h,

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp (abs ⟨a, f⟩) i = supp ⟨a', f'⟩ i
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1.e_g
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀✝ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁✝ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀✝) ((P F).wMk a₁ f'₁ f₁✝)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
_h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)
⊢ recF u ∘ f₀ = recF u ∘ f₁

Tactic:
funext

Goal state after:
case refine_1.e_g
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀✝ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁✝ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀✝) ((P F).wMk a₁ f'₁ f₁✝)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
_h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)
x✝ : ((P F).B a).last
⊢ (recF u ∘ f₀) x✝ = (recF u ∘ f₁) x✝
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ abs ⟨a₀, (P F).appendContents (g ⊚ f'₀) fun i ↦ g <$$> f₀ i⟩ =
    abs ⟨a₁, (P F).appendContents (g ⊚ f'₁) fun i ↦ g <$$> f₁ i⟩

Tactic:
change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))

Goal state after:
case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ abs ((P F).objAppend1 a₀ (g ⊚ f'₀) fun x ↦ (P F).wMap g (f₀ x)) =
    abs ((P F).objAppend1 a₁ (g ⊚ f'₁) fun x ↦ (P F).wMap g (f₁ x))
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
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
intro x
  rcases x; clear x; rename M (P F) α => x
  intro y
  rcases y; clear y; rename M (P F) α => y
  intro rxy
  apply Quot.sound
  let r' := fun x y => r (Quot.mk _ x) (Quot.mk _ y)
  have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := rfl
  have : IsPrecongr r' := by
    intro a b r'ab
    have h₀ :
      appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P a) =
        appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P b) := by
      rw [appendFun_comp_id, comp_map, comp_map]; exact h _ _ r'ab
    have h₁ : ∀ u v : q.P.M α, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      dsimp [r', hr']
      rw [Quot.sound cuv]
      apply h'
    let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁)
        (by
          intro c
          apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
          clear c
          intro c d
          apply Quot.inductionOn
            (motive := fun d => r (Quot.mk Mcongr c) d →
              Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
          clear d
          intro d rcd; apply Quot.sound; apply rcd)
    have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
    rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map,
      h₀]
  exact ⟨r', this, rxy⟩

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 α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ g (((TypeVec.id ::: recF g) ⊚ (TypeVec.id ::: fixToW)) <$$> abs ⟨a, f⟩) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
← h,

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 α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr x = ⟨a, f⟩
⊢ g (((TypeVec.id ::: recF g) ⊚ (TypeVec.id ::: fixToW)) <$$> abs (repr x)) = g ((TypeVec.id ::: rec g) <$$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

Tactic:
rw [yeq, ← abs_map]

Goal state after:
case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ((P F).map (fun t ↦ (↑t).2) ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ g ((recF g ∘ fixToW) <$> abs ⟨a, f⟩) = g (rec g <$> x)

Tactic:
← h,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ g ((recF g ∘ fixToW) <$> abs (repr x)) = g (rec g <$> x)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

pp: case inr.inl
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
· exact Or.inl <| sign_of_neg hn

Goal state after:
case inr.inl
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1

case inr.inr
r : ℝ
hp : 0 < r
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
Module: Mathlib.Data.Rat.Star

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

pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

pp: case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

pp: case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Tactic:
one_pow,

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

n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case ha
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ ↑x.den ≠ 0

case h
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ closure (range fun x ↦ x ^ n) = nonneg ℚ

Tactic:
convert! (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm

Goal state after:
case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n

case e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x ↦ x ^ n))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp ⟨a, f⟩ = supp ⟨a', f'⟩

Tactic:
← h,

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp (abs ⟨a, f⟩) = supp ⟨a', f'⟩
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
s : WSeq α
a : α
h : some a ∈ s.get? 0
⊢ ∃ a', some a' ∈ s.head

Tactic:
exact ⟨_, h⟩

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

Goal state before:
pp: case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s

Tactic:
· intro s'
    apply Equiv.trans
    simp [think_equiv]

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

Goal state before:
pp: case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
injection oe with h'

Goal state after:
case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
h' : f a = b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case hj
α : 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
x : α
⊢ x ∈ ↑hs.toFinset → (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩) x ∈ ↑(⋯.toFinset.sigma fun t ↦ ⋯.toFinset)

Tactic:
simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]

Goal state after:
case hj
α : 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
x : α
⊢ x ∈ s → Nat.card ↑(s ∩ ⋯.choose) ≠ 0 ∧ x ∈ s ∧ x ∈ ⋯.choose
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case left_inv
α : 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
t : ↑P
x y : α
hy : y ∈ s
⊢ y ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t

Tactic:
hyt

Goal state after:
case left_inv
α : 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
t : ↑P
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
⊢ Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
⊢ F l (parallel.aux2 l) →
    rmap (corec parallel.aux1)
          (rmap
            (fun l' ↦
              match Seq.destruct S with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S'))
            (parallel.aux2 l)) =
        Sum.inl a →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases parallel.aux2 l with a' | l'

Goal state after:
case h1.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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
⊢ F l (Sum.inl a') →
    rmap (corec parallel.aux1)
          (rmap
            (fun l' ↦
              match Seq.destruct S with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S'))
            (Sum.inl a')) =
        Sum.inl a →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h1.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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
l' : List (Computation α)
⊢ F l (Sum.inr l') →
    rmap (corec parallel.aux1)
          (rmap
            (fun l' ↦
              match Seq.destruct S with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S'))
            (Sum.inr l')) =
        Sum.inl a →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
⊢ F l (parallel.aux2 l) →
    rmap (corec parallel.aux1)
          (rmap
            (fun l' ↦
              match Seq.destruct S with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S'))
            (parallel.aux2 l)) =
        Sum.inr C' →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases parallel.aux2 l with a' | l'

Goal state after:
case h2.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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
a' : α
⊢ F l (Sum.inl a') →
    rmap (corec parallel.aux1)
          (rmap
            (fun l' ↦
              match Seq.destruct S with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S'))
            (Sum.inl a')) =
        Sum.inr C' →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2.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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
⊢ F l (Sum.inr l') →
    rmap (corec parallel.aux1)
          (rmap
            (fun l' ↦
              match Seq.destruct S with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S'))
            (Sum.inr l')) =
        Sum.inr C' →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.String.Basic

Goal state before:
pp: s₁ s₂ : String
⊢ ¬s₂.toList < s₁.toList ↔ s₁.toList ≤ s₂.toList

Tactic:
not_lt

Goal state after:
s₁ s₂ : String
⊢ s₁.toList ≤ s₂.toList ↔ s₁.toList ≤ s₂.toList
Module: Mathlib.Data.String.Basic

Goal state before:
pp: a b : String
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by
    simp only [lt_iff_toList_lt, le_iff_toList_le, lt_iff_le_not_ge]

Goal state after: