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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
⊢ u <*> (t <*> s) = comp <$> u <*> t <*> s

Tactic:
by
      ext a
      simp_rw [seq_def, fmap_def]
      simp only [mem_sup, mem_image]
      constructor
      · rintro ⟨g, hg, b, ⟨f, hf, a, ha, rfl⟩, rfl⟩
        exact ⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
      · rintro ⟨c, ⟨_, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
        exact ⟨g, hg, f a, ⟨f, hf, a, ha, rfl⟩, rfl⟩

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ Set.InjOn (fun p ↦ p.1 * p.2) ↑(m.divisors ×ˢ n.divisors)

Tactic:
rintro ⟨dm₁, dn₁⟩ h₁ ⟨dm₂, dn₂⟩ h₂ hd
  simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *
  suffices dm₁ = dm₂ from Prod.ext this <| by
    rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd
  exact dvd_antisymm
    (hmn.coprime_dvd_left h₁.1.1 |>.coprime_dvd_right h₂.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₁.dvd_mul_right dn₁))
    (hmn.coprime_dvd_left h₂.1.1 |>.coprime_dvd_right h₁.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₂.dvd_mul_right dn₂))

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ f.graph.toList
n : M
hc : (b, n) ∈ f.graph.toList
⊢ (b, m) = (b, n)

Tactic:
Finset.mem_toList,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ f.graph
n : M
hc : (b, n) ∈ f.graph
⊢ (b, m) = (b, n)
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l

Tactic:
lookupFinsupp_apply,

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ (lookup a l).getD 0 = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l
Module: Mathlib.Data.Holor

Goal state before:
pp: case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)

Tactic:
exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(count (fun x ↦ x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
have hr' : 0 < (r : ℚ) := by positivity
  rw [count_eq_card_filter_range, ← Ico_zero_eq_range, Ico_filter_modEq_card _ _ hr,
    max_eq_left (sub_nonneg.mpr <| by gcongr; positivity)]
  conv_lhs =>
    rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
    tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]
    rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]
  rw [sub_eq_self, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', neg_one_mul,
    zero_mul, neg_lt_neg_iff, cast_lt]
  exact ⟨mod_lt _ hr, by simp⟩

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

Goal state before:
pp: n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ Ico n m ++ Ico m l = Ico n l

Tactic:
by
  dsimp only [Ico]
  convert! range'_append using 2
  · rw [Nat.one_mul, Nat.add_sub_cancel' hnm]
  · lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ (Set.range fun l ↦ foldl f a l) ⊆ Set.range fun l ↦ foldl g a l

Tactic:
simp_rw [← (foldr_reverse), Set.range_comp' _ reverse,
    reverse_involutive.bijective.surjective.range_eq, Set.image_univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ Set.range (foldr (fun y x ↦ f x y) a) ⊆ Set.range (foldr (fun y x ↦ g x y) a)
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail

Tactic:
simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail
Module: Mathlib.Data.List.Shortlex

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

Tactic:
cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

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

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w.HasPeriod p

Tactic:
rw [HasPeriod]; simp_all [(take_eq_self_iff w).mpr large]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

Tactic:
rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Preorder α
M✝ : Multiset α
a : α
M : Multiset α
ih : (∀ (x : α), x ∈ M → Acc LT.lt x) → Acc OneStep M
hM : ∀ (x : α), x ∈ a ::ₘ M → Acc LT.lt x
⊢ Acc OneStep (a ::ₘ M)

Tactic:
| cons a M ih =>

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

Goal state before:
pp: q : ℚ
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
obtain hq | hq := le_total q 0

Goal state after:
case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
⊢ a ≡ b [MOD (m :: l).prod] ↔ ∀ (i : Fin (m :: l).length), a ≡ b [MOD (m :: l).get i]

Tactic:
| cons m l ih =>

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
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ↑z < (List.map s l).prod

Tactic:
hlp

Goal state after:
ι : 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
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ↑z < (List.map s l').prod
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a : ℕ
⊢ ceilRoot 0 a = 0

Tactic:
simp [ceilRoot]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
⊢ n.ceilRoot 0 = 0

Tactic:
simp [ceilRoot]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a : ℕ
⊢ ceilRoot 1 a = a

Tactic:
simp [ceilRoot]

Goal state after:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ k) = a
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p * a).choose (p * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
by
  grw [choose_modEq_choose_mod_mul_choose_div]
  simp [NeZero.pos, Int.ModEq.refl]

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

Goal state before:
pp: case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Tactic:
· simp only [not_forall, not_lt] at h'
    have h'b : ∃ hf : (Set.ofPred p).Finite, #hf.toFinset ≤ b := by
      rcases h' with ⟨hf, ha⟩
      exact ⟨hf, ha.trans hab⟩
    have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']
    have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]
    rw [ha0]
    rwa [hb0] at h

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : ∀ (hfi : (Set.ofPred p).Finite), 0 < #hfi.toFinset
⊢ f (nth (fun i ↦ p (f i)) 0) = nth p 0

Tactic:
simp_rw [nth_zero]
    replace h := nth_mem _ h
    rw [← hs h0, ← hf.monotone.map_csInf]
    rcases h0 _ h with ⟨t, ht⟩
    exact ⟨t, Set.mem_ofPred_eq ▸ ht ▸ h⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑↑a.pred' = ↑a - ↑1

Tactic:
pred'_to_nat,

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑↑b.pred' = ↑b - ↑1

Tactic:
pred'_to_nat,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(↑b).pred = ↑b - ↑1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = (l.rotateR x r.dual.dual).dual

Tactic:
dual_dual

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = (l.rotateR x r).dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (l.balanceR x r.dual.dual).dual

Tactic:
dual_dual

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (l.balanceR x r).dual
Module: Mathlib.Data.PFunctor.Univariate.M

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

Tactic:
induction s₂ using PFunctor.M.casesOn' with | _ a' f'
   =>  _ 

Goal state after:
case f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : Path F
a : F.A
f : F.B a → F.M
a' : F.A
f' : F.B a' → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
hh : IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a', f'⟩)
⊢ iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a', f'⟩) ∧
    ∃ 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)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
x : α
⊢ t.dual.dual.findMin' x = t.findMin' x

Tactic:
dual_dual

Goal state after:
α : Type u_1
t : Ordnode α
x : α
⊢ t.findMin' x = t.findMin' x
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.dual.dual.findMin = t.findMin

Tactic:
dual_dual

Goal state after:
α : Type u_1
t : Ordnode α
⊢ t.findMin = t.findMin
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.dual.eraseMax.dual

Tactic:
dual_dual

Goal state after:
α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.eraseMax.dual
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
r' : ℕ
e : Raised r.size r'
H : BalancedSz l.size r'
⊢ ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')

Tactic:
exact ⟨_, _, H, Or.inr ⟨e.dist_le, rfl⟩⟩

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
⊢ g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)

Tactic:
rw [this]

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
⊢ g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
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 : α
⊢ f x = M.corec g x

Tactic:
apply bisim' (fun _ => True) _ _ _ _ trivial

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 : α
⊢ ∀ (x : α),
    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'
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩

Tactic:
rw [this]

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ (g <$$> P.wMk a f' fun i ↦ ⟨(f i).fst, (f i).snd⟩) =
    P.wMk a (g ⊚ f') fun i ↦ ⟨((fun i ↦ ⟨(f i).fst, (f i).snd⟩) i).fst, g ⊚ ((fun i ↦ ⟨(f i).fst, (f i).snd⟩) i).snd⟩
Module: Mathlib.Data.PNat.Factors

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

Tactic:
rw [this]

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

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

Tactic:
rw [this]

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

Goal state before:
pp: case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p

Tactic:
intro q

Goal state after:
case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
⊢ q ∈ k • PrimeMultiset.ofPrime p → q = p
Module: Mathlib.Data.PNat.Factors

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

Tactic:
rw [this]

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = 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.factorMultiset ⊓ v).prod = n.gcd m

Tactic:
rw [this]

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ m.factorMultiset).prod = 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
⊢ (u ⊔ v).prod = n.lcm m

Tactic:
rw [this]

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm 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.factorMultiset ⊔ v).prod = n.lcm m

Tactic:
rw [this]

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
⊢ u.q = u.qp + 1

Tactic:
let h := u.rq_eq

Goal state after:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : u.r + (u.bp + 1) * u.q = u.ap + 1 := rq_eq u
⊢ u.q = u.qp + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
hr : u.r = 0
⊢ u.finish.v = u.v

Tactic:
let ha : u.r + u.b * u.q = u.a := u.rq_eq

Goal state after:
u : XgcdType
hr : u.r = 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
⊢ u.finish.v = u.v
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
hr : u.r ≠ 0
⊢ u.step.v = u.v.swap

Tactic:
let ha : u.r + u.b * u.q = u.a := u.rq_eq

Goal state after:
u : XgcdType
hr : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
⊢ u.step.v = u.v.swap
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ioi a) = ∏ i, #(Ici (a i)) - 1

Tactic:
rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]

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

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑z * ↑w + ↑z * x = x * y + x * ↑z + 1

Tactic:
mul_comm (z : ℕ),

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑w * ↑z + ↑z * x = x * y + x * ↑z + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (l.balance' x r).dual.dual = l.balance' x r

Tactic:
dual_dual

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ l.balance' x r = l.balance' x r
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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧

Tactic:
rw [this]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ ⟦wrepr ((P F).wMk a f' f)⟧ = ⟦(P F).wMk a f' f⟧
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)⟧
⊢ mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Tactic:
rw [this]

Goal state after:
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)⟧
⊢ ⟦Wrepr (WType.mk a f)⟧ = ⟦WType.mk a f⟧
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₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
this : (g₁ ∘ fun x ↦ ⟦f x⟧) = g₂ ∘ fun x ↦ ⟦f x⟧
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x ↦ ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x ↦ ⟦f x⟧)

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Data.Rat.Cast.OfScientific

Goal state before:
pp: case isTrue
K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
h✝ : s = true
⊢ ↑↑⟨↑m / 10 ^ e, ⋯⟩ = ↑m / 10 ^ e

Tactic:
norm_cast
      simp

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : Fix F
⊢ mk x.dest = x

Tactic:
change (Fix.mk ∘ Fix.dest) x = id x
  apply Fix.ind_rec (mk ∘ dest) id
  intro x
  rw [Function.comp_apply, id_eq, Fix.dest, Fix.rec_eq, id_map, comp_map]
  intro h
  rw [h]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
| (corec (fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) y.dest).dest

Tactic:
Cofix.dest_corec

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
| (TypeVec.id ::: corec fun x ↦ (TypeVec.id ::: fun i ↦ i.dest) <$$> x) <$$> (TypeVec.id ::: fun i ↦ i.dest) <$$> y.dest
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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
this : x = y.fst
⊢ β y.fst = β x

Tactic:
rw [this]

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

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

Tactic:
rw [this]

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n
⊢ (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n ∈ closure (range fun x ↦ x ^ n)