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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ 1 = 0

Tactic:
← map_one f,

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ f 1 = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y

Tactic:
exact (IsAddRightRegular.all _).withTop.eq_iff

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

Goal state before:
pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ 0 < ↑n ↔ 0 < n

Tactic:
by rw [← cast_zero, cast_lt]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n < 0 ↔ n < 0

Tactic:
by rw [← cast_zero, cast_lt]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ Nontrivial αˣ

Tactic:
obtain ⟨x, hx, hx'⟩ := exists_between (zero_lt_one' α)

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x : α
hx : 0 < x
hx' : x < 1
⊢ Nontrivial αˣ
Module: Mathlib.Order.WithBot

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), ↑a ≤ none → ↑a ≤ y) ↔ none ≤ y

Tactic:
simpa [WithBot.none_eq_bot, eq_bot_iff_forall_le] using! fun a ha ↦ (not_isBot _ ha).elim

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), ↑a ≤ none → ↑a ≤ y) ↔ none ≤ y

pp: case some
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
a : α
⊢ (∀ (a_1 : α), ↑a_1 ≤ Option.some a → ↑a_1 ≤ y) ↔ Option.some a ≤ y

Tactic:
· simpa [WithBot.none_eq_bot, eq_bot_iff_forall_le] using! fun a ha ↦ (not_isBot _ ha).elim

Goal state after:
case some
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
a : α
⊢ (∀ (a_1 : α), ↑a_1 ≤ Option.some a → ↑a_1 ≤ y) ↔ Option.some a ≤ y
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)

Tactic:
refine iff_of_true ?_ le_self_add

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d)
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ ⅟c * a = b ↔ a = c * b

Tactic:
by
  rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ 1 = 0

Tactic:
← map_one f,

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ f 1 = 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 2) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
rw [pow_succ]
    calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ -a / a = -1

Tactic:
rw [neg_div, div_self h]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a ^ 2 < b ^ 2 ↔ |a| < |b|

Tactic:
simpa only [sq_abs] using sq_lt_sq₀ (abs_nonneg a) (abs_nonneg b)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
exact image2_inter_union_subset hf

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
inst✝ : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
⊢ ∀ (x : β), x ∈ f '' s → ¬r x (f (⋯.min s hne))

Tactic:
rintro _ ⟨a, has, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
r : β → β → Prop
inst✝ : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
a : α
has : a ∈ s
⊢ ¬r (f a) (f (⋯.min s hne))
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB (insert a s) (a ⊔ b)

Tactic:
rw [insert_eq]

Goal state after:
γ : Type u_3
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest (insert a s) (max a b)

Tactic:
rw [insert_eq]

Goal state after:
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

Tactic:
Eq.comm

Goal state after:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length
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 / c < b / c ↔ b < a

Tactic:
rw [div_lt_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]

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

Goal state before:
pp: case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
exact .inr h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Surjective (map f) ↔ Surjective f

Tactic:
refine ⟨fun h x => ?_, (·.list_map)⟩
  let ⟨[y], hxy⟩ := h [x]
  exact ⟨_, List.singleton_injective hxy⟩

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

Goal state before:
pp: q : ℚ
⊢ -q = -q.num /. ↑q.den

Tactic:
by rw [← neg_divInt, num_divInt_den]

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

Goal state before:
pp: a b : ℤ
⊢ ↑(a /. b).den ∣ b

Tactic:
by_cases b0 : b = 0

Goal state after:
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * (b + c)

Tactic:
mul_add

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * b + a * c
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
⊢ (a - b) * c = a * c - b * c

Tactic:
obtain (hab | hba) := total_of (· ≤ ·) a b
  · rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]
  · apply h.eq_tsub_of_add_eq
    rw [← add_mul, tsub_add_cancel_of_le hba]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i ∈ s, a = a

Tactic:
← iSup_subtype'',

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i, a = a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Tactic:
iSup_subtype',

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ x, f ↑x ⋯) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ x, f ↑x ⋯) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Tactic:
iSup_subtype',

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ x, f ↑x ⋯) ⊔ a = ⨆ x, f ↑x ⋯ ⊔ a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ b ∈ range f, g b = ⨆ i, g (f i)

Tactic:
← iSup_subtype'',

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ i, g ↑i = ⨆ i, g (f i)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
← iSup_subtype'',

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ i, f ↑i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : (i, j) ∈ s ×ˢ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
mem_prod,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : i ∈ s ∧ j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a

Tactic:
simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · simp
  exact (isLUB_csSup' hs |>.union <| isLUB_csSup' ht).csSup_eq hne.inl

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
⊢ {x | Maximal (fun x ↦ x ∈ s) x} = t

Tactic:
refine Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
x : α
hx : x ∈ t
⊢ x ∈ {x | Maximal (fun x ↦ x ∈ s) x}
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
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 c : β
bc : a * b ≤ a * c
⊢ f a * f b ≤ f a * f c

Tactic:
rwa [← mul, ← mul, le]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
⊢ sSup ∅ = default

Tactic:
by
  simp [sSup]

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

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ↑num * ⅟↑den

Tactic:
apply mul_nonneg

Goal state after:
case ha
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ↑num

case hb
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ⅟↑den
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✝¹.mul db ≤ num✝.mul da) = true
h : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da

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✝¹.mul db ≤ num✝.mul da) = true
h : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑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
h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da

Goal state after:
α : 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
h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Notation.Support

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

Tactic:
image_inter_preimage

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι → M
s : Set κ
g : κ → ι
⊢ g '' s ∩ mulSupport f = g '' s ∩ mulSupport f
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
⊢ k * x - k * ↑⌊x⌋ = 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
sub_eq_iff_eq_add'

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
⊢ k * x = k * ↑⌊x⌋ + 1 ↔ ∃ n, k * x = k * ↑n + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ x = ↑(-z)

Tactic:
simp [← hz]

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

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ -x = ↑(-z)

Tactic:
simp [← hz]

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

Goal state before:
pp: case pos
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 : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x

Tactic:
use 1
    simp only [pow_one]
    exact y_pos.trans_lt hx

Goal state after:
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
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
rcases exists_nat_pow_near (one_le_inv_iff₀.2 ⟨xpos, hx⟩) (one_lt_inv_iff₀.2 ⟨ypos, hy⟩) with
    ⟨n, hn, h'n⟩

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
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
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
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋

Tactic:
simp [le_floor]

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

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ 0 < y

Tactic:
simpa using hxy

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

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ 1 < y

Tactic:
simpa using hxy

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) / (p₃ /ₛ p₁) = p₁ /ₛ p₂

Tactic:
rw [div_eq_mul_inv, inv_sdiv_eq_sdiv_rev, mul_comm, sdiv_mul_sdiv_cancel]

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)

Tactic:
rw [← coe_count, coe_replicate]

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n ?convert_1)

Tactic:
rw [← coe_count, coe_replicate]

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup

Tactic:
case cons a l IH =>
        exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons
          fun al => h a <| (singleton_sublist.2 al).cons_cons _

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
by_cases h : a ∈ l

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : ¬a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ filter p (map f (Quot.mk (⇑(isSetoid β)) l)) = map f (filter (p ∘ f) (Quot.mk (⇑(isSetoid β)) l))

Tactic:
by simp [List.filter_map]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ _root_.Disjoint u s ∧ s = t

Tactic:
rw [← add_eq_union_iff_disjoint]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)

Tactic:
rw [sub_cons, IH]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l

Tactic:
by_cases h : a ∈ l

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
by_cases h : a ∈ l

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∈ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∉ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint s t

Tactic:
rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]
  exact ⟨notMem_erase _ _, hst⟩

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

Goal state before:
pp: ⊢ univ.val = {True, False}.val

Tactic:
simp; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ Set.MapsTo f ↑s ↑t ↔ image f s ⊆ t

Tactic:
by
  simp [Set.MapsTo, image_subset_iff]

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

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1

Tactic:
exact pred_le_pred H

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
ha : a ∈ s
⊢ ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

Tactic:
obtain ⟨i, hi, rfl⟩ := hf a ha

Goal state after:
case mp
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
i : ℕ
hi : i < n
ha : f i hi ∈ s
⊢ ∃ i_1, ∃ (hi_1 : i_1 ∈ range n), f i_1 ⋯ = f i hi