mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (∃ x_1, ∃ (_ : x_1 ∈ Ioo x y), x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
exists_prop,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (∃ x_1 ∈ Ioo x y, x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (∃ x_1 ∈ Ioo x y, x_1 ∉ s) ↔ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
and_comm

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

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : a ≤ b
⊢ ∃ c, b = a + c

Tactic:
← Subtype.coe_le_coe

Goal state after:
α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a ≤ ↑b
⊢ ∃ c, b = a + c
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι → M
s : Set κ
g : κ → ι
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Tactic:
mulSupport_comp_eq_preimage f g,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι → M
s : Set κ
g : κ → ι
⊢ g '' s ∩ mulSupport f = g '' (s ∩ g ⁻¹' mulSupport f)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ p a

Tactic:
apply strongInductionOn a
  rintro ⟨k, kprop⟩ hk
  rcases k with - | k
  · exact (lt_irrefl 0 kprop).elim
  rcases k with - | k
  · exact hz
  exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (Nat.lt_succ_iff.2 hm)

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

Goal state before:
pp: n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ p n

Tactic:
rcases n with ⟨n, h⟩
  induction n with
  | zero => exact absurd h (by decide)
  | succ n IH =>
    rcases n with - | n
    · exact one
    · exact succ _ (IH n.succ_pos)

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

Goal state before:
pp: m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Tactic:
rw [hr, hq, mul_zero, zero_add] at h₀

Goal state after:
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ ⌊f a + 2⁻¹⌋ = ⌊f a + (f 2)⁻¹⌋

Tactic:
map_ofNat

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
z : ℤ
a : R
⊢ a < ↑z + 1 ∧ ↑z ≤ a ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
and_comm

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ↑z ≤ a ∧ a < ↑z + 1 ↔ ↑z ≤ a ∧ a < ↑z + 1
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
n : ℤ
hn : 0 ≤ n
a : k
⊢ ⌊a / ↑n⌋ = ⌊a⌋ / n

Tactic:
obtain rfl | hn := hn.eq_or_lt
  · simp
  nth_rw 2 [← div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))]
  rw [mul_cast_floor_div_cancel_of_pos hn]

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
z : ℤ
a : R
⊢ ⌈a⌉ ≤ z ∧ z ≤ ⌈a⌉ ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z

Tactic:
and_comm

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z ↔ z ≤ ⌈a⌉ ∧ ⌈a⌉ ≤ z
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
⊢ (fract q⁻¹).num < q.num

Tactic:
set q_inv : ℚ := q.den / q.num with q_inv_def

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
⊢ (fract q⁻¹).num < q.num
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ f a - ↑⌊f a⌋ = f a - f ↑⌊a⌋

Tactic:
map_intCast,

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ f a - ↑⌊f a⌋ = f a - ↑⌊a⌋
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
⊢ IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1

Tactic:
refine ⟨fun H _ _ ↦ IsCancelSMul.eq_one_of_smul, fun H ↦ ⟨fun g h x ↦ ?_⟩⟩
  rw [smul_eq_iff_eq_inv_smul, eq_comm, ← mul_smul, ← inv_mul_eq_one (G := α)]
  exact H (g⁻¹ * h) x

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

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
⊢ Archimedean (WithBot M)

Tactic:
constructor
  intro x y hxy
  cases y with
  | bot => exact absurd hxy bot_le.not_gt
  | coe y =>
    cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case mp
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ s
⊢ l = [] ∨ l = [a]

Tactic:
rwa [perm_singleton.mp hla, sublist_singleton] at h

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
⊢ ∀ (a : Multiset α), a.Le a

Tactic:
rintro ⟨l⟩; exact Subperm.refl _

Goal state after:
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:
smul_eq_smul_iff_inv_mul_eq_sdiv,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁⁻¹ * v₂ = p₁ /ₛ p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s

Tactic:
rw [h]

Goal state after:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ (xs ++ ys).dedup = ys.dedup

Tactic:
by
  rw [List.dedup_append, Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)]

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

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
⊢ strongDownwardInduction H s = H s fun {t₂} ht _hst ↦ strongDownwardInduction H t₂ ht

Tactic:
strongDownwardInduction

Goal state after:
α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
⊢ (H s fun {t} ht _h ↦ strongDownwardInduction H t ht) = H s fun {t₂} ht _hst ↦ strongDownwardInduction H t₂ ht
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a ↦ strongDownwardInduction H s a) = H s fun {t} ht _h ↦ strongDownwardInduction H t ht

Tactic:
strongDownwardInduction

Goal state after:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a ↦ H s (fun {t} ht _h ↦ strongDownwardInduction H t ht) a) = H s fun {t} ht _h ↦ strongDownwardInduction H t ht
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ l ∧ a ≠ b ↔ a ≠ b ∧ a ∈ l

Tactic:
and_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ≠ b ∧ a ∈ l ↔ a ≠ b ∧ a ∈ l
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ List.filter (fun b ↦ elem b l₂) l₁ ~ l₁ ∩ l₂

Tactic:
apply Perm.refl

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

Goal state before:
pp: n : ℕ
⊢ range n.succ = n ::ₘ range n

Tactic:
range,

Goal state after:
n : ℕ
⊢ ↑(List.range n.succ) = n ::ₘ range n
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: n : ℕ
⊢ ↑[n] + ↑(List.range n) = n ::ₘ range n

Tactic:
range,

Goal state after:
n : ℕ
⊢ ↑[n] + ↑(List.range n) = n ::ₘ ↑(List.range n)
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False

Tactic:
range,

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ ↑(List.range a)
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a b : α
s : Finset α
l : List α
head✝ : α
h : Nodup ⟦[head✝]⟧
⊢ ¬{ val := ⟦[head✝]⟧, nodup := h }.Nontrivial

Tactic:
by simp [SetLike.coe]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ sᶜ ↔ a ∈ s

Tactic:
mem_compl,

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ ¬a ∉ s ↔ a ∈ s
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
⊢ (filter p s).toFinset = Finset.filter (fun x ↦ p x = true) s.toFinset

Tactic:
by
  ext; simp [List.mem_filter]

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

Goal state before:
pp: case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
Fin.le_iff_val_le_val,

Goal state after:
case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ ↑1 ≤ ↑k
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ last n
⊢ (i.castPred h).castSucc = i

Tactic:
rcases exists_castSucc_eq.mpr h with ⟨y, rfl⟩

Goal state after:
n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ (y.castSucc.castPred h).castSucc = y.castSucc
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ Set.InjOn f ↑s

Tactic:
classical
  have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
  have : #(s.image f) = #t := by rw [this]
  have : #(s.image f) ≤ #s := card_image_le
  rw [← card_image_iff]
  lia

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

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i h, (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : (ofFn f)[i] = b
h : ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
⊢ f ⟨i, ⋯⟩ = b

Tactic:
simpa
        using! hfb

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
⊢ (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
⟨u, hu₁, hu₂, hu₃⟩

Goal state after:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Tactic:
← succ_inj (b := pred (succAbove a b) hk),

Goal state after:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ ((a.pred ha).succAbove (b.pred hb)).succ = ((a.succAbove b).pred hk).succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z = cons z p

Tactic:
ext j
  cases j using Fin.cases <;> simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ cast ⋯ (cons (Fin.cons x₀ x 0) (tail (Fin.cons x₀ x))) = cons x₀ x

Tactic:
cast_eq

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ cons (Fin.cons x₀ x 0) (tail (Fin.cons x₀ x)) = cons x₀ x
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : i < p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
rw [h]

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
rw [h]

Goal state after:
case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
· rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]

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

Goal state before:
pp: α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ α ≃ β

Tactic:
rw [h]

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

Goal state before:
pp: m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n' + m = n + m

Tactic:
rw [h]

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

Goal state before:
pp: m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m' = n + m

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction H s = H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
strongDownwardInduction

Goal state after:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ (H s fun {t} ht h ↦
      have this := ⋯;
      have this := ⋯;
      strongDownwardInduction H t ht) =
    H s fun {t} ht x ↦ strongDownwardInduction H t ht
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a ↦ strongDownwardInduction H s a) = H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
strongDownwardInduction

Goal state after:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a ↦
      H s
        (fun {t} ht h ↦
          have this := ⋯;
          have this := ⋯;
          strongDownwardInduction H t ht)
        a) =
    H s fun {t} ht x ↦ strongDownwardInduction H t ht
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
rw [h]

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) i = update (init q) i y i
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
obtain ⟨f, hf⟩ := IH
      refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
      simpa using hf

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ orderedInsert r a [] = takeWhile (fun b ↦ decide ¬r a b) [] ++ a :: dropWhile (fun b ↦ decide ¬r a b) []

Tactic:
grind [takeWhile, dropWhile]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
tail_ih✝ :
  orderedInsert r a tail✝ = takeWhile (fun b ↦ decide ¬r a b) tail✝ ++ a :: dropWhile (fun b ↦ decide ¬r a b) tail✝
⊢ orderedInsert r a (head✝ :: tail✝) =
    takeWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝) ++ a :: dropWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝)

Tactic:
grind [takeWhile, dropWhile]

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

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : (i.succAbove j).pred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: case cons
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s).Finite), motive (↑s) hs
hs : (↑(Finset.cons a s ha)).Finite
⊢ motive (↑(Finset.cons a s ha)) hs

Tactic:
simpa using @insert a s ha (Set.toFinite _) (ih _)

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
by_cases h : a ∈ s; swap; · simp [IH, h]
    simp only [h, dedup_cons_of_mem, IH, fold_cons_left]
    show fold op b s = op a (fold op b s)
    rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

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

Goal state before:
pp: α : Type u_1
L : List α
i : Nat
h : i < L.length
⊢ drop i (take (i + 1) L) = [L[i]]

Tactic:
induction L generalizing i with grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a c : α
l₁ l₂ : List α
⊢ IsChain R (a :: (l₁ ++ c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [c])) ∧ IsChain R (c :: l₂)

Tactic:
by
  simp_rw [← cons_append, isChain_split (l₂ := l₂)]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h : IsChain R (l₂ ++ l₁ ++ l₃)
⊢ IsChain R l₁

Tactic:
exact h.left_of_append.right_of_append

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
h : ¬IsChain R l
⊢ ∃ n h, ¬R l[n] l[n + 1]

Tactic:
by simp_all [isChain_iff_getElem]

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

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

Tactic:
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l)[n] = (replicate (a :: l).length a)[n]

Tactic:
by
      rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ m.bind f ≍ m.bind f'

Tactic:
simp [bind_congr hf]

Goal state after: