mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
⊢ CompleteLattice α

Tactic:
let top := e.top
  let bot := e.bot
  let supSet := e.supSet
  let infSet := e.infSet
  let lattice := e.lattice
  apply e.injective.completeLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      minAx.iInf_iSup_eq']

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective fun b ↦ Ι b a

Tactic:
by
  rintro b c h
  rw [Set.ext_iff] at h
  obtain ha | ha := le_or_gt b a
  · have hb := (h b).not
    simp only [ha, left_mem_uIoc, true_iff, notMem_uIoc, ← not_le,
      and_true, not_true, false_and, not_false_iff, or_false] at hb
    refine hb.eq_of_not_lt fun hc => ?_
    simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c
  · refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)
    simpa [ha, ha.not_ge, mem_uIoc] using h b

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun i j ↦ f i ≠ f j) ↔ Injective f

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ioo (e x) (e y) ∩ range ⇑e = Ioo (e x) (e y)

Tactic:
inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ Ioo (e x) (e y) = Ioo (e x) (e y)
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f a * f c ≤ f b * f c

Tactic:
le.2 ab

Goal state after:
α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f b * f c ≤ f b * f c
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ ↑q.num / ↑q.den

Tactic:
exact div_nonneg q.num.cast_nonneg q.den.cast_nonneg

Goal state after:
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : n✝¹.beq n✝ = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
by simpa using Nat.ne_of_beq_eq_false h

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
⊢ f '' mulSupport g ⊆ mulSupport (extend f g 1)

Tactic:
by
    rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s

Tactic:
disjoint_comm,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
by
    have h := Int.cast_mono (R := α) <| of_decide_eq_true h
    have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
    have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
    have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha
    rw [← mul_assoc, Int.commute_cast] at h
    simp only [Int.ofNat_eq_natCast, Int.mul_def, Int.cast_mul, Int.cast_natCast,
      mul_invOf_cancel_right'] at h
    rwa [Int.commute_cast] at h

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
← Nat.add_assoc

Goal state after:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k).succ * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)

Tactic:
← Nat.add_assoc

Goal state after:
n k : ℕ
⊢ (n + k).succ * ((n + k) * n.ascFactorial k) = (n + k + 1) * ((n + k) * n.ascFactorial k)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!

Tactic:
rw [Nat.sub_add_comm h, Nat.sub_one]
  nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
  rw [Nat.sub_one, factorial_mul_ascFactorial]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr
n k j : ℕ
hn : n > 0
⊢ j ≤ j * n

Tactic:
exact Nat.le_mul_of_pos_right j hn

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

Goal state before:
pp: n : ℕ+
⊢ n ≤ 1 ↔ n = 1

Tactic:
by
  simp

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (fract (↑m / ↑n)) (1 - fract (↑m / ↑n)) = min ↑(m % n) ↑(n - m % n) / ↑n

Tactic:
← min_div_div_right hn'.le,

Goal state after:
case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (fract (↑m / ↑n)) (1 - fract (↑m / ↑n)) = min (↑(m % n) / ↑n) (↑(n - m % n) / ↑n)
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 : n ≠ 0
a : R
⊢ ⌊↑n * a⌋ / ↑n = ⌊a⌋

Tactic:
by
  rw [Nat.cast_comm, mul_natCast_floor_div_cancel hn]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ⌈↑x⌉ = ⌈x⌉

Tactic:
← neg_inj,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ -⌈↑x⌉ = -⌈x⌉
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:
← neg_inj,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ -⌈a + ↑z⌉ = -(⌈a⌉ + z)
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 b : R
⊢ b + 1 ≤ ↑⌈a + b⌉ + 1 - a

Tactic:
le_sub_iff_add_le',

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + (b + 1) ≤ ↑⌈a + b⌉ + 1
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1

Tactic:
· exact n.cast_add_one_pos

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 : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
obtain rfl | hba := hba.eq_or_lt
  · rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
    positivity
  · exact (ceil_lt_mul hb hba).le

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

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
⊢ (fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f) = f

Tactic:
by ext x; simp [map_fract]

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

Goal state before:
pp: α : Type u_1
s₁ s₂ : Finset α
⊢ ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂

Tactic:
by
  simp

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

Goal state before:
pp: case mk
α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
x✝ : Multiset α
l : List α
hl : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x
⊢ ∃ y, map c y = Quot.mk (⇑(isSetoid α)) l

Tactic:
lift l to List β using hl

Goal state after:
case mk
α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
x✝ : Multiset α
l : List β
⊢ ∃ y, map c y = Quot.mk (⇑(isSetoid α)) (List.map c l)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ map val (s.attach.erase x) = s.erase ↑x

Tactic:
Multiset.map_erase _ val_injective,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ (map val s.attach).erase ↑x = s.erase ↑x
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse

Tactic:
rw [inter_reverse]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = [] :: map (fun t ↦ a :: t) l.inits

Tactic:
by
  simp

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

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
n : ℕ
h : n < (a :: l).tails.length
⊢ (a :: l).tails[n] = drop n (a :: l)

Tactic:
cases n with
    | zero => simp
    | succ n => simp [ihl]

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

Goal state before:
pp: α : Type u_1
l : List α
n : Fin l.tails.length
⊢ l.tails.get n = drop (↑n) l

Tactic:
by
  simp

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

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
n : ℕ
h : n < (a :: l).inits.length
⊢ (a :: l).inits[n] = take n (a :: l)

Tactic:
cases n with
    | zero => simp
    | succ n => simp [ihl]

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

Goal state before:
pp: α : Type u_1
l : List α
n : Fin l.inits.length
⊢ l.inits.get n = take (↑n) l

Tactic:
by
  simp

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

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) m)

Tactic:
rw [disjoint_left]

Goal state after:
a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬a_1 ∈ map (fun x ↦ a + x) m
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
⊢ x ∈ insert y s ↔ x ∈ insert y ↑s

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
simp only [insert_union, union_insert, insert_idem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.symm.toEmbedding t ⊆ s ↔ t ⊆ map f.toEmbedding s

Tactic:
simp only [← subset_map_symm, Equiv.symm_symm]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Subsingleton ↥s.toFinset ↔ s.Subsingleton

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
⊢ ↑(image f univ) = Set.range f

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset α
⊢ (fun s ↦ Finset.map e.symm.toEmbedding s) ((fun s ↦ Finset.map e.toEmbedding s) s) = s

Tactic:
by simp [Finset.map_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset β
⊢ (fun s ↦ Finset.map e.toEmbedding s) ((fun s ↦ Finset.map e.symm.toEmbedding s) s) = s

Tactic:
by simp [Finset.map_map]

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

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

Tactic:
← rev_castSucc,

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).castSucc.rev = i.rev
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
h : Nonempty (Fin (n + 1) ↪ Fin m)
⊢ n + 1 ≤ m

Tactic:
| succ n ihn =>

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (rev 0).succ = rev 0

Tactic:
← rev_castSucc,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ (castSucc 0).rev = rev 0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ↑0 = 0

Tactic:
by
  simp

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ a % m = a % m % n

Tactic:
Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)

Goal state after:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ a % m = a % m
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc + 1 = a

Tactic:
by
  simp

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < a

Tactic:
castSucc_pred_lt_iff,

Goal state after:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ a ≤ a
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

Tactic:
succAbove_of_castSucc_lt _ _ H

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ i.castSucc < p
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
succAbove_of_castSucc_lt _ _ H

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : ¬i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simp [succAbove_of_le_castSucc _ _ (Fin.not_lt.1 H)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun x ↦ f (l.get x)) univ = (List.map f l).toFinset

Tactic:
by
  simp

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯

Tactic:
refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · exact (Fin.cast hu l).elim0
  · rw [append_right, Function.comp_apply]
    refine congr_arg v (Fin.ext ?_)
    simp [hu]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [two_lt_card_iff, exists_and_left]

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

pp: case refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ natAdd m) i.castSucc = snoc (f ∘ natAdd m) a i.castSucc

Tactic:
· simp only [Function.comp_apply]
    rw [snoc_last, natAdd_last, snoc_last]

Goal state after:
case refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ natAdd m) i.castSucc = snoc (f ∘ natAdd m) a i.castSucc
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : Fintype α
h : univ.Finite
⊢ h.toFinset = Finset.univ

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
h : ∅.Finite
⊢ h.toFinset = ∅

Tactic:
by
  simp

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

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ insertNth 0 x p = cons x p

Tactic:
simp [insertNth_zero]

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

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

Tactic:
simp [insertNth_eq_iff]

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

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
ha : a ∈ head✝ :: tail✝
⊢ R (head✝ :: tail✝).head! a

Tactic:
cases ha with
    | head => exact refl_of ..
    | tail => exact rel_of_pairwise_cons h (by assumption)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % min l'.length l'.length) (zipWith f l l') ++ take (n % min l'.length l'.length) (zipWith f l l') =
    drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l')

pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
min_self

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l') =
    drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l')

α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
f : α → α → β
x y : α
l : List α
⊢ zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x])

Tactic:
by
  simp

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

Goal state before:
pp: case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ count a s ≤ count a (s.card • t)

Tactic:
count_le_card,

Goal state after:
case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ count a (s.card • t)
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]? = some a

Tactic:
← head?_rotate h₁,

Goal state after:
α : 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).rotate n).head? = some a
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:
rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]

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

Goal state before:
pp: α : Type u
l : List α
n : Fin l.cyclicPermutations.length
⊢ l.cyclicPermutations.get n = l.rotate ↑n

Tactic:
by
  simp

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = x • y • 1

Tactic:
smul_smul

Goal state after:
M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = (x * y) • 1
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b

Tactic:
have ha := mem_conjugatesOf_self (a := b)

Goal state after:
α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
ha : a✝ ∈ {1}
hb : b✝ ∈ {1}
⊢ a✝ * b✝ ∈ {1}

Tactic:
by
        push _ ∈ _ at *
        rw [ha, hb, mul_one]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inr
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j

Tactic:
· simp [h, eqComm]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup G
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
by cases x; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup (Additive G)
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
by cases x; rfl

Goal state after: