mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.ZNum

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

Tactic:
rw [sub', ZNum.cast_bit1, cast_sub' a b]

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑m * ↑↑n = ↑m * ↑n

Tactic:
cast_to_int

Goal state after:
α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑m * ↑n = ↑m * ↑n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)

Tactic:
simpa using

Goal state after:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by
  rw [← not_lt]; exact not_congr cast_lt

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

Goal state before:
pp: case bit0.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 < 2 * ↑d

Tactic:
simpa using

Goal state after:
case bit0.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r < ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos
a✝ : PosNum
⊢ (pos a✝).mod 0 = pos a✝

Tactic:
simp [Num.mod]

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

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑(Num.pos n % d.abs) = ↑(pos n) % ↑d

Tactic:
← Num.to_nat_to_int,

Goal state after:
n : PosNum
d : ZNum
⊢ ↑↑(Num.pos n % d.abs) = ↑(pos n) % ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d

Tactic:
← Num.to_nat_to_int,

Goal state after:
n : PosNum
d : ZNum
⊢ ↑↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑↑d.abs - ↑(n.pred' % d.abs).succ = -↑n % ↑d

Tactic:
← Num.to_nat_to_int,

Goal state after:
n : PosNum
d : ZNum
⊢ ↑↑d.abs - ↑↑(n.pred' % d.abs).succ = -↑n % ↑d
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rw [Nat.mul_succ]
    exact le_trans (Nat.dist_tri_right' _ _) (add_le_add h₂ (le_trans hr (by decide)))

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 α
⊢ (Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual

Tactic:
have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl
    rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]
    cases cmpLE x y <;>
      simp [Ordering.swap, dual_balanceL, dual_balanceR, dual_insert]

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

Goal state before:
pp: case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ n.factorMultiset

Tactic:
rw [← mul_div_exact h, factorMultiset_mul]

Goal state after:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * (u.r - 1 + 1) = u.y * ↑u.a + ↑u.z * ↑u.b

Tactic:
rw [← ha, hr]

Goal state after:
case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * u.r = u.y * (u.r + ↑u.b * u.q) + ↑u.z * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * (u.r - 1 + 1) = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
rw [← ha, hr]

Goal state after:
case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑u.w * u.q + u.x) * ↑u.b + ↑u.w * u.r = ↑u.w * (u.r + ↑u.b * u.q) + u.x * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case snd
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
⊢ u.step.v.2 = u.v.swap.2

Tactic:
· change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
    rw [← ha, hr]
    ring

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

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

Tactic:
size_node

Goal state after:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)
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 : α ⟹ β
⊢ ∀ (a b : (P F).M α), Mcongr a b → Quot.mk Mcongr (g <$$> a) = Quot.mk Mcongr (g <$$> b)

Tactic:
rintro aa₁ aa₂ ⟨r, pr, 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₂
⊢ Quot.mk Mcongr (g <$$> aa₁) = Quot.mk Mcongr (g <$$> aa₂)
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 := 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)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs (((TypeVec.id ::: Quot.mk r') ⊚ (g ::: fun x ↦ g <$$> x)) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)

Tactic:
← q.P.comp_map

Goal state after:
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 := 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)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs (((TypeVec.id ::: Quot.mk r') ⊚ (g ::: fun x ↦ g <$$> x)) <$$> M.dest (P F) a₁) =
    abs (((TypeVec.id ::: Quot.mk r') ⊚ (g ::: fun x ↦ g <$$> x)) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
use a, fun i => (f i).val

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ ↑(f i)⟩ ∧ ∀ (i : (P F).B a), p ((fun i ↦ ↑(f i)) i)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
intro h
  induction h with
  | ind a f f' _ ih => exact Wequiv.ind _ _ _ ih
  | abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm
  | trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

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

Goal state before:
pp: case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ Wequiv (Quotient.lift Wrepr ⋯ (Quot.mk (⇑Wsetoid) x)) x

Tactic:
apply Wrepr_equiv

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

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

Tactic:
apply Wrepr_equiv

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: ⊢ closure (range fun x ↦ x * x) = ⊤

Tactic:
simpa using

Goal state after:
⊢ closure (range fun x ↦ x * x) = ⊤
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: ⊢ closure (range fun x ↦ x * x) = nonneg ℚ

Tactic:
simpa using

Goal state after:
⊢ closure (range fun x ↦ x * x) = nonneg ℚ
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: ⊢ closure (range fun x ↦ x * x) = nonneg ℚ

Tactic:
by
  simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero even_two

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) → ∀ u ∈ supp (abs ⟨a, f⟩), p u

pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∀ u ∈ supp (abs ⟨a, f⟩), p u) → ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : (P F).B a_2), p (f_1 i)

Tactic:
· rintro ⟨a', f', abseq, hf⟩ u
    rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
    rintro ⟨i, _, hi⟩
    rw [← hi]
    apply hf

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∀ u ∈ supp (abs ⟨a, f⟩), p u) → ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : (P F).B a_2), p (f_1 i)
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s

Tactic:
exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left

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

Goal state before:
pp: case think
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c' : Computation (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c'.think).destruct.destruct (c'.think.bind destruct).destruct

Tactic:
simpa using

Goal state after:
case think
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c' : Computation (WSeq α)
⊢ (flatten c').destruct = c'.bind destruct ∨
    ∃ c, (flatten c').destruct = (flatten c).destruct ∧ c'.bind destruct = c.bind destruct
Module: Mathlib.Data.Set.Finite.List

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length ≤ n}.Finite
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux (some (a, s))) (tail.aux (some (b, t)))

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
m : a ∈ nil.tail
e : some (some a) = (↑nil.tail).get 0
⊢ a ∈ nil

Tactic:
simpa using

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

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u
a x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get 0
⊢ a ∈ s✝

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get (n✝ + 1)
⊢ a ∈ s✝
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
f : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard) → ↑s := ⋯
hf : ∀ (t : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
⊢ Function.Injective f

Tactic:
intro t t' h

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
f : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard) → ↑s :=
  fun x ↦
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
t t' : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)
h : f t = f t'
⊢ t = t'
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some (a, s))) (destruct_append.aux t2 (some (b, t)))

Tactic:
simpa using

Goal state after:
case some.some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ R a b ∧
    (LiftRel R (s.append s2) (t.append t2) ∨
      ∃ s1, s.append s2 = s1.append s2 ∧ ∃ x, t.append t2 = x.append t2 ∧ LiftRel R s1 x)
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩

Tactic:
· simp [hij, lt_def]

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

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := s₂.s, i := s₂.i }.hasNext = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := s₁.s, i := s₁.i }.hasNext = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case1.hc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
simpa using

Goal state after:
case case1.hc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ Pos.Raw.get s₁.s s₁.i = Pos.Raw.get s₂.s s₂.i
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := s₂.s, i := s₂.i }.hasNext = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := s₁.s, i := s₁.i }.hasNext = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
simpa using

Goal state after:
case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬Pos.Raw.get s₁.s s₁.i = Pos.Raw.get s₂.s s₂.i
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ { s := s₂.s, i := s₂.i }.hasNext = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ ¬{ s := ofList s₁.s.toList, i := s₁.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ { s := s₁.s, i := s₁.i }.hasNext = false
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ ¬{ s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using

Goal state after:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ { s := s₂.s, i := s₂.i }.hasNext = false
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s : WSeq α
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f (cons s S).join))) (Seq.destruct (nil.append (map (map f) (cons s S)).join))

Tactic:
simpa using

Goal state after:
case bisim.nil.cons
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1,
    (map f s).append (map f S.join) = s_1.append (map f S_1.join) ∧
      (map f s).append (map (map f) S).join = s_1.append (map (map f) S_1).join
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.nil.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f S.think.join))) (Seq.destruct (nil.append (map (map f) S.think).join))

Tactic:
simpa using

Goal state after:
case bisim.nil.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

Tactic:
simpa using

Goal state after:
case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ ∃ s S_1,
    s✝.append (map f S.join) = s.append (map f S_1.join) ∧
      s✝.append (map (map f) S).join = s.append (map (map f) S_1).join
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))

Tactic:
simpa using

Goal state after:
case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ ∃ s S_1,
    s✝.append (map f S.join) = s.append (map f S_1.join) ∧
      s✝.append (map (map f) S).join = s.append (map (map f) S_1).join