mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b✝ : α
hbc : r b b✝
⊢ TransGen r a b✝

Tactic:
exact tail' hab hbc

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f) g e' b = g (f.symm b)

Tactic:
rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b

Tactic:
simpa [Pi.lt_def] using le_of_lt

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap < (b, a) ↔ x < (a, b)

Tactic:
rw [← swap_lt_swap]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap.swap < (b, a).swap ↔ x < (a, b)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P a (b + 1)

Tactic:
apply diag_induction P ha hb hd a (b + 1)

Goal state after:
case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a < b + 1
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s

Tactic:
simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop]

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ {x | x ∈ l} = {a} → l = [a]

Tactic:
ofPred_mem_list_eq_replicate

Goal state after:
case mp
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ (∃ n, n > 0 ∧ l = List.replicate n a) → l = [a]
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b ≠ a ⊔ b ↔ a ≠ b

Tactic:
Ne,

Goal state after:
α : Type u
inst✝ : Lattice α
a b : α
⊢ ¬a ⊓ b = a ⊔ b ↔ a ≠ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b ⊔ b = a

Tactic:
by rw [sup_comm, sup_sdiff_cancel_right h]

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

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

Tactic:
rw [le_sup_iff, or_iff_right h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
a : α
⊢ (fun b ↦ ((↑e).symm ↑b).get ⋯) ((fun a ↦ ⟨↑e (some a), ⋯⟩) a) = a

Tactic:
rw [← some_inj, some_get]
        exact symm_apply_apply (e : Option α ≃ β) a

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ≤ z

Tactic:
by
    conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
    refine le_of_inf_le_sup_le ?_ H.le
    rw [inf_sdiff_self_right]
    exact bot_le

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
i : (a : α) × β a
f : (i : (a : α) × β a) → γ i.fst i.snd
x : γ i.fst i.snd
⊢ curry (update f i x) = update (curry f) i.fst (update (curry f i.fst) i.snd x)

Tactic:
by
  obtain ⟨ia, ib⟩ := i
  ext ja jb
  unfold Sigma.curry
  obtain rfl | ha := eq_or_ne ia ja
  · simp
    grind
  · rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
    · exact ha.symm
    · exact ha.symm

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x ∧ x \ y ≠ x ↔ ¬Disjoint y x

Tactic:
Ne,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x ∧ ¬x \ y = x ↔ ¬Disjoint y x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
⊢ LeftInverse (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val)

Tactic:
rintro (⟨x, hx⟩ | ⟨x, hx⟩)

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inl ⟨x, hx⟩)) =
    Sum.inl ⟨x, hx⟩

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inr ⟨x, hx⟩)) =
    Sum.inr ⟨x, hx⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ x ⊓ xᶜ ≤ ⊥

Tactic:
by constructor <;> simp

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤ ≤ x ⊔ xᶜ

Tactic:
by constructor <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s \ f '' t ⊆ f '' (s \ t)

Tactic:
sdiff_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' t ∪ f '' (s \ t)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (preimage f) ↔ Injective f

Tactic:
rw [← Surjective.of_comp_iff _ Set.ofPred_bijective.surjective,
    ← Surjective.of_comp_iff' Set.mem_bijective]
  exact surjective_comp_right_iff_injective

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t ≠ ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
Ne,

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
exact bijOn_empty f

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ (f a ^ (n + 1))⁻¹ = f a ^ Int.negSucc n

Tactic:
← zpow_negSucc

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f a ^ Int.negSucc n = f a ^ Int.negSucc n
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' f '' s

Tactic:
rcases ha hxt with ⟨x, hxs, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' f '' s

Tactic:
h x

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ ↑(f (g₁ (g₂ a))) = ↑(f a)

Tactic:
h ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ ↑(f (g₂ (g₁ a))) = ↑(f a)

Tactic:
h ha

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

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
⊢ SurjOn (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
rintro x hx
  obtain ⟨a₁, ha₁, hx₁⟩ := h₁ hx.1
  obtain ⟨a₂, ha₂, hx₂⟩ := h₂ hx.2
  exact ⟨(a₁, a₂), ⟨ha₁, ha₂⟩, Prod.ext hx₁ hx₂⟩

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

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

Tactic:
mul_eq_left,

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ b⁻¹ = 1 ↔ b = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
apply div_mul_div_cancel

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit a

Tactic:
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * ↑u * ↑u⁻¹)
⊢ IsUnit a
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
by
    ext <;> apply pow_left_injective hn; exacts [congr(($hab).1), congr(($hab).2)]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: F : Type → Type v
inst✝ : Alternative F
h : Decidable False
⊢ guard False = failure

Tactic:
by
  simp [guard]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
by
  split_ifs with h
  · rw [h, pow_zero]
  · rw [zero_pow h]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j = σ ↔ i = j

Tactic:
mul_eq_left,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j = 1 ↔ i = j
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c

Tactic:
by
  simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : c * a = b
⊢ a * c = b

Tactic:
by rw [mul_comm] at h; apply h

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
⊢ (fun x ↦ r * x) r' = (fun x ↦ r * x) 0

Tactic:
simp_rw [eq, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b * (1 / a)) = -(b / a)

Tactic:
rw [mul_one_div]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
⊢ y = x * z

Tactic:
← h1,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
⊢ y = x * (x⁻¹ʳ * y)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
⊢ x = y * z⁻¹ʳ

Tactic:
← h1,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
⊢ x = x * z * z⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False

Tactic:
simp [hb] at h

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : αˣ
⊢ ↑a = -1 ↔ a = -1

Tactic:
← Units.coe_neg_one,

Goal state after:
α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : αˣ
⊢ ↑a = ↑(-1) ↔ a = -1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a = 2 * b + 1 ↔ a = 2 * b + 1

Tactic:
rw [two_mul]

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

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
⊢ f = id

Tactic:
by rwa [hf.iterate_odd hn] at H

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False

Tactic:
simp [hb] at h

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

Goal state before:

Tactic:
_ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Goal state after:
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
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹

Tactic:
exact mul_nonneg ha (inv_nonneg.2 hb)

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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
iterate 3 rw [mul_nonneg_iff]
  have or_a := le_total 0 a
  have or_b := le_total 0 b
  have or_c := le_total 0 c
  aesop

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ 1 < a ^ n ↔ n < 0

Tactic:
simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ n < 1 ↔ 0 < n

Tactic:
simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
rcases le_total d b with h | h

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
by
  obtain h | h := le_total 1 a
  · simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h
  · simp [mabs_of_le_one h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine Iff.trans ?_ isRegular_mul_and_mul_iff
  exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

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

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

Tactic:
exact ⟨a, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b ≠ 0 ↔ ¬a ≤ b

Tactic:
Ne,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ ¬a - b = 0 ↔ ¬a ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

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:
· exact (add_top _).symm

Goal state after:
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✝
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑m = ↑(m + n) - ↑n

Tactic:
cast_add,

Goal state after:
case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑m = ↑m + ↑n - ↑n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos.mpr.inl
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ k + 1
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
hlt : m < k + 1
⊢ k + 1 = m

pp: case pos.mpr.inr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
hle : k + 1 ≤ k + 1
h0 : k + 1 ≠ 0 → P (k + 1)
hm : ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ k + 1 → ¬P n
⊢ k + 1 = k + 1

Tactic:
exacts [(hm hlt (le_refl _) hk).elim, rfl]

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k ≠ 0 ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
Ne,

Goal state after:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ ¬findGreatest P k = 0 ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
hf : StrictMono ⇑f
⊢ StrictMono ⇑(map' f)

Tactic:
by simpa [StrictMono, WithZero.forall]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
← le_floor_iff ha,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n

Tactic:
tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)),

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + (0 + 1) ∧ ⌈a⌉₊ ≤ n
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ m ^ n * ⅟m ^ n = 1

Tactic:
← (commute_invOf m).mul_pow,

Goal state after:
α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ (m * ⅟m) ^ n = 1
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
exact le_add_of_nonneg_right h1

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Tactic:
rw [two_mul]

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
h : Relator.RightTotal r
⊢ False

Tactic:
obtain ⟨a, -, ha⟩ := wf.has_min Set.univ Set.univ_nonempty

Goal state after:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
h : Relator.RightTotal r
a : α
ha : ∀ (x : α), x ∈ Set.univ → ¬r x a
⊢ False
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
⊢ False

Tactic:
obtain ⟨a, -, ha⟩ := wf.has_min Set.univ Set.univ_nonempty

Goal state after:
α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
a : α
ha : ∀ (x : α), x ∈ Set.univ → ¬Function.swap r x a
⊢ False
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)
x : α
hx : x ∈ s
hts : ∃ x, ∃ (_ : x ∈ t), ∀ x_1 ∈ s, ¬x ≤ x_1
⊢ ∃ b ∈ t, x ≤ b

Tactic:
obtain ⟨y, hy, hys⟩ := hts

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
⊢ ∃ b ∈ t, x ≤ b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t

Tactic:
by
  ext; rw [← nonempty_coe_sort] at hs ht; aesop (add simp [upperBounds, Prod.le_def, forall_and])

Goal state after: