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 ↦ a * x) b = (fun x ↦ a * x) c
⊢ a⁻¹ * (a * b) = c

Tactic:
show a * b = a * c from h,

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ∃ x, ¬f x = g x
⊢ Nontrivial β

Tactic:
obtain ⟨a, h⟩ := h

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
a : α
h : ¬f a = g a
⊢ Nontrivial β
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ (¬a ∨ ¬b) ∨ b ∧ (¬a ∨ ¬b)

Tactic:
and_or_left,

Goal state after:
a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∧ ¬a ∨ a ∧ ¬b) ∨ b ∧ (¬a ∨ ¬b)
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ (¬a ∨ ¬b)

Tactic:
and_or_left,

Goal state after:
a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ b ∧ ¬b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hp : P

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hp : P

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
exact h.mono (fun _ _ ↦ .single) x y

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧

Tactic:
rw [Quotient.out_eq y]

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

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

Tactic:
by rw [iterate_succ_apply, h, ihn]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_sum, not_or]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b

Tactic:
by
  cases h : compare a b
  · simpa using le_of_lt <| compare_lt_iff_lt.1 h
  · simpa using le_of_eq <| compare_eq_iff_eq.1 h
  · simpa using compare_gt_iff_gt.1 h

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f b c) a ≤ f (f a b) c

Tactic:
comm.comm b,

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f (f a b) c
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]

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

Goal state before:
pp: α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤

Tactic:
cases PartialOrder.ext H
  apply top_unique
  exact @le_top _ _ A _

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

Goal state before:
pp: α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Bijective (rangeFactorization f) ↔ Function.Injective f

Tactic:
by simp [Function.Bijective]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

Tactic:
by_cases h : a < b <;> by_cases h₂ : b < a

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
h₂ : b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
h₂ : ¬b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
h₂ : b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
h₂ : ¬b < a
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq
Module: Mathlib.Tactic.Lift

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
⊢ ∃ g, (fun i ↦ g i.val) = f

Tactic:
by
  haveI : DecidablePred p := fun i ↦ Classical.propDecidable (p i)
  exact ⟨fun i => if hi : p i then f ⟨i, hi⟩ else Classical.choice (ne i),
    funext fun i ↦ dif_pos i.2⟩

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z

Tactic:
rw [disjoint_iff]
  exact h.inf_left_eq_bot_iff

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x' ⊔ (x ⊔ y') = ⊤

Tactic:
sup_left_comm,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ (x' ⊔ y') = ⊤
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
@sup_le_iff α A,

Goal state after:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
by
    rw [← le, map_inf, map_sup, map_sup, map_sup, map_inf]
    exact le_sup_inf

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊔ c ≤ a ⇨ b ⊓ a ⊔ c ⊓ a

Tactic:
sup_le_iff,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ≤ a ⇨ b ⊓ a ⊔ c ⊓ a ∧ c ≤ a ⇨ b ⊓ a ⊔ c ⊓ a
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_left_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a \ c ⊔ (b ⊔ c \ b)
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_left_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c)
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_left_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a \ b ⊔ (c ⊔ b \ c)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ z ⊔ x ≤ z ⊔ x

Tactic:
by rw [sup_assoc, sup_comm, sup_assoc, sup_idem]

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 : α ≃ { y // y ≠ x }
a : Option α
⊢ (fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) ((fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) a) = a

Tactic:
cases a with
          | none => simp
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ⊔ xᶜ ≤ z ↔ y ≤ z ∧ Codisjoint x z

Tactic:
sup_le_iff,

Goal state after:
α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ≤ z ∧ xᶜ ≤ z ↔ y ≤ z ∧ Codisjoint x z
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Tactic:
sup_le_iff,

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

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

Tactic:
{ rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff] }

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ ((piCongrRight h₂).trans (piCongrLeft Z h₁)) f (h₁ a) = (h₂ a) (f a)

Tactic:
trans_apply,

Goal state after:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (piCongrLeft Z h₁) ((piCongrRight h₂) f) (h₁ a) = (h₂ a) (f a)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)

Tactic:
simp [piCongr', piCongr_apply_apply]

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁

Tactic:
have := image_mono (f := Prod.snd) H
    rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
by_cases h : i = j

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl = {x | x.isLeft = true}

Tactic:
by ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inr = {x | x.isRight = true}

Tactic:
by ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
by
  intro i ht
  by_cases hs : i ∈ s <;> simp [hf i ht, hg i ht, hs]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
i : α
s : Set (β i)
⊢ Sigma.mk i ⁻¹' Sigma.mk i '' s = s

Tactic:
simp [image]

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

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

Tactic:
pred_succ

Goal state after:
a : ℤ
⊢ -a = -a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
this : ¬x ∈ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
simp only [mem_preimage, invFun_neg hx, h, this]

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

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

Tactic:
by rw [← Units.val_one, val_inj]

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

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x : M
hx : IsUnit (f x)
⊢ IsUnit x

Tactic:
simpa using hx.map <| MonoidHom.mk ⟨EquivLike.inv f, EquivLike.injective f <| by simp⟩
      fun x y ↦ EquivLike.injective f <| by simp

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
⊢ f (x * x⁻¹) = f 1

Tactic:
rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ n * b = 0

Tactic:
rw [show n = n - m + m by lia, pow_add, mul_assoc, h]

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m) * 0 = 0
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 * (1 / a))

Tactic:
by rw [neg_mul_eq_mul_neg]

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
⊢ -1 * (b / a) = -(b / a)

Tactic:
← neg_eq_neg_one_mul

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b / a) = -(b / a)
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a - b /ₚ u = (a * ↑u - b) /ₚ u

Tactic:
by
  simp only [divp, sub_mul, Units.mul_inv_cancel_right]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
← (Commute.one_right a).mul_self_sub_mul_self_eq,

Goal state after:
R : Type u
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = a * a - 1 * 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
rintro ⟨c, rfl⟩ a
  simp_rw [← two_mul, pow_mul, neg_sq]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (fun b a ↦ mu a b) r ↔ Covariant N N mu r

Tactic:
h.comm

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (fun b a ↦ mu a b) r ↔ Contravariant N N mu r

Tactic:
h.comm

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n

Tactic:
by
  rintro ⟨c, rfl⟩ a; simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : -1 ≠ 1
⊢ (-1) ^ n = 1 ↔ Even n

Tactic:
simp [neg_one_pow_eq_ite, h]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : IsMulCommutative α
⊢ PosMulReflectLT α ↔ MulPosReflectLT α

Tactic:
simp [posMulReflectLT_iff, mulPosReflectLT_iff, mul_comm']

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

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

Tactic:
div_le_iff_le_mul,

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a / c < b ↔ a < b * c

Tactic:
rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
⊢ a * c < b * c

Tactic:
by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
  refine (add_lt_add_iff_right (b * d + a * d)).1 ?_
  calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
a b : R
ha : a < 0
hb : b < 0
⊢ 0 < a * b

Tactic:
by
  simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb

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₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (-↑(n + 1))

Tactic:
by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos 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₀
ha₀ : 0 < a
ha₁ : a ≤ 1
⊢ Antitone fun n ↦ a ^ n

Tactic:
by
  refine antitone_int_of_succ_le fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

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

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

Tactic:
sub_nonneg,

Goal state after:
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
⊢ a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
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
⊢ a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x

Tactic:
sub_nonneg,

Goal state after:
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
⊢ a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
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₀
hb : 0 < b
hc : 0 < c
⊢ a / b < c ↔ a / c < b

Tactic:
rw [div_lt_iff₀ hb, div_lt_iff₀' hc]

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

Goal state before:
pp: case refine_1.a
α : 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
⊢ ¬r b a

Tactic:
exact fun h => irrefl (r := s) (f b) (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
⊢ 0 ≤ x - a ∧ x - b ≤ 0 ∨ x - a ≤ 0 ∧ 0 ≤ x - b ↔ a ≤ x ∧ x ≤ b

Tactic:
sub_nonneg,

Goal state after:
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
⊢ a ≤ x ∧ x - b ≤ 0 ∨ x - a ≤ 0 ∧ 0 ≤ x - b ↔ a ≤ x ∧ x ≤ b
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
⊢ a ≤ x ∧ x - b ≤ 0 ∨ x - a ≤ 0 ∧ 0 ≤ x - b ↔ a ≤ x ∧ x ≤ b

Tactic:
sub_nonneg,

Goal state after:
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
⊢ a ≤ x ∧ x - b ≤ 0 ∨ x - a ≤ 0 ∧ b ≤ x ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
⊢ DenselyOrdered Y

Tactic:
refine ⟨fun a b h ↦ ?_⟩

Goal state after:
case mp
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
⊢ DenselyOrdered X

Tactic:
refine ⟨fun a b h ↦ ?_⟩

Goal state after:
case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b