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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
⊢ Monotone fun n ↦ a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_
  rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']
  exact le_mul_of_one_le_right (zpow_nonneg (zero_le_one.trans ha) _) ha

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)

Tactic:
by
    rw [pow_succ, pow_succ]
    exact mul_le_mul' (pow_le_pow_left' hab k) hab

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: case one
α : Type u
d y : α
⊢ unoneD d 1 = y ↔ 1 = ↑y ∨ 1 = 1 ∧ y = d

Tactic:
simp [@eq_comm _ d]

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: case coe
α : Type u
d y a✝ : α
⊢ unoneD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = 1 ∧ y = d

Tactic:
simp [@eq_comm _ d]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulZeroOneClass β
f : α →* β
hf : Surjective ⇑f
⊢ Surjective ⇑(lift' f)

Tactic:
by
  intro b
  obtain ⟨a, rfl⟩ := hf b
  exact ⟨a, by simp⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ a + -a = 0

Tactic:
simp [ha, add_neg_cancel_of_ne_top]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ exp x = exp 0 ↔ x = 0

Tactic:
exp_inj

Goal state after:
M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ x = 0 ↔ x = 0
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ -1

Tactic:
rw [← Int.cast_one, ← Int.cast_neg, cast_le]
  exact Int.le_sub_one_of_lt h

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
d y : α
⊢ unbotD d ⊥ = y ↔ ⊥ = ↑y ∨ ⊥ = ⊥ ∧ y = d

Tactic:
simp [@eq_comm _ d]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
d y a✝ : α
⊢ unbotD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = ⊥ ∧ y = d

Tactic:
simp [@eq_comm _ d]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → IsAddLeftRegular x

Tactic:
simp; simp +contextual [bot_eq_zero, IsRegular.of_ne_zero]

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
EX : ∃ n, P (b + ↑n)
z : ℤ
h : P z
⊢ b + ↑(Nat.find EX) ≤ z

Tactic:
by
    obtain ⟨n, rfl⟩ := le.dest (Hb _ h); grw [Nat.find_min' EX h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
h : IsUnit (f 0)
⊢ IsUnit 0

Tactic:
obtain ⟨t, ht⟩ := hf
      refine (ht ?_).elim
      have := map_mul f t 0
      rw [← one_mul (f (t * 0)), mul_zero] at this
      exact (h.mul_right_cancel this).symm

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

Goal state before:
pp: case hbc
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n

Tactic:
· exact abs_geomSum_le ..

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ t ⊆ ⇑e.symm ⁻¹' s ↔ t ⊆ ⇑e '' s

Tactic:
image_eq_preimage_symm

Goal state after:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ t ⊆ ⇑e.symm ⁻¹' s ↔ t ⊆ ⇑e.symm ⁻¹' s
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

Tactic:
exact (wellFounded_iff_isEmpty_descending_chain.1 h.wf).elim ⟨f, hf⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ ∅ = Ioo a b

Tactic:
Ioo_eq_empty (mt le_of_lt h)

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ ∅ = ∅
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
    · rw [← Icc_sdiff_right]
      exact subset_sdiff_singleton hc hb
    · rwa [← Ico_sdiff_left, sdiff_singleton_subset_iff, insert_eq_of_mem ha] at ho

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

Goal state before:
pp: case inr
γ : Type u_3
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ a

Tactic:
apply (not_lt_of_ge (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim

Goal state after:
γ : Type u_3
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ b
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)

Tactic:
exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
⊢ IsBot 0

Tactic:
have hb := hs (b + b)

Goal state after:
case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
hb : b ≤ b + b
⊢ IsBot 0
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / c ↔ b < a * c

Tactic:
rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
hn : n < l.length
⊢ (l.eraseIdx n).insertIdx n l[n] = l

Tactic:
by
  simp [Nat.ne_of_lt hn]

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
x✝ : l₂.length < n ∨ l₂.length ≥ n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge (length l₂) n with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → (map f as).prod = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
    rw [List.map_cons, List.prod_cons, count_cons, h]
    simp only [beq_iff_eq]
    split_ifs with ha'
    · rw [ha', _root_.pow_succ']
    · rw [hf a' ha' mem_cons_self, one_mul, add_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
⊢ ∀ (L : List G), L.reverse.prod = (map (fun x ↦ x⁻¹) L).prod⁻¹

Tactic:
simp [prod_inv_reverse]

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

Goal state before:
pp: case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective lh

Tactic:
apply hl _ mem_cons_self

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
x✝ : α
h : x✝ ∣ x * y
hz : x✝ ∣ z
⊢ IsUnit x✝

Tactic:
by
    obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h
    exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

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

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionRing α
inst✝¹ : FunLike F ℚ α
inst✝ : RingHomClass F ℚ α
f : F
q : ℚ
⊢ f q = ↑q

Tactic:
rw [← map_ratCast f, Rat.cast_id]

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

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

Tactic:
exact isLUB_sSup _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x ↦ range (f x))) → ↑↑a
a : ι
⊢ ↑(g ⟨range (f a), ⋯⟩) ≤ f a ((fun a ↦ Classical.choose ⋯) a)

Tactic:
rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]

Goal state after:
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
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))

Tactic:
exact isLUB_sSup _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ sSup (image2 (fun x1 x2 ↦ x1 ∆ x2) s t)

Tactic:
sSup_image2

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
simpa [sSup_image] using sSup_symmDiff_le hs

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

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s

Tactic:
intro _ _

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
intro _ _

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)

Tactic:
intro _ _

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a✝¹ : WithTop β
a✝ : a✝¹ ∈ lowerBounds s
⊢ a✝¹ ≤ ⊤
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
⊢ False

Tactic:
have : y ∈ Ici x := H.le

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ Ici x
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
rw [← pairwise_univ] at h

Goal state after:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
rw [← pairwise_univ] at h

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
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 : α
⊢ Ioc (e x) (e y) ∩ range ⇑e = Ioc (e x) (e y)

Tactic:
inter_eq_left.2 <| Ioc_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 : α
⊢ Ioc (e x) (e y) = Ioc (e x) (e y)
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : ⇑e '' c ⊆ t
⊢ c = ⇑e.symm '' t

Tactic:
exact hc.2 (ht.image _ fun _ _ ↦ e.symm.map_rel_iff.mp)
      ((e.toEquiv.subset_symm_image _ _).2 hf)

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)

Tactic:
exact (Subtype.mono_coe (· ∈ s)).le_csInf_image ⟨c, hct⟩ hB

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
simpa using of_decide_eq_false h

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

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
rw [extend, dif_pos hf, ← notMem_mulSupport]

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ ¬Classical.choose hf ∈ mulSupport g
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
⊢ ↑⌊a + b⌋ - ↑1 - a ≤ ↑⌊b⌋

Tactic:
Int.cast_one

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⌋
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
x : R
hx : fract x ≠ 0
⊢ fract (-x) = 1 - fract x

Tactic:
by
  rw [fract_eq_iff]
  constructor
  · rw [le_sub_iff_add_le, zero_add]
    exact (fract_lt_one x).le
  refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 1, ?_⟩
  simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]
  conv in -x => rw [← floor_add_fract x]
  simp [-floor_add_fract]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a ≤ ↑⌊a⌋ + ↑1

Tactic:
Int.cast_one

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a ≤ ↑⌊a⌋ + 1
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b

Tactic:
by_cases p <;> simp [*]

Goal state after:
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b

Tactic:
by_cases p <;> simp [*]

Goal state after:
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0

Tactic:
by_cases p <;> simp [*]

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x + ↑n) = f x + n • b

Tactic:
by simp [← map_add_nsmul]

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

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

Tactic:
sdiv_self

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
⊢ 1 • p₁ = 1 • p₁
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉

Tactic:
← Int.natCast_ceil_eq_ceil_of_neg_one_lt ha,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ = ↑↑⌈a⌉₊
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
⊢ mulAction'.toSMul = instSMulOfMul

Tactic:
fail_if_success rfl

Goal state after:
G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
⊢ mulAction'.toSMul = instSMulOfMul
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
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ ↑z + ↑1 < y * ↑n

Tactic:
Int.cast_one

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ ↑z + 1 < y * ↑n
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✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
⊢ MulArchimedean (WithZero M)

Tactic:
constructor
  intro x y hxy
  cases y with
  | zero => cases hxy.pos.false
  | coe y =>
    cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

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

Goal state before:
pp: α : Type u_1
s : Multiset α
nodup✝¹ : s.Nodup
t : Multiset α
nodup✝ : t.Nodup
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }

Tactic:
cases h; rfl

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {p /ₛ p} = {1}

Tactic:
sdiv_self

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {1} = {1}
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α)) _l) ↔ replicate n a ≤ Quot.mk (⇑(isSetoid α)) _l

Tactic:
simp only [quot_mk_to_coe'', coe_count]
    exact replicate_sublist_iff.symm.trans replicate_le_coe.symm

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

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

Tactic:
← coe_dedup,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (↑(s ++ t)).dedup = ↑s.dedup
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
· rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
cons_inter_of_neg _ h,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + t ∩ s = s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t

Tactic:
rintro ⟨h0, rfl⟩
    exact h0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : (i : α) → i ∈ insert a s → f i
⊢ prodPiInsert f (insertPiProd f x✝) = x✝

Tactic:
grind [prodPiInsert, insertPiProd]

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

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (insertPiProd f (prodPiInsert f x✝)).1 = x✝.1

Tactic:
grind [prodPiInsert, insertPiProd]

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

Goal state before:
pp: case snd
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (insertPiProd f (prodPiInsert f x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi

Tactic:
grind [prodPiInsert, insertPiProd]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun x ↦ x ∪ s) {t | Disjoint s t}

Tactic:
by
  grind [Set.InjOn, union_sdiff_cancel_right]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 < last (n + 1)

Tactic:
by
  rw [lt_def, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]
  exact NeZero.ne n

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi < j ↔ i < j.succ

Tactic:
rw [← succ_lt_succ_iff, succ_pred]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j < i.pred hi ↔ j.succ < i

Tactic:
rw [← succ_lt_succ_iff, succ_pred]

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

Goal state before:
pp: case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
i : Fin n
⊢ r (f i.castSucc) (f i.succ)

Tactic:
exact H i.castSucc_lt_succ

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

Goal state before:
pp: n : ℕ
⊢ (last n).succAbove = castSucc

Tactic:
by
  ext; simp only [succAbove_of_castSucc_lt, castSucc_lt_last]

Goal state after: