mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
· decide

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x

Tactic:
· exact ⟨y, Ne.symm hx⟩

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
⊢ x = y

Tactic:
have : Inhabited (∀ i, α i) := ⟨fun _ => Classical.choice inferInstance⟩

Goal state after:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ x = y
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f g : α → α
h : Commute f g
n✝ : ℕ
x : α
hx : f x = g x
n : ℕ
ihn : f^[n] x = g^[n] x
⊢ f^[n.succ] x = g^[n.succ] x

Tactic:
simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
⊢ DenselyOrdered αᵒᵈ → DenselyOrdered α

Tactic:
by convert! @OrderDual.denselyOrdered αᵒᵈ _

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · by_cases h₁ : y.1 ≤ x.1
    · exact Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
    · exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩
  · rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩
    · exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩

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

Goal state before:
pp: case inl
⊢ 2 * 0 ^ 2 + 1 ≤ 2 ^ (2 * 0)

pp: case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
· decide

Goal state after:
case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

Tactic:
obtain ⟨ha', hb⟩ | ⟨ha', hb⟩ := Prod.lt_iff.1 hx

Goal state after:
case ind.ind.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
by_cases hy : p y

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Disjoint x y

Tactic:
by grind [disjoint_iff_inf_le]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : b ≤ c
⊢ a ≤ ⊤ ↔ min a b ≤ c

pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ min a b ≤ c

Tactic:
· exact iff_of_true le_top (inf_le_of_right_le h)

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ min a b ≤ c
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ x \ y ⊓ y \ x = x \ y ⊓ y \ x

Tactic:
by rw [inf_of_le_right sdiff_le']

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image (f ∘ f^[n]) = image f ∘ (image f)^[n]

Tactic:
← ih,

Goal state after:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image (f ∘ f^[n]) = image f ∘ image f^[n]
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)

Tactic:
by
  ext
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
rw [← injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
    (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
⊢ val ⁻¹' s = ?m.9 ⁻¹' range ?m.9

pp: α : Type u_1
s : Set α
⊢ { x // x ∈ s } → ?m.8

pp: α : Type u_1
s : Set α
⊢ Type ?u.14

Tactic:
range_coe

Goal state after:
α : Type u_1
s : Set α
⊢ val ⁻¹' s = val ⁻¹' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, s ⊆ range val ∧ p s) ↔ ∃ s, s ⊆ t ∧ p s

Tactic:
range_coe

Goal state after:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, s ⊆ t ∧ p s) ↔ ∃ s, s ⊆ t ∧ p s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set α), s ⊆ range val → p s) ↔ ∀ (s : Set α), s ⊆ t → p s

Tactic:
range_coe

Goal state after:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set α), s ⊆ t → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ (∃ y, f y = x) → (f ⋯.choose).2 = x.2

Tactic:
rintro ⟨g, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
g : α
⊢ (f ⋯.choose).2 = (f g).2
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝

Tactic:
simp only [map_one, coe_comp, Function.comp_apply, one_apply]

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

Goal state before:
pp: case ofNat.succ
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i : ℕ
ih : motive (ofNat i)
⊢ motive (ofNat (i + 1))

Tactic:
| succ i ih =>

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ Int.leInductionDown base pred (n - 1) ⋯ = pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
rw [Int.leInductionDown, inductionOn'_sub_one hnm]
  rfl

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : b = a * c
⊢ a⁻¹ * b = c

Tactic:
by rw [h, inv_mul_cancel_left]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a = b / c ↔ c * a = b

Tactic:
by rw [eq_div_iff_mul_eq', mul_comm]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
div_eq_div_iff_mul_eq_mul

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a * d = c * b ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : b = ↑a * c
⊢ ↑a⁻¹ * b = c

Tactic:
by rw [h, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u a : αˣ
⊢ a ^ 0 = 1

Tactic:
simp only [HPow.hPow, Pow.pow]; simp

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
⊢ x✝¹ = x✝

Tactic:
have := congr_arg f He
    rw [mul, mul] at this
    exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

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

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a

Tactic:
· rw [mul_inv_cancel₀ h, one_mul]

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + -[n+1]) = ↑-[m+1] + ↑-[n+1]

Tactic:
rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]

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

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

Tactic:
by
  rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
⊢ 0⁻¹ʳ = 0

Tactic:
by
  nontriviality
  exact inverse_non_unit _ not_isUnit_zero

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ ↑0 • b = 0 • b

Tactic:
rw [Nat.cast_zero, zero_smul, zero_smul]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (swap fun x1 x2 ↦ x1 * x2) r ↔ Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r

Tactic:
by
  refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
    exact h a⁻¹ bc
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
    exact h a⁻¹ bc

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
h : 1 ≤ a * a
⊢ 1 ≤ a

Tactic:
contrapose! h; exact mul_lt_one' h h

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ^ (n + 1) ≤ 1

Tactic:
zero_pow n.succ_ne_zero

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)

Tactic:
rw [pow_succ']; exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

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

Goal state before:
pp: R : Type u
α : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
a b c : R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ 1

Tactic:
simpa only [one_mul] using mul_self_nonneg (1 : R)

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x

Tactic:
rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
⊢ False

Tactic:
have := Int.natAbs_le_of_dvd_ne_zero h1 h

Goal state after:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1

Tactic:
rwa [div_le_one']

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

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q - 1 ≤ ↑n - 1

Tactic:
sub_le_sub_iff_right,

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q ≤ ↑n
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).log = x.log - y.log

Tactic:
by
  lift x to Multiplicative G using hx; lift y to Multiplicative G using hy; rfl

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P (n + 1)
⊢ findGreatest P (n + 1) = n + 1

Tactic:
simp [Nat.findGreatest, h]

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) = findGreatest P n

Tactic:
simp [Nat.findGreatest, h]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
⊢ ∃ n, x ≤ ↑n

Tactic:
obtain ⟨n, hn⟩ := bounded x

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
n : ℕ
hn : x ≤ ↑n
⊢ ∃ n, x ≤ ↑n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
⊢ ∃ k, exp (-↑k) < x

Tactic:
by
  obtain ⟨y, hnz, hyx⟩ := WithZero.exists_ne_zero_and_lt hx
  use (-y.log).toNat
  apply lt_of_le_of_lt _ hyx
  rw [← WithZero.le_log_iff_exp_le hnz, Int.neg_le_iff]
  exact Int.self_le_toNat _

Goal state after:
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
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n + ↑n⌉₊ = ⌈a⌉₊

pp: case inr.ha
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ 0 ≤ a - ↑n

Tactic:
tsub_add_cancel_of_le hna

Goal state after:
case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a⌉₊ = ⌈a⌉₊

case inr.ha
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ 0 ≤ a - ↑n
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
· exact (OrderIso.mulRight₀ c hc).map_inf a b

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

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

Tactic:
← ih,

Goal state after:
case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a ^ (n + 1) - b ^ (n + 1)) * a + (a - b) * b ^ (n + 1)
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
⊢ wf.min (f '' s) ⋯ = f (⋯.min s hne)

Tactic:
apply min_eq_of_forall_not_lt wf <| Set.mem_image_of_mem f <| min_mem wf.onFun s hne

Goal state after:
α : 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))
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
by
  simp only [isMin_iff_forall_not_lt, eq_empty_iff_forall_notMem, mem_Iio]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
by
  intro x hx y hy
  obtain ⟨z, hz, hxz, hyz⟩ := hd x (hst hx) y (hst hy)
  obtain ⟨w, hw, hzw⟩ := hc hz
  exact ⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩

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

Goal state before:
pp: case cons
M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a * l.prod)

Tactic:
simp only [mem_cons, forall_eq_or_imp] at base

Goal state after:
case cons
M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a * l.prod)

Tactic:
simp only [mem_cons, forall_eq_or_imp] at base

Goal state after:
case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
hl_empty : ¬l = []
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionSemiring α
x✝³ x✝² : α
x✝¹ x✝ : ℕ
h : IsNNRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsNNRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
by simpa [div_eq_mul_inv] using h

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

Goal state before:
pp: α : Type u
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
by simpa [div_eq_mul_inv] using h

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ b / a ≤ 1

Tactic:
div_le_one_of_neg (h.trans_lt hb)

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ a ≤ b
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
    forall₂_drop (length l₁) h
  rwa [drop_left] at h'

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

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Tactic:
by
  refine ⟨?_, map_subset f⟩; intro h2 x hx
  rcases mem_map.1 (h2 (mem_map_of_mem hx)) with ⟨x', hx', hxx'⟩
  cases h hxx'; exact hx'

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:
by
  rw [h, hn, div_one]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
p : ℤ × M
l : NF M
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        (p :: l)).prod =
    (map
          (fun x ↦
            match x with
            | (r, x) => zpow' x r)
          l).prod *
      zpow' p.2 p.1

Tactic:
simp [mul_comm]

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

Goal state before:
pp: p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
← coe_le_coe,

Goal state after:
p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ ↑q ≤ ↑p.toNNRat ↔ ↑q ≤ p
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: m : ℕ
⊢ ↑(m + 1).toPNat' = if 0 < m + 1 then m + 1 else 1

Tactic:
rw [if_pos (succ_pos m)]
    rfl

Goal state after: