mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
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:
by_cases hb : b = 0

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

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
⊢ idxOf a l + 1 < l.length

Tactic:
have := idxOf_lt_length_of_mem ha

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
this : idxOf a l.dropLast < l.dropLast.length
⊢ idxOf a l + 1 < l.length
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
⊢ L.eval * l₀.eval = ((0, e) ::ᵣ l').eval

Tactic:
← eval_mul_eval_cons 0 e h,

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
e : M
L l l' l₀ : NF M
h : L.eval * l.eval = l'.eval
h' : ((0, e) ::ᵣ l).eval = l₀.eval
⊢ L.eval * l₀.eval = L.eval * ((0, e) ::ᵣ l).eval
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b tail✝) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb tail✝
mb✝ : m β
⊢ (do
      let b ← mb✝
      foldlM f b (head✝ :: tail✝)) =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      mb✝ (head✝ :: tail✝)

Tactic:
simp only [List.foldlM, foldl, ← l_ih, functor_norm]

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

Goal state before:
pp: q r : ℚ
⊢ q / r = q.num /. ↑q.den / (r.num /. ↑r.den)

Tactic:
num_divInt_den,

Goal state after:
q r : ℚ
⊢ q / r = q / (r.num /. ↑r.den)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: n : ℤ
⊢ n /. 1 = ↑n

Tactic:
simp [divInt, mkRat, normalize]

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

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
rw [← coe_inj]; simp [Rat.mkRat_eq_iff, h₁, h₂]; norm_cast

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

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q.num /. ↑q.den * (r.num /. ↑r.den) = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
num_divInt_den,

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * (r.num /. ↑r.den) = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑b = 0

Tactic:
obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d = 0
k : ℕ
hb : ↑(d * k) ≠ 0
e : divNat a (d * k) = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
this : Rat.divInt ↑a ↑(d * k) = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑(d * k) = 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q.num /. ↑q.den + r.num /. ↑r.den = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
num_divInt_den,

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r.num /. ↑r.den = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)

Tactic:
rw [iInf_subtype', iInf_subtype']
  exact gi.l_iInf_of_u_l_eq_self _ fun _ => hf _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Set β
b : β
⊢ ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x

Tactic:
simp [iSup_or, iSup_sup_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋂ x ∈ {a, b}, s x = s a ∩ s b

Tactic:
by
  rw [biInter_insert, biInter_singleton]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝¹ : CompleteBooleanAlgebra α
f : ι → α
inst✝ : Nonempty ι
a : α
⊢ (⨆ i, f i) ∆ a ≤ ⨆ i, f i ∆ a

Tactic:
by
  simpa [iSup_const] using iSup_symmDiff_iSup_le (g := fun _ : ι ↦ a)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, Ioi_subset_Ioi⟩
  by_contra ba
  exact lt_irrefl _ (h (not_le.mp ba))

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ CompletelyDistribLattice α

Tactic:
apply e.injective.completelyDistribLattice <;> intros

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊥ = ⊥

case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ : α
⊢ e (￢a✝) = ￢e a✝

case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
have : Std.Symm fun a b ↦ a ≺ b ∨ b ≺ a := { symm _ _ := Or.symm }
  rw [IsChain, IsChain, IsChain, pairwise_union_of_symm]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x} ↦ ↑x) '' t) ↑(sInf t)

Tactic:
rw [← subset_sInf_of_within s ht h_bdd (h_Inf ht h_bdd)]

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x} ↦ ↑x) '' t) (sInf (Subtype.val '' t))
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * db < num✝ * da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have h := (Nat.cast_lt (α := α)).mpr <| of_decide_eq_true h

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * db < num✝ * da) = true
h : ↑(num✝¹ * db) < ↑(num✝ * da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
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:
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: m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < k * k ! + k !

Tactic:
Nat.lt_add_left_iff_pos

Goal state after:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
constructor
  · intro h
    rw [← not_lt, ← one_lt_factorial, h]
    apply lt_irrefl
  · rintro (_ | _ | _) <;> rfl

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

Goal state before:
pp: ⊢ ascFactorial 0 (succ 0) = 0

Tactic:
rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ 0 ≤ 2 • f a

Tactic:
rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
        exact map_div_le_add _ _ _

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

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑m = 2 * x
⊢ round x = ⌈↑m⌉ / 2

Tactic:
ceil_intCast

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑m = 2 * x
⊢ round x = m / 2
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
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
⊢ ⌊x⌋ = n

Tactic:
have hk0 : 0 < (k : R) := zero_le_one.trans_lt hk

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ ⌊x⌋ = n
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 / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)

Tactic:
sub_eq_iff_eq_add',

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 / ↑n = ↑(m % n) / ↑n + ↑(↑m / ↑n)
Module: Mathlib.Data.Rat.Floor

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

Tactic:
← floor_neg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ⌊-↑x⌋ = -⌈x⌉
Module: Mathlib.Data.Rat.Floor

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

Tactic:
← floor_neg,

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:
← floor_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
z : ℤ
⊢ ⌊-(a + ↑z)⌋ = -⌈a⌉ - z

Tactic:
← floor_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
⊢ ↑⌈a⌉ < a + 1

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

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

Tactic:
ceil_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ 0 = 0
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
⊢ ⌈↑1⌉ = 1

Tactic:
ceil_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-m + -1 + 1)

Tactic:
neg_add_cancel_right,

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-m)
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ (g • p₁ /ₛ p₂) • p₂ = (g * (p₁ /ₛ p₂)) • p₂

Tactic:
rw [sdiv_smul, mul_smul, sdiv_smul]

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
⊢ (∀ (x : K), ∃ n, x < ↑n) → Archimedean K

Tactic:
rw [archimedean_iff_nat_lt]

Goal state after:
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ (∀ (x : K), ∃ n, x < ↑n) → ∀ (x : K), ∃ n, x < ↑n
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ ¬x ∈ t

Tactic:
by simp only [← coe_subset, Set.not_subset, mem_coe]

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

Goal state before:
pp: G : Type u_5
inst✝ : AddCommGroup G
x : G
⊢ pointReflection x = Equiv.subLeft (2 • x)

Tactic:
ext; simp [pointReflection, sub_add_eq_add_sub, two_nsmul]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ Rel (flip fun x1 x2 ↦ x1 = x2) s t ↔ s = t

Tactic:
rw [rel_flip, rel_eq, eq_comm]

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

Goal state before:
pp: case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x ↦ l[x]?

pp: case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?

Tactic:
· exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩

Goal state after:
case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x✝ : α
⊢ List.count x✝ (l₁.bagInter l₂) = List.count x✝ (l₂.bagInter l₁)

Tactic:
simp [List.count_bagInter, Nat.min_comm]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then {a}.card else 0) + (filter (fun a ↦ p (f a)) t).card

Tactic:
card_singleton,

Goal state after:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then 1 else 0) + (filter (fun a ↦ p (f a)) t).card
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : Multiset α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l = l'

Tactic:
by
  simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ countP p (map f (a ::ₘ t)) = (filter (fun a ↦ p (f a)) (a ::ₘ t)).card

Tactic:
· rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ count a (filter p (Quot.mk (⇑(isSetoid α)) _l)) = count a (Quot.mk (⇑(isSetoid α)) _l)

Tactic:
simp only [quot_mk_to_coe'', filter_coe, coe_count]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ List.count a (List.filter (fun b ↦ decide (p b)) _l) = List.count a _l
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ _root_.Disjoint s t

Tactic:
by rw [← subset_zero]; simp [subset_iff, disjoint_left]

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

Goal state before:
pp: α : Type u_4
H : ∀ (s : Finset α), s = ∅
a : α
⊢ False

Tactic:
by specialize H {a}; aesop

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

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v - ↑n

Tactic:
· rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> lia

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ ↑1 - 1 = ↑0

Tactic:
val_one',

Goal state after:
n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ 1 % (n + 1) - 1 = ↑0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ = a + 1

Tactic:
cases a using lastCases

Goal state after:
case last
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ (n - ↑b + ↑a) % n = (m - ↑b + ↑a) % m + n - m

Tactic:
repeat rw [Nat.mod_eq_of_lt (by omega)]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]

Goal state after: