mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false

Tactic:
cases n <;> cases b <;> simp [bit, Nat.two_mul, ← Nat.add_assoc]

Goal state after:
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'
⊢ y * (y' * a) = y * y' * a

Tactic:
← mul_assoc

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'
⊢ y * y' * a = y * y' * a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ IsCancelMul R ↔ ∀ (r : R), IsRegular r

Tactic:
rw [isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, ← forall_and]
  exact forall_congr' fun _ ↦ isRegular_iff.symm

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * (npowRec' k.succ m * m)

Tactic:
← mul_assoc

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
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
⊢ b = c

Tactic:
by
    rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y

Tactic:
← hx',

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ f x' = y
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

Tactic:
by
  simp +contextual [update_le_iff]

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

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 2 * k ^ 2 = (2 * k) ^ 2

Tactic:
Nat.mul_pow,

Goal state after:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 2 * k ^ 2 = 2 ^ 2 * k ^ 2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
⊢ leRec (le_succ_of_le ⋯ refl) (fun x h ih ↦ le_succ_of_le ⋯ ih) h2 = leRec refl le_succ_of_le h1

Tactic:
rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']

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

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
⊢ n - 1 ≠ 0

Tactic:
have := prop (n := n); lia

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Tactic:
· intro h x hf hg i
    apply h i (hf i) (hg i)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ a ⊓ b ≤ c

Tactic:
by rwa [inf_comm]

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

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∀ (n : ℤ), (casesOn n f fun n ↦ g (n + 1)) < casesOn (n + 1) f fun n ↦ g (n + 1)

Tactic:
rintro (n | _ | n)

Goal state after:
case ofNat
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn (ofNat n) f fun n ↦ g (n + 1)) < casesOn (ofNat n + 1) f fun n ↦ g (n + 1)

case negSucc.zero
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (casesOn -[0+1] f fun n ↦ g (n + 1)) < casesOn (-[0+1] + 1) f fun n ↦ g (n + 1)

case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ h, x ∈ t h

Tactic:
exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
a₁ : α
b₁ b₂ : β a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

Tactic:
exact congr_arg (mk a₁) <| Subsingleton.elim _ _

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

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

Tactic:
sup_inf_inf_sdiff,

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

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

Tactic:
rw [sdiff_sdiff_right', inf_eq_right.2 h]

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

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

Tactic:
sup_inf_inf_sdiff,

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

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

Tactic:
refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)

Goal state after:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b

case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ a ∆ b = ⊤

Tactic:
rw [h.eq_hnot, hnot_symmDiff_self]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp [← bihimp_assoc]

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_9
β : Type u_10
γ : Type u_11
p : (α → γ) × (β → γ)
⊢ (fun f ↦ (f ∘ inl, f ∘ inr)) ((fun p ↦ Sum.elim p.fst p.snd) p) = p

Tactic:
cases p
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t, t ⊆ f '' s ∧ p t) ↔ ∃ t, t ⊆ s ∧ p (f '' t)

Tactic:
simp [subset_image_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∀ (t : Set β), t ⊆ f '' s → p t) ↔ ∀ (t : Set α), t ⊆ s → p (f '' t)

Tactic:
simp [subset_image_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
obtain hi | hi := eq_or_ne (σ i) i

Goal state after:
case inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

case inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁

Tactic:
eq_self_iff_true,

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ True ∧ t = t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ val ⁻¹' (s ∩ t) = val ⁻¹' t

Tactic:
by
  rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]

Goal state after:
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₂
⊢ s₁ = s₂

Tactic:
rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ b, b ∈ t ∧ p b

Tactic:
exact ⟨f a, hf.mapsTo ha, h⟩

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

Goal state before:
pp: case zero
ι : 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✝ : MulOne M
f : Monoid.End M
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

Tactic:
simp [npowRec, *]

Goal state after:
case zero
ι : 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✝ : MulOne M
f : Monoid.End M
⊢ id = ⇑1
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case succ
ι : 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✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)

Tactic:
simp [npowRec, *]

Goal state after:
case succ
ι : 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✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ ⇑(npowRec n✝ f) ∘ ⇑f = ⇑(npowRec n✝ f * f)
Module: Mathlib.Data.Int.Init

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

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

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
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)

Tactic:
by
  rw [← image_univ] at *
  exact h.injOn_image ha.injOn hf

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * (↑u * ↑u⁻¹) = a

Tactic:
rw [Units.mul_inv, mul_one]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * (y * z) = 1

Tactic:
← mul_assoc

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * y * z = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
⊢ ↑(1 / u) = 1 /ₚ u

Tactic:
by
  rw [one_div, one_divp]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]

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

Goal state before:
pp: case inr
M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
h✝ : Nontrivial M₀
⊢ b✝ * a✝ = 1

Tactic:
exact (IsRightCancelMulZero.mul_right_cancel_of_ne_zero
      (right_ne_zero_of_mul_eq_one h)).mul_eq_one_symm h

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

Goal state before:
pp: case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ g • x⁻¹ = (g • x)⁻¹

pp: case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
· rw [hx, inv_zero, smul_zero, inv_zero]

Goal state after:
case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x⁻¹ = (g • x)⁻¹
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: ⊢ 0 = sqrt 0

Tactic:
simp [eq_sqrt]

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

Goal state before:
pp: ⊢ 1 = sqrt 1

Tactic:
simp [eq_sqrt]

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

Goal state before:
pp: ⊢ 1 = sqrt 2

Tactic:
simp [eq_sqrt]

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

Goal state before:
pp: case inl
a b c : ℕ
h : a = b * c
bc : b ≤ c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

pp: case inr
a b c : ℕ
h : a = b * c
cb : c ≤ b
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
· exact Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc

Goal state after:
case inr
a b c : ℕ
h : a = b * c
cb : c ≤ b
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

Tactic:
simp [npowRec, *]

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

Goal state before:
pp: case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)

Tactic:
simp [npowRec, *]

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
ha : a = 0
⊢ SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

Tactic:
simp only [ha, inv_zero, SemiconjBy.zero_left]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
by_cases h : IsUnit a

Goal state after:
case pos
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n

Tactic:
rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]

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

Goal state before:
pp: case inl
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Even n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
h.neg_one_pow,

Goal state after:
case inl
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Even n
⊢ 1 = if Even n then 1 else -1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
h.neg_one_pow,

Goal state after:
case inr
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ -1 = if Even n then 1 else -1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
by
  obtain hac | rfl | hca := lt_trichotomy a c
  · grind
  · left; simpa using mul_right_inj_of_comparable (le_total d b) |>.1 h
  · obtain hbd | rfl | hdb := lt_trichotomy b d
    · grind
    · exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm
    · exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
c d : α
hcd : a * b * c ≤ a * b * d
⊢ a * b * c ≤ a * (b * d)

Tactic:
← mul_assoc

Goal state after:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
c d : α
hcd : a * b * c ≤ a * b * d
⊢ a * b * c ≤ a * b * d
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ ∀ (a : α), a + 0 = a

Tactic:
simp [add_zero]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * b + (c + d) * a = d * b

Tactic:
← hcd,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * b + 0 * a = d * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = (c + d) * b + d * a

Tactic:
← hcd,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 * b + d * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d + a * (c + d) = b * d

Tactic:
← hcd,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d + a * 0 = b * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = b * (c + d) + a * d

Tactic:
← hcd,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = b * 0 + a * d
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✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * b + (c + d) * a = d * b

Tactic:
← hcd,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * b + 0 * a = d * b
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✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = (c + d) * b + d * a

Tactic:
← hcd,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 * b + d * a
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
⊢ b * d + a * (c + d) = b * d

Tactic:
← hcd,

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

Tactic:
← hcd,

Goal state after:
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 * d = b * 0 + a * d
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
⊢ a✝ = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ }

Tactic:
ext v

Goal state after:
α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
v : α
⊢ a✝ v = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ } v
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y

pp: case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
· rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
      exact mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left

Goal state after:
case right
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z