mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)

Tactic:
| swap x y l =>

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
· ext a
        rw [if_neg hs.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := ha
        obtain ⟨_, _, rfl⟩ := hf
        exact hb

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

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
filter_lt_of_ge hlm

Goal state after:
case inr
n m l : ℕ
hlm : l ≤ m
⊢ Ico n l = Ico n l
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.cons.h_lex
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
exact List.Lex.append_left r h2.2 (head :: tail)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l R a = 0 ↔ a = 0

Tactic:
constructor <;> intro h
  · inhabit l
    ext i j
    classical
    replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
    simpa using Matrix.ext_iff.2 h default j
  · rw [h]
    exact mulRightLinearMap_zero_eq_zero _ _

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

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?

Tactic:
simp_rw [← getLast_of_mem_getLast? hx, getLast_getLast_splitBy _ hl]

Goal state after:
case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ l.getLast hl ∈ l.getLast?
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ (inl (diagonal (fun m ↦ r) i j)).fst, of fun i j ↦ (inl (diagonal (fun m ↦ r) i j)).snd) =
    inl (diagonal fun m ↦ r)

Tactic:
fst_inl,

Goal state after:
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ diagonal (fun m ↦ r) i j, of fun i j ↦ (inl (diagonal (fun m ↦ r) i j)).snd) = inl (diagonal fun m ↦ r)
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)

Tactic:
simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
z : ℕ
hz : ∀ i ∈ l, z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]

Tactic:
by
  induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    exact chineseRemainder_modEq_unique this
      (hz i List.mem_cons_self) (ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))

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

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n

Tactic:
exact fib_mono (hn _ rfl)

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

Goal state before:
pp: a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (fib a :: map fib l).sum < fib n

Tactic:
← map_cons

Goal state after:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib (a :: l)).sum < fib n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0

Tactic:
by
  rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
  exact fun n h₁ h₂ => (mem_range.1 h₁).not_ge (Nat.sInf_le h₂)

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ {x | p x ∧ ∀ k < count p n, nth p k < x} = {i | p i ∧ n ≤ i}

Tactic:
refine Set.ext fun a => and_congr_right fun hpa => ?_

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.zero.succ
α : 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₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
mm : 0 + (n✝ + 1) ≤ 1
⊢ BalancedSz 1 0 ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + 0 + 1) (n✝ + 1 + 1 + 1)

Tactic:
rw [zero_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
        decide

Goal state after:
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 <;> simp only [Num.cast_bit1, cast_bit1]

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

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
⊢ MvFunctor P.M

Tactic:
delta M

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
⊢ MvFunctor fun α ↦ ↑P.mp α
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i)

Tactic:
by simp only [iselect, isubtree_cons]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀))

Tactic:
by
  dsimp only [M.corec, M.mk]
  congr with n
  rcases n with - | n
  · dsimp only [sCorec, Approx.sMk]
  · dsimp only [sCorec, Approx.sMk]
    cases f x₀
    dsimp only [PFunctor.map]
    congr

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ ∃ a f f',
    PFunctor.M.dest ⟨a₁, f₁⟩.fst = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i

Tactic:
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
f' : (P.B a').drop ⟹ (α ::: P.M α).drop
f₁' f₂' : (P.B a').last → (α ::: P.M α).last
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun f' f₂'⟩
h' : ∀ (i : (P.B a').last), R (f₁' i) (f₂' i)
⊢ ∃ a f f',
    PFunctor.M.dest ⟨a₁, f₁⟩.fst = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
f' : (P.B a').drop ⟹ (α ::: P.M α).drop
f₁' f₂' : (P.B a').last → (α ::: P.M α).last
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun f' f₂'⟩
h' : ∀ (i : (P.B a').last), R (f₁' i) (f₂' i)
⊢ ∃ a f f',
    PFunctor.M.dest ⟨a₁, f₁⟩.fst = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i

Tactic:
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
f₂' : (P.B a').last → (α ::: P.M α).last
g₁' : P.last.B a' → P.last.M
e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) f₂'⟩
h' : ∀ (i : (P.B a').last), R ((fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) (f₂' i)
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
⊢ ∃ a f f',
    PFunctor.M.dest ⟨a₁, f₁⟩.fst = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then nil.node' x (nil.node' rx (node rrs rrl rrx rrr))
    else nil.rotateL x (nil.node' rx (node rrs rrl rrx rrr))

Tactic:
have : size rrl = 0 ∧ size rrr = 0 := by
          have := balancedSz_zero.1 hr.1.symm
          rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
        cases sr.2.2.2.1.size_eq_zero.1 this.1
        cases sr.2.2.2.2.size_eq_zero.1 this.2
        obtain rfl : rrs = 1 := sr.2.2.1
        rw [if_neg, rotateL_node, if_pos]; · rfl
        all_goals (try dsimp only [size]); decide

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

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

Tactic:
dsimp [rotateL]

Goal state after:
case pos.node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
⊢ (if rls < ratio * rrs then (node ls ll lx lr).node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
h₇ : ↑(a.gcd b) ∣ a.gcdX b * ↑b + ↑(a.gcdD b)
h₈ : ↑(a.gcd b) ∣ a.gcdX b * ↑b
⊢ a.gcd b ∣ a.gcdD b

Tactic:
rw [dvd_iff]

Goal state after:
case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
h₇ : ↑(a.gcd b) ∣ a.gcdX b * ↑b + ↑(a.gcdD b)
h₈ : ↑(a.gcd b) ∣ a.gcdX b * ↑b
⊢ ↑(a.gcd b) ∣ ↑(a.gcdD b)
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 := ⋯
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₂
⊢ r' (g <$$> a₁) (g <$$> a₂)

Tactic:
exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩

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
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (corecF g x)) = (TypeVec.id ::: corec g) <$$> g x

Tactic:
corecF_eq,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs ((TypeVec.id ::: corecF g) <$$> MvQPF.repr (g x)) =
    (TypeVec.id ::: corec g) <$$> g x
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil.coe.coe
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a✝¹ a✝ : α
h : Valid' (↑a✝¹) nil ↑a✝
⊢ f a✝¹ < f a✝

Tactic:
exact f_strict_mono h.ord

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

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
⊢ Valid' a₁ (erase x (Ordnode.node size✝ t_l t_x t_r)) a₂ ∧
    Raised (erase x (Ordnode.node size✝ t_l t_x t_r)).size (Ordnode.node size✝ t_l t_x t_r).size

Tactic:
simp only [erase, size_node]

Goal state after:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ x = y

Tactic:
apply Cofix.bisim_aux r'

Goal state after:
case h'
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x y : Cofix F α
rxy : r x y
⊢ ∀ (x : Cofix F α), r' x x

case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x y : Cofix F α
rxy : r x y
⊢ ∀ (x y : Cofix F α), r' x y → (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x y : Cofix F α
rxy : r x y
⊢ r' x y
Module: Mathlib.Data.QPF.Univariate.Basic

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

pp: case h.right.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2

Tactic:
· rw [← yeq, ← abs_repr u, h, ← abs_map]
      rfl

Goal state after:
case h.right.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (corecF g x).dest = corec g <$> g x

Tactic:
corecF_eq,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs ((P F).map (corecF g) (repr (g x))) = corec g <$> g x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = y

Tactic:
apply Cofix.bisim_aux r'

Goal state after:
case h'
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x : Cofix F), r' x x

case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

case a
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ r' x y
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
· rw [hp]
    exact inv_one

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

Goal state before:
pp: case cons.inl
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

Tactic:
← e

Goal state after:
case cons.inl
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1, parallel.aux2 (pure a :: l) = Sum.inl a_1