mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ≥0
⊢ ↑q < 0 ↔ q < 0

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ ↑p ≤ 1 ↔ p ≤ 1

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ 1 ≤ ↑p ↔ 1 ≤ p

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ ↑p < 1 ↔ p < 1

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ 1 < ↑p ↔ 1 < p

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ (-↑n)) = ↑q ^ (-↑n)

Tactic:
simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ ^ n = (↑q)⁻¹ ^ n
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ ↑↑(↑a✝ * 10 ^ ↑n✝) = ↑(a✝ * 10 ^ n✝)

Tactic:
norm_cast

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

Goal state before:
pp: case succ.succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n + 1) → p ⟨n + 1, h⟩
h : 0 < n + 1 + 1
⊢ p ⟨n + 1 + 1, h⟩

Tactic:
exact succ _ (IH n.succ_pos)

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y

Tactic:
norm_cast

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑(-y)) = round x - y
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1

Tactic:
norm_cast

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ 0 < ↑n

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)

Tactic:
zpow_add_one

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n

Tactic:
zpow_add_one

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
zpow_add_one

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
⊢ a ^ 2 + ↑2 * a ^ 1 * b + b ^ 2 = (a + b) ^ 2

Tactic:
by simp [sq, add_mul, mul_add, two_mul, Hcomm.eq, add_assoc]

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
m n : ℕ
hn : n > 0
⊢ 0 < ↑n

Tactic:
norm_cast

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

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)

Tactic:
norm_cast

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑(n * (m / n))
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
m : ℤ
n : ℕ
hn : n > 0
⊢ 0 < ↑n

Tactic:
norm_cast

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
⊢ ↑⌈a⌉ < a + 1

Tactic:
by
  rw [← lt_ceil, ← Int.cast_one, ceil_add_intCast]
  apply lt_add_one

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

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ round (↑n / ↑d) = ↑(round (↑n / ↑d))

Tactic:
norm_cast

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

Goal state before:
pp: n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n % ↑d).natAbs.Coprime d

Tactic:
have : d.Coprime n := n_coprime_d.symm

Goal state after:
n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.Coprime n
⊢ (↑n % ↑d).natAbs.Coprime d
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this✝ : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
this : R (f (x - m • a)) (f (y - m • a))
⊢ R (f x) (f y)

Tactic:
simpa using hR (m • b) 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_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this✝ : (↑q.den).natAbs = q.den
this : ↑(↑q.den / ↑q.num).den = ↑q.num.natAbs
⊢ (↑q.den / ↑q.num).den = q.num.natAbs

Tactic:
by exact mod_cast this

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
a : R
⊢ Int.cast ⁻¹' Ioi a = Ioi ⌊a⌋

Tactic:
ext
  simp [floor_lt]

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b

Tactic:
induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩

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

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_mem h']; exact h

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

Goal state before:
pp: α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f x s)

Tactic:
foldl_swap

Goal state after:
α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun x y ↦ f y x) x s)
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ [].bagInter l = []

Tactic:
cases l <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.bagInter [] = []

Tactic:
cases l <;> rfl

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

Goal state before:
pp: case pos.e_a
α : 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 s).erase a

Tactic:
by_cases m : a ∈ s

Goal state after:
case pos
α : 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 s).erase a

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 s).erase a
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 t

Tactic:
by_cases m : a ∈ s

Goal state after:
case pos
α : 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

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
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (t ∪ s) ∩ s = s

Tactic:
union_inter_cancel_right

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = s
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∈ s
⊢ insert a ∅ ∩ s = insert a ∅

Tactic:
rw [insert_inter_of_mem H, empty_inter]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
⊢ x ∈ ↑(s ∆ t) ↔ x ∈ ↑s ∆ ↑t

Tactic:
by simp [mem_symmDiff, Set.mem_symmDiff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ image f s ⊆ t ↔ f '' ↑s ⊆ ↑t

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ ↑t ⊆ f '' ↑s ↔ t ⊆ image f s

Tactic:
norm_cast

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

Goal state before:
pp: n m : ℕ
a b : Fin n
ha : ↑a < m
hab : b ≤ a
⊢ ↑(a - b) < m

Tactic:
by
  rw [Fin.sub_val_of_le hab]
  exact sub_lt_of_lt ha

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ Injective predAbove

Tactic:
intro i

Goal state after:
n : ℕ
i : Fin n
⊢ ∀ ⦃a₂ : Fin n⦄, i.predAbove = a₂.predAbove → i = a₂
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
w✝ : ↥s
left✝ : w✝ ∈ s.attach
h : i ↑w✝ ⋯ ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ i ↑w✝ ⋯ ∈ t

Tactic:
apply hi

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.succ ≤ b.castSucc ↔ a < b

Tactic:
rw [le_castSucc_iff, succ_lt_succ_iff]

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

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ k, k ≤ b ∧ b = a + k

Tactic:
by
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h
  have hkb : k ≤ b := by lia
  refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩
  simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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

Goal state before:
pp: case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last 0))

Tactic:
rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]

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

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
· rw [← hij] at hj
    cases hi <| Nat.lt_trans i.castSucc_lt_succ hj

Goal state after:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_1.inr
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}

Tactic:
· exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩

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

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ Injective (cons x₀ x)

Tactic:
intro i

Goal state after:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin (n + 1)
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x i = cons x₀ x a₂ → i = a₂
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin n
⊢ Surjective p.predAbove

Tactic:
intro i

Goal state after:
n : ℕ
p i : Fin n
⊢ ∃ a, p.predAbove a = i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

Tactic:
intro i

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
intro i

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin n), «repeat» 1 a (Fin.cast ⋯ x) = (a ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
intro i

Goal state after:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
i : Fin n
⊢ «repeat» 1 a (Fin.cast ⋯ i) = (a ∘ Fin.cast h) (Fin.cast ⋯ i)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Fintype β
hlt : card β < card α
⊢ P β

Tactic:
rw [hn] at hlt

Goal state after:
case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Fintype β
hlt : card β < n
⊢ P β
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = snoc (f ∘ natAdd m) a (last n)

Tactic:
snoc_last,

Goal state after:
case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = a
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
by
  obtain rfl | hs₀ := s.eq_empty_or_nonempty
  · simp
  obtain ⟨n, hn', hn⟩ := image_iterate_stabilises_lt_card hs hs₀
  exact ⟨n, hn'.le, hn⟩

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

Goal state before:
pp: case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
intro i

Goal state after:
case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)

Tactic:
intro i

Goal state after:
case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ l <+ l'

Tactic:
induction l generalizing l' f with
  | nil => simp
  | cons hd tl IH => ?_
  have : some hd = l'[f 0]? := by simpa using hf 0
  rw [eq_comm, List.getElem?_eq_some_iff] at this
  obtain ⟨w, h⟩ := this
  let f' : ℕ ↪o ℕ :=
    OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b => by
      rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos
  have : ∀ ix, tl[ix]? = (l'.drop (f 0 + 1))[f' ix]? := by
    intro ix
    rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
    · simp only [getElem?_cons_succ]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact ix.succ_pos
  rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
  apply List.Sublist.append _ (IH _ this)
  rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
  exact List.getElem_mem _

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

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

Tactic:
intro i

Goal state after:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
i : ℕ
⊢ i < l.length → f i < l'.length
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
⊢ ¬Infinite ι

Tactic:
intro i

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
⊢ False
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: 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, ⋯⟩) ⋯) ix)

Tactic:
intro i

Goal state after:
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
i : Fin l.length
⊢ l.get i = l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) i)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ StrictMono fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length

Tactic:
intro i

Goal state after:
case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i : ℕ
⊢ ∀ ⦃b : ℕ⦄,
    i < b →
      (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) i <
        (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) b
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedLE ↔ Pairwise (fun x1 x2 ↦ x1 ≤ x2) l

Tactic:
by
  simp only [sortedLE_iff_monotone_get, monotone_iff_forall_lt, Fin.forall_iff]
  grind [pairwise_iff_getElem]

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
have := h.choose_spec

Goal state after:
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
this : h.choose < n ∧ p h.choose
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s

Tactic:
by
  induction s using Finset.induction_on with
  | empty => simp only [fold_empty]
  | insert a s has ih => rw [fold_insert has, ih, insert_eq]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' 0 = l

Tactic:
cases l <;> rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)

Tactic:
intro i

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
i : α
⊢ ∀ (s : Finset α),
    i ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (a ::ₘ s).sigma t = map (Sigma.mk a) (t a) + s.sigma t

Tactic:
by
  simp [Multiset.sigma]

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ List.count (x, y) l.offDiag ≤ 1

Tactic:
count_offDiag_eq_mul_sub_ite l x y

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1