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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ a * c + b / c * c = a * c + b

Tactic:
div_mul_cancel₀ _ hc

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ a * c + b = a * c + b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
a : K
⊢ f (q • a) = f (↑q * a)

Tactic:
by rw [nnqsmul, NNRat.smul_def, mul, nnratCast]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
by
  rw [image2_union_left]
  nth_grw 1 [inter_subset_left, inter_subset_right]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

Tactic:
exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩

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

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

Tactic:
by rw [e.symm.symm_image_subset]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t

Tactic:
directedOn_union_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)

Tactic:
simp [Iic]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ IsLUB s a ↔ IsLUB s b

Tactic:
simp [isLUB_iff_le_iff, h.le_congr_left]

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b * (a / max (b + 1) 1) < a

Tactic:
rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < max (b + 1) 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
· simp [hab, Set.Subsingleton.antitoneOn]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
· simp [hab, Set.Subsingleton.antitoneOn]

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0

Tactic:
simp [zero_lt_one.not_ge]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝ : List α
_hlu : l₁✝ ~ l₂✝
ih : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
v : List β
huv : Forall₂ r (u :: l₂✝) v
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) v

Tactic:
obtain - | ⟨hab, huv'⟩ := huv
    rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
    exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
⊢ l = n

Tactic:
rw [h, hn, div_one]

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

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
⊢ f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
by
  generalize ha : a /. b = x; obtain ⟨n₁, d₁, h₁, c₁⟩ := x; rw [mk_eq_divInt] at ha
  generalize hc : c /. d = x; obtain ⟨n₂, d₂, h₂, c₂⟩ := x; rw [mk_eq_divInt] at hc
  rw [fv]
  have d₁0 := Int.ofNat_ne_zero.2 h₁
  have d₂0 := Int.ofNat_ne_zero.2 h₂
  exact (divInt_eq_divInt_iff (f0 d₁0 d₂0) (f0 b0 d0)).2
    (H ((divInt_eq_divInt_iff b0 d₁0).1 ha) ((divInt_eq_divInt_iff d0 d₂0).1 hc))

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

Goal state before:
pp: a b : ℕ
⊢ range' a b 0 = replicate b a

Tactic:
induction b with

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

Goal state before:
pp: case inr
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
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c

Tactic:
apply h.eq_tsub_of_add_eq

Goal state after:
case inr
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
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
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)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
apply h.eq_tsub_of_add_eq

Goal state after:
case inr
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)
hba : b ≤ a
⊢ (a - b) * c + b * c = a * c
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Tactic:
have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
  rw [← Monotone.iSup_nat_add hf k]
  · simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
s : ι → α
⊢ ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i

Tactic:
simp [bot_lt_iff_ne_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Type u_8
ι' : Type u_9
g : ι' → α
e : ι ≃ ι'
s : Set ι'
⊢ ⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i

Tactic:
by
  simpa only [iSup_subtype'] using! (image e.symm s).symm.iSup_comp (g := g ∘ (↑))

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
⊢ (⋃ i, s i).pi t = ⋂ i, (s i).pi t

Tactic:
ext f
  simp
  grind

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Ici (f i j)

Tactic:
simp_rw [Ici_iSup]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
a : α
⊢ ¬g a (f a) ≤ rhs

Tactic:
by simpa using hf a

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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
⊢ ↑(sSup ∅) = ⊥

Tactic:
_root_.sSup_empty,

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
⊢ ↑⊥ = ⊥
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∃ x, ∃ (_ : x ∈ ⋃₀ S), p x) ↔ ∃ s, ∃ (_ : s ∈ S), ∃ x, ∃ (_ : x ∈ s), p x

Tactic:
← iSup_Prop_eq,

Goal state after:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ ⨆ x ∈ ⋃₀ S, p x ↔ ⨆ s ∈ S, ⨆ x ∈ s, p x
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ c ∈ {⊤}

Tactic:
rw [mem_singleton_iff, ← top_le_iff]

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ Icc a (a ⊔ b) = Icc a b

Tactic:
sup_eq_right.2 h

Goal state after:
α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioo a (max a b) = Ioo a b

Tactic:
sup_eq_right.2 h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioo a b = Ioo a b
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
⊢ 0 ≤ f a

Tactic:
rwa [← zero, le]

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
⊢ f b * f a ≤ f c * f a

Tactic:
refine mul_le_mul_of_nonneg_right (le.2 hbc) ?_

Goal state after:
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
⊢ 0 ≤ f a
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ 0 ≤ c

Tactic:
rw [← add_zero a.val, hc] at h

Goal state after:
α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
c : α
h : ↑a + 0 ≤ ↑a + c
hc : ↑b = ↑a + c
⊢ 0 ≤ c
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsRat a (Int.negOfNat num) den
⊢ IsNNRat |a| num den

Tactic:
by
  obtain ⟨ha1, rfl⟩ := ra
  simp only [Int.cast_negOfNat, neg_mul, abs_neg]
  refine ⟨ha1, abs_of_nonneg ?_⟩
  apply mul_nonneg
  · exact Nat.cast_nonneg' num
  · simp only [invOf_eq_inv, inv_nonneg, Nat.cast_nonneg]

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n

Tactic:
simp [← cast_le (K := K)]

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p

Tactic:
simp [← cast_le (K := K)]

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

Goal state before:
pp: m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + n + 1)!

Tactic:
factorial_succ,

Goal state after:
m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + n + 1) * (m + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (k + 1)!

Tactic:
factorial_succ,

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

Goal state before:
pp: n k : ℕ
⊢ n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!

Tactic:
factorial_succ,

Goal state after:
n k : ℕ
⊢ n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1)! * n ^ (j + 1)

Tactic:
factorial_succ,

Goal state after:
case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1) * j ! * n ^ (j + 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
a : R
b : ℕ
⊢ ∃ z, fract a * ↑b - fract (a * ↑b) = ↑z

Tactic:
induction b with

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
a : G
b : H
inst✝² : AddZeroClass G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
⊢ f a = f 0 + b

Tactic:
simpa using map_add_const f 0

Goal state after:
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
⊢ fract (↑(negOfNat n) * ⅟↑d) = ↑(-↑n % ↑d) * ⅟↑d

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_intCast_eq_div_intCast_mod,
    negOfNat_eq, ofNat_eq_natCast]

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

Goal state before:
pp: case inr
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
· rcases le_or_gt b 1 with hb₁ | hb₁
    · obtain ⟨n, hn⟩ := exists_pow_btwn_of_lt_mul h hb₀ hb₁ hc₀ hc₁
      exact ⟨n, mod_cast hn⟩
    · rcases lt_or_ge a 1 with ha₁ | ha₁
      · refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩
      · have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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
n m : ℤ
m0 : 0 < m
⊢ ↑n.toNat ≤ n.toNat • m

Tactic:
simpa only [nsmul_eq_mul, zero_add, mul_one] using
          mul_le_mul_of_nonneg_left (Int.add_one_le_iff.2 m0) (Int.natCast_nonneg n.toNat)

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ ↑l = {a} ↔ l = [a]

Tactic:
← coe_singleton,

Goal state after:
α : Type u_1
l : List α
a : α
⊢ ↑l = ↑[a] ↔ l = [a]
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a

Tactic:
← replicate_le_coe,

Goal state after:
α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ replicate k a ≤ ↑(List.replicate n a)
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ replicate k a ≤ ↑(List.replicate n a)

Tactic:
coe_replicate

Goal state after:
α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ replicate k a ≤ replicate n a
Module: Mathlib.Data.Multiset.Replicate

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

Tactic:
coe_replicate

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = count a (replicate n a)
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) = count a ↑(List.replicate n ?convert_1)

Tactic:
coe_replicate

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

case e'_2.a
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ α
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup

Tactic:
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
      from forall_comm.trans <| forall_congr' fun _ => forall_eq']

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : List α
⊢ [] <+ []

Tactic:
by rfl

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∧ ¬x ∈ ys

Tactic:
exact ⟨hx, h.1⟩

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂

Tactic:
by rw [List.map_append, List.map_diff finj]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.replicate (List.count b l) b) = replicate (List.count b l) b

Tactic:
coe_replicate

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ replicate (List.count b l) b = replicate (List.count b l) b
Module: Mathlib.Data.List.Infix

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

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
· simp only [insert_of_mem h, suffix_refl]

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

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

Tactic:
by
  rw [← disjoint_erase_comm, erase_insert ha]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩

Tactic:
simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
  rw! [Finset.union_symm_left h hi hi']
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ map f s = ∅ ↔ s = ∅

Tactic:
map_eq_empty

Goal state after:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
rw [val_add]

Goal state after:
n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ (↑a + ↑b) % n = ↑a + ↑b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
⊢ #s = #t

Tactic:
by
  refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)
  rw [← left_inv a1 h1, ← left_inv a2 h2]
  simp only [eq]

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

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

Tactic:
exact (ha rfl).elim

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.succ ≤ p

Tactic:
by
  rw [succAbove_lt_iff_castSucc_lt, castSucc_lt_iff_succ_le]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.predAbove 0 = 0

Tactic:
cases n
  · exact i.elim0
  · rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
obtain h | h := Fin.lt_or_lt_of_ne h
  · rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]
  · rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
classical
    simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
      ← exists_and_left, exists_comm (α := Finset α)]
    constructor
    · rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩
      exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
      exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

Goal state after: