mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: case h
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (Opposite.op 0))

pp: case hc
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ IsLimit ((forget R).mapCone c)

pp: case hF
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)

Tactic:
· simp only [LightProfinite.effectiveEpi_iff_surjective]
    exact fun x h ↦ Concrete.surjective_π_app_zero_of_surjective_map (limit.isLimit x) h

Goal state after:
case hc
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ IsLimit ((forget R).mapCone c)

case hF
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝² : WriterT ω M α✝
x✝¹ : α✝ → WriterT ω M β✝
x✝ : β✝ → WriterT ω M γ✝
⊢ (x✝² >>= x✝¹ >>= x✝).run = (x✝² >>= fun x ↦ x✝¹ x >>= x✝).run

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ F.F.f s
⊢ 𝓝 a ≤ 𝓟 (F.F.f s)

Tactic:
simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i

Tactic:
notMem_support_iff.1 (mt h.1 hi),

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ t i
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → DecidableEq (α i)
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), IsBotZeroClass (α i)
inst✝¹ : (i : ι) → OrderBot (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
by
  rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ a ∈ q, ∀ b ∈ q, f a = f b
a : α
aq : a ∈ q
⊢ q.liftOn f h = f a

Tactic:
revert h; rw [eq_mk_of_mem aq]; intro; rfl

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
by
  by_cases h : k' = k
  · subst h; simp
  · simp_all [lookup_insert_ne h]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
⊢ m.keys.Nodup ↔ m.NodupKeys

Tactic:
rcases m with ⟨l⟩; rfl

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys

Tactic:
| cons s _ _ =>

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝

Tactic:
| cons s _ _ =>

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

Tactic:
| cons s _ _ =>

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

Goal state before:
pp: case cons
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))

Tactic:
| cons s _ _ =>

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)

Tactic:
| cons s _ _ =>

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
rw [lookup_union_left_of_not_in this, lookup_erase_ne h']

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' l).NodupKeys

Tactic:
have : NodupKeys l' := by
    rw [← hl]
    apply nodup_nil

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
this : l'.NodupKeys
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' l).NodupKeys
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b ∈ lookup a l, decide (b ≠ 0) = true) ↔ (lookup a l).getD 0 ≠ 0

Tactic:
cases lookup a l

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b ∈ none, decide (b ≠ 0) = true) ↔ none.getD 0 ≠ 0

case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
val✝ : M
⊢ (∃ b ∈ some val✝, decide (b ≠ 0) = true) ↔ (some val✝).getD 0 ≠ 0
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) ↑l.dedup

Tactic:
List.dedup_eq_self.mpr hn,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) ↑l
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 g = f.neLocus (-g)

Tactic:
← neLocus_neg_neg,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (- -f).neLocus (-g) = f.neLocus (-g)
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
a✝ : α
⊢ ((r • f) • m) a✝ = (r • f • m) a✝

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
i : ι k
this : f.embSigma ⟨k, i⟩ = g.embSigma ⟨k, i⟩
⊢ f i = g i

Tactic:
simpa using this

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

Goal state before:
pp: case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
· change ofNat _ = _
    rw [Nat.div_eq_of_lt] <;> simp

Goal state after:
case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p ([].get ⟨0, hl⟩) = true

Tactic:
simp only [takeWhile_nil, Bool.not_eq_true, true_iff]

Goal state after:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < [].length), p ([].get ⟨0, hl⟩) = false
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
hn : n ∈ {n | n ≤ l.length}
m : ℕ
hm : m ∈ {n | n ≤ l.length}
h : (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) m
⊢ n = m

Tactic:
induction l generalizing n m with

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

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

Tactic:
cases s with

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

Goal state before:
pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), l.length ≤ tail✝.sum → (tail✝.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head✝ :: tail✝).sum
⊢ ((head✝ :: tail✝).splitLengths l).flatten = l

Tactic:
case cons head tail ih =>
    simp only [splitLengths_cons, flatten_cons]
    rw [ih, take_append_drop]
    simpa [add_comm] using h

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

Goal state before:
pp: α : Type u_1
u : List α
p : ℕ
s t : List α
per : (s ++ u ++ t).HasPeriod p
⊢ u.HasPeriod p

Tactic:
exact per.factor

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ ∀ (m : List α), m ∈ [].head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [head✝]).head hb) = false

Tactic:
rintro _ ⟨⟩

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

Goal state before:
pp: case nil.cons
α : Type u_1
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
c : α
m : List α
ha : ∀ (x : α), x ∈ (c :: m).head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r (c :: m) a g [] = (g.reverse ++ [a]) :: splitBy r (c :: m)

Tactic:
simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]

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
this : p = p - q + q
⊢ (drop q w).HasPeriod (p - q)

Tactic:
exact per_q.drop_of_hasPeriod_add (this ▸ per_p)

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

Goal state before:
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:
· exact (gcd_stable ▸ IH).take_append (p.gcd q) q (drop q w)
          (gcd_dvd_right p q) drop_len

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

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

Tactic:
Finset.card_Ioo_eq_card_Icc_sub_two,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) - 2 = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 2
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
· simp [hn]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
by
  simp +contextual [floorRoot, not_or]

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

Goal state before:
pp: case inr.inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ 0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b

pp: case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
· simp [hn]

Goal state after:
case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a b n : ℕ
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  obtain rfl | ha := eq_or_ne a 0
  · simp [hn]
  rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

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

Goal state before:
pp: case inr.inl
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0

pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
· simp [hn]

Goal state after:
case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: n m : ℕ
⊢ hyperoperation (n + 2) m 1 = m

Tactic:
by
  induction n with grind

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

Goal state before:
pp: n : ℕ
⊢ hyperoperation (n + 1) 2 2 = 4

Tactic:
by
  induction n with grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ emultiplicity n.minFac ((n.minFac ^ k).choose (n.minFac ^ (k - 1))) < ↑2

Tactic:
rw [Nat.Prime.emultiplicity_choose_prime_pow isPrime this (pow_ne_zero _
      (Nat.Prime.ne_zero isPrime)), multiplicity_pow_self_of_prime (prime_iff.mp isPrime)]

Goal state after:
case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ↑(k - (k - 1)) < ↑2
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n : PosNum
⊢ n.bit0.Prime ↔ n = 1

Tactic:
refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)

Goal state after:
case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit0

case refine_2
n : PosNum
⊢ ↑n.bit0 = (↑n.bit0).minFac ↔ n = 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
this : ↑(-↑a) = -1 + ↑(-↑a + 1)
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑a.succ + -↑a.succ + 1

Tactic:
simpa using this

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
conv =>
    lhs
    rw [← zneg_zneg n]

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

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

Tactic:
rw [sub', ZNum.cast_bitm1, cast_sub' a b]
    have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b) : ℤ) := by
      simp [add_comm, add_left_comm]
    simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(0 + zero) = ↑0 + ↑zero

Tactic:
exact (_root_.zero_add _).symm

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + pos a✝) = ↑0 + ↑(pos a✝)

Tactic:
exact (_root_.zero_add _).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + neg a✝) = ↑0 + ↑(neg a✝)

Tactic:
exact (_root_.zero_add _).symm

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
⊢ AllAgree fun n ↦ children' (x.approx n.succ) (cast ⋯ i)

Tactic:
intro n
      have P' := x.2 (succ n)
      apply agree_children _ _ _ P'
      trans i
      · apply cast_heq
      symm
      apply cast_heq

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

Goal state before:
pp: d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d

Tactic:
induction n with
  | one =>
    exact divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
  | bit1 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
    · lia
  | bit0 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux
    · simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
    · simpa using IH.2

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

Goal state before:
pp: case succ.step.step.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : F.B a✝⁴ → F.M
a✝³ : M.mk ⟨a✝⁴, f✝¹⟩ = M.mk ⟨a✝⁸, y✝¹⟩
a✝² : F.A
f✝ : F.B a✝² → F.M
a✝¹ : M.mk ⟨a✝², f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁴, f✝¹⟩) = iselect ps (M.mk ⟨a✝², f✝⟩)
a✝ : M.mk ⟨a✝⁸, x✝¹⟩ = M.mk ⟨a✝⁶, x✝⟩
⊢ (M.mk ⟨a✝⁴, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝², f✝⟩).approx (n + 1 + 1)

Tactic:
have := mk_inj ‹_›; cases this

Goal state after:
case succ.step.step.f.f.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
have := mk_inj ‹_›; cases this

Goal state after:
case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
have := mk_inj ‹_›; cases this

Goal state after:
case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
⊢ ∀ (x : α), Emem x nil → P x

Tactic:
rintro _ ⟨⟩

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)

Tactic:
by
  rw [M.dest_map]; congr
  apply eq_of_drop_last_eq (by simp)
  simp only [lastFun_appendFun]
  ext1; apply h

Goal state after: