mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  unfold SemiconjBy; rw [mul_assoc, inv_mul_cancel, mul_one]

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃ hx, q x hx

Tactic:
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
by
  rw [← not_exists]; exact em _

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b

Tactic:
by
  classical
  simp [Function.extend_def, hb]

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

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' (f₂₃ b)

Tactic:
Injective.extend_apply h₂₃

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
⊢ Injective fun g ↦ extend f g e'

Tactic:
intro g₁ g₂ hg
  refine funext fun x ↦ ?_
  have H := congr_fun hg (f x)
  simp only [hf.extend_apply] at H
  exact H

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b

Tactic:
apply curry_injective

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ curry (uncurry (update f a (update (f a) a' b))) = curry (update (uncurry f) (a, a') b)
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
⊢ (r ∘r fun x1 x2 ↦ x1 = f x2) = fun x1 x2 ↦ r x1 (f x2)

Tactic:
ext x y
  simp [Comp]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
⊢ (fun x1 x2 ↦ f x1 = x2) ∘r r = fun x ↦ r (f x)

Tactic:
ext x y
  simp [Comp]

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
intro a _ h
  induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩

Goal state after:
α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ ReflGen r = r

Tactic:
by
  ext x y
  simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ refl y

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction hab with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
ih : Join (ReflTransGen r) d c
⊢ Join (ReflTransGen r) e c

Tactic:
rcases ih with ⟨b, hdb, hcb⟩

Goal state after:
case tail
α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ Join (ReflTransGen r) e c
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) b c

Tactic:
induction hab 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:
rw [smul_iterate]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
exact Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
exact Iff.rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
a✝ b x a : α
⊢ a = x ↔ a ∈ {x}

Tactic:
exact Iff.rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ min a b ≤ c

Tactic:
by
      split_ifs with h
      · exact iff_of_true le_top (inf_le_of_right_le h)
      · rw [inf_le_iff, or_iff_left h]

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

Goal state before:
pp: α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ (sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩

Tactic:
by
  rw [Equiv.symm_apply_eq]; simp

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ c ∆ b

Tactic:
symmDiff_assoc,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = a ∆ (c ∆ b)
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_assoc,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ (c ∆ d)) = a ∆ (c ∆ (b ∆ d))
Module: Mathlib.Order.SymmDiff

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

Tactic:
bihimp_bihimp_cancel_left

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ b = b
Module: Mathlib.Data.Set.Image

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

Tactic:
rcases em (∃ b, f ⁻¹' {b} = univ) with ⟨b, hb⟩ | hf'
  · exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩
  · have : ∀ x b, f x ≠ b := fun x b ↦
      eq_empty_iff_forall_notMem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x
    exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩
  simp only [← and_and_left, mem_inter_iff, mem_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Tactic:
prod_eq_prod_iff,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = s₁ ∧ True ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t = ∅) ↔ s = s₁
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, ⟨f a, ⋯⟩ = ⟨x, hx⟩) ↔ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x

Tactic:
simp only [Subtype.mk.injEq, exists_prop, mem_ofPred_eq]

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔
    (↑(fst ⟨(p₁, p₂), he⟩)).1 = (↑(snd ⟨(p₁, p₂), he⟩)).1 ∧ (↑(fst ⟨(p₁, p₂), he⟩)).2 = (↑(snd ⟨(p₁, p₂), he⟩)).2

Tactic:
exact (and_iff_left he).symm

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (∃ i, ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
refine exists_congr fun i => ?_

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂ → f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i

Tactic:
rintro ⟨ht₁, ht₂⟩ i his
    by_cases p i <;> simp_all

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
⊢ y ∈ s₂ → f x ≠ f y

Tactic:
hy

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
⊢ f x ≠ f y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
⊢ y ∈ t₁ ∩ t₂ → y ∈ f '' (s₁ ∩ s₂)

Tactic:
hy

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
⊢ y ∈ f '' (s₁ ∩ s₂)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
⊢ y ∈ s → f y ∈ g ⁻¹' s

Tactic:
hy

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), True

Tactic:
implies_true

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (x₁ x₂ : G), True

Tactic:
implies_true

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℕ
x✝ : ↑(n + 1) ≠ 0
⊢ Injective fun a ↦ a ^ ↑(n + 1)

Tactic:
simpa [← Int.natCast_one, ← Int.natCast_add] using! pow_left_injective n.succ_ne_zero

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
⊢ y ∈ f ⁻¹' s → fa x = fa y → x = y

Tactic:
hy

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ fa x = fa y → x = y
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
simp only [mul_div_cancel_right]

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

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

Tactic:
by
  rw [← div_eq_one, H, div_eq_one]

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

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ (n + 1)) = (c f)^[n + 1]

Tactic:
by rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]

Goal state after:
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
⊢ a * d = c * b

Tactic:
rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x : { x // p x }
⊢ p (f (f⁻¹ ↑x))

Tactic:
simpa using x.2

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

Goal state before:
pp: x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
simp_rw [isLeftCancelMulZero_iff, isRightCancelMulZero_iff, isCancelMulZero_iff_forall_isRegular,
    isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul,
    isRegular_iff_eq_zero_of_mul]
  tfae_have 1 ↔ 2 := noZeroDivisors_iff_right_eq_zero_of_mul
  tfae_have 1 ↔ 3 := noZeroDivisors_iff_left_eq_zero_of_mul
  tfae_have 1 ↔ 4 := noZeroDivisors_iff_eq_zero_of_mul
  tfae_finish

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

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

Tactic:
or_iff_not_imp_right,

Goal state after:
α : Type u_3
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ ¬Subsingleton α → IsDomain α
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
by_cases hab : IsUnit (a * b)
  · obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
    rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
  obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
  · rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
  · rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑n • b = n • b

Tactic:
by
  cases n with
  | ofNat => simp [Nat.cast_smul_eq_nsmul]
  | negSucc => simp [add_smul, Nat.cast_smul_eq_nsmul]

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

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

Tactic:
rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : b < 1
⊢ a * b < a

Tactic:
simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : 1 < b
⊢ a < a * b

Tactic:
simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

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

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

Tactic:
exact pow_le_pow_of_le_one a0 a1 mn

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

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

Tactic:
by simpa only [pow_succ']
      using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_succ_nonneg ha _) (ha.trans hab)

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 : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ 1 < a ^ n ↔ 1 < a

Tactic:
simp only [← not_le, pow_le_one_iff_of_nonneg ha hn]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 - a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]
  gcongr

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
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) < b * c + (b * d + a * d)

Tactic:
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✝¹ : LinearOrder R
a b : R
inst✝ : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : LinearOrder R
a b : R
inst✝ : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]

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) ↔ x < a ∨ b < x

Tactic:
mul_pos_iff,

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b < a ↔ b < f a

Tactic:
← map_lt_map_iff f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ f (EquivLike.inv f b) < f a ↔ b < f a
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
mabs_of_one_le <| one_le_div'.mpr h

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ b / d ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a⁻¹

Tactic:
by simpa using inv_mabs_le a⁻¹

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

Goal state before:
pp: case ofNat
M : Type u_1
inst✝ : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1

Tactic:
obtain n | n := n

Goal state after:
case ofNat.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1

case ofNat.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case negSucc
M : Type u_1
inst✝ : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1

Tactic:
obtain n | n := n

Goal state after:
case negSucc.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1

case negSucc.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + -a = 0 → a ≠ ⊤

Tactic:
by contrapose; simp +contextual

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = max ↑a ↑b

Tactic:
simp_rw [max_def, val_le_val, ← apply_ite]

Goal state after:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = ↑(if a ≤ b then b else a)
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)

Tactic:
hb.tsub_add_eq_add_tsub hba,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a + (c - d) - b = a + c - (b + d)
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - min a b

Tactic:
rw [min_eq_right h]

Goal state after: