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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')

Tactic:
unfold SemiconjBy

Goal state after:
S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z

Tactic:
unfold SemiconjBy

Goal state after:
S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x : G
⊢ SemiconjBy a x (a * x * a⁻¹)

Tactic:
unfold SemiconjBy

Goal state after:
G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Tactic:
unfold SemiconjBy

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = b * (a * c)

Tactic:
hac,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = b * 1
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
by
  rw [← zpow_natCast]
  exact DivInvMonoid.zpow_neg' n a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ x, f x ≠ y

Tactic:
rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
⊢ ∃ x, f x ≠ y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : ReflTransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝

Tactic:
induction h using ReflTransGen.trans_induction_on with

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x : α
⊢ (fun x ↦ a • x)^[n] x = a ^ n • x

Tactic:
by
  rw [smul_iterate]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Tactic:
by
  rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
⊢ some b = Option.map f x ↔ ∃ a, x = some a ∧ f a = b

Tactic:
rw [eq_comm, map_eq_some_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (.left _ _ hij)
    · exact (total_of s a b).imp (.right _) (.right _)
    · exact Or.inr (.left _ _ hji)

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a

Tactic:
exact T.trichotomous b a

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ False

Tactic:
rw [e] at h

Goal state after:
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
by
  simp_rw [← le_bot_iff, inf_le_iff]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)

Tactic:
sup_inf_right,

Goal state after:
α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (x ⊔ z)
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ Subsingleton ↑s ↔ s.Subsingleton

Tactic:
by
  constructor
  · intro h a ha b hb
    exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)
  · exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial

Tactic:
simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
⊢ SemilatticeSup α

Tactic:
by
  let max := e.max
  let partialOrder := e.partialOrder
  apply e.injective.semilatticeSup <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ⊔ b \ c = a \ c

Tactic:
refine (sdiff_triangle ..).antisymm' <| sup_le ?_ <| by simpa [sup_comm]
  rw [← sdiff_inf_self_left (b := c)]
  exact sdiff_le_sdiff_left hinf

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ x ⊔ z = y

Tactic:
sup_inf_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ (y ⊔ z) ⊓ (x ⊔ z) = y
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: case inr
α : 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
ja : α
jb : β ja
ha : ia ≠ ja
⊢ f ⟨ja, jb⟩ = update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

pp: α : 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
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ⟨ja, jb⟩.fst ≠ ⟨ia, ib⟩.fst

Tactic:
Function.update_of_ne

Goal state after:
case inr
α : 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
ja : α
jb : β ja
ha : ia ≠ ja
⊢ f ⟨ja, jb⟩ = f ⟨ja, jb⟩

case inr.h
α : 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
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ja ≠ ⟨ia, ib⟩.fst

α : 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
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ⟨ja, jb⟩.fst ≠ ⟨ia, ib⟩.fst
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_inf_right,

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

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

Tactic:
sup_inf_right,

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

Goal state before:
pp: α' : Type u_9
β' : Type u_10
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
e e' : Perm α'
⊢ Equiv.trans (e.extendDomain f) (e'.extendDomain f) = extendDomain (Equiv.trans e e') f

Tactic:
by
  simp [Perm.extendDomain, permCongr_trans]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : 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
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⊔ f aᶜ = f ⊤

Tactic:
by
    rw [map_compl, sup_compl_eq_top, map_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
by
  classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

Goal state after:
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:
hg heq

Goal state after:
α : 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 y = f y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (Prod.map (fun x ↦ ↑x) fun x ↦ ↑x) ⁻¹' diagonal α = diagonal ↑s

Tactic:
ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩

Goal state after:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (⟨x, hx⟩, ⟨y, hy⟩) ∈ (Prod.map (fun x ↦ ↑x) fun x ↦ ↑x) ⁻¹' diagonal α ↔ (⟨x, hx⟩, ⟨y, hy⟩) ∈ diagonal ↑s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
apply Set.preimage_subset_preimage_iff
  rw [hf.range_eq]
  apply subset_univ

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ g 1 = 1

Tactic:
rw [← f.map_one, h₁]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n

Tactic:
by simp_rw [zpow_natCast, mul_pow]

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

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

Tactic:
by rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
⊢ IsUnit a → IsUnit b → IsUnit (a * b)

Tactic:
rintro ⟨x, rfl⟩ ⟨y, rfl⟩

Goal state after:
M : Type u_1
inst✝ : Monoid M
x y : Mˣ
⊢ IsUnit (↑x * ↑y)
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

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

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

Tactic:
by rw [mul_neg, mul_one]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)

Tactic:
unfold SemiconjBy

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / a = 1 → a ≠ 0

Tactic:
contrapose!; simp +contextual

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

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

Tactic:
by rw [mul_add, ← two_mul, add_assoc]

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 (flip mu) r ↔ Covariant N N mu r

Tactic:
unfold flip

Goal state after:
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
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 (flip mu) r ↔ Contravariant N N mu r

Tactic:
unfold flip

Goal state after:
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
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * a + ↑u⁻¹ * a

Tactic:
by rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]

Goal state after:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f b c) = f b (f a c)

Tactic:
by rw [← ha.assoc, hc.comm a, ha.assoc]

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

Goal state before:
pp: case inl
k : ℕ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
· use k
    grind

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

Goal state before:
pp: case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
· use k
    grind

Goal state after:
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 / b ≤ a / c ↔ c ≤ b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a b : M₀
inst✝ : MulPosMono M₀
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b

Tactic:
exact lt_of_pow_lt_pow_left₀ _ 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✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a / c ≤ b / c

Tactic:
by
  rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  gcongr; exact Right.inv_nonneg.2 hc

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✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 4 * a * b = 2 * a * b + 2 * a * b

Tactic:
rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]

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

Goal state before:
pp: case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)

Tactic:
· exact RelHomClass.wellFounded (Quotient.mkRelHom H)

Goal state after:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)
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:
by
  rw [mul_nonpos_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos, or_iff_left_iff_imp, and_comm]
  exact And.imp h.trans h.trans'

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
s : β → β → Prop
a : α
h : ¬r a a
⊢ ∀ {a_1 b : β}, Prod.Lex r s ({ toFun := Prod.mk a, inj' := ⋯ } a_1) ({ toFun := Prod.mk a, inj' := ⋯ } b) ↔ s a_1 b

Tactic:
by simp [Prod.lex_def, 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
r : α → α → Prop
b : β
h : ¬s b b
⊢ ∀ {a b_1 : α},
    Prod.Lex r s ({ toFun := fun a ↦ (a, b), inj' := ⋯ } a) ({ toFun := fun a ↦ (a, b), inj' := ⋯ } b_1) ↔ r a b_1

Tactic:
by simp [Prod.lex_def, h]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f a ⊓ f b ≤ ⊥

Tactic:
← f.map_inf,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (b * a) = b ^ (n + 1) * a

Tactic:
by rw [← mul_assoc, ← pow_succ]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ |a / b|ₘ < n

Tactic:
mabs_div_lt_iff,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ a / b < n ∧ b / a < n
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
· use k
    grind

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

Goal state before:
pp: case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
· use k
    grind

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

Goal state before:
pp: case zero
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
b : ℕ
eq : n = q * b
⊢ ∃ a b, a * 0 + b * q = n

Tactic:
exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : MulZeroOneClass G
inst✝ : MulZeroOneClass H
f g : G ≃* H
⊢ f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g

Tactic:
by
  simp [MonoidWithZeroHom.ext_iff, MulEquiv.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ (fun n ↦ recZeroCoe 0 Units.val n) ((fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) x✝) = x✝

Tactic:
simp only; split <;> simp_all

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rw [floor_lt ha]
    exact h.trans_le (le_ceil _)

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : c * a = c * b
⊢ a = b

Tactic:
by simpa using congr_arg (⅟c * ·) h

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1 + 1) + b ^ (n + 1) * a + (b ^ (n + 1 + 1) + a ^ (n + 1) * b)) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Tactic:
add_add_add_comm,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1 + 1) + b ^ (n + 1 + 1) + (b ^ (n + 1) * a + a ^ (n + 1) * b)) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
← map_dvd_iff f,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h : f a ∣ f (b * c)
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ EquivLike.inv f a₁ ∣ b ∧ EquivLike.inv f a₂ ∣ c ∧ a = EquivLike.inv f a₁ * EquivLike.inv f a₂

Tactic:
← map_dvd_iff f,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ f (EquivLike.inv f a₁) ∣ f b ∧ f (EquivLike.inv f a₂) ∣ f c ∧ a = EquivLike.inv f a₁ * EquivLike.inv f a₂
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y

Tactic:
convert dvd_add (hxy.mul_left a) (hab.mul_right y)
  rw [mul_sub_left_distrib, mul_sub_right_distrib]
  simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]

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

Goal state before:
pp: u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩

Goal state after:
u : ℤ
h : u = 1 ∨ u = -1
⊢ IsUnit u
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl
⊢ IsUnit 1

pp: case inr
⊢ IsUnit (-1)

Tactic:
· exact isUnit_one

Goal state after:
case inr
⊢ IsUnit (-1)