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

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ bitCasesOn (bit b n) h = h b n

Tactic:
change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ⋯ ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ⋯ ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Tactic:
generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a i✝ b✝ c✝ : α
a✝ : TransGen r a b✝
bc : r b✝ c✝
ab : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝

Tactic:
| tail _ bc ab =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1.refl
α : Type u_1
r : α → α → Prop
a : α
⊢ a = a ∨ TransGen r a a

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ f (foldr (fun x ↦ f) b l) = f^[l.length + 1] b

Tactic:
foldr_const f b l,

Goal state after:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ f (f^[l.length] b) = f^[l.length + 1] b
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : γ → α → β
x : α → β
i : Option γ
y : α
⊢ i.elim x f y = i.elim (x y) fun j ↦ f j y

Tactic:
rw [elim_comp fun f : α → β => f y]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ a, g a = d

Tactic:
obtain ⟨⟨a, b⟩, h⟩ := h (default, d)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ a, g a = d
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
⊢ Injective (@toPreorder α)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Goal state after:
α : Type u_2
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝¹ } =
    { toPreorder := toPreorder✝, le_antisymm := le_antisymm✝ }
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 ^ 2 * k ^ 2

Tactic:
← Nat.add_mul

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

Goal state before:
pp: m n : ℕ
⊢ ¬0 = 1 % 2

Tactic:
mod_eq_of_lt

Goal state after:
m n : ℕ
⊢ ¬0 = 1

m n : ℕ
⊢ 1 < 2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case refl
m n k : ℕ
hmn : m ≤ n
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
decreasingInduction_self

Goal state after:
case refl
m n k : ℕ
hmn : m ≤ n
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ = decreasingInduction (fun x x_1 ↦ of_succ x ⋯) self hmn
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : Disjoint a b
x : α
h₁ : x ≤ a
h₂ : x ≤ b
⊢ x = ⊥

Tactic:
simpa using h h₁ h₂

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ (Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd) ∧ Codisjoint x y ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd

Tactic:
Prod.codisjoint_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ (Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd) ∧ Codisjoint x.fst y.fst ∧ Codisjoint x.snd y.snd ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: 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

Tactic:
exact ⟨b + 1, strictMono _ le_rfl⟩

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s ⊂ univ ↔ sᶜ.Nonempty

Tactic:
rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]

Goal state after:
α : Type u
s : Set α
⊢ (s ⊆ univ ∧ ∃ a, ¬a ∈ s) ↔ ∃ x, x ∈ sᶜ
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ sᶜ ⊂ univ ↔ s.Nonempty

Tactic:
rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]

Goal state after:
α : Type u
s : Set α
⊢ (sᶜ ⊆ univ ∧ ∃ a, ¬a ∈ sᶜ) ↔ ∃ x, x ∈ s
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ a

Tactic:
apply inf_le_left

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b = b ↔ a ⊓ b = a

Tactic:
rw [sup_eq_right, ← inf_eq_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
cases h1 : e.symm (some (removeNoneAux e x)) <;> cases h2 : e (some x)

Goal state after:
case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by rw [inf_sup_left]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f (a ⇨ ⊥) = f aᶜ

Tactic:
rw [map_himp, map_compl, map_bot, himp_bot]

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

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

Tactic:
by rw [inf_sup_left]

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:
by
  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.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (piCongrRight h₂) f a = (h₂ a) (f a)

Tactic:
piCongrRight_apply,

Goal state after:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ Pi.map (fun a ↦ ⇑(h₂ a)) f a = (h₂ a) (f a)
Module: Mathlib.Data.Set.Prod

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

pp: case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁

pp: case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
· have := image_mono (f := Prod.fst) H
    rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁

case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn (s.piecewise f g) s ∧
      InjOn (s.piecewise f g) sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
(piecewise_eqOn s f g).injOn_iff,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧
      InjOn (s.piecewise f g) sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ x ∈ f '' {x | p x}

Tactic:
mem_range,

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ y, Subtype.map f h y = ⟨x, hx⟩) ↔ x ∈ f '' {x | p x}
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: F : 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
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
⊢ h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y)

Tactic:
map_mul,

Goal state after:
F : 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
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
⊢ h2 (h1 x * h1 y) = h2 (h1 x) * h2 (h1 y)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
map_mul,

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ f a * f b⁻¹ = f a * (f b)⁻¹
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ n * a) = f a ^ n * f a

Tactic:
map_mul,

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ n) * f a = f a ^ n * f a
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✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 * ?m.21 = 1 * ?m.21

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✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ G

Tactic:
← map_mul _ 1,

Goal state after:
ι : 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✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f (1 * 1) = 1 * f 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ x ∈ s₁

Tactic:
by rwa [← hf h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) = x

Tactic:
obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
    rw [invFunOn_apply_eq (f := f) hx']

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

Goal state before:
pp: F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f (x * y⁻¹) = 1

Tactic:
map_mul,

Goal state after:
F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f x * f y⁻¹ = 1
Module: Mathlib.Algebra.Group.Hom.Basic

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

Tactic:
map_mul,

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

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

Tactic:
by rw [h, div_self']

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
⊢ a ^ (-1 + 1) = a ^ (-1) * a

Tactic:
by simp [Int.add_left_neg]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b / a) = b

Tactic:
mul_div_cancel a b

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ b = b
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
@CommApplicative.commutative_prod m h

Goal state after:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> ((fun b a ↦ (a, b)) <$> b <*> a) = (fun b a ↦ f a b) <$> b <*> a
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ single i 1 j • x = single i x j

Tactic:
rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -(r • -x) = r • x

Tactic:
smul_neg,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ - -(r • x) = r • x
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
⊢ (∀ (x : R), r * x = 0 → x = 0) ∧ IsRightRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0

Tactic:
isRightRegular_iff_left_eq_zero_of_mul

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
⊢ ((∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0) ↔
    (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f (x * 1) = 0

Tactic:
map_mul,

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f x * f 1 = 0
Module: Mathlib.Algebra.Ring.Semiconj

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)

Tactic:
by
  simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y

Tactic:
by
  simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

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

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

Tactic:
obtain ⟨u, rfl⟩ := h
  rw [inverse_unit, inverse_unit, inv_inv]

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

Goal state before:
pp: case inr.inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

pp: case inr.inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
· have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]
    simp [Ring.inverse_non_unit, ha, this]

Goal state after:
case inr.inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ (a * if h0 : a = 0 then 0 else ↑⋯.unit⁻¹) = 1

Tactic:
change (a * if h0 : a = 0 then 0 else ↑((h a).resolve_right h0).unit⁻¹) = 1

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ (a * if h0 : a = 0 then 0 else ↑⋯.unit⁻¹) = 1
Module: Mathlib.Data.Int.Cast.Lemmas

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

Tactic:
by rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * (a * 2 * b + b + a) + 1 = 2 * (2 * a * b + b + a) + 1

Tactic:
← Nat.cast_two,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ ↑2 * (a * ↑2 * b + b + a) + 1 = ↑2 * (↑2 * a * b + b + a) + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
⊢ IsUnit 2 ↔ ∀ (a : α), Even a

Tactic:
refine ⟨Even.of_isUnit_two, fun h => ?_⟩
  obtain ⟨a, ha⟩ := h 1
  rw [← two_mul, eq_comm] at ha
  exact ⟨⟨2, a, ha, .trans (Commute.ofNat_right _ _).eq ha⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

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:
by
  rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]

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
⊢ a * b⁻¹ < c * d⁻¹

Tactic:
apply mul_lt_mul hac (by gcongr; assumption) _ hc

Goal state after:
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
⊢ 0 < b⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a / b < c / d

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]
  exact mul_lt_mul' hac ((inv_lt_inv₀ (hd.trans hdb) hd).2 hdb)
    (inv_nonneg.2 <| hd.le.trans hdb.le) hc

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (b * a) = b ^ (n + 1) * a

Tactic:
rw [← mul_assoc, ← pow_succ]

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

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

Tactic:
rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ d / b ≤ max (c / d) (d / a)
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n < 1 ↔ n = 0

Tactic:
rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]

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

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → 1 < c

Tactic:
rw [one_lt_iff_ne_one]

Goal state after:
case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → c ≠ 1