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

Goal state before:
pp: b : Bool
n : Nat
⊢ 0 + n = n

pp: b : Bool
n : Nat
⊢ b.toNat < 2

pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
Nat.zero_add

Goal state after:
b : Bool
n : Nat
⊢ n = n

b : Bool
n : Nat
⊢ b.toNat < 2

case H
b : Bool
n : Nat
⊢ 0 < 2
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Trichotomous r
a b : α
⊢ ¬Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true → a = b

Tactic:
by simpa using trichotomous a b

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

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

Tactic:
rw [div_eq_mul_inv, mul_inv_cancel_right a b]

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

Goal state before:
pp: α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ f ≍ f'

Tactic:
have : β = β' := by funext a; exact type_eq_of_heq (this a)

Goal state after:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this✝ : ∀ (a : α), f a ≍ f' a
this : β = β'
⊢ f ≍ f'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂

Tactic:
by rw [← comp_assoc, h₁.comp_eq_id, id_comp]

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 : α₂
h₂ : ∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
obtain ⟨c, rfl⟩ := h₂
      rw [h₁₂.extend_apply]
      exact (h₂₃.comp h₁₂).extend_apply _ _ _

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
exact IsTrans.trans _ _ _ hac hcd

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (ReflTransGen r) ≤ ReflTransGen (Function.swap r)

Tactic:
by
  intro _ _ h
  induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc

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

Goal state before:
pp: case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g (0 + k))

Tactic:
Nat.zero_add

Goal state after:
case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂

Tactic:
· rw [← inv_inv a₂, eq_inv_of_mul_eq_one_left (h (a₂⁻¹ * a₁) ?_), inv_inv]
    simpa only [mul_smul, inv_smul_eq_iff] using h'

Goal state after:
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
⊢ mulSingle i x = 1 ↔ x = 1

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ mulSingle_one i⟩

Goal state after:
ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
h : mulSingle i x = 1
⊢ x = 1
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ r ^ (n + 1) • (x * x ^ n) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
← pow_succ'

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ r ^ (n + 1) • x ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {x y : α}, compare x y = Ordering.lt ↔ x < y

Tactic:
by simp [compare_lt_iff_lt]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a < a₂ ∧ a₁ < a

Tactic:
by
  simp_rw [and_comm]; exact dense

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, *, Ordering.swap]
  cases not_or_intro xy yx (total_of _ _ _)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ ⊥ = b ⊓ x

Tactic:
sup_bot_eq

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x = b ⊓ x
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_) <;>
  (rintro rfl; simp at h)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case e_sup
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ sup✝¹ x✝¹ x✝ = sup✝ x✝¹ x✝

Tactic:
apply SemilatticeSup.ext_sup H

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
⊢ PartialOrder α

Tactic:
apply e.injective.partialOrder <;> intros <;> rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ⊔ ⊥ = a \ b

Tactic:
sup_bot_eq

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = a \ b
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [← inf_eq_right] at hs

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
⊢ HeytingAlgebra α

Tactic:
let generalizedHeytingAlgebra := e.generalizedHeytingAlgebra
  let bot := e.bot
  let compl := e.compl
  apply e.injective.heytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ⊔ ⊥ = a

Tactic:
sup_bot_eq

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a = a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b ⊔ ⊥ = a \ b

Tactic:
sup_bot_eq

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b = a \ b
Module: Mathlib.Logic.Equiv.Basic

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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (y : Subtype q) × { x // f x = ↑y } ≃ (y : Subtype q) × { x // ⟨f ↑x, ⋯⟩ = y }

Tactic:
by {
          apply sigmaCongrRight
          intro y
          apply Equiv.symm
          refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)
          intro x
          exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩ }

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_eq_sup_sdiff_inf,

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

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

Tactic:
symmDiff_eq_sup_sdiff_inf,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : (a ⊔ b) \ (a ⊓ b) = a ⊔ b
⊢ Disjoint a b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

Tactic:
symmDiff_eq_sup_sdiff_inf,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⊔ b) \ (a ⊓ b) = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
simp [hy]

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

Goal state before:
pp: case mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
rintro ⟨x, hx, rfl⟩
    exact ⟨rfl, hx, hx⟩

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

Goal state before:
pp: case mp
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

pp: case mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
· rintro ⟨h0 | h0, h1 | h1, h2⟩ <;> simp [h0, h1, h2]

Goal state after:
case mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t

Tactic:
by
  ext x
  rw [mem_image]
  exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

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

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

Tactic:
by
  rw [inter_comm, preimage_coe_self_inter]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
