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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ (erase a ⟦s⟧).keys = ⟦s⟧.keys.erase a

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ a' ∈ erase a ⟦s⟧ ↔ a' ≠ a ∧ a' ∈ ⟦s⟧

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ ¬(b :: c :: l).length ≤ 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ ¬hd.fst ∈ [].keys

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ kerase hd.fst (hd :: tl) = [] ++ tl

Tactic:
by simp

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
this : dm₁ = dm₂
⊢ (dm₁, dn₁).2 = (dm₂, dn₂).2

Tactic:
rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd

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

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

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

Tactic:
· subst a'
      rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ⟨i, x⟩.snd ∈ update g i (insert x (g i)) ⟨i, x⟩.fst

Tactic:
by simp

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
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
by
  classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm
  obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp
  subst hl
  rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise,
    ← List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : Mul α
x : Holor α []
y : Holor α ds
⊢ x ⊗ y = x ⟨[], ⋯⟩ • y

Tactic:
simp +unfoldPartialApp [mul, SMul.smul, HolorIndex.take, HolorIndex.drop,
    HSMul.hSMul]

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ ↑n

Tactic:
by simp

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

Goal state before:
pp: case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))

Tactic:
· by_cases h : f true true <;> simp +decide [h]

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

Goal state before:
pp: n : ℕ
⊢ Nat.shiftLeft' false 0 n = 0

Tactic:
by simp

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

Goal state before:
pp: a✝ : ℕ
⊢ 0 >>> a✝.succ = 0

Tactic:
by simp

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -↑(v % r) ≤ 0

Tactic:
by simp

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ r ≤ r + v % r

Tactic:
by simp

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ r ≤ r + b % r

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : List β
⊢ map₂Left f [] x✝ = (map₂Left' f [] x✝).fst

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
⊢ map₂Left f (a :: as) [] = (map₂Left' f (a :: as) []).fst

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : [].length ≤ [].length
⊢ map₂Left f [] [] = zipWith (fun a b ↦ f a (some b)) [] []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : β
tail✝ : List β
x✝ : [].length ≤ (head✝ :: tail✝).length
⊢ map₂Left f [] (head✝ :: tail✝) = zipWith (fun a b ↦ f a (some b)) [] (head✝ :: tail✝)

Tactic:
by simp

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

Goal state before:
pp: n m : ℕ
⊢ ¬m ∈ Ico n m

Tactic:
by simp

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ [].reverse = []

Tactic:
(exact rfl)

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

Goal state before:
pp: case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

Tactic:
(exact rfl)

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

Goal state before:
pp: case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])

Tactic:
(exact rfl)

Goal state after:
case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ ∀ (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (x :: (l ++ [b])).reverse = x :: (l ++ [b]) → (x :: (l ++ [b])).Palindrome

Tactic:
l

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
⊢ ∀ (b : α), (l.reverse = l → l.Palindrome) → (x :: (l ++ [b])).reverse = x :: (l ++ [b]) → (x :: (l ++ [b])).Palindrome
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ l ++ m = (splitBy r l ++ splitBy r m).flatten

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ ¬[] ∈ splitBy r l ++ splitBy r m

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t x : Multiset α
⊢ x ∈ Finset.map equivDFinsupp.symm.toEmbedding (Finset.Icc (toDFinsupp s) (toDFinsupp t)) ↔ s ≤ x ∧ x ≤ t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ {a} ≠ ∅

Tactic:
by simp

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

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

Tactic:
convert! Rat.mul_num q₁ q₂ <;> norm_cast

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ⌈↑m⌉₊ = ↑m

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ⌈↑(Int.negOfNat m)⌉₊ = ↑0

Tactic:
by simp

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

Goal state before:
pp: case cons
ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ a ≡ b [MOD (List.map s (i :: l)).prod] ↔ ∀ i_1 ∈ i :: l, a ≡ b [MOD s i_1]

Tactic:
have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
x✝ : List.Pairwise (Coprime on s) []
⊢ ∀ i ∈ [], 0 ≡ a i [MOD s i]

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ 10 % 3 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ 10 % 9 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ ↑11 ∣ ↑10 - -1

Tactic:
by simp

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + (k + 1))!
⊢ IsUnit ↑m !

Tactic:
| succ k ih =>

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

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 ≤ a.factorization ⌊/⌋ n

Tactic:
by simp

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ↑(n.choose k) ≡
    ↑((n / p ^ zero).choose (k / p ^ zero)) * ↑(∏ i ∈ range zero, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
by simp

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

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

Tactic:
| succ k ih =>

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

Goal state before:
pp: α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a

Tactic:
by simp

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ BddBelow {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
by simp

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

Goal state before:
pp: n : PosNum
⊢ ↑n + ↑n + 1 ≤ ↑n + ↑n + ↑n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit1 = ↑(pos p) + ↑(pos p) + 1

Tactic:
ZNum.bit1,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p.bit1) = ↑(pos p) + ↑(pos p) + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p).bit1 = ↑(neg p) + ↑(neg p) + 1

Tactic:
ZNum.bit1,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg (Num.casesOn p.pred' 1 bit1)) = ↑(neg p) + ↑(neg p) + 1
Module: Mathlib.Data.Num.ZNum

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

Tactic:
dsimp only [Num.succ'] at ep
      subst p
      have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (-↑a : ℤ) 1]
      simpa using this

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

Goal state before:
pp: n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).toZNumNeg.pred + 1

Tactic:
@ofNat'_succ n,

Goal state after:
n : ℕ
⊢ (ofNat' n + 1).toZNumNeg = (ofNat' n + 1).toZNumNeg.pred + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNumNeg = -(Num.ofNat' (n + 1)).toZNum

Tactic:
rw [Num.zneg_toZNum]

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

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ LiftP p x → ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
rintro ⟨y, hy⟩
    rcases h : y with ⟨a, f⟩
    refine ⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩
    rw [← hy, h, map_eq]
    rfl

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

Goal state before:
pp: α : Type u_1
t : Ordnode α
ht : t.Sized
⊢ t.size = 0 ↔ t = nil

Tactic:
cases t

Goal state after:
case nil
α : Type u_1
ht : nil.Sized
⊢ nil.size = 0 ↔ nil = nil

case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ht : (node size✝ l✝ x✝ r✝).Sized
⊢ (node size✝ l✝ x✝ r✝).size = 0 ↔ node size✝ l✝ x✝ r✝ = nil
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.dual.size = t.size

Tactic:
cases t

Goal state after:
case nil
α : Type u_1
⊢ nil.dual.size = nil.size

case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).dual.size = (node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), (a + b) * c = a * c + b * c

Tactic:
by
      transfer
      simp [mul_add, _root_.mul_comm]

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

Goal state before:
pp: n : ℤ
⊢ ↑↑0 = 0

Tactic:
by simp

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

Goal state before:
pp: n : ℤ
⊢ ∀ (k : ℤ), 0 ≤ k → ↑↑k = k → ↑↑(k + 1) = k + 1

Tactic:
by simp

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

Goal state before:
pp: n : ℤ
⊢ ∀ (k : ℤ), k ≤ 0 → ↑↑k = k → ↑↑(k - 1) = k - 1

Tactic:
by simp

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

Goal state before:
pp: d : PosNum
⊢ ↑1 + ↑d * (↑0 + ↑0) = ↑one

Tactic:
by simp

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x : F.M
⊢ M.mk x.dest = x

Tactic:
apply ext'

Goal state after:
F : PFunctor.{uA, uB}
x : F.M
⊢ ∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
by simp

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

Goal state before:
pp: ⊢ ↑(0 % 0) = ↑0 % ↑0

Tactic:
by simp

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

Goal state before:
pp: F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ (M.mk ⟨a, x⟩).children i = x (cast ⋯ i)

Tactic:
apply ext'

Goal state after:
F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ ∀ (i_1 : ℕ), ((M.mk ⟨a, x⟩).children i).approx i_1 = (x (cast ⋯ i)).approx i_1
Module: Mathlib.Data.Ordmap.Ordset

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

Tactic:
replace H3 := H3p l0

Goal state after:
case pos.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size > 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ ⟨a₁, f₁⟩ = ⟨a₂, f₂⟩

Tactic:
dsimp [mp] at *

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ ⟨a₁, f₁⟩ = ⟨a₂, f₂⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: 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
⊢ x = y

Tactic:
apply ext'

Goal state after:
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 : ℕ), x.approx i = y.approx i
Module: Mathlib.Data.Ordmap.Ordset

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

Tactic:
exact
      Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Sized
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
cases t

Goal state after:
case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size

case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.merge nil = t

Tactic:
cases t

Goal state after:
case nil
α : Type u_1
⊢ nil.merge nil = nil

case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).merge nil = node size✝ l✝ x✝ r✝
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
⊢ dropFun g = dropFun (dropFun g ::: fun x ↦ dropFun g <$$> x)

Tactic:
by simp

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ 1 < PNat.find h ↔ ¬p 1

Tactic:
by simp

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

Goal state before:
pp: u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
⊢ u.r - 1 < u.bp

Tactic:
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos

Goal state after:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r < u.bp + 1
⊢ u.r - 1 < u.bp
Module: Mathlib.Data.PNat.Xgcd

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

Tactic:
by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h, flip_isReduced]
      apply reduce_isReduced

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

Goal state before:
pp: n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1

Tactic:
rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
⊢ t.Bounded o₁ o₂

Tactic:
have := Bounded.dual h

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ IsPrecongr r'

Tactic:
intro a b r'ab

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)