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 b : G₀
ha : 0 < a
⊢ 1 < a⁻¹ * b ↔ a < b

Tactic:
lt_inv_mul_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a * 1 < b ↔ a < b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ ¬r a b

pp: case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ ¬r b a

Tactic:
· exact fun h => irrefl (r := s) (f a) (by simpa [e] using H _ _ h)

Goal state after:
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ ¬r b a
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : b ≤ c
h2 : a ≤ c - b
⊢ a + b ≤ c

Tactic:
by
  grw [h2, tsub_add_cancel_of_le h]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Tactic:
exact ha.le_tsub_iff_left h

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a = a - c + c

Tactic:
tsub_add_cancel_of_le h₂

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a = a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
· induction b
    · exact (add_top _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ a ∣ b

Tactic:
rw [← f.left_inv a, ← f.left_inv b]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
⊢ |↑↑a| = 1

Tactic:
cases Int.units_eq_one_or a

Goal state after:
case inl
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = 1
⊢ |↑↑a| = 1

case inr
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = -1
⊢ |↑↑a| = 1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
a b : α
n : ℕ
⊢ a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n

Tactic:
induction n with | zero => simp [geomSum] | succ n ih => ?_
  rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih,
    sub_mul, sub_mul, ← pow_succ, ← pow_succ', mul_comm, sub_add_sub_cancel]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
hne : Even n ∧ ¬Odd n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
simp only [*, and_true, ← abs_eq_abs,
    ← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]

Goal state after:
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:
by
  rw [insert_eq]
  exact isLUB_singleton.union hs

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ b < a

Tactic:
simpa using one_div_lt_one_div_of_lt (by simpa) h

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝ : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d

Tactic:
obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝¹ : a * b < d
a' : α
ha' : a' > a
hd✝ : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 ↦ x1 = map f x2) ∘r fun x1 x2 ↦ x1 ~ x2) = Perm ∘r fun x1 x2 ↦ x1 = map f x2

Tactic:
simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]

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

Goal state before:
pp: case refine_1
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : a ∈ l₁
⊢ idxOf a l₂ < l₁.length

pp: case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁

Tactic:
· exact hl.idxOf_eq_of_mem h ▸ idxOf_lt_length_of_mem h

Goal state after:
case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) * (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
ih

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * (map (fun x ↦ if x = a then f x else g x) xs).prod =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
ih

Goal state after:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr / ↑dr * (↑nr / ↑dr)

Tactic:
rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

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

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
· push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0

Tactic:
· push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
· push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: p : ℚ → Prop
⊢ (∃ r, p r) ↔ ∃ a b, b ≠ 0 ∧ p (↑a / ↑b)

Tactic:
simpa using Rat.forall (p := (¬ p ·)).not

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

Tactic:
iSup_le_iff

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

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
mem_iInter

Goal state after:
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 γ
⊢ ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
simp_rw [iSup_prod, mem_prod, iSup_and]
  exact iSup_congr fun _ => iSup_comm

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨆ g, ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ a, f (g a)

Tactic:
mem_iInter

Goal state after:
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i = ⨆ g, ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ a, f (g a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
⊢ sSup ∅ = sSup t

pp: case inr
α : 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
⊢ sSup s = sSup t

Tactic:
· have : t = ∅ := eq_empty_of_forall_notMem (fun y yt ↦ by simpa using ht y yt)
    rw [this]

Goal state after:
case inr
α : 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
⊢ sSup s = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f b

Tactic:
have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc a b) = f b
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case mp.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
· exact H hx hy hne

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Tactic:
by
  rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]

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

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected

Tactic:
exact ordConnected_Icc

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
rw [← le, mul, mul]; refine mul_le_mul_of_nonneg_right (le.2 hbc) ?_; rwa [← zero, le]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
n₁ n₂ : ℕ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ = ⅟a₂ * (↑n₂ * a₁) ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
← mul_left_eq_iff_eq_invOf_mul,

Goal state after:
α : Type u_1
inst✝² : Semiring α
n₁ n₂ : ℕ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ a₂ * ↑n₁ = ↑n₂ * a₁ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ = ⅟a₂ * (↑n₂ * a₁) ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
← mul_left_eq_iff_eq_invOf_mul,

Goal state after:
α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ a₂ * ↑n₁ = ↑n₂ * a₁ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
Module: Mathlib.Algebra.Notation.Support

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

Tactic:
by
  simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]

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

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

Tactic:
nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]

Goal state after:
n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) * f (b / c)

Tactic:
by
  simpa only [div_mul_div_cancel] using map_mul_le_mul f (a / b) (b / c)

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

Goal state before:
pp: n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k

Tactic:
exact fun h _ => h

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

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]
    refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
    refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

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

Goal state before:
pp: case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1

Tactic:
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
    rfl

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

Goal state before:
pp: m k : ℕ+
⊢ m.mod k ≤ m ∧ m.mod k ≤ k

Tactic:
by
  change (mod m k : ℕ) ≤ (m : ℕ) ∧ (mod m k : ℕ) ≤ (k : ℕ)
  rw [mod_coe]
  split_ifs with h
  · have hm : (m : ℕ) > 0 := m.pos
    rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
    simp
    lia
  · exact ⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ |x - ↑z|

Tactic:
abs_eq_neg_self.mpr (sub_neg.mpr hx).le

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Tactic:
simp_rw [← zpow_lt_zpow_iff_right hlt]

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ a⁻¹ ^ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < a⁻¹ ^ 1
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ 0 < k ∧ k < 1

Tactic:
simp_rw [← zpow_lt_zpow_iff_right hlt]

Goal state after:
case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ a ^ 0 < a ^ k ∧ a ^ k < a ^ 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case zero
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ∃ z, fract a * ↑0 - fract (a * ↑0) = ↑z

Tactic:
use 0; simp

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

Goal state before:
pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
m : ℤ
y : R
hys : y ∈ s
h0 : 0 ≤ y - ↑m
h1 : y - ↑m < 1
⊢ ∃ x ∈ s, fract x = y - ↑m

Tactic:
obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩

Goal state after:
case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
y : R
hys : y ∈ s
h0 : 0 ≤ y - ↑⌊y⌋
h1 : y - ↑⌊y⌋ < 1
⊢ ∃ x ∈ s, fract x = y - ↑⌊y⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat (-(-↑n / ↑d)).toNat

Tactic:
← ceil_intCast_div_natCast n d,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑↑n / ↑d⌉.toNat
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = ↑(-(-↑n / ↑d)).toNat

Tactic:
← ceil_intCast_div_natCast n d,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = ↑⌈↑↑n / ↑d⌉.toNat
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
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • ↑m⁻¹ * g • ↑m = 1

Tactic:
rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]

Goal state after:
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:
by
  fail_if_success rfl -- there is an instance diamond here
  ext
  rfl

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
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
⊢ 1 < y * ↑n - x * ↑n

Tactic:
← sub_mul,

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
⊢ 1 < (y - x) * ↑n
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) * δ - q| ≤ δ

Tactic:
← sub_mul,

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
⊢ |(↑m.pred + 1 - ↑m.pred) * δ| ≤ δ
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
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂

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
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
⊢ ((∀ (x : α), x ∈ m → r x x) → Rel r m m) → (∀ (x : α), x ∈ a ::ₘ m → r x x) → Rel r (a ::ₘ m) (a ::ₘ m)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_1
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
⊢ (∀ (x : α), x ∈ a ::ₘ m → r x x) → Rel r (a ::ₘ m) (a ::ₘ m)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
u : Multiset α
a : α
s✝ : Multiset α
IH : ∀ {s : Multiset α}, s - s✝ ≤ u ↔ s ≤ u + s✝
s : Multiset α
⊢ s - a ::ₘ s✝ ≤ u ↔ s ≤ u + a ::ₘ s✝

Tactic:
| cons a s IH =>

Goal state after: