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

Goal state before:
pp: a b r v x : ℕ
h : (↑a < ↑x ∧ ↑x ≤ ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ((a < x ∧ x ≤ b) ∧ x ≡ v [MOD r]) ∧ ↑x = ↑x

Tactic:
by simp_all [natCast_modEq_iff]

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
conv_lhs =>
    rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
    tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]
    rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈-↑(v % r) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑r * ↑(b / r) + (↑(b % r) - ↑(v % r))) / ↑r⌉

Tactic:
_root_.add_div,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈↑r * ↑(b / r) / ↑r + (↑(b % r) - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case h_2
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x✝ : Bool
heq✝ : p head = false
⊢ (head :: tail).length ≤ tail.length + 1

Tactic:
· simp

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
⊢ dropWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p [][0] = true

pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
· simp

Goal state after:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true

Tactic:
hp,

Goal state after:
case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match true with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
⊢ rdropWhile p [] = []

Tactic:
by simp [rdropWhile]

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

Goal state before:
pp: case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ some head = (head :: tail).head?

pp: case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true

Tactic:
· simp

Goal state after:
case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by simp [rdropWhile]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []

Tactic:
by
  simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []

Tactic:
rw [rtakeWhile_concat, if_neg h]

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

Goal state before:
pp: case e'_3
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
x✝ : α
⊢ p x✝ = !!p x✝

pp: case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true

Tactic:
· simp

Goal state after:
case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])

Tactic:
simp only [nil_append, modifyLast.go]

Goal state after:
case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ r.toListAppend [f a] = r.toListAppend (#[].toListAppend [f a])
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ Ico n l ++ [] = Ico n l

Tactic:
append_nil

Goal state after:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ Ico n l = Ico n l
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)

Tactic:
exact ⟨c :: m, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)

Tactic:
change (Set.range fun l => _) ⊆ Set.range fun l => _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ (Set.range fun l ↦ foldl f a l) ⊆ Set.range fun l ↦ foldl g a l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l

pp: case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l

Tactic:
· simp

Goal state after:
case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]

pp: case succ
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]

Tactic:
· simp

Goal state after:
case succ
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]
Module: Mathlib.Data.List.SplitLengths

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

pp: 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✝

Tactic:
· simp

Goal state after:
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.SplitBy

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

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

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
⊢ splitBy r (l ++ m) = splitBy r l ++ splitBy r m
Module: Mathlib.Data.List.SplitBy

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

pp: case inr.inr
α : 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 ++ m) = splitBy r l ++ splitBy r m

Tactic:
· simp

Goal state after:
case inr.inr
α : 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 ++ m) = splitBy r l ++ splitBy r m
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:
induction ha with | _ a _ ha

Goal state after:
case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
⊢ ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (a ::ₘ M)
Module: Mathlib.Data.Multiset.DershowitzManna

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

Tactic:
← transGen_oneStep_eq_isDershowitzMannaLT

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded (TransGen OneStep)
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
⊢ ⌈↑0⌉₊ = ⌈0⌉₊

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:
· simp

Goal state after:
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⌉₊
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b

pp: case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
· simp

Goal state after:
case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
· simp

Goal state after:
case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case pos
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)
⊢ 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

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:
· simp

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 : (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))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
i : ℕ
hi : i ∈ Icc 1 (n - 1)
⊢ i ≠ 0

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
i : ℕ
hi : i ∈ Icc 1 (n - 1)
⊢ i ≠ n.minFac ^ k

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ 1 ∈ Icc 1 (n - 1)

Tactic:
by grind

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

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

Tactic:
by
  constructor
  · rintro ⟨u, xeq, yeq⟩
    rcases h : u with ⟨a, f⟩
    use a, fun i => (f i).val.fst, fun i => (f i).val.snd
    constructor
    · rw [← xeq, h]
      rfl
    constructor
    · rw [← yeq, h]
      rfl
    intro i
    exact (f i).property
  rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
  use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
  constructor
  · rw [xeq]
    rfl
  rw [yeq]; rfl

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

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
by
    transfer_rw
    apply mul_pos

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑n = ↑n

Tactic:
by
  rw [← cast_to_int, to_of_int]

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

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r - ↑(Num.pos d) = ↑r₂ ↔ ↑r = ↑r₂ + ↑d

Tactic:
sub_eq_iff_eq_add,

Goal state after:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑r = ↑r₂ + ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d

Tactic:
rwa [this, two_mul, add_lt_add_iff_right] at h₂

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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
⊢ Approx.sMk x.dest (n + 1) = x.approx (n + 1)

Tactic:
| succ n =>

Goal state after:
case succ
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
⊢ Approx.sMk x.dest (n + 1) = x.approx (n + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case h₂
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) ≤ ↑(pos a) * (↑(pos a) / ↑(pos a))

pp: case hy
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 0 < ↑(pos a)

Tactic:
· simp

Goal state after:
case hy
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 0 < ↑(pos a)
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:
by
  induction ps generalizing x with
  | nil =>
    exfalso
    apply h
    constructor
  | cons ps_hd ps_tail ps_ih =>
    obtain ⟨a, i⟩ := ps_hd
    induction x using PFunctor.M.casesOn' with | _ x_a x_f
    simp only [iselect, isubtree] at ps_ih ⊢
    by_cases h'' : a = x_a
    · subst x_a
      simp only [dif_pos, casesOn_mk']
      rw [ps_ih]
      intro h'
      apply h
      constructor <;> try rfl
      apply h'
    · simp [*]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨i, a, hji⟩ | ⟨i, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b → b ≤ a → a = b

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨_, _, hlt₁⟩ | ⟨_, hlt₁⟩) (⟨_, _, hlt₂⟩ | ⟨_, hlt₂⟩)

Goal state after:
case left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
hlt₁ : a₁ < a₂
hlt₂ : a₂ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩
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 : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : ?m.119
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
suffices H₁ : _ by
      refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
      · rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
      · rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel
    · rw [e, add_right_comm]; rintro ⟨⟩

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

Goal state before:
pp: a b : ℕ+
this : 0 < ↑a
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
have := b.pos

Goal state after:
a b : ℕ+
this✝ : 0 < ↑a
this : 0 < ↑b
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)
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
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ (corec₁ g x).dest = g _root_.id (corec₁ g) x

Tactic:
Cofix.corec₁,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ (corec' (fun x ↦ g Sum.inl Sum.inr x) x).dest = g _root_.id (corec₁ g) x
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) none none

pp: case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
a : α × WSeq α
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) (some a) (some a)

Tactic:
· simp

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
a : α × WSeq α
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) (some a) (some a)
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case none
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
simp [enumerate_eq_none_of_sel, h]

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h_1
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : s.think = c
o✝ : α ⊕ List (Computation α)
a✝ : α
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a✝
⊢ Sum.inl a✝ = Sum.inr l' → s ∈ l'

pp: case h_2
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : s.think = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls✝
⊢ (match s.think.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls✝)) =
      Sum.inr l' →
    s ∈ l'

Tactic:
· simp

Goal state after:
case h_2
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : s.think = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls✝
⊢ (match s.think.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls✝)) =
      Sum.inr l' →
    s ∈ l'