mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case right
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 = x + 1 / 2 - 1

Tactic:
linarith

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊a - ↑z⌋ = ⌊a + ↑(-z)⌋

Tactic:
by rw [Int.cast_neg, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊↑n * a⌋ / n = ⌊a⌋

Tactic:
Commute.intCast_left,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊a * ↑n⌋ / n = ⌊a⌋
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ False

Tactic:
suffices 0 < k ∧ k < 1 by lia

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ False

Tactic:
suffices 0 < k ∧ k < 1 by lia

Goal state after:
case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ 0 < k ∧ k < 1
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ 1 + ↑n * (a - 1) ≤ a ^ n

Tactic:
have : -2 ≤ a - 1 := by
    rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
this : -2 ≤ a - 1
⊢ 1 + ↑n * (a - 1) ≤ a ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌈a - ↑z⌉ = ⌈a + ↑(-z)⌉

Tactic:
by rw [Int.cast_neg, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ 0 < 1 - b

Tactic:
linarith

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
⊢ 0 < a - 1

Tactic:
linarith

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

Goal state before:
pp: q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1

Tactic:
simp [this]

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num

Tactic:
have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den := by
    have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
    have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
    rwa [← sub_lt_iff_lt_add'] at this

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
h : p₁ /ₛ p₂ = 1
⊢ 1 • p₂ = p₂

Tactic:
one_smul

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
h : p₁ /ₛ p₂ = 1
⊢ p₂ = p₂
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ 1 • 1 = 1

Tactic:
one_smul

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ 1 = 1
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Multiset α
nodup✝¹ : s.Nodup
t : Multiset α
nodup✝ : t.Nodup
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }

Tactic:
cases h

Goal state after:
case refl
α : Type u_1
s : Multiset α
nodup✝¹ nodup✝ : s.Nodup
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ • p₁ = v₂ • p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂

Tactic:
rw [smul_eq_smul_iff_inv_mul_eq_sdiv, inv_mul_eq_div]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁴ : Group G
inst✝³ : Torsor G P
inst✝² : SMul G Q
inst✝¹ : SDiv G Q
inst✝ : Nonempty Q
f : Q → P
hf : Injective f
smul : ∀ (c : G) (x : Q), f (c • x) = c • f x
sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y
x y : Q
⊢ f ((x /ₛ y) • y) = f x

Tactic:
simp only [sdiv, smul, sdiv_smul]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t

Tactic:
by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ {a} + s + t = {a} + (s + t)

Tactic:
Multiset.add_assoc

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ {a} + (s + t) = {a} + (s + t)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧

Tactic:
convert! List.count_erase_of_ne ab (l := l) <;> rw [← coe_count] <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
by_cases h : x = y

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b

Tactic:
← filter_eq',

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = filter (fun x ↦ x = b) s
Module: Mathlib.Data.Finset.Empty

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ (∃ a, a ∈ s ∧ true = true) ↔ s.Nonempty

Tactic:
by simp [Finset.Nonempty]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
rw [erase_of_notMem m]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
· rw [filter_cons_of_neg _ h]
    by_cases m : a ∈ s
    · rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
        cons_erase m]
    · rw [erase_of_notMem m]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter p s.attach = map (Subtype.map id ⋯) (filter (fun x ↦ ∃ h, p ⟨x, h⟩) s).attach

Tactic:
classical
  refine Multiset.map_injective Subtype.val_injective ?_
  rw [map_filter' _ Subtype.val_injective]
  simp only [Subtype.exists, exists_and_right, exists_eq_right, attach_map_val, Subtype.map, id,
    map_map, comp]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length

Tactic:
tauto

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
htq : x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s
⊢ x✝ = ∅

Tactic:
by_contra! ⟨_, hx⟩

Goal state after:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
htq : x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s
w✝ : α
hx : w✝ ∈ x✝
⊢ False
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∈ s, a ∈ t) ↔ (s ∩ t).Nonempty

Tactic:
by simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ insert a (s.erase a) = t

Tactic:
← insert_erase ht,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ insert a (s.erase a) = insert a (t.erase a)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = i.rev.rev.pred ⋯

Tactic:
predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)),

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ i.pred ⋯ = i.rev.rev.pred ⋯
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ f ≍ g

