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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

Tactic:
rw [binaryRec, dif_neg h']
    change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
    generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
⊢ binaryRec' zero bit (Nat.bit b n) = bit b n h (binaryRec' zero bit n)

Tactic:
by
  rw [binaryRec', binaryRec_eq _ _ (by simp), dif_pos h, binaryRec']

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Relation.Map r id id = r

Tactic:
ext; simp [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : r b c
⊢ ReflGen r a c

Tactic:
obtain (rfl | h₁) := h₁

Goal state after:
case single.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b c✝ : α
inst✝ : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c

case single.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
a b b✝ c✝ : α
a✝ : ReflTransGen r a b✝
h₂ : r b✝ c✝
IH : r a b✝
⊢ r a c✝

Tactic:
| tail _ h₂ IH =>

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ x ≈ y.out

Tactic:
by
  refine Iff.trans ?_ Quotient.eq
  rw [Quotient.out_eq y]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ : α
⊢ r x✝ x✝

Tactic:
exact h.1 _

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ (m • n) • q = m • n • q

Tactic:
← smul_one_smul P,

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ ((m • n) • 1) • q = m • n • q
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
⊢ ¬IsMax a

Tactic:
intro ha'
  obtain ⟨b, hb⟩ := exists_ne a
  exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a < b ↔ a ≤ b → b ≤ a

Tactic:
simp [not_lt_iff_not_le_or_ge, or_iff_not_imp_left]

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

Goal state before:
pp: a b c : ℕ
⊢ a / b / c = a / c / b

Tactic:
Nat.div_div_eq_div_mul,

Goal state after:
a b c : ℕ
⊢ a / (b * c) = a / c / b
Module: Mathlib.Data.Nat.Init

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

Tactic:
by
  conv =>
    lhs
    rw [leRec, Or.by_cases, dif_pos h1]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

pp: case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

Tactic:
· exact iha x.1 (ha'.trans_le ha) x.1 le_rfl x.2

Goal state after:
case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Tactic:
simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]

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

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

Tactic:
induction h : f 0 using Nat.strongRecOn generalizing f with
  | ind n ih =>
    by_cases heq : f 0 = f 1
    · have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
      exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩
    · have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
      let g (i : ℕ) := f (i + 1)
      have hg_anti : Antitone g := by grind [Antitone]
      obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl
      refine ⟨p + 1, by omega, fun m hm => ?_⟩
      specialize hp' (m - 1) (by lia)
      grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeInf α

Tactic:
apply e.injective.semilatticeInf <;> intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ

Tactic:
refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)
    rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
      le_compl_iff_disjoint_right]
    exact inf_himp_le

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ ¬Disjoint t s ↔ (s ∩ t).Nonempty

Tactic:
not_disjoint_iff_nonempty_inter,

Goal state after:
α : Type u_1
s t : Set α
⊢ (t ∩ s).Nonempty ↔ (s ∩ t).Nonempty
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rw [removeNone_none _ h]

Goal state after:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e none = e none ↔ e.symm none = some x
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ {a, b} \ {b} = {a}

Tactic:
rw [pair_comm, pair_sdiff_left hab.symm]

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

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ t.ite s s' ∩ t = s ∩ t

Tactic:
rw [Set.ite, union_inter_distrib_right, sdiff_inter_self, inter_assoc, inter_self, union_empty]

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s : Set α
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

Tactic:
by
  rw [ite_inter_inter, ite_same]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
⊢ BooleanAlgebra α

Tactic:
let top := e.top
  let compl := e.compl
  let himp := e.himp
  let generalizedBooleanAlgebra := e.generalizedBooleanAlgebra
  apply e.injective.booleanAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ

Tactic:
ext ⟨x, x_in_s⟩
  constructor
  · intro x_in_u x_in_v
    exact eq_empty_iff_forall_notMem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩
  · grind

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t ∈ insert a '' 𝒫 s

Tactic:
refine ⟨t \ {a}, by grind⟩

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

Goal state before:
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.snd) H
    rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this

Goal state after:
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
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
by_cases hy : y = x

Goal state after:
case pos
α : 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

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
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 = ∅)

Tactic:
rw [← Set.prod_eq_empty_iff]

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

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

Tactic:
· obtain ⟨⟨x, y⟩, h⟩ := x
    rintro ⟨rfl : x = y, h2x⟩
    exact mem_image_of_mem _ h2x.1

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (({i} ∪ s \ {i}).pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (f j)

Tactic:
rw [union_pi, singleton_pi', update_self, pi_update_of_notMem]; simp

Goal state after:
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✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f a ^ n = f a ^ ↑n

Tactic:
zpow_natCast

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f a ^ n = f a ^ n
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
⊢ MapsTo f s t

Tactic:
by simp [← this, mapsTo_iff_image_subset]

Goal state after:
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
H : Type u_8
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
by simpa only [div_eq_mul_inv] using hf

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

Goal state before:
pp: a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a ≤ c - b ↔ b < c

Tactic:
← Int.sub_pos,

Goal state after:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a ≤ c - b ↔ 0 < c - b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
⊢ LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩; simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
⊢ RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩; simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop x✝ * unop x✝ ^ ↑x✝¹

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop x✝ * unop x✝ ^ x✝¹
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✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ n * f x = f x ^ ↑n * f x

Tactic:
zpow_natCast

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (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.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ (f x ^ (n + 1))⁻¹ = (f x ^ ↑n.succ)⁻¹

Tactic:
zpow_natCast

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ (f x ^ (n + 1))⁻¹ = (f x ^ n.succ)⁻¹
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_inv]

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

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

Tactic:
div_mul_div_cancel

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / b = a / b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-(↑(n + 1) + 1) + 1) = (a ^ (n + 1))⁻¹

Tactic:
Int.neg_add,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1) + -1 + 1) = (a ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
div_mul_div_cancel

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ b / a = b / a
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
by_cases hx : p x
    · exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx
    · rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
      exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : p x
⊢ p ((ofSubtype f) x) ↔ p x

Tactic:
simpa only [h, iff_true, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by rw [← comp_apply, h,
    comp_apply]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a⁻¹ * a = a

Tactic:
mul_inv_mul_cancel a

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g ↦ a * g) (a⁻¹ * g) = g

Tactic:
by simp [← mul_assoc, mul_inv_cancel₀ h]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-(↑(n + 1) + 1) + 1) = (a ^ (↑(n + 1) + 1))⁻¹ * a

Tactic:
Int.neg_add,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-↑(n + 1) + -1 + 1) = (a ^ (↑(n + 1) + 1))⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
x y : B
⊢ c • (x + y) = c • x + c • y

Tactic:
rcases hf x with ⟨x, rfl⟩
      rcases hf y with ⟨y, rfl⟩
      simp only [smul_add, ← smul, ← map_add]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
rw [← Int.natCast_one, cast_natCast, Nat.cast_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
c₁ c₂ : R
x : M₂
⊢ (c₁ + c₂) • x = c₁ • x + c₂ • x

Tactic:
by
      rcases hf x with ⟨x, rfl⟩
      simp only [add_smul, ← smul, ← f.map_add]

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
obtain hn | hn := natAbs_eq m

Goal state after:
case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ m ∣ ↑n ↔ m.natAbs ∣ n
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit a⁻¹ʳ

Tactic:
Ring.inverse_non_unit _ h

Goal state after:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ ↑a✝ ≠ 0

Tactic:
zpow_natCast

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ a✝ ≠ 0
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
u : αˣ
⊢ -(a /ₚ u) = -a /ₚ u

Tactic:
by simp only [divp, neg_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ ↑a ^ 2 = ↑b ^ 2 ↔ ↑a = ↑b ∨ ↑a = ↑(-b)

Tactic:
sq_eq_sq_iff_eq_or_eq_neg,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ ↑a = ↑b ∨ ↑a = -↑b ↔ ↑a = ↑b ∨ ↑a = ↑(-b)
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (-(↑x + 1)) = g (-(↑x + 1))

Tactic:
← neg_one_mul,

Goal state after:
case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (-1 * (↑x + 1)) = g (-1 * (↑x + 1))
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

Tactic:
exact hcd.trans_le <| add_le_of_nonpos_left hc

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

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

Tactic:
exact hcd.trans_le <| add_le_of_nonpos_left hc

Goal state after: