mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.AdaptationNote

Goal state before:
pp: ⊢ True

Tactic:
#adaptation_note /-- This is a test -/
  trivial

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1) * a = a * (a ^ n * a)

Tactic:
pow_succ',

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a * a ^ n * a = a * (a ^ n * a)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * (a * a)

Tactic:
pow_succ',

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a * a ^ 2 = a * (a * a)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ a'₂ : α
ha' : a'₁ = a'₂
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₂ v₂ a₂

Tactic:
subst ha'

Goal state after:
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₂ a₂
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝¹ i✝ : α
hab : TransGen r i✝¹ i✝
⊢ (TransGen p on f) i✝¹ i✝

Tactic:
simpa [transGen_eq_self] using hab.lift f h

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ r • s • x = s • r • x

Tactic:
by
    rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
pow_succ',

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ r • x * (r • x) ^ n = r ^ (n + 1) • x ^ (n + 1)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
⊢ Function.Injective (mk a)

Tactic:
intro b₁

Goal state after:
α : Type u_5
β : Type u_6
a : α
b₁ : β
⊢ ∀ ⦃a₂ : β⦄, (a, b₁) = (a, a₂) → b₁ = a₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
⊢ Function.Injective fun a ↦ (a, b)

Tactic:
intro b₁

Goal state after:
α : Type u_5
β : Type u_6
b : β
b₁ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) a₂ → b₁ = a₂
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
c : α
h : c < a
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a

Tactic:
by
    classical
    obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
    exact ⟨_, update_lt_self_iff.2 hb⟩

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬(a ≤ b ∧ ¬b ≤ a) ↔ ¬a ≤ b ∨ b ≤ a
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
⊢ p (min a b)

Tactic:
obtain hab | hba := le_total a b <;> simp [min_eq_left, min_eq_right, *]

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (β i)
inst✝ : Preorder α
f : α → (i : ι) → β i
⊢ Monotone f ↔ ∀ (i : ι), Monotone fun x ↦ f x i

Tactic:
simp [Monotone, Pi.le_def, @forall_comm ι]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a ≤ f b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x

Tactic:
rintro rfl
  exact (hf.reflect_lt h2).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h1)

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

Goal state before:
pp: x : Prop
⊢ x = True ∨ x = False

Tactic:
exact Classical.propComplete x

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

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

Tactic:
rw [sup_sdiff, sdiff_self, sup_bot_eq]

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
⊢ Functor.map ⇑(Equiv.refl α) = id

Tactic:
ext
    apply LawfulFunctor.id_map

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
removeNone_some _ ⟨a, h⟩

Goal state after:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ e (some x) = e none ↔ e.symm none = some x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by
          rw [inf_sup_left, inf_sup_right]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z

Tactic:
← sup_sdiff_cancel_right hxz

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
⊢ subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε

Tactic:
by
  ext x
  by_cases h : p x <;> simp [h]

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

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
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h_1 : p a then x₀ ⟨↑⟨a, h⟩, h_1⟩ else x ⟨↑⟨a, h⟩, h_1⟩) = x ⟨a, h⟩

Tactic:
dsimp only
        rw [dif_neg h]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b

Tactic:
← compl_inf,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : g x = g y
⊢ f x = f y

Tactic:
rw [hg heq]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise f g x ∈ f '' s

Tactic:
use x

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = s.piecewise f g x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise f g x ∈ g '' sᶜ

Tactic:
use x

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = s.piecewise f g x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mpr.inl
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ f x ∈ range (s.piecewise f g)

Tactic:
use x

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ s.piecewise f g x = f x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mpr.inr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ g x ∈ range (s.piecewise f g)

Tactic:
use x

Goal state after:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ s.piecewise f g x = g x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
⊢ range Function.diag = diagonal α

Tactic:
by
  ext ⟨x, y⟩
  simp [diagonal, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h ⟨a, b⟩ = ⟨x, hx⟩) ↔ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x

Tactic:
Subtype.map

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, ⟨f a, ⋯⟩ = ⟨x, hx⟩) ↔ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ f ⁻¹' g ⁻¹' s = s

Tactic:
rw [← preimage_comp, h.comp_eq_id, preimage_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ InjOn Prod.fst (graphOn f s)

Tactic:
by aesop (add simp InjOn)

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ (x : α), x ∈ Prod.fst '' s → (x, f x) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
rw [forall_mem_image] at hf

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: R : Type u_10
S : Type u_11
F : Type u_12
inst✝³ : One R
inst✝² : One S
inst✝¹ : FunLike F R S
inst✝ : OneHomClass F R S
f : F
x : R
hx : f x ≠ 1
⊢ f x ≠ f 1

Tactic:
(map_one f)

Goal state after:
R : Type u_10
S : Type u_11
F : Type u_12
inst✝³ : One R
inst✝² : One S
inst✝¹ : FunLike F R S
inst✝ : OneHomClass F R S
f : F
x : R
hx : f x ≠ 1
⊢ f x ≠ 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ t ⊆ f₂ '' s

Tactic:
← H.image_eq

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ t ⊆ f₁ '' s
Module: Mathlib.Data.Int.Init

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

Tactic:
suffices ∀ n : ℕ, motive (-n) from this (i + 1)

Goal state after:
case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i : ℕ
⊢ ∀ (n : ℕ), motive (-↑n)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
pow_succ',

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ a * b * (a * b) ^ n = a ^ (n + 1) * b ^ (n + 1)

Tactic:
pow_succ',

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ a * b * (a * b) ^ n = a * a ^ n * b ^ (n + 1)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ a * b * (a * b) ^ n = a * a ^ n * b ^ (n + 1)

Tactic:
pow_succ',

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ a * b * (a * b) ^ n = a * a ^ n * (b * b ^ n)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹

Tactic:
pow_succ',

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ * a⁻¹ ^ n = (a ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ ^ x✝¹.succ = unop (op (unop x✝ ^ ↑x✝¹) * x✝)

Tactic:
pow_succ',

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop (op (unop x✝ ^ ↑x✝¹) * x✝)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1 + 1))⁻¹ * a

Tactic:
pow_succ',

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a * a ^ (n + 1))⁻¹ * a
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
div_mul_eq_mul_div,

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

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

Tactic:
div_mul_eq_mul_div,

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = b⁻¹

Tactic:
rw [mul_comm, h.div_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
not_iff_comm

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
not_iff_comm

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
not_iff_comm

Goal state after:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ c / d * b * d = c * b

Tactic:
div_mul_eq_mul_div,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ c * b / d * d = c * b
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
pow_succ',

Goal state after:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x * x ^ n * y) = f x ^ (n + 1) * f y
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x * x ^ n * y) = f x ^ (n + 1) * f y

Tactic:
pow_succ',

Goal state after:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x * x ^ n * y) = f x * f x ^ n * f y
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
⊢ (∀ (x : α), p (f (f⁻¹ x)) ↔ p (f⁻¹ x)) ↔ ∀ (x : α), p (f⁻¹ x) ↔ p x

Tactic:
simp [Iff.comm]

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

Goal state before:
pp: case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm ⋯

Tactic:
pow_succ',

Goal state after:
case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf * f.subtypePerm hf ^ n = (f * f ^ n).subtypePerm ⋯
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ x = 0

Tactic:
← one_smul R x,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ 1 • x = 0
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M✝ : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
hf : ∀ (x y : M), Commute (f x) (f y)
x y : M
⊢ (op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y

Tactic:
by simp [(hf x y).eq]

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M✝ : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : ∀ (x y : M), Commute (f x) (f y)
x y : M
⊢ (op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y

Tactic:
by simp [(hf x y).eq]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ

Tactic:
pow_succ',

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ (n + 1))⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ c / d * b * d = c * b

Tactic:
div_mul_eq_mul_div,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ c * b / d * d = c * b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = c * (b / d)

Tactic:
div_mul_eq_mul_div,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c * b / d ↔ a = c * (b / d)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
div_mul_eq_mul_div,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ 1 * a / (a * b) = 1 / b
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c

Tactic:
by simpa using mul_le_mul_right bc a⁻¹

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
a b c : α
bc : b * a ≤ c * a
⊢ b ≤ c

Tactic:
by simpa using mul_le_mul_right bc a⁻¹

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ b, b < a

Tactic:
exact fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) < b ^ (n + 2)

Tactic:
by
    simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
      (pow_le_pow_left₀ ha hab.le _) hab ha (pow_succ_pos (ha.trans_lt hab) _)

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
m : ℕ
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
hm : 1 < m
⊢ a < a ^ m

Tactic:
simpa only [pow_one] using pow_lt_pow_right₀ h hm

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hb : b ≤ 0
h : a ≤ 1
⊢ b ≤ a * b

Tactic:
by
  simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hb : b ≤ 0
h : 1 ≤ a
⊢ a * b ≤ b

Tactic:
by
  simpa only [one_mul] using mul_le_mul_of_nonpos_right h 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✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
⊢ 0 ≤ a * a

Tactic:
by simpa only [sq] using sq_nonneg a

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
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔
      Sum.LiftRel r t a b

Tactic:
rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]

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
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔ Sum.Lex r t a b

Tactic:
rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]

Goal state after: