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']

Goal state after:
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
⊢ (have x := bit (1 &&& Nat.bit b n != 0) (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1));
    ⋯ ▸ x) =
    bit b n (binaryRec zero bit n)
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

Tactic:
exact h₁

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

Goal state before:
pp: M : Type u
⊢ ∀ ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂

Tactic:
by
  rintro @⟨@⟨⟨one₁⟩, ⟨mul₁⟩⟩, one_mul₁, mul_one₁⟩ @⟨@⟨⟨one₂⟩, ⟨mul₂⟩⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩
  -- FIXME (See https://github.com/leanprover/lean4/issues/1711)
  -- congr
  suffices one₁ = one₂ by cases this; rfl
  exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

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

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

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

Tactic:
· exact (hn rfl).elim

Goal state after:
case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : α = β
a : α
c : γ
⊢ cast e a ≍ c ↔ a ≍ c

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β γ : Sort u_1
e : β = γ
a : α
b : β
⊢ a ≍ cast e b ↔ a ≍ b

Tactic:
by subst e; rfl

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

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

Tactic:
by
  subst hα
  have : ∀ a, f a ≍ f' a := fun a ↦ h a a (HEq.refl a)
  have : β = β' := by funext a; exact type_eq_of_heq (this a)
  subst this
  grind

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
x✝⁴ x✝³ x✝² : β
x✝¹ : Relation.Map r f f x✝⁴ x✝³
x✝ : Relation.Map r f f x✝³ x✝²
x y : α
hxy : r x y
hx : f x = x✝⁴
hy : f y = x✝³
y' z : α
hyz : r y' z
hy' : f y' = x✝³
hz : f z = x✝²
⊢ Relation.Map r f f x✝⁴ x✝²

Tactic:
exact ⟨x, z, trans_of r hxy <| trans_of r (hf y y' <| hy' ▸ hy) hyz, hx, hz⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case 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 b : α
h₁ : ReflGen r a b
⊢ ReflGen r a b

Tactic:
exact h₁

Goal state after:
Module: Mathlib.Logic.Relation

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

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

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ : α
h : EqvGen r i✝¹ i✝
⊢ EqvGen p i✝¹ i✝

Tactic:
induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc

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

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by simpa using h 1

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

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by simpa using h 1

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

Goal state before:
pp: case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂

Tactic:
simpa using hr 1

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁵ : SMul M α
inst✝⁴ : SMul M N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • n) • a = m • n • a

Tactic:
by
    rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]

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

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

Tactic:
simp only [LeftTotal, IsEmpty.exists_iff, isEmpty_iff]

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝ * c✝) x✝ = (a✝ * (b✝ * c✝)) x✝

Tactic:
exact mul_assoc _ _ _

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
intros; ext; exact mul_inv_rev _ _

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by intros; ext; exact mul_inv_rev _ _

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.lt
⊢ compare a b = Ordering.lt.swap

Tactic:
simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.eq
⊢ compare a b = Ordering.eq.swap

Tactic:
simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.gt
⊢ compare a b = Ordering.gt.swap

Tactic:
simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

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

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

Tactic:
rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ≤ ⊥ ⊔ z ↔ x ≤ z

Tactic:
bot_sup_eq

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ≤ z ↔ x ≤ z
Module: Mathlib.Order.Disjoint

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

Tactic:
isCompl_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ Disjoint x y ∧ Codisjoint x y ↔
    (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: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x

Tactic:
by
  rintro rfl
  exact (hf.reflect_lt h2).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h1)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ IsCompl ↑a ↑b ↔ IsCompl a b

Tactic:
isCompl_iff,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Disjoint ↑a ↑b ∧ Codisjoint ↑a ↑b ↔ Disjoint a b ∧ Codisjoint a b
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Tactic:
rw [Set.subset_pair_iff_eq, or_iff_right]

Goal state after:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_sdiff_cancel_right h

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ max b c

Tactic:
· rw [le_sup_iff, or_iff_right h]

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

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

Tactic:
bot_sup_eq

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ ⊔ ⊥ = ⊥

Tactic:
bot_sup_eq

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}

Tactic:
by
  simp_rw [← union_singleton, union_sdiff_distrib,
    sdiff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]

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

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

Tactic:
inf_bot_eq,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
bot_sup_eq

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_bot_eq,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
bot_sup_eq

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y = x ⊓ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by
  rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]

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

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

Tactic:
rw [sdiff_sdiff_right_self, inf_of_le_right h]

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

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

Tactic:
inf_bot_eq,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ ⊓ y \ z = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ a \ b = a

Tactic:
by rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
bot_sup_eq

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

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

Tactic:
bot_sup_eq

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

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ IsCompl a b

Tactic:
isCompl_iff,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ Disjoint a b ∧ Codisjoint a b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ IsCompl a b

Tactic:
isCompl_iff,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ Disjoint a b ∧ Codisjoint a b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)

Tactic:
simp_rw [Set.symmDiff_def, image_union, image_sdiff hf]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ (range fun o ↦ o.elim b f) = insert b (range f)

Tactic:
range_eq

Goal state after:
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ insert (none.elim b f) (range ((fun o ↦ o.elim b f) ∘ some)) = insert b (range f)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : f a' = a
⊢ a * b = b * a

Tactic:
have ⟨b', hb'⟩ := is_surj b

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : f a' = a
b' : M
hb' : f b' = b
⊢ a * b = b * a
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 s t
⊢ ∀ (x : α), x ∈ s → ¬f x = f a

Tactic:
exact fun _ hx h₂ ↦ hfa (h₂ ▸ h.mapsTo hx)

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✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
f.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✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f x * f y * g (x * y) = f x * g x * (f y * g y)
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✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
f.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✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ f x * f y * g (x * y) = f x * g x * (f y * g y)
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ Injective fun a ↦ a ^ Int.negSucc n

Tactic:
by simpa using! inv_injective.comp (pow_left_injective n.succ_ne_zero)

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]

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

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

Tactic:
rw [div_eq_mul_inv, one_div]

Goal state after:
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
x : M₁
⊢ f (x ^ 0) = f 1

Tactic:
rw [zpow, zpow_zero, one]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = 1

Tactic:
← h.unit.mul_inv

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b

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

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ (n + 1) • a = n • a + a

Tactic:
change (n + 1) • a = n • a + a; rw [add_nsmul, one_nsmul]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b

Tactic:
rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)

Tactic:
by
  rw [mk_mul_mk, mul_one]

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

Tactic:
by
  rw [mk_mul_mk, mul_one]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ x✝ <* y✝ = Function.const β✝ <$> x✝ <*> y✝

Tactic:
casesm Sum _ _ <;> rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝

Tactic:
casesm Sum _ _ <;> rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : e ⊕ (α✝ → β✝)
x✝ : e ⊕ α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    f✝ <*> x✝

Tactic:
casesm Sum _ _ <;> rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
casesm Sum _ _ <;> rfl

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

Goal state before:
pp: case pos
α : 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 : α
hx : p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

pp: case neg
α : 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 : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
· exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx

Goal state after:
case neg
α : 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 : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h
  · rw [h, pow_zero]
  · rw [zero_pow h]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀ β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
g : α →*₀ β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| a * b

Tactic:
rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| 1
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) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
← zpow_add_one₀ ha,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1 + 1) * a⁻¹ = a ^ n * 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:
by
      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.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

Tactic:
rw [← succ_mul]; exact le_of_lt_succ (lt_succ_sqrt n)

Goal state after: