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

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝ : ReflTransGen r b b✝
hcd : r b✝ c✝
hac : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝

Tactic:
| tail _ hcd hac =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
b✝ c✝ : α
a✝ : ReflTransGen r b b✝
hcd : r b✝ c✝
hac : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝

Tactic:
| tail _ hcd hac =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| tail _ hcd hac =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
| tail _ hcd hac =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b b✝ c✝ : α
a✝ : TransGen r a b✝
hcd : r b✝ c✝
hac : r a b✝
⊢ r a c✝

Tactic:
| tail _ hcd hac =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ b✝ c✝ : α
a✝ : TransGen r a b✝
hcd : r b✝ c✝
hac : (TransGen p on f) a b✝
⊢ (TransGen p on f) a c✝

Tactic:
| tail _ hcd hac =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ gb' (f (ga (ga' x))) = gb' (f x)

Tactic:
ha x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ gb' (f x) = gb' (f x)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ min a b

Tactic:
by
  rw [min_def]
  split_ifs <;> assumption

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ (a ≤ b ∧ ∃ i, a i < b i) → ∃ a_2, (a ≤ a_2 ∧ ∃ i, a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ i, a_2 i < b i

Tactic:
rintro ⟨hab, i, hi⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : x = ⊤
⊢ ¬P x

pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x

Tactic:
· exact hx ▸ hexists

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑a ⊓ ↑b = ⊥

Tactic:
← Subtype.coe_inf Pinf,

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑(a ⊓ b) = ⊥
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeSup α

Tactic:
apply e.injective.semilatticeSup <;> intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ b ≤ a ⇨ c

Tactic:
le_himp_iff'

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ a ⊓ b ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ a ⇨ b ↔ a ≤ b

Tactic:
by rw [le_himp_iff, inf_idem]

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

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ {b} \ {a} = {b}

Tactic:
sdiff_singleton_eq_self (by simpa)

Goal state after:
α : Type u_1
a b : α
hab : a ≠ b
⊢ {b} = {b}
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: case inl
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
jb : β ia
⊢ update f ⟨ia, ib⟩ x ⟨ia, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ia jb

Tactic:
simp
    grind

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

Goal state before:
pp: α : 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)

Tactic:
inf_sdiff_sup_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]

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

Goal state before:
pp: α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

Tactic:
ext i
  cases i <;> rfl

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

Goal state before:
pp: α : Type u_9
β : Type u_10
⊢ (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)

Tactic:
ext i
  cases i <;> rfl

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)

Tactic:
exact ⟨sdiff_sdiff_sdiff_le_sdiff,
    (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩

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

Goal state before:
pp: case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ (swap i j) a ∈ insert j s \ {i}

Tactic:
swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)

Goal state after:
case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)) (a, b) =
    ((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm) (a, b)

Tactic:
simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]

Goal state after:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ⟨((sigmaEquivProd α₁ β₁).symm (a, b)).fst,
      (e ((sigmaEquivProd α₁ β₁).symm (a, b)).fst) ((sigmaEquivProd α₁ β₁).symm (a, b)).snd⟩ =
    (sigmaEquivProd α₁ β₂).symm (a, (e a) b)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Tactic:
simp_rw [← bihimp_assoc, bihimp_comm]

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

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
⊢ RightInverse (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
    Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst

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

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.18
β : Type ?u.17
γ : Type ?u.15
fst✝ : α
snd✝ : γ
⊢ (fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst)
      ((fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inl (fst✝, snd✝))) =
    inl (fst✝, snd✝)

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
fst✝ : β
snd✝ : γ
⊢ (fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst)
      ((fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inr (fst✝, snd✝))) =
    inr (fst✝, snd✝)
Module: Mathlib.Logic.Equiv.Prod

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
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g)) = (f, g)

Tactic:
ext1

Goal state after:
case fst
α✝ : 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
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).fst =
    (f, g).fst

case snd
α✝ : 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
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).snd =
    (f, g).snd
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ compl ∘ compl '' s = s

Tactic:
compl_comp_compl,

Goal state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ id '' s = s
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).domRestrict (extend f g g') = fun x ↦ g (Exists.choose ⋯)

Tactic:
classical
  exact domRestrict_dite _ _

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

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

Tactic:
simp [h, prod_eq_empty_iff.1 h]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
h : IsEmpty α
⊢ ∃ a, const α a = f

Tactic:
exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
this : ∀ (i : ι), ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)
⊢ b ∈ Pi.map f '' s.pi t

Tactic:
choose a hab hat using this

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
a : (i : ι) → α i
hab : ∀ (i : ι), f i (a i) = b i
hat : ∀ (i : ι), i ∈ s → a i ∈ t i
⊢ b ∈ Pi.map f '' s.pi t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ ∀ (i_1 : ι), y i_1 ∈ update (fun j ↦ {x j}) i s i_1

Tactic:
rw [forall_update_iff (p := fun x s => y x ∈ s)]

Goal state after:
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → y x_1 ∈ {x x_1}
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ f ⁻¹' f '' s₂ ∩ s = s₂

Tactic:
h.preimage_image_inter hs₂

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ s₂ = s₂
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : α × β
⊢ x ∈ graphOn f s ↔ x.1 ∈ s ∧ f x.1 = x.2

Tactic:
aesop (add simp graphOn)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Tactic:
refine (bijOn_singleton.mpr rfl).union h ?_

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ InjOn f ({a} ∪ s)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ -a.pred = (-a).succ

Tactic:
by
  rw [← Int.neg_eq_comm.mp (neg_succ (-a)), Int.neg_neg]

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

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy (op (unop a)) (op (unop x)) y

Tactic:
← op_unop y,

Goal state after:
α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy (op (unop a)) (op (unop x)) (op (unop y))
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
div_eq_inv_mul,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (a * b) = b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ ↑{ val := NPow.npow (n + 1) ↑a, inv := NPow.npow (n + 1) ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } =
    ↑({ val := NPow.npow n ↑a, inv := NPow.npow n ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } * a)

Tactic:
simp [pow_succ]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ NPow.npow n.succ a = NPow.npow n a * a

Tactic:
simp [pow_succ]

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

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

Tactic:
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
    hd.div_mul_cancel]

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

Goal state before:
pp: case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ a * b = 1

Tactic:
conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ ↑(n + 1))⁻¹ = (a ^ (↑(n + 1) + 1))⁻¹ * a

Tactic:
← Int.natCast_succ,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ ↑(n + 1))⁻¹ = (a ^ ↑(n + 1).succ)⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a ^ 2 * b / a = a * b

Tactic:
rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]

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
⊢ (1 + 1) • x = x + x

Tactic:
add_smul,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 1 • x + 1 • x = x + x
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
x✝ : ℕ
ih : ∀ (n : ℤ), ↑(↑x✝ * n) = ↑x✝ • ↑n
⊢ ∀ (n : ℤ), ↑((↑x✝ + 1) * n) = (↑x✝ + 1) • ↑n

Tactic:
simp [add_mul, add_zsmul, ih]

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

Goal state before:
pp: α : Type u_3
inst✝ : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.refine
   "refine"
   (Term.anonymousCtor
    "⟨"
    [(Term.fun "fun" (Term.basicFun [`t] [] "↦" (Term.syntheticHole "?" "_")))
     ","
     (Term.fun
      "fun"
      (Term.basicFun
       [`h]
       []
       "↦"
       (Term.app
        `h.elim
        [(Term.paren
          (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
          (Term.fun "fun" (Term.basicFun [(Term.hole "_")] [] "↦" `inferInstance))
          ")")
         (Term.paren
          (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
          (Term.fun "fun" (Term.basicFun [(Term.hole "_")] [] "↦" `inferInstance))
          ")")])))]
    "⟩"))
  []
  (Tactic.rwSeq
   "rw"
   (Tactic.optConfig [])
   (Tactic.rwRuleSeq
    "["
    [(Tactic.rwRule [] `or_iff_not_imp_right) "," (Tactic.rwRule [] `not_subsingleton_iff_nontrivial)]
    "]")
   [])
  []
  (Tactic.exact
   "exact"
   (Term.fun
    "fun"
    (Term.basicFun
     [(Term.hole "_")]
     []
     "↦"
     (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 0 = 1 ↔ f 1 = 0

Tactic:
map_one,

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 0 = 1 ↔ 1 = 0
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
by simp [h.pow_right n]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ n = (-1) ^ (n % 2)

Tactic:
by
  rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ (↑n + 1) • b = (n + 1) • b

Tactic:
add_smul,

Goal state after:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑n • b + 1 • b = (n + 1) • b
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑n • b + 1 • b = (n + 1) • b

Tactic:
add_smul,

Goal state after:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑n • b + 1 • b = n • b + 1 • b
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
rw [two_mul, two_mul]

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ a + b - (a + c) = b - c

Tactic:
add_comm a b,

Goal state after:
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ b + a - (a + c) = b - c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a

Tactic:
use 1
    rwa [mul_one]

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
⊢ ∃ a, 1 < a

Tactic:
obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)

Goal state after:
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
⊢ ∃ a, 1 < a
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
a : α
n : ℕ
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
simp [pow_succ]

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
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b ^ 2 + a * (a + b) = a ^ 2 + (a + b) * b

Tactic:
by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
⊢ 0 < a

Tactic:
by_cases! ha : 0 < a
  · exact ha
  · grind [mul_le_mul_of_nonpos_left hbc ha]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < c⁻¹ * b ↔ a * c < b

Tactic:
by
  rw [lt_inv_mul_iff₀ hc, mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
rwa [Int.cast_natCast]

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

Goal state before:
pp: case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
rw [eq_one_of_inv_eq' h.symm] at ha

Goal state after:
case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ↔ 1 ≤ a

Tactic:
mabs_eq_max_inv,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ max a a⁻¹ = a ↔ 1 ≤ a