mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ traverse (pure ∘ f✝) x✝ = pure (f✝ <$> x✝)

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Goal state after:
case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ tsnd (pure ∘ f✝) x✝ = pure (f✝ <$> x✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ (fun {α} ↦ η✝.app α) (traverse f✝ x✝) = traverse ((fun {α} ↦ η✝.app α) ∘ f✝) x✝

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Goal state after:
case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ η✝.app (t α β✝) (tsnd f✝ x✝) = tsnd (η✝.app β✝ ∘ f✝) x✝
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a ↦ b ∈ f a) (b :: bs) (a :: as)

Tactic:
by simp [mem_traverse as bs]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : σ
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inl val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inl val✝)

Tactic:
simp! [Sum.traverse, functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inr val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inr val✝)

Tactic:
simp! [Sum.traverse, functor_norm]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 β_1 : Type ?u.17} (x : Const α (α_1 → β_1)) (y : Const α α_1), f (x <*> y) = f x <*> f y

Tactic:
by intros; simp only [Seq.seq, map_mul]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝

Tactic:
← ih

Goal state after:
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ g = g'

Tactic:
← lastFun_splitFun f g,

Goal state after:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f g) = g'
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))

Tactic:
exact card_Icc _ _

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

Goal state before:
pp: C : FloatCfg
n d : ℕ+
⊢ Float × Bool

Tactic:
let e₁ : ℤ := n.1.size - d.1.size - prec
  obtain ⟨d₁, n₁⟩ := Int.shift2 d.1 n.1 (e₁ + prec)
  let e₂ := if n₁ < d₁ then e₁ - 1 else e₁
  let e₃ := max e₂ emin
  obtain ⟨d₂, n₂⟩ := Int.shift2 d.1 n.1 (e₃ + prec)
  let r := mkRat n₂ d₂
  let m := r.floor
  refine (Float.finite Bool.false e₃ (Int.toNat m) ?_, r.den = 1)
  exact lcProof

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
⊢ InternallyProjective ((free R).obj ℕ∪{∞}.toCondensed)

Tactic:
free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}

Goal state after:
R : Type
inst✝ : CommRing R
⊢ ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ e
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α

Tactic:
simp only [toList, List.mem_map, List.mem_finRange, true_and]

Goal state after:
α : Type u
inst✝ : FinEnum α
x : α
⊢ ∃ a, equiv.symm a = x
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂).entries ↔ y ∈ dlookup x (s₂ ∪ s₁).entries

Tactic:
intros; simp only [union_entries, Option.mem_def, dlookup_kunion_eq_some]
      constructor <;> intro h'
      · rcases h' with h' | h'
        · right
          refine ⟨?_, h'⟩
          apply h
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl
        · left
          rw [h'.2]
      · rcases h' with h' | h'
        · right
          refine ⟨?_, h'⟩
          intro h''
          apply h _ h''
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl
        · left
          rw [h'.2]

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

Goal state before:
pp: case refine_1
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
⊢ (if a = a' then some ⟨a, b⟩ else none) = if decide (a = a') = true then some ⟨a', b'⟩ else none

Tactic:
split_ifs

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : decide (a = a') = true
⊢ some ⟨a, b⟩ = some ⟨a', b'⟩

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : ¬decide (a = a') = true
⊢ False

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (s.sum id).support ⊆ s.sup Finsupp.support

Tactic:
convert! Multiset.support_sum_subset s.1

Goal state after:
case e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: m n : ℕ
⊢ ↑m - ↑n ≤ ↑(m - n)

Tactic:
by
  lia

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

Goal state before:
pp: case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _

Goal state after:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
Module: Mathlib.Data.List.Sections

Goal state before:
pp: α : Type u_1
L : List (List α)
f : List α
⊢ f ∈ L.sections ↔ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · induction L generalizing f
    · cases mem_singleton.1 h
      exact Forall₂.nil
    simp only [sections, mem_flatMap, mem_map] at h
    rcases h with ⟨_, _, _, _, rfl⟩
    simp only [*, forall₂_cons, true_and]
  · induction h with
    | nil => simp only [sections, mem_singleton]
    | @cons a l f L al fL fs =>
      simp only [sections, mem_flatMap, mem_map]
      exact ⟨f, fs, a, al, rfl⟩

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

Goal state before:
pp: case intro.intro.inr.cons
α : 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
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < (xa :: xb).length

Tactic:
rw [List.length_cons, ← h2len]

Goal state after:
case intro.intro.inr.cons
α : 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
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| sz[i]

Tactic:
rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]

Goal state after:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| ((take (i + 1) sz).splitLengths l)[i].length
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.rel
α : 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
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < (xa :: xb).length

Tactic:
rw [List.length_cons, ← h2len]

Goal state after:
case intro.intro.inr.rel
α : 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
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i % 0]? = w[i]?

Tactic:
mod_zero

Goal state after:
case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i]? = w[i]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length, w[i]? = w[i % p]?) → w.HasPeriod p

Tactic:
· intro mod
    rw [hasPeriod_iff_getElem?]
    intro i less
    rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)

Tactic:
by
  induction l generalizing a g gs with
  | nil =>
    rw [splitBy.loop, reverse_cons]
    apply List.isChain_reverse.1
    simpa using isChain_cons.2 ⟨hga, hgs⟩
  | cons b l IH =>
    rw [splitBy.loop]
    split
    · refine IH hgs' hgs fun m hm ↦ ?_
      obtain ⟨ha, _, H⟩ := hga m hm
      refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
      rwa [reverse_cons, head_append_of_ne_nil]
    · apply IH
      · simpa using hgs'
      · rw [reverse_cons]
        apply isChain_cons.2 ⟨hga, hgs⟩
      · simpa

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

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ w = take q (drop q w) ++ drop q w

pp: case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)

Tactic:
· rw [take_eq, take_append_drop q w]

Goal state after:
case inr.inr.gt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
IH : (drop q w).HasPeriod ((p - q).gcd q)
⊢ (take q (drop q w) ++ drop q w).HasPeriod (p.gcd q)
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
⊢ (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) =
    (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))

Tactic:
by
    ext
    · dsimp [mul_apply]
      simp_rw [fst_sum]
      rfl
    · simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
      simp only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]
      rw [← Finset.sum_add_distrib]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

Tactic:
rw [← singleton_add, add_comm] at h0

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum

Tactic:
rw [ofDigits_neg_one] at t

Goal state after:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
this : ∃ a b, ↑p ^ m * a + ↑n * b = 1
⊢ IsUnit ↑n

Tactic:
obtain ⟨a, b, h⟩ := this
    refine .of_mul_eq_one b ?_
    simpa [hm] using h

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

Goal state before:
pp: a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ k) = a

Tactic:
split_ifs

Goal state after:
case pos
a : ℕ
h✝ : a = 0
⊢ 0 = a

case neg
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun p k ↦ p ^ k) = a
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.floorRoot (a ^ n) = a

Tactic:
simp [floorRoot_def, pos_iff_ne_zero.2, hn]

Goal state after:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : a = 0
⊢ 0 = a

case neg
n : ℕ
hn : n ≠ 0
a : ℕ
h✝ : ¬a = 0
⊢ (a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) =
    if n < k.bit1 * k.bit1 then ↑n else if k.bit1 ∣ n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
split_ifs

Goal state after:
case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝ : n < k.bit1 * k.bit1
⊢ ↑n = ↑n

case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : k.bit1 ∣ n
⊢ ↑k.bit1 = ↑k.bit1

case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact node (ls + 1) l x nil
    · refine if rs > delta * ls then ?_ else node (ls + rs + 1) l x r
      rcases id rr with _ | rrs
      · exact nil
      --should not happen
      rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · exact nil
      --should not happen
      exact
        if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
        else
          node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
            (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: case e'_3.e'_3
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'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ nth p m' < f k ↔ nth (fun i ↦ p (f i)) m' < k

Tactic:
← hf.lt_iff_lt

Goal state after:
case e'_3.e'_3
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'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ nth p m' < f k ↔ f (nth (fun i ↦ p (f i)) m') < f k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ ⦃x : ℕ⦄, x ∈ range (sInf (Set.ofPred p)) → ¬p x

Tactic:
exact fun n h₁ h₂ => (mem_range.1 h₁).not_ge (Nat.sInf_le h₂)

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

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

Tactic:
have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b) : ℤ) := by
      simp [add_comm, add_left_comm]

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

Goal state before:
pp: l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l

Tactic:
refine ⟨?_, h₂.resolve_left h⟩

Goal state after:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: 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

Tactic:
split_ifs

Goal state after:
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

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