mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros; simp only [callCC, ReaderT.callCC, ReaderT.goto_mkLabel, ReaderT.run_bind,
      ReaderT.run_monadLift, monadLift_self, callCC_bind_left]
    ext; rfl

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α : Type u
x : t' α
⊢ Equiv.map eqv id x = x

Tactic:
by
  simp [Equiv.map, id_map]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
⊢ fix _f = _f (fix _f)

Tactic:
dsimp [fix]
    conv_lhs => erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]
    rfl

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (z % 2 ^ (w + 1)).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))

Tactic:
have h : (2 ^ (w + 1) : Int) = (2 ^ (w + 1) : Nat) := by simp

Goal state after:
z : ℤ
w : ℕ
h : 2 ^ (w + 1) = ↑(2 ^ (w + 1))
⊢ (z % 2 ^ (w + 1)).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ f (E.symm (E (T x)))

Tactic:
by simpa using h₁ x

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
⊢ take m h (update v (castLE h i) x) = update (take m h v) i x

Tactic:
by
  ext j
  by_cases h' : j = i
  · rw [h']
    simp only [take, update_self]
  · have : castLE h j ≠ castLE h i := by simp [h']
    simp only [take, update_of_ne h', update_of_ne this]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ s ∈ enum (x :: xs) ↔ ∀ x_1 ∈ s, x_1 ∈ x :: xs

Tactic:
simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons,
        List.not_mem_nil, or_false, ih]

Goal state after:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs

Tactic:
induction xs generalizing s with

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s

Tactic:
rcases s with ⟨⟨a⟩, h⟩

Goal state after:
case mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) a)
⊢ C { entries := Quot.mk (⇑(isSetoid (Sigma β))) a, nodupKeys := h }
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ ⟨a, b'⟩ :: map (Sigma.mk a) (lookupAll a l) <+ ⟨a, b'⟩ :: l

Tactic:
exact (lookupAll_sublist a l).cons_cons _

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH : x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ tl ↔ ∃ f ∈ tl, f x ≠ 0
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ (hd :: tl) ↔ ∃ f ∈ hd :: tl, f x ≠ 0

Tactic:
simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
      mem_cons, exists_eq_or_imp]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g ↦ F f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
by
  ext
  simpa only [mem_neLocus] using! (hF _).ne_iff

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f ↦ F f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
by
  ext
  simpa only [mem_neLocus] using! (hF _).ne_iff

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

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

Tactic:
change ofNat _ = _

Goal state after:
case true
n : ℤ
⊢ ofNat (1 / 2) = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor] <;> simp

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

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

Tactic:
ext x
  simp only [mem_map, mem_filter, mem_Ico, castEmbedding_apply]
  constructor
  · simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h
  · intro h; lift x to ℕ using (by omega); exact ⟨x, by simp_all [natCast_modEq_iff]⟩

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

Goal state before:
pp: α : Type u_1
p : α → Bool
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]

Tactic:
by
  rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]

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

Goal state before:
pp: n m k : ℕ
⊢ range' (k + n) (m - n) = range' (n + k) (m + k - (n + k))

Tactic:
Nat.add_sub_add_right m k,

Goal state after:
n m k : ℕ
⊢ range' (k + n) (m - n) = range' (n + k) (m - n)
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
⊢ Acc (Shortlex r) l

Tactic:
apply ih

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 < (xa :: xb).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
⊢ Acc (Shortlex r) l

Tactic:
apply ih

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 < (xa :: xb).length
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: q : ℚ≥0
⊢ (↑q).num / ↑q.den = ↑q.num / ↑q.den

Tactic:
num_coe

Goal state after:
q : ℚ≥0
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit ↑(n + 1)! ↔ n + 1 < p

Tactic:
rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]

Goal state after:
case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ ¬p ∣ n + 1 ∧ n + 1 ≤ p ↔ n + 1 < p
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ {x | x ∈ t.val}.Pairwise (Coprime on s)

Tactic:
by simpa using pp

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

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

Tactic:
by
  induction k with
  | zero => simp [Int.ModEq.refl]
  | succ k ih =>
    grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp : Nat.Prime p ∧ p ∣ (Icc 1 (n - 1)).gcd n.choose ∧ ¬(Icc 1 (n - 1)).gcd n.choose = 0
⊢ p = n.minFac

Tactic:
obtain ⟨hp₁, hp₂, hp₃⟩ := hp

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₂ : p ∣ (Icc 1 (n - 1)).gcd n.choose
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
⊢ p = n.minFac
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 ↔ f (nth (fun i ↦ p (f i)) m') < f k

Tactic:
convert! Iff.rfl using 2

Goal state after:
case e'_2.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
⊢ f (nth (fun i ↦ p (f i)) m') = nth p m'
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ sub' 1 (a + a) = (neg a).bit1

Tactic:
rw [PosNum.one_sub', a.bit0_of_bit0]

Goal state after:
a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : (Ordnode.node s ml z mr).size = 1
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1

Goal state after:
case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Num.ZNum

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

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

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

Goal state before:
pp: n : ℕ
⊢ (↑(n + 1)).toZNum = ZNum.ofInt' ↑(n + 1)

Tactic:
rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]

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

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(neg a) = neg a

Tactic:
rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]

Goal state after:
a : PosNum
⊢ -(Num.pos a).toZNum = neg a
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
by
  rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F n
y : CofixA F n.succ
h : Agree x y
⊢ truncate y = x

Tactic:
by
  induction n with
  | zero =>
    cases x
    cases y
    rfl
  | succ n n_ih =>
    cases h with | intro f y h₁ =>
    simp only [truncate, Function.comp_def]
    congr with y
    exact n_ih _ _ (h₁ y)

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

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑(Num.pos n % d.abs) = ↑(pos n) % ↑d

Tactic:
rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]
      rfl

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

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : 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
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)

Tactic:
have := mk_inj h₂

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : 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
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
this : ⟨a✝, f✝⟩ = ⟨a, f₂⟩
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

Tactic:
← agree_iff_agree'

Goal state after:
case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (x.approx i) (x.approx (i + 1))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
rw [r0]; exact Nat.zero_le _

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).size + (Ordnode.node rs rl rx rr).size = ls + rs

Tactic:
hl.2.1

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).size + (Ordnode.node rs rl rx rr).size = ll.size + lr.size + 1 + rs
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: m n : ℕ+
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset

Tactic:
by
  apply le_antisymm
  · rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
    apply lcm_dvd <;> rw [← factorMultiset_le_iff']
    · exact le_sup_left
    · exact le_sup_right
  · apply sup_le_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
    · exact dvd_lcm_left m n
    · exact dvd_lcm_right m n

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : t.size = ls + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
hl.2.1

Goal state after:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h✝ : lrs < ratio * lls
⊢ (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)

Tactic:
simp [node3R, node']; abel

Goal state after:
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⟩
⊢ y = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩

pp: case h.right.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 α
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⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2

Tactic:
· rw [← yeq, ← abs_repr u, h, ← abs_map]; rfl

Goal state after:
case h.right.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 α
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⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2