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

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

Tactic:
isCancelMul_iff,

Goal state after:
R : Type u_2
inst✝ : Mul R
⊢ IsLeftCancelMul R ∧ IsRightCancelMul R ↔ ∀ (r : R), IsRegular r
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
| =>

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * 0) m = npowRec' 0 (m * m)
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
| =>

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

Tactic:
| =>

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * (k + 2)) m = npowRec' (k + 2) (m * m)
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
| =>

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

Tactic:
| =>

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k + 2 ≠ 0
⊢ m * npowRec' (k + 2) m = npowRec' (k + 2) m * m
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
| =>

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

Tactic:
| =>

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 + 1) m = 1 * npowRec' (k + 1 + 1) m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec 0 m = npowBinRec.go 0 1 m

Tactic:
| =>

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec 0 m = npowBinRec.go 0 1 m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k✝ : ℕ
m : M
k : ℕ
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m

Tactic:
| =>

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k✝ : ℕ
m : M
k : ℕ
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)

Tactic:
by
  by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ (a ↔ b) = (b ↔ a)

Tactic:
by rw [@iff_comm a b]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
by_cases p : P <;> simp [p]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
by_cases p : P <;> simp [p]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive ⋯

Tactic:
exact refl a

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a c b✝ : α
hac : r a b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b b✝

Tactic:
exact ⟨_, hac, by rfl⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
a b : α
⊢ r a a

Tactic:
exact refl a

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

Goal state before:
pp: α : Type u_4
⊢ IsEmpty (ULift α) ↔ IsEmpty α

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_ulift]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ RightTotal R

Tactic:
by
  simp only [RightTotal, IsEmpty.forall_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : OrderBot α), a = b

Tactic:
by rintro @⟨⟨a⟩, ha⟩ @⟨⟨b⟩, hb⟩; congr; exact le_antisymm (ha _) (hb _)

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

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn hnm fun {k} ↦ next)

Tactic:
induction hnm with

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

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn hnm fun {k} ↦ next)

Tactic:
induction hnm with

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'

Tactic:
rw [← not_lt, ← not_lt]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)

Tactic:
by simp [h₁, h₂]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictMono f

Tactic:
by
  rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictMonoOn f s

Tactic:
by
  rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]

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

Goal state before:
pp: case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m + 1 ≤ f (n + m + 1)

Tactic:
Nat.succ_le_iff

Goal state after:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m < f (n + m + 1)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
apply le_antisymm
  · exact h_anti h₁
  · rw [h_fa]; exact h_anti h₂

Goal state after:
Module: Mathlib.Order.Disjoint

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

Tactic:
sup_top_eq

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

Goal state before:
pp: f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
⊢ ∃ m, m ≤ b ∧ f m = f (m + 1)

Tactic:
contrapose! hfb

Goal state after:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ), m ≤ b → f m ≠ f (m + 1)
⊢ ∃ m, b < f m
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [sup_inf_sdiff, sup_inf_sdiff]

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

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
x : (α ⊕ β) ⊕ γ ⊕ δ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        x) =
    x

Tactic:
rcases x with ((a | b) | (c | d)) <;> simp

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
refine (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_
  rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]

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

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

Tactic:
prod_subset_prod_iff,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ ↔ s ⊆ s₁ ∧ t ⊆ t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
hs : s.Nonempty
⊢ EqOn g g' t

Tactic:
obtain ⟨x, hxs⟩ := hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x : α
hxs : x ∈ s
⊢ EqOn g g' t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' univ.pi fun i' ↦ t (f i')) = univ.pi t

Tactic:
by
  simpa [f.surjective.range_eq] using piCongrLeft_symm_preimage_pi f univ t

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
⊢ u ∈ f '' f ⁻¹' t

Tactic:
rw [image_preimage_eq_inter_range]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
⊢ u ∈ t ∩ range f
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t

Tactic:
refine ⟨?_, h.rightInvOn_invFunOn⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
⊢ Int.leInductionDown base pred m ⋯ = base

Tactic:
Int.leInductionDown,

Goal state after:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
⊢ Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) m m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
      (fun k hle ih x ↦ pred k hle (ih hle)) ⋯ =
    base
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ Int.leInductionDown base pred (n - 1) ⋯ = pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
Int.leInductionDown,

Goal state after:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) (n - 1) m (fun x ↦ base)
      (fun x x_1 x_2 x_3 ↦ ⋯.elim) (fun k hle ih x ↦ pred k hle (ih hle)) ⋯ =
    pred n hnm (Int.leInductionDown base pred n hnm)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ n * f x = f (x ^ n) * f x

Tactic:
npow

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ n * f x = f x ^ n * f x
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b = 1 ↔ b⁻¹ = a

Tactic:
by
  rw [mul_eq_one_iff_eq_inv, eq_comm]

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
⊢ x • y • z = y • x • z

Tactic:
induction y using MulOpposite.rec'
    simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ y * x) y = (fun y ↦ y * x) y'
⊢ y = y'

Tactic:
by
  simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 1 = 3

Tactic:
rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1) = 3
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑m = ↑n✝
⊢ m + 1 = n✝ + 1

Tactic:
rwa [ih]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n

Tactic:
Nat.add_sub_cancel_right

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
x✝ : Even n
m : ℕ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
by simp [← Nat.two_mul, hm]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = n • f 1

Tactic:
by
  rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]

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

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

Tactic:
by
  rw [zpow_neg]; exact inv_mul_cancel₀ (zpow_ne_zero n ha)

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + (1 + a))

Tactic:
simp [add_comm 1 a]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat 0 = ↑0

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat 0 = ↑0
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat 1 = ↑1

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat 1 = ↑1
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ n : ℕ
⊢ OfNat.ofNat (n + 2) = ↑(n + 2)

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : Semiring α
n✝ n : ℕ
⊢ OfNat.ofNat (n + 2) = ↑(n + 2)
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 : G₀
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
rw [div_lt_iff₀ hb, one_mul]

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
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
⊢ r ↪r s

Tactic:
refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ a = b

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s ({ toFun := f, inj' := ⋯ } a) ({ toFun := f, inj' := ⋯ } b)
⊢ r a b
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h]⟩
  obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h <;>
    simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

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

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k % k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
mod_eq_of_lt hk

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
simp [ceil_le, lt_ceil]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.coe
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
| coe c =>

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

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

Tactic:
by rw [← h, invOf_mul_self]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.coe
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
| coe c =>

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

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a

Tactic:
rw [H₁.gc_floor, H₂.gc_floor]

Goal state after:
case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
· apply eq_inv_of_mul_eq_one_left
    rw [← map_mul, inv_mul_cancel₀ h, map_one]

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

Goal state before:
pp: case inr
⊢ IsUnit (-1)

Tactic:
· exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (s.domRestrict f) ↔ StrictMonoOn f s

Tactic:
simp [Set.domRestrict, StrictMono, StrictMonoOn]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ |a * b| = |a| * |b|

Tactic:
abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b

Tactic:
suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
⊢ ∀ ⦃x₂ : β → γ⦄, x₂ ∈ {f | StrictMono f} → range f = range x₂ → f = x₂

Tactic:
g

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
⊢ g ∈ {f | StrictMono f} → range f = range g → f = g
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLUB s a ↔ IsLUB t a

Tactic:
IsLUB,

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLeast (upperBounds s) a ↔ IsLUB t a
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLeast (upperBounds s) a ↔ IsLUB t a

Tactic:
IsLUB,

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLeast (upperBounds s) a ↔ IsLeast (upperBounds t) a