Tactic:
cases h

Goal state after:
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ f ≍ f
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ) (finRange n) ~ finRange n

Tactic:
rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
  simpa [mem_map, mem_finRange] using! σ.surjective

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i ≤ p
hp : p ≠ last n
⊢ (p.castPred hp).predAbove i = i.castPred ⋯

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.6
s : Multiset α
l : List α
h : ∃ x, x ∈ ⟦l⟧
x✝ : ∃ x, x ∈ ⟦[]⟧
⊢ False

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]

Goal state after:
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset = univ ↔ s = Set.univ

Tactic:
← Set.toFinset_univ,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset = Set.univ.toFinset ↔ s = Set.univ
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case refine_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

pp: case refine_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
· exact Or.inl ⟨rfl, hm⟩

Goal state after:
case refine_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
⊢ [x, x] <+ l

Tactic:
cases h

Goal state after:
case neg.cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
a✝ : [x, x] <+ l
⊢ [x, x] <+ l

case neg.cons_cons
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
⊢ init (update q (last n) z) = init q

Tactic:
by
  ext j
  simp [init, Fin.ne_of_lt]

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b

pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

pp: case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
· have := Nat.lt_add_right m lt_n
    contradiction

Goal state after:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b

Tactic:
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
      rw [hx a, hx b]

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: case step
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : (n + 2).le 0
⊢ False

Tactic:
cases h

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

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hf : l[i]? = l'[f i]?
hi : i < l.length
⊢ f i < l'.length

Tactic:
getElem?_eq_getElem hi,

Goal state after:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : some l[i] = l'[f i]?
⊢ f i < l'.length
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩

Goal state after:
case mp.refine_1
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∀ (a b : Fin l.length), ⟨f ↑a, ⋯⟩ ≤ ⟨f ↑b, ⋯⟩ ↔ a ≤ b

case mp.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∀ (ix : Fin l.length), l.get ix = l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ?mp.refine_1) ix)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) → ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

pp: case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)) → ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
· rintro ⟨f, hf⟩
    have h : ∀ {i : ℕ}, i < l.length → f i < l'.length := by
      intro i hi
      specialize hf i
      rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
      obtain ⟨h, -⟩ := hf
      exact h
    refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩
    · simp
    · intro i
      apply Option.some_injective
      simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i

Goal state after:
case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)) → ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.removeNth (p.insertNth a f) x✝ = f x✝

Tactic:
unfold removeNth

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.insertNth a f (p.succAbove x✝) = f x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = i.removeNth fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)

Tactic:
unfold removeNth

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = fun i_1 ↦
      (fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)) (i.succAbove i_1)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ ∀ (a a' : Fin n), a ≍ a' → i.removeNth (j.removeNth m) a ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) a'

Tactic:
simp only [heq_iff_eq]

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ ∀ (a a' : Fin n), a = a' → i.removeNth (j.removeNth m) a ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) a'
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ i.removeNth (j.removeNth m) k ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) k

Tactic:
unfold removeNth

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ m (j.succAbove (i.succAbove k)) ≍ m ((j.succAbove i).succAbove ((i.predAbove j).succAbove k))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h)

Tactic:
by simp_rw [find?_eq_dite, h, dite_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))

Tactic:
induction s using Finset.induction_on with
    | empty => simp [hb]
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
l₁ : List α
h : Lex r l₁ []
⊢ False

Tactic:
cases h

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁

Tactic:
exact hl.sublist h

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

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Tactic:
mod_eq_of_lt hm,

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[m + n % l.length]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate i = l.rotate j
⊢ i % l.length = j % l.length

Tactic:
rw [← rotate_mod l i, ← rotate_mod l j] at h

Goal state after:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
x✝ : β
⊢ (∃ t, (∃ i ∈ I, t ∈ f i) ∧ x✝ ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x✝ ∈ t

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ (↑s).PairwiseDisjoint fun a ↦ (f a).disjUnion (g a) ⋯

Tactic:
by
  intros i hi j hj hij
  simp [hf hi hj hij, hg hi hj hij, hfg' hi hj hij, (hfg' hj hi hij.symm).symm]

Goal state after: