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

Goal state before:
pp: case inl
n : Nat
h : n % 2 = 0
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
| _ h =>

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

Goal state before:
pp: case inr
n : Nat
h : n % 2 = 1
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
| _ h =>

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
ih : motive n
h : ¬(n = 0 → b = true)
⊢ Nat.bit b n = 0

Tactic:
bit_eq_zero_iff

Goal state after:
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
ih : motive n
h : ¬(n = 0 → b = true)
⊢ n = 0 ∧ b = false
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:
case =>

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

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ b * a * a⁻¹ = b

Tactic:
mul_inv_cancel_right

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ b = b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b a : G
⊢ a⁻¹⁻¹ = a

Tactic:
by exact inv_eq_of_mul (inv_mul_cancel a)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ c * a * a⁻¹ = c

Tactic:
mul_inv_cancel_right

Goal state after:
G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ c = c
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ b * a * a⁻¹ = b

Tactic:
mul_inv_cancel_right

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

Goal state before:
pp: α β : Sort u_2
γ : Sort u_3
f : α → γ
g : β → γ
x : α
y : β
h₁ : f ≍ g
h₂ : x ≍ y
⊢ f x = g y

Tactic:
by
  cases h₂; cases h₁; rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a

Tactic:
simp [eq_comm]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p

Tactic:
simp [eq_comm]

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ f = update f a b ↔ f a = b

Tactic:
by simp [eqComm]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)

Tactic:
induction ha with

Goal state after:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)
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) → DivInvMonoid (f i)
n✝ : ℕ
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ ^ ↑n✝.succ) x✝ = (a✝ ^ ↑n✝ * a✝) x✝

Tactic:
exact DivInvMonoid.zpow_succ' _ _

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝¹ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝¹ a a
le_trans✝¹ : ∀ (a b c : α), le✝¹ a b → le✝¹ b c → le✝¹ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝¹ a b ∧ ¬le✝¹ b a
le✝ B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff }.toLE =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }.toLE →
    { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }

Tactic:
rintro ⟨⟩

Goal state after:
α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
    { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

Tactic:
by
  simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x

Tactic:
rw [h.symm.inf_eq_bot, sup_bot_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y

Tactic:
by
  constructor
  · rintro rfl x
    exact (gc x y).symm
  · intro H
    exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

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

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

Tactic:
by simp [Set.ite]

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

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

Tactic:
by simp [Set.ite]

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

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

Tactic:
by simp [Set.ite]

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

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

Tactic:
by simp [Set.ite]

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

Goal state before:
pp: α : Type u_1
t s : Set α
⊢ t.ite ∅ s = s \ t

Tactic:
by simp [Set.ite]

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

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

Tactic:
by simp [Set.ite]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ≤ b ∆ a ↔ Disjoint a b

Tactic:
le_symmDiff_iff_left,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint b a ↔ Disjoint a b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ s → f x = f y → x = y
b : β
x✝ : b ∈ f '' s ∩ f '' t
a₁ : α
ha₁ : a₁ ∈ s
h₁ : f a₁ = b
a₂ : α
ha₂ : a₂ ∈ t
h₂ : f a₂ = b
⊢ f a₂ = f a₁

Tactic:
by simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Tactic:
refine (range_extend_subset _ _ _).antisymm ?_
  rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
  exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ range (t.restrictPreimage f) = Subtype.val ⁻¹' range f

Tactic:
simp only [← image_univ, ← image_restrictPreimage, preimage_univ]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩

Tactic:
obtain ⟨a, ha, rfl⟩ := h' hb

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ ∃ a_1, restrict f s t h a_1 = ⟨f a, hb⟩
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
by simp [*]

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

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : ¬i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
by simp [*]

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

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Tactic:
apply piecewise_le <;> intros

Goal state after:
case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : i✝ ∈ s
⊢ f₁ i✝ ≤ s.piecewise g₁ g₂ i✝

case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : ¬i✝ ∈ s
⊢ f₂ i✝ ≤ s.piecewise g₁ g₂ i✝
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁

Tactic:
heq,

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
⊢ (f '' s).Nontrivial

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := hs
  exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

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

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : p i
⊢ f i ∈ t₁ i

Tactic:
simpa [*] using h i

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

Goal state before:
pp: case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i

Tactic:
simpa [*] using h i

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

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

Tactic:
rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
⊢ InjOn g (range f)

Tactic:
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → y x_1 ∈ {x x_1}

Tactic:
simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
⊢ EqOn g₁ g₂ t

Tactic:
intro b hb
  obtain ⟨a, ha, rfl⟩ := hf' hb
  exact hf ha

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
by simp [*]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
by simp [*]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
rcases eq_or_ne j i with rfl | h

Goal state after:
case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
j : ι
a : M j
⊢ mulSingle j (ofAdd a) j = ofAdd (single j a j)

case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)
Module: Mathlib.Algebra.Group.TypeTags.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
rcases eq_or_ne j i with rfl | h

Goal state after:
case inl
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
a : M j
⊢ single j (ofMul a) j = ofMul (mulSingle j a j)

case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
mul_inv_cancel_right

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

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

Tactic:
mul_inv_cancel_right

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

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

Tactic:
← zpow_add_one,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
⊢ ↑u⁻¹ = 1 /ₚ u

Tactic:
by rw [one_divp]

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ f ↑u * f u.inv = 1

Tactic:
simp [← map_mul]

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
u : Mˣ
⊢ f u.inv * f ↑u = 1

Tactic:
simp [← map_mul]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a * ↑c = b
⊢ a = a * ↑c * ↑c⁻¹

Tactic:
mul_inv_cancel_right

Goal state after:
α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a * ↑c = b
⊢ a = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = c * ↑b
⊢ c * ↑b * ↑b⁻¹ = c

Tactic:
mul_inv_cancel_right

Goal state after:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = c * ↑b
⊢ c = c
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ a * ↑u * ↑u⁻¹ = a

Tactic:
mul_inv_cancel_right

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ a = a
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : FunLike F M N
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ f ↑h.unit⁻¹ * ↑⋯.unit = 1

Tactic:
simp [← map_mul]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * b ↔ a = 0 ∨ b = 0

Tactic:
by simp [eqComm]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (f x) (f y) = swap (f x) (f y) * f * f⁻¹

Tactic:
mul_inv_cancel_right

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (f x) (f y) = swap (f x) (f y)
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x

Tactic:
← swap_apply_apply,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap ((swap y z) x) ((swap y z) y) = swap z x
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: R : Type v
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d

Tactic:
simp [right_distrib]

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

Goal state before:
pp: n : ℤ
⊢ sqrt (n * n) = ↑n.natAbs

Tactic:
sqrt,

Goal state after:
n : ℤ
⊢ ↑(n * n).toNat.sqrt = ↑n.natAbs
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: n : ℕ
⊢ sqrt ↑n = ↑n.sqrt

Tactic:
sqrt,

Goal state after:
n : ℕ
⊢ ↑(↑n).toNat.sqrt = ↑n.sqrt
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
a : α
f : F
x✝ : IsSquare a
r : α
h✝ : a = r * r
⊢ f a = f r * f r

Tactic:
by simp [*]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hf : Function.Surjective ⇑f
b : β
x✝ : b ∈ {b | IsSquare b}
r : α
h✝ : b = f r * f r
⊢ r * r ∈ {a | IsSquare a} ∧ f (r * r) = b

Tactic:
by simp [*]

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

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

Tactic:
simp [← Nat.two_mul, hm]

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

Goal state before:
pp: m✝ n✝ m n : ℤ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
simp +decide [*, parity_simps]

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

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

Tactic:
obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind

Goal state after:
case 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⁻¹ʳ

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⁻¹ʳ

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: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1

Tactic:
exact inv_mul_cancel₀ (zpow_ne_zero n ha)

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ c / a * (a / b) = c / b

Tactic:
div_mul_div_cancel₀ ha

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ c / b = c / b
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : αˣ
⊢ ↑a = -1 ↔ a = -1

Tactic:
by
  rw [← Units.coe_neg_one, val_inj]

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

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b

Tactic:
rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]

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

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

Tactic:
refine ⟨2 * a * b + b + a, ?_⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * a + ↑u⁻¹ * a

Tactic:
rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a⁻¹ * a ≤ b * a ↔ 1 ≤ b * a

Tactic:
rw [inv_mul_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a * b ≤ b⁻¹ * b ↔ a * b ≤ 1

Tactic:
rw [inv_mul_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a⁻¹ * a < b * a ↔ 1 < b * a

Tactic:
rw [inv_mul_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a * b < b⁻¹ * b ↔ a * b < 1

Tactic:
rw [inv_mul_cancel]

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a b : M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ 2 = b ^ 2 ↔ a = b

Tactic:
simp [ha, hb]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ (1 + b) * (1 - c)

Tactic:
by
  rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr

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₀
a b c : G₀
hc : 0 < c
⊢ a ≤ c⁻¹ * b ↔ c * a ≤ b

Tactic:
by
  rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

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₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ c * a

Tactic:
by
  rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Goal state after: