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 β✝
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t) = s ×ˢ t

Tactic:
rw [product_eq_biUnion]

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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ Prod.mk <$> s <*> t = (fun b a ↦ (a, b)) <$> t <*> s

Tactic:
by
      simp_rw [seq_def, fmap_def, sup_image, sup_eq_biUnion]
      change (s.biUnion fun a => t.image fun b => (a, b))
        = t.biUnion fun b => s.image fun a => (a, b)
      trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
b : β a
⊢ dlookup a (⟨a, b⟩ :: tail✝).dedupKeys = dlookup a (⟨a, b⟩ :: tail✝)

Tactic:
dedupKeys_cons,

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
b : β a
⊢ dlookup a (kinsert ⟨a, b⟩.fst ⟨a, b⟩.snd tail✝.dedupKeys) = dlookup a (⟨a, b⟩ :: tail✝)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
dedupKeys_cons,

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (kinsert ⟨a', b⟩.fst ⟨a', b⟩.snd tail✝.dedupKeys) = dlookup a (⟨a', b⟩ :: tail✝)
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = g.support

Tactic:
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).drop.take = ↑(take ⟨is, h⟩).drop

Tactic:
by simp [assocRight, take, drop, cast_type, List.drop_take]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds
⊢ x.slice i hid ⟨is, hisds⟩ = y.slice i hid ⟨is, hisds⟩

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Data.Holor

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

Tactic:
simp [hbi']

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

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ (ofNat m * ofNat n).bodd = ((ofNat m).bodd && (ofNat n).bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (↑(m * n)).bodd = ((↑m).bodd && (↑n).bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ (ofNat m * -[n+1]).bodd = ((ofNat m).bodd && -[n+1].bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ (-↑(m * n.succ)).bodd = ((↑m).bodd && -[n+1].bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ (-↑(m.succ * n)).bodd = (-[m+1].bodd && (↑n).bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] * -[n+1]).bodd = (-[m+1].bodd && -[n+1].bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ (↑(m.succ * n.succ)).bodd = (-[m+1].bodd && -[n+1].bodd)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ x ∈ Ioc a b ∧ x ≡ v [ZMOD r] ↔
    ∃ a_1, (a_1 ∈ Ioc (a - v) (b - v) ∧ r ∣ a_1) ∧ { toFun := fun x ↦ x + v, inj' := ⋯ } a_1 = x

Tactic:
mem_Ioc,

Goal state after:
a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔
    ∃ a_1, ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ { toFun := fun x ↦ x + v, inj' := ⋯ } a_1 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ {x ∈ Ioc a b | r ∣ x} = map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)

Tactic:
by
  ext x
  simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
  aesop

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

Goal state before:
pp: case cons
α : Type u
β : Type v
bs : List β
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) bs = (zipWithLeft' Prod.mk (head✝ :: atl) bs).fst

Tactic:
cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl

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

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ w <+: take p w ++ w

Tactic:
have drop : drop p w <+: w := by
      simp only [prefix_iff_getElem?, length_drop, getElem_drop]
      intro i leni
      have len : i + p < w.length := by lia
      simp_all only [getElem?_pos, add_comm p i]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
drop : List.drop p w <+: w
⊢ w <+: take p w ++ w
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
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✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0

Tactic:
rw [h]

Goal state after:
case mpr
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✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R 0 = 0
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
less_mod : i % p < n + w.length
⊢ (take n w ++ w)[i]? = (take n w ++ w)[i % p]?

Tactic:
rw [mod_p i less_i, mod_p (i % p) less_mod, mod_mod]

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

Goal state before:
pp: case mpr
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
h : a = 0
⊢ mulRightLinearMap l R a = 0

Tactic:
rw [h]

Goal state after:
case mpr
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
h : a = 0
⊢ mulRightLinearMap l R 0 = 0
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case pos
α : 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
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
w : α
hw : w ∈ Z₂
hzw : z < w
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨w, .inl hw, hyz.trans hzw⟩

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

Goal state before:
pp: case intro.intro.inr.cons
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ (x : α), x ∈ N → x < a) → Acc OneStep (M + N)
hN : b < a ∧ ∀ (a_1 : α), a_1 ∈ N → a_1 < a
⊢ Acc OneStep (b ::ₘ (M + N))

Tactic:
obtain ⟨hba, hN⟩ := hN

Goal state after:
case intro.intro.inr.cons
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ (x : α), x ∈ N → x < a) → Acc OneStep (M + N)
hba : b < a
hN : ∀ (a_1 : α), a_1 ∈ N → a_1 < a
⊢ Acc OneStep (b ::ₘ (M + N))
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case left
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1

Tactic:
exact_mod_cast NNRat.cast_strictMono <| Nat.ceil_lt_add_one zero_le

Goal state after:
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1

Tactic:
rw [h]

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

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
← prod_factorization_pow_eq_self hn

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
← prod_factorization_pow_eq_self hn

Goal state after:
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by
  unfold ceilRoot
  split_ifs with h <;>
    simp [Finsupp.ceilDiv_def, prod_mapRange_index pow_zero, Nat.ceilDiv_eq_add_pred_div]

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

Goal state before:
pp: case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ ∀ b ∈ {x | p x ∧ ∀ k < n + 1, nth p k < x}, f (n + 1) ≤ b

Tactic:
rintro b ⟨hb, h⟩

Goal state after:
case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
b : ℕ
hb : p b
h : ∀ k < n + 1, nth p k < b
⊢ f (n + 1) ≤ b
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id rr with _ | rrs
        · exact node 3 (ι x) rlx ι rx
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ r.sub' (Num.pos d) = r₂.toZNum ↔ ↑r = ↑r₂ + ↑d

Tactic:
rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]

Goal state after:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑↑r = ↑(↑r₂ + ↑d)
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
cases r <;> simp [rotateL, rotateR]

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).dual =
    if l✝.size < ratio * r✝.size then r✝.dual.node3R x✝ l✝.dual x l.dual else r✝.dual.node4R x✝ l✝.dual x l.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).dual = r✝.dual.node3R x✝ l✝.dual x l.dual

Tactic:
simp [dual_node3L, dual_node4L, node3R]

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

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).dual = r✝.dual.node4R x✝ l✝.dual x l.dual

Tactic:
simp [dual_node3L, dual_node4L, node3R]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x : F.M
n : ℕ
⊢ (M.mk x.dest).approx n = x.approx n

Tactic:
dsimp only [M.mk]

Goal state after:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
⊢ Approx.sMk x.dest n = x.approx n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (x.approx n.succ))), a ≍ a'' → children' (x.approx n.succ) a'' = ch a

Tactic:
rw [h]

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))),
    a ≍ a'' → children' (CofixA.intro (head' (x.approx 1)) ch) a'' = ch a
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
a : F.A
i : F.B a
ps : List F.Idx
x : F.M
a' : F.A
f : F.B a' → F.M
h : a = a'
⊢ F.B a = F.B a'

Tactic:
rw [h]

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
rl0 : rl.size = 0
h : rr.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Goal state after:
case neg.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta = 0 ∨ l.size = 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
rl0 : rl.size = 0
h : rr.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
have := prod_ofNatMultiset (l : Multiset ℕ) h

Goal state after:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = (↑l).prod
⊢ ↑(ofNatList l h).prod = l.prod
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b a_1, p ⟨a, ⋯⟩) ↔ ∃ h, p ⟨n', h⟩

Tactic:
exists_prop,

Goal state after:
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a, n' = a ∧ ∃ a_1, p ⟨a, ⋯⟩) ↔ ∃ h, p ⟨n', h⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
let n := u.prod
  let m := v.prod
  change (u ⊔ v).prod = PNat.lcm n m
  have : u = n.factorMultiset := u.factorMultiset_prod.symm; rw [this]
  have : v = m.factorMultiset := v.factorMultiset_prod.symm; rw [this]
  rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]

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

Goal state before:
pp: α : 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 : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
this : delta * Nat.succ 0 < rs
⊢ delta ≤ rl.size + rr.size

Tactic:
rwa [sr.1, Nat.lt_succ_iff] at this

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

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
⊢ x✝.reduce.IsSpecial

Tactic:
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h]
      exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

Goal state after:
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 : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ico a b) = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
card_Ico_eq_card_Icc_sub_one,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Icc a b) - 1 = ∏ i, #(Icc (a i) (b i)) - 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
⊢ LiftR r x y → ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)

Tactic:
rintro ⟨u, xeq, yeq⟩
    rcases h : repr u with ⟨a, f⟩
    use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
    constructor
    · rw [← xeq, ← abs_repr u, h, ← abs_map]; rfl
    constructor
    · rw [← yeq, ← abs_repr u, h, ← abs_map]; rfl
    intro i j
    exact (f i j).property

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
⊢ LiftP (fun i u ↦ u ∈ supp x i) x

Tactic:
rw [h]

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
⊢ ∀ (i : Fin2 n), ∀ u ∈ supp x i, u ∈ supp x i
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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) = g (abs ⟨a, splitFun (TypeVec.id ⊚ f') (recF g ∘ f)⟩)

Tactic:
TypeVec.id_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' (recF g ∘ f)⟩) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inl
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 : Cofix F α
h : x = y
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
rw [h]

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

Goal state before:
pp: case h.inr
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 : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$$> x.dest =
    (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$$> y.dest

Tactic:
appendFun_comp_id

Goal state after:
case h.inr
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 : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ ((TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> x.dest =
    ((TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) ⊚ (TypeVec.id ::: Quot.mk r)) <$$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
rw [h]

Goal state after: