mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ b = c

Tactic:
← mul_inv_cancel_right b a,

Goal state after:
G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ b * a * a⁻¹ = c
Module: Mathlib.Logic.Relation

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

Tactic:
induction hab generalizing c with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen r ≤ EqvGen r

Tactic:
by
  intro _ _ h
  induction h using ReflTransGen.trans_induction_on with
  | refl => exact .refl _
  | trans _ _ h1 h2 => exact _root_.trans h1 h2
  | single h => exact .rel _ _ h

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

Goal state before:
pp: α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[n.succ] = id

Tactic:
rw [iterate_succ, ihn, id_comp]

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

Goal state before:
pp: case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + 1 + k))

Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]
    exact (H k).trans (ihn (k + 1))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
⊢ (map f g)^[n] = map f^[n] g^[n]

Tactic:
induction n <;> simp [*, Prod.map_comp_map]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ cmp a b = compare a b

Tactic:
refine ((compare_iff ..).2 ?_).symm

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
first | rfl | contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
first | rfl | contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
first | rfl | contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False

Tactic:
first | rfl | contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
first | rfl | contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
first | rfl | contradiction

Goal state after:
case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False

Tactic:
first | rfl | contradiction

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
first | rfl | contradiction

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt

Tactic:
first | rfl | contradiction

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

Goal state before:
pp: f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (m + n)

Tactic:
Nat.add_comm m

Goal state after:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (n + m)
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y

Tactic:
exact (gc x y).symm

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

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

Tactic:
sup_comm y,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
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.18
β : Type ?u.17
γ : Type ?u.15
⊢ LeftInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))

Tactic:
rintro (⟨_ | _⟩ | _)

Goal state after:
case inl.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.18
β : Type ?u.17
γ : Type ?u.15
val✝ : α
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val✝))) =
    inl (inl val✝)

case inl.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.18
β : Type ?u.17
γ : Type ?u.15
val✝ : β
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val✝))) =
    inl (inr val✝)

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.18
β : Type ?u.17
γ : Type ?u.15
val✝ : γ
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val✝)) =
    inr val✝
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = ⊥ ∧ b \ a = ⊥ ↔ a = b

Tactic:
sdiff_eq_bot_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ b ∧ b ≤ a ↔ a = b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ (b \ a) = a ⊔ b

Tactic:
rw [symmDiff, sdiff_idem]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
⊢ ⇑ε₂.symm ∘ f ∘ ⇑ε₁.symm = f' ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁

Tactic:
rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
b : β
hb : f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
· exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ range f

Tactic:
rw [← image_univ]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
⊢ range val = s

Tactic:
rw [← image_univ]

Goal state after:
α : Type u_1
s : Set α
⊢ val '' univ = s
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
by
        show f (x * y) * g (x * y) = f x * g x * (f y * g y)
        rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)

Tactic:
rw [← image_univ]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)

Tactic:
rw [← image_univ]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ ↑n.succ) = f (x ^ ↑n * x)

Tactic:
by rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]

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

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
    exact h_inv _ ih

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

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

Tactic:
inv_mul_cancel_left,

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b✝ u a b : αˣ
⊢ ↑a * ↑a⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
inv_mul_cancel_left,

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b✝ u a b : αˣ
⊢ ↑b * ↑b⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a⁻¹ * a = 1

Tactic:
rintro ⟨u, rfl⟩
  rw [← Units.val_inv_eq_inv_val, Units.inv_mul]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> f <$> y = (fun x ↦ x ∘ f) <$> x <*> y

Tactic:
simp only [← pure_seq]

Goal state after:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> (pure f <*> y) = (pure fun x ↦ x ∘ f) <*> x <*> y
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ f <$> (x <*> y) = (fun x ↦ f ∘ x) <$> x <*> y

Tactic:
simp only [← pure_seq]

Goal state after:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ pure f <*> (x <*> y) = (pure fun x ↦ f ∘ x) <*> x <*> y
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : ¬p x
⊢ p ((ofSubtype f) x) ↔ p x

Tactic:
by simp [h, ofSubtype_apply_of_not_mem f h]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(negOfNat n) = -↑n

Tactic:
simp [Int.cast_neg, negOfNat_eq]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (b + 1) = a * b + a

Tactic:
rw [mul_add, mul_one]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (1 + b) = a + a * b

Tactic:
rw [mul_add, mul_one]

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → IsLeftRegular a, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
isRightCancelMulZero_iff,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → IsLeftRegular a, ∀ {a : R}, a ≠ 0 → IsRightRegular a, IsCancelMulZero R].TFAE
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ b * a / a = b

Tactic:
mul_div_cancel_of_imp h

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ b = b
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ Int.negSucc z • a = -1 • ↑z.succ • a

Tactic:
by
    change (Int.negSucc z : R) • a = -1 • ((z.succ : ℤ) : R) • a
    simp [← smul_assoc]

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

Goal state before:
pp: case negSucc
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : M
a✝ : ℕ
⊢ ↑-[a✝+1] • b = -[a✝+1] • b

Tactic:
| negSucc =>

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

Goal state before:
pp: case negSucc
R✝ : Type u_1
S : Type u_2
M✝ : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M
a✝ : ℕ
⊢ (Int.negSucc a✝ • x) • y = Int.negSucc a✝ • x • y

Tactic:
| negSucc =>

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

Tactic:
← mul_inv_cancel_right b a,

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
← mul_inv_cancel_right b a,

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)

Tactic:
exact ha.add_odd hb.neg

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)

Tactic:
exact ha.add_odd hb.neg

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a

Tactic:
by rwa [← zero, lt]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a

Tactic:
by rwa [← zero, lt]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a

Tactic:
← mul_le_mul_iff_right b,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 * b ≤ a * b⁻¹ * b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b c d : α
inst✝ : MulRightMono α
⊢ d * (a * b⁻¹) ≤ d * (d⁻¹ * c) ↔ d * a ≤ c * b

Tactic:
← mul_le_mul_iff_right b,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b c d : α
inst✝ : MulRightMono α
⊢ d * (a * b⁻¹) * b ≤ d * (d⁻¹ * c) * b ↔ d * a ≤ c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b⁻¹ < c ↔ a < b * c

Tactic:
rw [← inv_mul_lt_iff_lt_mul, mul_comm]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
← mul_le_mul_iff_right b,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 * b ≤ a / b * b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
← mul_le_mul_iff_right b,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a / b * b ≤ 1 * b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
← mul_le_mul_iff_right b,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * b ≤ c / b * b ↔ a * b ≤ c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ a⁻¹ * (a * b⁻¹) ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b

Tactic:
inv_mul_cancel_left,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ b⁻¹ ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ b⁻¹ ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b

Tactic:
inv_mul_cancel_left,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ b⁻¹ ≤ c⁻¹ ↔ c ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b

Tactic:
inv_mul_cancel_left,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ b⁻¹ < a⁻¹ * (a * c⁻¹) ↔ c < b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ b⁻¹ < a⁻¹ * (a * c⁻¹) ↔ c < b

Tactic:
inv_mul_cancel_left,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ b⁻¹ < c⁻¹ ↔ c < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
m n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
· exact pow_le_pow_of_le_one a0 a1 mn

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * r ≤ a + b

Tactic:
by
  apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)
  rw [mul_mul_mul_comm, ← pow_two r, two_mul, two_add_two_eq_four]
  grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]

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

Goal state before:
pp: α : 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
h : r a b
⊢ s (f a) (f a)

Tactic:
by simpa [e] using H _ _ h

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

Goal state before:
pp: α : 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
h : r b a
⊢ s (f b) (f b)

Tactic:
by simpa [e] using H _ _ h

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
⊢ (x - a) * (x - b) < 0 ↔ a < x ∧ x < b

Tactic:
rw [mul_neg_iff, sub_pos, sub_pos, sub_neg, sub_neg, or_iff_left_iff_imp, and_comm]
  exact And.imp h.trans_lt h.trans_lt'

Goal state after: