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

Goal state before:
pp: G : Type u_1
inst✝ : CommMagma G
a : G
⊢ IsLeftRegular a ↔ IsRegular a

Tactic:
simp [isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm]

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

Goal state before:
pp: G : Type u_1
inst✝ : CommMagma G
a : G
⊢ IsRightRegular a ↔ IsRegular a

Tactic:
simp [isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm]

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

Goal state before:
pp: case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]

Goal state after:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a
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:
simp only [existsUnique_iff_exists]

Goal state after:
α : 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
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

Tactic:
simp [or_comm, Decidable.forall_or_left]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
q : Prop
p : α → Prop
⊢ ((∀ (x : α), q) ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x

Tactic:
forall_const

Goal state after:
α : Sort u_1
inst✝ : Nonempty α
q : Prop
p : α → Prop
⊢ (q ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
p : α → Prop
q : Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q) ↔ (∀ (x : α), p x) ∧ q

Tactic:
forall_const

Goal state after:
α : Sort u_1
inst✝ : Nonempty α
p : α → Prop
q : Prop
⊢ (∀ (x : α), p x) ∧ q ↔ (∀ (x : α), p x) ∧ q
Module: Mathlib.Logic.Unique

Goal state before:
pp: α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α i

Tactic:
by
  rw [Unique.eq_default i]
  exact x

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
y : α
x✝ : { x // x = y }
x : α
hx : x = y
⊢ ⟨x, hx⟩ = ⟨y, ⋯⟩

Tactic:
by congr

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Irrefl r ↔ r ≤ Ne

Tactic:
by
  unfold Pi.hasLe Prop.le
  grind [Std.Irrefl]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (ReflGen r) = ReflTransGen r

Tactic:
by
  simp only [← transGen_reflGen, reflGen_eq_self]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
⊢ ReflTransGen r = ReflGen r

Tactic:
rw [← reflGen_transGen, transGen_eq_self]

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (x * a) = r • b * x

Tactic:
smul_mul_assoc,

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (x * a) = r • (b * x)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • x * a = r • (b * x)

Tactic:
smul_mul_assoc,

Goal state after:
M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ r • (x * a) = r • (b * x)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • 1 * y = x • y

Tactic:
smul_mul_assoc,

Goal state after:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • (1 * y) = x • y
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_4
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ Pi.mulSingle i x j = x

Tactic:
rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

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

Goal state before:
pp: α : Type u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
by congr

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

Goal state before:
pp: α : Sort u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
by congr

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

Goal state before:
pp: n m : ℕ
⊢ m * 2 ≤ n ↔ ↑m * 2 ≤ ↑n

Tactic:
← Int.ofNat_le,

Goal state after:
n m : ℕ
⊢ ↑(m * 2) ≤ ↑n ↔ ↑m * 2 ≤ ↑n
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
⊢ cmpLE x y = cmp x y

Tactic:
by
  by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]
  cases not_or_intro xy yx (total_of _ _ _)

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

Goal state before:
pp: α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ {x | x ∈ s ∧ p x} = s ∩ {x | x ∈ t ∧ p x}

Tactic:
rw [← inter_ofPred_eq_sep s p, ← inter_ofPred_eq_sep t p,
    ← inter_assoc, ← left_eq_inter.mpr hst]

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

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), x ∈ s ∧ p x ↔ False) ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
iff_false,

Goal state after:
α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), ¬(x ∈ s ∧ p x)) ↔ ∀ (x : α), x ∈ s → ¬p x
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ⊔ y ≤ c

Tactic:
by simp only [sup_le_iff]; rw [← H, @sup_le_iff α A, H, H]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| ⊥

Tactic:
rw [← inf_inf_sdiff x y, inf_comm]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| x \ y ⊓ (x ⊓ y)
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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
⊢ LeftInverse (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) fun b ↦ ⟨inr b.fst, b.snd⟩) fun x ↦
    match x with
    | ⟨inl x, y⟩ => inl ⟨x, y⟩
    | ⟨inr x, y⟩ => inr ⟨x, y⟩

Tactic:
by rintro ⟨x|x,y⟩ <;> simp

Goal state after:
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
⊢ LeftInverse (Sum.elim Int.ofNat Int.negSucc) fun z ↦ Int.casesOn z inl inr

Tactic:
rintro (m | n)

Goal state after:
case ofNat
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
m : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z ↦ Int.casesOn z inl inr) (Int.ofNat m)) = Int.ofNat m

case negSucc
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
n : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z ↦ Int.casesOn z inl inr) (Int.negSucc n)) = Int.negSucc n
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
⊢ RightInverse (Sum.elim Int.ofNat Int.negSucc) fun z ↦ Int.casesOn z inl inr

Tactic:
rintro (m | n)

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
m : ℕ
⊢ (fun z ↦ Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inl m)) = inl m

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
n : ℕ
⊢ (fun z ↦ Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inr n)) = inr n
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
p : α → Prop
q : Subtype p → Prop
a : Subtype q
⊢ q ⟨↑↑a, ⋯⟩

Tactic:
by
      rcases a with ⟨⟨a, hap⟩, haq⟩
      exact haq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
⊢ InjOn (extend f g j) (range f)

Tactic:
by
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ heq
  rw [hf.extend_apply, hf.extend_apply] at heq
  rw [hg heq]

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

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

Tactic:
← image_preimage_coe,

Goal state after:
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t = val ⁻¹' u ↔ val '' val ⁻¹' t = s ∩ u
Module: Mathlib.Data.Set.Image

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

Tactic:
← image_preimage_coe,

Goal state after:
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t = val ⁻¹' u ↔ val '' val ⁻¹' t = val '' val ⁻¹' u
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → s ∩ t ⊆ s ∩ u

Tactic:
← image_preimage_coe,

Goal state after:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → val '' val ⁻¹' t ⊆ s ∩ u
Module: Mathlib.Data.Set.Image

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

Tactic:
← image_preimage_coe,

Goal state after:
α : Type u_1
s t : Set α
⊢ (val ⁻¹' t).Nonempty ↔ (val '' val ⁻¹' t).Nonempty
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) → ∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i

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

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
hi : ¬i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
else

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
hi : ¬i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ univ.pi t = {a} ↔ ∀ (i : ι), t i = {a i}

Tactic:
simp only [eq_singleton_iff_unique_mem]

Goal state after:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a) ↔ ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = univ.pi (update (fun x ↦ univ) i s)

Tactic:
ext x
  simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)

Tactic:
by
  rw [disjoint_iff_inter_eq_empty] at h ⊢
  rw [← hf.image_inter hs ht, h, image_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ SurjOn f s t

Tactic:
by simp [← this, surjOn_image]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

Tactic:
rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * (↑u₂ * u₂.inv * u₁.inv) = 1

Tactic:
val_inv,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * (1 * u₁.inv) = 1
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ a * b / a = b

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ ha]

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

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ (n + 1) = 0
⊢ a = 0

Tactic:
rw [pow_succ, mul_eq_zero] at ha; exact ha.elim ih id

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

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a

Tactic:
rw [inv_mul_cancel₀ h, one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b

Tactic:
rw [add_mul, one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b

Tactic:
rw [add_mul, one_mul]

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

Goal state before:
pp: ⊢ log2 2 = 1

Tactic:
simp [log2_def]

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

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℤ
⊢ n • a = a * ↑n

Tactic:
zsmul_eq_mul,

Goal state after:
α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℤ
⊢ ↑n * a = a * ↑n
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : LeftDistribClass R
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f x * (f y + f z) = f x * f y + f x * f z

Tactic:
simp only [← add, ← mul, left_distrib]

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

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ m • 1 = ↑m

Tactic:
zsmul_eq_mul,

Goal state after:
R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ ↑m * 1 = ↑m
Module: Mathlib.Logic.OpClass

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

Tactic:
← ha.assoc,

Goal state after:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f a b) c = f b (f a c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a * a < 1 ↔ a < 1

Tactic:
by contrapose!; exact one_le_mul_self_iff

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ a * c < b

Tactic:
← mul_lt_mul_iff_of_pos_right hc,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c < b * c⁻¹ * c ↔ a * c < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < a * c

Tactic:
← mul_lt_mul_iff_of_pos_right hc,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ * c < a * c ↔ b < a * c
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s (e₁ a) (e₁ b) ↔ r a b
e₂ : α ≃ β
map_rel_iff'✝ : ∀ {a b : α}, s (e₂ a) (e₂ b) ↔ r a b
h : { toEquiv := e₁, map_rel_iff' := o₁ }.toEquiv = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }.toEquiv
⊢ { toEquiv := e₁, map_rel_iff' := o₁ } = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }

Tactic:
by congr

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

Goal state before:
pp: case refine_2
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
e : Xᵒᵈ ≃o Y := { toEquiv := ofDual.trans ↑f, map_rel_iff' := ?refine_1 }
⊢ DenselyOrdered Xᵒᵈ ↔ DenselyOrdered Y

pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ {a b : Xᵒᵈ}, (ofDual.trans ↑f) a ≤ (ofDual.trans ↑f) b ↔ a ≤ b

Tactic:
· exact denselyOrdered_iff_of_orderIsoClass e

Goal state after:
case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ {a b : Xᵒᵈ}, (ofDual.trans ↑f) a ≤ (ofDual.trans ↑f) b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Group.Lattice

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

Tactic:
← inf_mul_sup x z

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 ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a b : α
inst✝ : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
by
  rwa [mabs_of_one_le ha, mabs_of_one_le (ha.trans hab)]

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
by simp [← not_even_iff_odd, not_or, parity_simps]

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

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ a_n % ↑q.succ * ↑(p + 1) + ↑b.toNat * ↑(q + 1) = ↑n

Tactic:
Int.natCast_toNat_eq_self.mpr,

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ a_n % ↑q.succ * ↑(p + 1) + b * ↑(q + 1) = ↑n

case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ 0 ≤ b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ IsAddUnit a → a ≠ ⊤

Tactic:
rintro ⟨⟨b, c, hbc, -⟩, rfl⟩ rfl

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
c : α
hbc : ⊤ + c = 0
⊢ False
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
⊢ b - a = 0 ↔ b = a

Tactic:
rw [← sub_self_eq_zero_of_ne_top ha, sub_left_inj_of_ne_top ha]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a b c : α
⊢ ↑a + ↑b = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ↑b ∧ a' + b' = c

Tactic:
by norm_cast; simp

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

Goal state before:
pp: case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

Tactic:
cases z

Goal state after:
case top.top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ⊤ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤)

case top.top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ ↑a✝ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

Tactic:
cases z

Goal state after:
case top.coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝ ⊤ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤)

case top.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑a✝¹ ↑a✝ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝¹) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝)