mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < l.length + 1

Tactic:
Nat.succ_lt_succ_iff

Goal state after:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k < l.length
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (filterMap g (b :: bs))

Tactic:
filterMap_cons

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)

Tactic:
exact
      match f a, g b, hfg h₁ with
      | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
      | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ Relation.Comp (fun x1 x2 ↦ x1 = map f x2) (fun x1 x2 ↦ x1 ~ x2) (map f l) l' ↔ l ~ l'

Tactic:
simp [Relation.Comp, map_inj_right hf]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
· simp [ha]

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

pp: case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
· simp [ha]

Goal state after:
case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : ℕ
h : i < l.tail.length
⊢ i + 1 < l.length

Tactic:
simp only [length_tail] at h; lia

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : b ≠ a
⊢ idxOf a (b :: l) = (idxOf a l).succ

Tactic:
simp [idxOf_cons, beq_false_of_ne h]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (l ^ r).eval = zpow' l.eval r

Tactic:
unfold NF.eval at ⊢

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        (l ^ r)).prod =
    zpow'
      (map
          (fun x ↦
            match x with
            | (r, x) => zpow' x r)
          l).prod
      r
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
ext l; rw [comp_map, Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(NNRat.divNat m (10 ^ d))

Tactic:
congr 2

Goal state after:
case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ OfScientific.ofScientific m b d = Rat.divInt ↑m ↑(10 ^ d)
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)

Tactic:
congr 2

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ OfScientific.ofScientific m b d = ↑(m * 10 ^ d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ ↑(divNat q.num q.den) = ↑q

Tactic:
rw [← (q : ℚ).mkRat_num_den']

Goal state after:
q : ℚ≥0
⊢ ↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)

Tactic:
by conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]

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

Goal state before:
pp: q : ℚ
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
← num_divInt_den q

Goal state after:
q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → ℕ → α
a : α
an cn ad b b' cd : ℕ
⊢ f = HPow.hPow → IsNNRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsNNRat (f a b) cn cd

Tactic:
by
  rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)
  have := invertiblePow (ad:α) b
  rw [← Nat.cast_pow] at this
  use this; simp [invOf_pow, Commute.mul_pow, Nat.cast_commute]

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

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ pure (node v) <*> pure l <*> pure r = pure (node v l r)

Tactic:
pure_seq,

Goal state after:
case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ node v <$> pure l <*> pure r = pure (node v l r)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b a : R
e : ℕ
hone : Nat.rawCast 1 = e
hb : a ^ e * Nat.rawCast 1 = b
⊢ a = b + 0

Tactic:
by
  simp [← hone, ← hb]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h

Tactic:
rw [← iSup_sup_eq]

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = ⨆ x, (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ ⋂ x, ⋂ y, ⋂ (h : p y ∧ q x y), s x y h = ⋂ y, ⋂ (hy : p y), ⋂ x, ⋂ (hx : q x y), s x y ⋯

Tactic:
by
  simp only [iInter_and, @iInter_comm _ ι]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ sSup s ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a

Tactic:
sSup_eq_iSup'

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : ¬(BddAbove s ∨ BddAbove t)
⊢ sSup s = sSup t

Tactic:
· simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹² : Max α
inst✝¹¹ : Min α
inst✝¹⁰ : LE α
inst✝⁹ : LT α
inst✝⁸ : SupSet α
inst✝⁷ : InfSet α
inst✝⁶ : Top α
inst✝⁵ : Bot α
inst✝⁴ : Compl α
inst✝³ : HImp α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι✝ : 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,
      iInf_iSup_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ upperBounds s

Tactic:
change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
⊢ b₁ ≠ b₂ → (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
hne

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
⊢ x✝ ≠ y✝ → (fun x y ↦ r x y ∨ r y x) x✝ y✝

Tactic:
hne

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
hne : x✝ ≠ y✝
⊢ r x✝ y✝ ∨ r y✝ x✝
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain (fun x1 x2 ↦ r ↑x1 ↑x2) (s ↓∩ t) ↔ IsChain r (s ∩ t)

Tactic:
simp [IsChain, Set.Pairwise]

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

Goal state before:
pp: case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Tactic:
cases lt_irrefl _ hnm

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

Goal state before:
pp: case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Tactic:
cases lt_irrefl _ hnm

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

Goal state before:
pp: case refl
i : ℕ
⊢ i + 1! ≤ (i + 1)!

Tactic:
exact self_le_factorial _

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
hn : (↑q.num / ↑q.den).num = ↑q.num
hd : (↑q.num / ↑q.den).den = q.den
⊢ ↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den

Tactic:
rw [hn, hd, Int.cast_natCast]

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ ↑↑(OfScientific.ofScientific m s e) = ↑(OfScientific.ofScientific m s e)

Tactic:
cast_nnratCast

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ ↑(OfScientific.ofScientific m s e) = ↑(OfScientific.ofScientific m s e)
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⟩

Goal state after:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ p ⟨n, h⟩
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:
sub_eq_add_neg

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: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round x + -y = round x - y

Tactic:
sub_eq_add_neg

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.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 ∧ a < ↑z + 1

Tactic:
rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]

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:
sub_eq_add_neg

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: case inr.inr.calc_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ ↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
congr 2

Goal state after:
case inr.inr.calc_2.e_a
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ m₁ % ↑n = -↑m₀ % ↑n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
⊢ -⌊-(↑n / ↑d)⌋ = -(-n / ↑d)

Tactic:
← neg_div,

Goal state after:
n : ℤ
d : ℕ
⊢ -⌊-↑n / ↑d⌋ = -(-n / ↑d)
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:
sub_eq_add_neg

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 : R
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
rcases eq_or_ne (fract a) 0 with ha | ha

Goal state after:
case inl
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a b : R
⊢ Int.cast ⁻¹' Ioc a b = Ioc ⌊a⌋ ⌊b⌋

Tactic:
ext
  simp [floor_lt, le_floor]

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |(↑m.pred + 1 - ↑m.pred) * δ| ≤ δ

Tactic:
add_sub_cancel_left,

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |1 * δ| ≤ δ
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
⊢ (t + s).erase a = s + t.erase a

Tactic:
erase_add_left_pos s h,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
⊢ t.erase a + s = s + t.erase a
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.map (fun p ↦ ⟨↑p, ⋯⟩) (List.pmap mk l ⋯)

Tactic:
rw [List.map_pmap]; exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.ext rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
· rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
    exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ (a : α), a ∈ s' → P a
card : (filter P s').card ≤ n
⊢ False

Tactic:
exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
simp_rw [Finset.ssubset_def, toFinset_subset]
  rfl

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

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
a✝ : { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ toFinset '' {l | l.Nodup}

Tactic:
exact ⟨l, hl, (toFinset_eq hl).symm⟩

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:
by
  simp_rw [← filter_eq', eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = (a ::ₘ s.val).dedup

Tactic:
dedup_cons,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val.dedup
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹

Tactic:
by simp_rw [@ne_comm _ b]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {x | x ∈ s} = s.toFinset

Tactic:
by
  ext
  rw [mem_filter_univ, mem_toFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)

Tactic:
by simp_rw [image_image, comp_def, h_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ 0 < #({x ∈ s | f x = y}) ↔ y ∈ image f s

Tactic:
card_pos,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin n
h : 2 < n
⊢ ∃ k, k ≠ i ∧ k ≠ j

Tactic:
by
  have : NeZero n := ⟨by lia⟩
  rcases i with ⟨i, hi⟩
  rcases j with ⟨j, hj⟩
  simp_rw [← Fin.val_ne_iff]
  by_cases h0 : 0 ≠ i ∧ 0 ≠ j
  · exact ⟨0, h0⟩
  · by_cases h1 : 1 ≠ i ∧ 1 ≠ j
    · exact ⟨⟨1, by lia⟩, h1⟩
    · refine ⟨⟨2, by lia⟩, ?_⟩
      dsimp only
      lia

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

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

Tactic:
pred_castSucc_lt_iff,

Goal state after:
n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a ≤ a
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (n✝ + 1 + 1 - 1) % (n✝ + 1 + 1) = n✝ + 1

Tactic:
Nat.add_one_sub_one,

Goal state after:
case succ
n✝ : ℕ
⊢ (n✝ + 1) % (n✝ + 1 + 1) = n✝ + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove 1 = (i.succAbove 0).succ

Tactic:
rw [← succ_zero_eq_one']

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
by
  rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]

Goal state after:
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)
g : (j : Fin (n + 1)) → α j
⊢ g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f

Tactic:
by
  simpa [eq_comm] using insertNth_eq_iff

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

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ cons a f ∘ rev = snoc (f ∘ rev) a

Tactic:
by
  funext i; exact cons_rev ..

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 α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
unfold fold

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))