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

Goal state before:
pp: case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
rcases h' with h' | h'

Goal state after:
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

Tactic:
by by_cases h : a = s.1 <;> simp [h, kerase_comm a s.1 l, kunion_kerase]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ l.lookupFinsupp a = x ↔ x ∈ lookup a l

Tactic:
rw [lookupFinsupp_apply]
  rcases lookup a l with - | m <;> simp [hx.symm]

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

Goal state before:
pp: b : Bool
n : ℤ
⊢ (bit b n).bodd = b

Tactic:
rw [bit_val]
  cases b <;> cases bodd n <;> simp [(show bodd 2 = false by rfl)]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod x

Tactic:
have h_dds_prod : (List.cons d ds).prod = Finset.card (Finset.range d) * prod ds := by
      simp [Finset.card_range]

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
⊢ CPRankMax (d :: ds).prod x
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n

Tactic:
· congr
    simp

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

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]

Tactic:
· congr
    simp

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ x && !!y) m n) = ↑(m &&& n)

pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x && !y)) m n = m ||| n

pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)

Tactic:
· congr
    simp

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x && !y)) m n = m ||| n

case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x && !y)) m n = m ||| n

pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)

Tactic:
· congr
    simp

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (Ico n m).length = m - n

Tactic:
by
  dsimp [Ico]
  simp [length_range']

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

Goal state before:
pp: case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
eq_nil_of_le hml,

Goal state after:
case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = []
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
⊢ (sz.splitLengths l).length = sz.length

Tactic:
induction sz generalizing l

Goal state after:
case nil
α : Type u_1
l : List α
⊢ ([].splitLengths l).length = [].length

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (tail✝.splitLengths l).length = tail✝.length
l : List α
⊢ ((head✝ :: tail✝).splitLengths l).length = (head✝ :: tail✝).length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
h : l.length ≤ sz.sum
⊢ (sz.splitLengths l).flatten = l

Tactic:
induction sz generalizing l

Goal state after:
case nil
α : Type u_1
l : List α
h : l.length ≤ [].sum
⊢ ([].splitLengths l).flatten = l

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), l.length ≤ tail✝.sum → (tail✝.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head✝ :: tail✝).sum
⊢ ((head✝ :: tail✝).splitLengths l).flatten = l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
⊢ map length (sz.splitLengths l) = sz

Tactic:
induction sz generalizing l

Goal state after:
case nil
α : Type u_1
l : List α
h : [].sum ≤ l.length
⊢ map length ([].splitLengths l) = []

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), tail✝.sum ≤ l.length → map length (tail✝.splitLengths l) = tail✝
l : List α
h : (head✝ :: tail✝).sum ≤ l.length
⊢ map length ((head✝ :: tail✝).splitLengths l) = head✝ :: tail✝
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| (take (i + 1) sz)[i]

Tactic:
simp +singlePass only [← map_splitLengths_length l _ h]

Goal state after:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| (map length ((take (i + 1) sz).splitLengths l))[i]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun b a ↦ r a b = true) (a :: g).reverse.reverse

Tactic:
rw [reverse_reverse]

Goal state after:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun b a ↦ r a b = true) (a :: g)
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
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
by_cases j_lt_n : j < n

Goal state after:
case pos
α : 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_lt_n : j < n
⊢ (take n w ++ w)[j]? = w[j % p]?

case neg
α : 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_lt_n : ¬j < n
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_2
α : 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
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

Tactic:
rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded IsDershowitzMannaLT

Tactic:
rw [← transGen_oneStep_eq_isDershowitzMannaLT]
  exact isDershowitzMannaLT_singleton_wf.transGen

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

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ b ∣ n ↔ ↑b ∣ ofDigits c (b'.digits n)

Tactic:
← Int.natCast_dvd_natCast

Goal state after:
b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ ↑b ∣ ↑n ↔ ↑b ∣ ofDigits c (b'.digits n)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
rw [mem_product, mem_range, mem_range, not_and_or, Nat.lt_succ_iff, not_le, not_lt] at h

Goal state after:
case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : n % p < (k % p, k / p).1 ∨ n / p + 1 ≤ (k % p, k / p).2
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ (map fib n.zeckendorf).sum = n

Tactic:
induction n using zeckendorf.induct

Goal state after:
case case1
⊢ (map fib (zeckendorf 0)).sum = 0

case case2
n✝ : ℕ
ih1✝ : (map fib (n✝ + 1 - fib (n✝ + 1).greatestFib).zeckendorf).sum = n✝ + 1 - fib (n✝ + 1).greatestFib
⊢ (map fib n✝.succ.zeckendorf).sum = n✝.succ
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
have isPrime := minFac_prime_iff.mpr (IsPrimePow.ne_one h)

Goal state after:
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
⊢ ¬n.minFac ^ 2 ∣ (Icc 1 (n - 1)).gcd n.choose
Module: Mathlib.Data.Nat.Choose.Lucas

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

Tactic:
refine emultiplicity_lt_iff_not_dvd.mp ?_
    nth_rw 2 [hn₁]
    rw [Nat.Prime.emultiplicity_choose_prime_pow isPrime this (pow_ne_zero _
      (Nat.Prime.ne_zero isPrime)), multiplicity_pow_self_of_prime (prime_iff.mp isPrime)]
    norm_cast
    grind

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

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

Tactic:
· refine emultiplicity_lt_iff_not_dvd.mp ?_
    nth_rw 2 [hn₁]
    rw [Nat.Prime.emultiplicity_choose_prime_pow isPrime this (pow_ne_zero _
      (Nat.Prime.ne_zero isPrime)), multiplicity_pow_self_of_prime (prime_iff.mp isPrime)]
    norm_cast
    grind

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
⊢ ((Icc 1 (n - 1)).gcd n.choose).primeFactors = {n.minFac}

Tactic:
have isPrime := minFac_prime_iff.mpr (IsPrimePow.ne_one h)

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ ((Icc 1 (n - 1)).gcd n.choose).primeFactors = {n.minFac}
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac

Tactic:
have isPrime := minFac_prime_iff.mpr (IsPrimePow.ne_one h)

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac
Module: Mathlib.Data.Nat.Nth

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

Tactic:
Finset.length_sort

Goal state after:
case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ #hf.toFinset ≤ n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
    exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]

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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact node (rs + 1) nil x r
    · refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r
      rcases id ll with _ | lls
      · exact nil
      --should not happen
      rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
      · exact nil
      --should not happen
      exact
        if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x r)
        else
          node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
            (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) → Liftr r x y

Tactic:
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩

Goal state after:
case mpr
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
Module: Mathlib.Data.PFunctor.Multivariate.Basic

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

Tactic:
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩

Goal state after:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a ⟹ α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
⊢ LiftR r x y
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
x : F.M
h : ¬IsPath ps x
⊢ iselect ps x = default.head

Tactic:
induction ps generalizing x with

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

Goal state before:
pp: case succ.hrec
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
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y

Tactic:
dsimp only [iselect] at H

Goal state after:
case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y
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
i : ℕ
⊢ x.approx i = y.approx i

Tactic:
induction i with

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

Goal state before:
pp: case mpr
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 f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)) → LiftR r x y

Tactic:
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩

Goal state after:
case mpr
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)
⊢ LiftR r x y
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
by
  rw [Nat.dist_comm]; exact H.dist_le

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

Goal state before:
pp: case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size

Tactic:
intro l1

Goal state after:
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
⊢ 1 ≤ r.size → r.size ≤ delta * l.size
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 ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get) (f✝ <$$> p✝) =
    f✝ <$$> (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get) p✝

Tactic:
simp only [(· ∘ ·)]

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 ((fun x ↦ abs) <$$> abs (comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun x ↦ abs) <$$> abs (comp.get p✝))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ (∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)) → Liftr r x y

Tactic:
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩

Goal state after:
case mpr
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → 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 : (P F).B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv x x

Tactic:
by
  obtain ⟨a, f⟩ := x
  exact Wequiv.abs a f a f rfl

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ (-r).sign = -r.sign

Tactic:
rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
⊢ 0 ≤ r.sign * r

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn]
    exact mul_nonneg_of_nonpos_of_nonpos (by simp) hn.le
  · rw [mul_zero]
  · rw [sign_of_pos hp, one_mul]
    exact hp.le

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ 0 < r.sign * r

Tactic:
by
  refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_
  have hs0 := (zero_eq_mul.mp h).resolve_right hr
  exact sign_eq_zero_iff.mp hs0

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

Goal state before:
pp: case h₀
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
i : Fin2 n
x : (α ::: ι).drop i
⊢ subtypeVal α.repeatEq i (diagSub i x) = prod.diag i x

Tactic:
induction i with

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
s : WSeq α
a : α
md : none ∈ s.tail.destruct
e : Prod.fst <$> none = some a
⊢ ∃ a', some a' ∈ s.head

Tactic:
injection e

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
have := Computation.mem_unique (Computation.mem_map _ om) h

Goal state after:
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
this : Prod.fst <$> o = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
⊢ F l
      (List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) l) →
    F (c :: l)
      (match
        List.foldr
          (fun c o ↦
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
cases List.foldr (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c)) (Sum.inr List.nil) l <;>
        intro IH

Goal state after:
case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
IH : F l (Sum.inl val✝)
⊢ F (c :: l)
    (match Sum.inl val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
⊢ F (c :: l)
    (match Sum.inr val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
f : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard) → ↑s :=
  fun x ↦
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
t t' : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)
h : f t = f t'
⊢ ↑↑t = ↑↑t'

Tactic:
exact (hP.2 (f t)).unique (hf t) (h ▸ hf t')

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬⟨i, b⟩ ≤ ⟨i, a⟩
⊢ ⟨i, a⟩ < ⟨i, b⟩

Tactic:
mk_le_mk_iff

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬b ≤ a
⊢ ⟨i, a⟩ < ⟨i, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_2.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
a b : α i✝
hab : a ≤ b
hba : ¬⟨i✝, b⟩ ≤ ⟨i✝, a⟩
⊢ ⟨i✝, a⟩ < ⟨i✝, b⟩

Tactic:
· exact Sigma.Lex.right _ _ (hab.lt_of_not_ge fun h => hba <| Sigma.Lex.right _ _ h)

Goal state after: