mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.AdaptationNote

Goal state before:
pp: ⊢ True

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Tactic:
by

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

Goal state before:
pp: α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
⊢ (-if P then b else c) = if P then -b else -c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: c : Permutation
x✝ : { l // 2 ≤ l.length }
⊢ 2 ≤ x✝.val.reverse.length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r✝ r : ArgReorder
n : Nat
cycle : { l // 2 ≤ l.length }
⊢ cycle.val ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: n : Nat
map✝¹ : Vector (Option (Fin n)) n
map✝ : Vector (Option (Fin n)) n := map✝¹
perm✝ : List { l // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
__r✝² : Option Permutation := __s✝¹.fst
__s✝ : Vector (Option (Fin n)) n × List { l // 2 ≤ l.length } := __s✝¹.snd
map : Vector (Option (Fin n)) n := __s✝.fst
perm : List { l // 2 ≤ l.length } := __s✝.snd
j✝ : Fin n
j : Fin n := j✝
__r✝ : Unit
⊢ 2 ≤ [i, ↑j].length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: n : Nat
map✝³ : Vector (Option (Fin n)) n
map✝² : Vector (Option (Fin n)) n := map✝³
perm✝ : List { l // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
__r✝⁷ : Option Permutation := __s✝⁴.fst
__s✝³ : Vector (Option (Fin n)) n × List { l // 2 ≤ l.length } := __s✝⁴.snd
map✝¹ : Vector (Option (Fin n)) n := __s✝³.fst
perm : List { l // 2 ≤ l.length } := __s✝³.snd
j✝² : Fin n
j✝¹ : Fin n := j✝²
__r✝⁵ : Unit
cycle✝ : { l // 2 ≤ l.length } := ⟨[i, ↑j✝¹], ⋯⟩
x✝ : Unit
__r✝³ : Option Permutation := __s✝².fst
__s✝¹ : Vector (Option (Fin n)) n × Fin n × { l // 2 ≤ l.length } := __s✝².snd
map✝ : Vector (Option (Fin n)) n := __s✝¹.fst
__s✝ : Fin n × { l // 2 ≤ l.length } := __s✝¹.snd
j✝ : Fin n := __s✝.fst
cycle : { l // 2 ≤ l.length } := __s✝.snd
j' : Fin n
map : Vector (Option (Fin n)) n := map✝.set! (↑j✝) none
__r✝¹ : Unit
j : Fin n := j'
⊢ 2 ≤ (cycle.val ++ [↑j]).length

Tactic:
by

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

Goal state before:
pp: n : Nat
⊢ bit (decide (n % 2 = 1)) (n >>> 1) = n

Tactic:
by

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

Goal state before:
pp: n : Nat
⊢ bit (n.testBit 0) (n >>> 1) = n

Tactic:
by

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

Goal state before:
pp: n : Nat
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false

Tactic:
by

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

Goal state before:
pp: n : Nat
b : Bool
⊢ bit b n ≠ 0 ↔ n = 0 → b = true

Tactic:
by

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

Goal state before:
pp: b : Bool
x n : Nat
⊢ bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
by

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

Goal state before:
pp: n : Nat
hn : n >>> 1 ≠ 0
⊢ n ≠ 0

Tactic:
by

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

Goal state before:
pp: n : Nat
hn : n >>> 1 ≠ 0
⊢ 0 < 2

Tactic:
by

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

Goal state before:
pp: n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ 2 ≠ 0

Tactic:
by

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:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n = 2 * n + b.toNat

Tactic:
by

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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n / 2 = n

Tactic:
by

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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n % 2 = b.toNat

Tactic:
by

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

Goal state before:
pp: b : Bool
n : Nat
⊢ (bit b n).testBit 0 = b

Tactic:
by

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

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)
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

Tactic:
by

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)
⊢ binaryRec' zero bit 0 = zero

Tactic:
by

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)
⊢ 0 = 0 → true = true

Tactic:
by

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)
⊢ binaryRec' zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero

Tactic:
by

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
⊢ (if h : 0 = 0 → false = true then bit false 0 h zero
      else
        have this := ⋯;
        ⋯ ▸ zero) =
      zero ∨
    (n = 0 → b = true)

Tactic:
by

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

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
⊢ binaryRecFromOne zero one bit 1 = one

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
⊢ binaryRecFromOne zero one bit (Nat.bit b n) = bit b n h (binaryRecFromOne zero one bit n)

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ SemiconjBy a 1 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x : G
⊢ SemiconjBy a x (a * x * a⁻¹)

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Irrefl r
a : α
⊢ ¬Decidable.decide (r a a) = true

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Refl r
a : α
⊢ Decidable.decide (r a a) = true

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
a b c : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b c) = true → Decidable.decide (r a c) = true

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Symm r
a b : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b a) = true

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r a b

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r b a

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Asymm r
a b : α
⊢ Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Total r
a b : α
⊢ Decidable.decide (r a b) = true ∨ Decidable.decide (r b a) = true

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Trichotomous r
a b : α
⊢ ¬Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true → a = b

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : Std.Antisymm r
a b : α
⊢ a = b → r a b ∧ r b a

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Symm r
inst✝ : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
⊢ r a c ↔ r b d

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
b c : S
h : Commute b c
a : S
⊢ a * b * c = a * c * b

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
h : Commute a b
c : S
⊢ a * (b * c) = b * (a * c)

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
b c : S
hbc : Commute b c
a d : S
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
m n : ℕ
⊢ Commute (a ^ m) (b ^ n)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
rw [pow_zero, pow_zero, pow_zero, one_mul]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
by

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

Tactic:
by

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
⊢ a * (b * a⁻¹) = b

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
reg : IsLeftRegular a
⊢ Commute (a * b) a ↔ Commute a b

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
reg : IsRightRegular a
⊢ Commute (b * a) a ↔ Commute a b

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ IsCancelMul R ↔ ∀ (r : R), IsRegular r

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
⊢ IsMulCommutative M ↔ ∀ (a b : M), a * b = b * a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
this : one₁ = one₂
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₂, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec' (2 * k) m = npowRec' k (m * m)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
k0 : k ≠ 0
m : M
⊢ m * npowRec' k m = npowRec' k m * m

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec (k + 1) m = 1 * npowRec' (k + 1) m

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ k' ≠ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ 2 * k' ≠ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ go (k + 1) m n = m * npowRec' (k + 1) n

Tactic:
by

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

Goal state before:
pp: ⊢ @npowRecAuto = @npowBinRecAuto

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 = a

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ (0 + 1) = a * a ^ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
n : ℕ
⊢ (a * b) ^ n * a = a * (b * a) ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ n * a = a * a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 2 = a * a

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * a * a

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * (a * a)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
⊢ 1 ^ (n + 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: b : Prop
α : Sort u_2
i : Nonempty α
inst✝ : Subsingleton α
⊢ (∃! x, b) ↔ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
a' : α
⊢ ∃! a, a = a'

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
a' : α
⊢ ∃! a, a' = a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: p q : Prop
⊢ (∃! x, q) ↔ p ∧ q

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x, ∃! h, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃! hx, q x hx

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x, ∃! hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
⊢ ¬∃! x, x ∈ [] ∧ p x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : p x
h : ∀ (y : α), y ∈ xs → p y → x = y
⊢ (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) x ∧ ∀ (y : α), (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : p x
x✝ : ∃! x_1, x_1 ∈ x :: xs ∧ p x_1
y : α
hy : y ∈ xs
hp : p y
z : α
h : (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) z ∧ ∀ (y : α), (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = z
⊢ z = y

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m * 0) = (a ^ m) ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : ¬p x
this : Decidable (∃! x, x ∈ xs ∧ p x)
⊢ (∃! x, x ∈ xs ∧ p x) ↔ ∃! x_1, x_1 ∈ x :: xs ∧ p x_1

Tactic:
by

Goal state after: