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

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ : Type u_1
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝

Tactic:
simp only [fmap_def, id_eq, map_id']

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ some b = lookup x s

Tactic:
h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ some b = some b
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
⊢ x.fst ≠ y.fst →
    ∀ (c : Sigma β),
      (c ∈ if a = x.fst then some ⟨a, b⟩ else none) →
        ∀ (d : Sigma β), (d ∈ if a = y.fst then some ⟨a, b⟩ else none) → x = y ∧ c = d

Tactic:
h

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
⊢ ∀ (c : Sigma β),
    (c ∈ if a = x.fst then some ⟨a, b⟩ else none) →
      ∀ (d : Sigma β), (d ∈ if a = y.fst then some ⟨a, b⟩ else none) → x = y ∧ c = d
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
⊢ ∀ (c : Sigma β),
    (c ∈ if a = x.fst then some ⟨a, b⟩ else none) →
      ∀ (d : Sigma β), (d ∈ if a = y.fst then some ⟨a, b⟩ else none) → x = y ∧ c = d

Tactic:
z

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
⊢ (z ∈ if a = x.fst then some ⟨a, b⟩ else none) →
    ∀ (d : Sigma β), (d ∈ if a = y.fst then some ⟨a, b⟩ else none) → x = y ∧ z = d
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
ha : a ∈ t
⊢ a ∈ image id t

Tactic:
by rwa [image_id]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys
h₂ : ¬a = s.fst
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂

Tactic:
simp_all [kerase_append_left]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert.refine_1
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j = i ∨ j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j

Tactic:
obtain (rfl | hj) := hj

Goal state after:
case insert.refine_1.inl
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
s : Finset ι
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
g : (a : ι) → a ∈ s → κ a
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
j : ι
hi : j ∉ s
h :
  ∀ (b : (a : ι) → a ∈ insert j s → κ a),
    (∀ (a : ι) (h : a ∈ insert j s), b a h ∈ t a) →
      f j (b j ⋯) ⊓ s.attach.inf ((fun i ↦ f (↑i) (b ↑i ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ j
ha : a ∈ t j
aux : ∀ (j_1 : ↥s), ↑j_1 ≠ j
hj : j ∈ insert j s
⊢ (if hji : j = j then cast ⋯ a else g j ⋯) ∈ t j

case insert.refine_1.inr
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ l'.NodupKeys

Tactic:
← hl

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ [].NodupKeys
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ (p ^ 2).divisors = {p ^ 2, p, 1}

Tactic:
by
  simp [divisors_prime_pow hp, range_add_one]

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
⊢ f.embSigma = g.embSigma → f = g

Tactic:
h

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
⊢ f = g
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← hiis]; exact t.2

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds
⊢ x.slice i hid ⟨is, hisds⟩ = y.slice i hid ⟨is, hisds⟩

Tactic:
h

Goal state after:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds
⊢ y.slice i hid ⟨is, hisds⟩ = y.slice i hid ⟨is, hisds⟩
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b

Tactic:
rw [Nat.testBit_bit_zero, Bool.not_not]

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

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)

Tactic:
by
  rw [← bitwise_xor, testBit_bitwise]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ foldr f b (a :: l) = foldr f (f a b) l

Tactic:
foldr_cons

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
a : α
b : β
hf : LeftCommutative f
⊢ f a (foldr f b l) = foldr f (f a b) l
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l.reverse = (dropWhile p l).reverse

Tactic:
simp_rw [rdropWhile, reverse_reverse]

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

Goal state before:
pp: case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
eq_nil_of_le h

Goal state after:
case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) []
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}
⊢ (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) m → n = m

Tactic:
h

Goal state after:
α : 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
Module: Mathlib.Data.List.Sections

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

Tactic:
induction h with

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

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ Acc (Shortlex r) (head :: tail)

Tactic:
apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ ∀ (s : List α), s.length < (head :: tail).length → Acc (Shortlex r) s
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ w[(j - n) % p]? = w[j % p]?

Tactic:
j_mod

Goal state after:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ w[j % p]? = w[j % p]?
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0

Tactic:
h

Goal state after:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R a = 0

Tactic:
h

Goal state after:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R 0 = 0
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case mpr
α : Type u_1
r : α → α → Bool
l : List (List α)
hn : ¬[] ∈ l
hc : ∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l
⊢ splitBy r l.flatten = l

Tactic:
exact splitBy_flatten hn hc hc'

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
⊢ Function.Injective2 fromRows

Tactic:
intro x1

Goal state after:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 : Matrix m₁ n R
⊢ ∀ ⦃a₂ : Matrix m₁ n R⦄ ⦃b₁ b₂ : Matrix m₂ n R⦄, x1.fromRows b₁ = a₂.fromRows b₂ → x1 = a₂ ∧ b₁ = b₂
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
⊢ Function.Injective2 fromCols

Tactic:
intro x1

Goal state after:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 : Matrix m n₁ R
⊢ ∀ ⦃a₂ : Matrix m n₁ R⦄ ⦃b₁ b₂ : Matrix m n₂ R⦄, x1.fromCols b₁ = a₂.fromCols b₂ → x1 = a₂ ∧ b₁ = b₂
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
ha : Acc LT.lt a
⊢ ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (a ::ₘ M)

Tactic:
by
  induction ha with | _ a _ ha
  rintro M hM
  induction hM with | _ M hM ihM
  refine .intro _ fun N hNM ↦ ?_
  obtain ⟨N, ⟨rfl, hNM'⟩ | ⟨rfl, hN⟩⟩ := isDershowitzMannaLT_singleton_insert hNM
  · exact ihM _ hNM'
  clear hNM
  induction N using Multiset.induction with
  | empty =>
    simpa using .intro _ hM
  | @cons b N ihN =>
    simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢
    obtain ⟨hba, hN⟩ := hN
    exact ha _ hba <| ihN hN

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

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat * p.toNNRat = q.toNNRat⁻¹ * p.toNNRat

Tactic:
toNNRat_inv

Goal state after:
p q : ℚ
hq : 0 ≤ q
⊢ q.toNNRat⁻¹ * p.toNNRat = q.toNNRat⁻¹ * p.toNNRat
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Tactic:
refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1

Tactic:
h

Goal state after:
n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ n + 1 ∣ n + 1
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits (b' % b) (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0

Tactic:
h

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits 1 (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
· rw [← h, ← prod_factorization_pow_eq_self hn]
    exact prod_dvd_prod_of_subset_of_dvd (support_mono hle) fun p _ ↦ Nat.pow_dvd_pow p <| hle p

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib - 2).succ + fib n.greatestFib

Tactic:
Nat.sub_succ,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib - 1).pred.succ + fib n.greatestFib
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inr
n a : ℕ
ha : a ∈ some (n + 1 - fib (n + 1).greatestFib).greatestFib
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
Option.mem_some_iff

Goal state after:
case inr
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k

Tactic:
rcases (Set.ofPred p).finite_or_infinite with hf | hf
  · rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
    rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk
    · rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
        ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h
    · rw [nth_of_card_le _ hk] at h
      exact absurd h (zero_le _).not_gt
  · rcases subset_range_nth ha with ⟨n, rfl⟩
    rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h

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

Goal state before:
pp: c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
by
  by_cases c <;> simp [*]

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

Goal state before:
pp: c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
by
  by_cases c <;> simp [*]

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

Goal state before:
pp: c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
by
  by_cases c <;> simp [*]

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ls

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordset

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

Tactic:
have := Valid'.dual h

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ n' ≥ n

Tactic:
simpa using hp

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:
← zneg_bit1,

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

Goal state before:
pp: case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).1) <$> u = ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
h

Goal state after:
case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).1) <$> ⟨a, f⟩ = ⟨a, fun i ↦ (↑(f i)).1⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : 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 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (1 + ml.size + 1) (mr.size + r.size + 1)

Tactic:
r1

Goal state after:
case pos
α : 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 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).2) <$> u = ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
h

Goal state after:
case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).2) <$> ⟨a, f⟩ = ⟨a, fun i ↦ (↑(f i)).2⟩
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P 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.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> u = ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
h

Goal state after:
case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P 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.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> ⟨a, f⟩ = ⟨a, fun i j ↦ (↑(f i j)).1⟩
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P 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.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).2) <$$> u = ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
h

Goal state after:
case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P 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.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).2) <$$> ⟨a, f⟩ = ⟨a, fun i j ↦ (↑(f i j)).2⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
⊢ x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch →
    (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch

Tactic:
h

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
⊢ (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (x.approx n.succ))), a ≍ a'' → children' (x.approx n.succ) a'' = ch a

Tactic:
h

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))),
    a ≍ a'' → children' (CofixA.intro (head' (x.approx 1)) ch) a'' = ch a
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
a : F.A
i : F.B a
ps : List F.Idx
x : F.M
a' : F.A
f : F.B a' → F.M
h : a = a'
⊢ F.B a = F.B a'

Tactic:
h

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f✝ : X → ↑F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
a : F.A
i : F.B a
ps : List F.Idx
x : F.M
a' : F.A
f : F.B a' → F.M
h : a = a'
⊢ F.B a' = F.B a'