⊢ (∃ f, s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
· rintro ⟨f, hf⟩
    rw [hf]
    exact InjOn.image_of_comp <| injOn_id _

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)

Tactic:
have : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s := forall_mem_image.2 fun (x, y) h ↦ ⟨y, h⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
this : ∀ (x : α), x ∈ Prod.fst '' s → ∃ y, (x, y) ∈ s
⊢ ∃ f, s = graphOn f (Prod.fst '' s)
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✝ : MulOne M
n : ℕ
f : Monoid.End M
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
induction n <;> 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

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.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
⊢ ∀ (a b : H), a * b = b * a

Tactic:
simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]

Goal state after:
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
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
    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✝ : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b

Tactic:
by
  rw [mul_comm c, mul_comm c, h.mul_div_mul_right]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : (ofSubtype x) ↑a = (ofSubtype y) ↑a
⊢ x a = y a

Tactic:
rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n = -↑(m + 1) + (↑n + ↑m.succ)

Tactic:
eq_neg_add_iff_add_eq,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(m + 1) + ↑n = ↑n + ↑m.succ
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a c : α
⊢ a ∣ c * a

Tactic:
exact ⟨c, mul_comm _ _⟩

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

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

Tactic:
inv_eq_one_div,

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

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

Tactic:
inv_eq_one_div,

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

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

Tactic:
induction n <;> simp [npowRec, *]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m - n) = a ^ m / a ^ n

Tactic:
rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = b ^ 2 + a * b

Tactic:
by rw [sq, ← add_mul, add_comm, hab, zero_mul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
by
      rw [add_mul, ← pow_add, add_right_comm]; rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
hp : Odd a
⊢ Odd (-a)

Tactic:
by
  obtain ⟨k, hk⟩ := hp
  use -(k + 1)
  rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
    ← neg_add, hk]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
← mul_le_mul_iff_left a

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
← mul_le_mul_iff_left a

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

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

Tactic:
← mul_le_mul_iff_left a

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a₁ = a₂ ∧ b₁ = b₂ → a₂ * b₂ ≤ a₁ * b₁

Tactic:
rintro ⟨rfl, rfl⟩; rfl

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
ha : 0 < ↑a
⊢ b < c

Tactic:
· exact @ContravariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨_, ha⟩ _ _ h

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
⊢ a = b ∧ c = d → a * c = b * d

Tactic:
rintro ⟨rfl, rfl⟩; rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
⊢ a = b ∧ c = d → a * c = b * d

Tactic:
rintro ⟨rfl, rfl⟩; rfl

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 d : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosMono R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ c * b ≤ c * d

Tactic:
gcongr; assumption

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
ha : a ≤ 0
h : b ≤ 1
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
ha : a ≤ 0
h : 1 ≤ b
⊢ a * b ≤ a

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

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
⊢ 2 * a * b ≤ a ^ 2 + b ^ 2

Tactic:
simpa [fn_min_add_fn_max (fun x ↦ x * x), sq, two_mul, add_mul]
    using mul_add_mul_le_mul_add_mul (@min_le_max _ _ a b) (@min_le_max _ _ a b)

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₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ b⁻¹ ≤ d⁻¹

Tactic:
gcongr; assumption

Goal state after:
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
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsRightCancelAdd α
hz : z ≠ ⊤
⊢ x + z = y + z ↔ x = y

Tactic:
lift z to α using hz; exact (IsAddRightRegular.all _).withTop.eq_iff

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ b⁻¹ * a < c

Tactic:
by
  rw [mul_comm] at *
  exact mul_inv_lt_of_lt_mul₀ h

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
a✝ : WithTop α
H : ∀ (a : α), ↑↑a ≤ ↑a✝
⊢ ↑a✝ = ⊤

Tactic:
simpa [WithTop.eq_top_iff_forall_ge] using H

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ b ≤ ⌊a + ↑n⌋₊ ↔ b ≤ ⌊a⌋₊ + n

Tactic:
rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ↔ IsDirectedOrder ↑s

Tactic:
by
  rw [directedOn_iff_directed, IsDirectedOrder]
  exact ⟨fun h ↦ ⟨h⟩, fun ⟨h⟩ ↦ h⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)

Tactic:
inv_eq_one_div,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + b⁻¹ = (a + b) / (a * b)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + b⁻¹ = (a + b) / (a * b)

Tactic:
inv_eq_one_div,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
inv_eq_one_div,

Goal state after:
K : Type u_1
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a - b⁻¹ = (b - a) / (a * b)