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

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt8.ofFin UInt8.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt16.ofFin UInt16.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt16.ofFin UInt16.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt32.ofFin UInt32.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt32.ofFin UInt32.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt64.ofFin UInt64.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt64.ofFin UInt64.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int8.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int8.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int8.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int8.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int16.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int16.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int16.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int16.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int32.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int32.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int32.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int32.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int64.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int64.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int64.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int64.toBitVec)

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ LeftInverse BitVec.ofFin BitVec.toFin

Tactic:
intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ RightInverse BitVec.ofFin BitVec.toFin

Tactic:
intro x; simp

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:
have (h : a ≠ s.fst) : ¬ f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
    by_cases a = s.fst <;> grind [Sigma.map]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
· simp [*, mem_lookupAll]

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π' = 𝟙 (S' ⊗ ℕ∪{∞})

Tactic:
ext x; all_goals exact h.elim x

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → ¬a ∈ (kerase a tl).keys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
h : a = hd.fst
⊢ ¬a ∈ (kerase a (hd :: tl)).keys

Tactic:
subst h
      simp [nd.1]

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

Goal state before:
pp: case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ r % b = r

Tactic:
← emod_abs,

Goal state after:
case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ r % |b| = r
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ m.natAbs
⊢ ↑(p ^ (k + 1)) ∣ m

Tactic:
apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd1

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

Goal state before:
pp: a b r v : ℕ
x : ℤ
⊢ x ∈ map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]}) ↔ x ∈ {x ∈ Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}

Tactic:
simp only [mem_map, mem_filter, mem_Ico, castEmbedding_apply]

Goal state after:
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) ↔ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n k : ℕ
⊢ -[m+1] >>> (↑n + ↑k) = -[m+1] >>> ↑n >>> ↑k

Tactic:
rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]

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

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

Tactic:
| cons _ btl =>

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)
h2len : (xa :: xs).length = (xa :: xb).length
h : Lex r xs xb
⊢ Acc (Shortlex r) (xa :: xs)

Tactic:
simp only [length_cons, add_left_inj] at 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
⊢ Acc (Shortlex r) (xa :: xs)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
splitByLoop_eq_append,

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
· rw [splitByLoop_eq_append, mem_append]
      simpa using IH

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

Goal state before:
pp: α : Type u_1
p : ℕ
⊢ [].HasPeriod p

Tactic:
by
  simp

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

Goal state before:
pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
splitByLoop_eq_append,

Goal state after:
case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ [g.reverse ++ [a]].reverse ++ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ j < v.length

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length

Tactic:
all_goals lia

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

Goal state before:
pp: case refine_4.refine_1
α : 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, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
by_cases z_in : z ∈ Y₂

Goal state after:
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₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

case neg
α : 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₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iic n.factorization)

Tactic:
by
  apply Finset.coe_inj.mp
  grind [coe_divisors_eq_prod_pow_le_factorization]

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

Goal state before:
pp: case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(Quotient.recOn (motive := fun x ↦
        x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
        (Quot.mk (⇑(List.isSetoid ι)) l) (fun l nod x co ↦ chineseRemainderOfList a s l ⋯) ⋯ nod hs pp) <
    (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simpa using! chineseRemainderOfList_lt_prod a s l
    (List.Nodup.pairwise_of_forall_ne nod pp) (by simpa using! hs)

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

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

Tactic:
by gcongr; exact sum_fib_lt hl.2 this

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).getD n 0 = 0

Tactic:
List.getD_eq_default

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ 0 = 0

case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).length ≤ n
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
x : ↑P α
f : α → β
⊢ (P.map f x).fst = x.fst

Tactic:
by cases x; rfl

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

Goal state before:
pp: n : ℕ
⊢ (↑(n + 1)).toZNumNeg = -↑(n + 1)

Tactic:
← neg_inj,

Goal state after:
n : ℕ
⊢ -(↑(n + 1)).toZNumNeg = - -↑(n + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d * (2 * ↑q) =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
two_mul

Goal state after:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d * (↑q + ↑q) =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 + ↑d * (↑q + ↑q) = ↑n.bit0

Tactic:
simp only [Num.cast_bit0, cast_bit0]

Goal state after:
case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (↑q + ↑q) = ↑n + ↑n
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 : α
⊢ ∀ (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'

Tactic:
clear x

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 : α),
    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.PNat.Factors

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

Tactic:
by
  have := prod_ofPNatMultiset (l : Multiset ℕ+) h
  rw [Multiset.prod_coe] at this
  exact this

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

Goal state before:
pp: case e'_3.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ Multiset.card (k • PrimeMultiset.ofPrime p) = k

Tactic:
rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]

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

Goal state before:
pp: u : XgcdType
⊢ u.v = succ₂ u.vp

Tactic:
ext <;> dsimp [v, vp, w, z, a, b, succ₂]

Goal state after:
case fst
u : XgcdType
⊢ (u.wp + 1) * (u.ap + 1) + u.x * (u.bp + 1) = u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp + 1

case snd
u : XgcdType
⊢ u.y * (u.ap + 1) + (u.zp + 1) * (u.bp + 1) = u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp + 1
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 α
⊢ TypeVec.id <$$> abs (repr x) = abs (repr x)

Tactic:
← abs_map

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs ((g ⊚ f) <$$> repr x) = g <$$> abs (f <$$> repr x)

Tactic:
← abs_map

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ (fun i ↦ Subtype.val) <$$> abs ⟨a, f⟩ = abs ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
← abs_map

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((fun i ↦ Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ ↑(f i j)⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> abs ⟨a, f⟩ = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
← abs_map

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
← abs_map

Goal state after:
case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, f⟩) = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t ↦ (↑t).1) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = abs ⟨a, f₀⟩

Tactic:
← abs_map

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t ↦ (↑t).2) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = abs ⟨a, f₁⟩

Tactic:
← abs_map

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
H1 : l.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * l.size
⊢ l.balanceL x (node rs rl rx rr) = l.balance x (node rs rl rx rr)

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l
    · have : size rl = 0 ∧ size rr = 0 := by
        have := H1 rfl
        rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
      cases sr.2.1.size_eq_zero.1 this.1
      cases sr.2.2.size_eq_zero.1 this.2
      rw [sr.eq_node']; rfl
    · replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)
      simp [balanceL, balance, H2]; split_ifs <;> simp [add_comm]

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

Goal state before:
pp: n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ β✝ : TypeVec.{u} m
f✝ : α✝ ⟹ β✝
p✝ : ↑((P F).comp fun i ↦ P (G i)) α✝
⊢ Comp.mk ((fun x ↦ abs) <$$> abs (comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun x ↦ abs) <$$> abs (comp.get p✝))

Tactic:
← abs_map

Goal state after:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ β✝ : TypeVec.{u} m
f✝ : α✝ ⟹ β✝
p✝ : ↑((P F).comp fun i ↦ P (G i)) α✝
⊢ Comp.mk (abs ((fun x ↦ abs) <$$> comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun x ↦ abs) <$$> abs (comp.get p✝))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H : ?m.233
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
refine ⟨vl.balanceL h.right H, ?_⟩
        rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
        exact (e.add_right _).add_right _

Goal state after: