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) → (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

Tactic:
]

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
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 true 0 = Nat.bit true 0

Tactic:
]

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

Goal state before:
pp: b : Bool
n : Nat
⊢ n = n

pp: b : Bool
n : Nat
⊢ b.toNat < 2

pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
]

Goal state after:
b : Bool
n : Nat
⊢ b.toNat < 2

case H
b : Bool
n : Nat
⊢ 0 < 2
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
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n

Tactic:
]

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n
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
⊢ (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)

Tactic:
]

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.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
⊢ ∀ (e : motive (Nat.bit b n) = motive (Nat.bit b n)),
    e ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)

Tactic:
]

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
⊢ ∀ (e : motive (Nat.bit b n) = motive (Nat.bit b n)),
    e ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)
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)
⊢ zero = zero

Tactic:
]

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

pp: case hc
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:
]

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

Tactic:
]

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)
⊢ (have this := ⋯;
    ⋯ ▸ one) =
    one

Tactic:
]

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
⊢ bit b n h
      (binaryRec' zero
        (fun b n h ih ↦
          if h' : n = 0 then
            have this := ⋯;
            ⋯ ▸ one
          else bit b n h' ih)
        n) =
    bit b n h
      (binaryRec' zero
        (fun b n h ih ↦
          if h' : n = 0 then
            have this := ⋯;
            ⋯ ▸ one
          else bit b n h' ih)
        n)

Tactic:
]

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'
⊢ y * y' * a = y * y' * a

Tactic:
]

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1

Tactic:
]

Goal state after:
case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1

Tactic:
exact SemiconjBy.one_right _

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

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

Tactic:
]

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ n * y)
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x

Tactic:
]

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

Tactic:
]

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * (x * b⁻¹) = b * y * a * b⁻¹ ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

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

Tactic:
]

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * a * b⁻¹ ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

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

Tactic:
]

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

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

Tactic:
]

Goal state after:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x y b : G
⊢ a * x = y * a ↔ a * x = y * a

Tactic:
]

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
⊢ y * a = y * a

Tactic:
]

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 b d ↔ r b d

Tactic:
]

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
⊢ 1 = 1

Tactic:
]

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

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 = b

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : Mul R
⊢ (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
]

Goal state after:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a
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
⊢ a * npowRec n a = a * npowRec n a

Tactic:
]

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m

Tactic:
]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case bit
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
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 b k' ≠ 0
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n

Tactic:
]

Goal state after:
case bit
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
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 b k' ≠ 0
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case bit.true
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
⊢ m * (n * npowRec' (2 * k') n) = m * (n * npowRec' (2 * k') n)

Tactic:
]

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

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m

Tactic:
]

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

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
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m

Tactic:
]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
]

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowRecAuto n m * m
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 = b

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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 + (n + 1))

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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 * a ^ m = (a ^ m) ^ n * a ^ m

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ y * z = 1

Tactic:
]

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ y * z = 1
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ z * x = 1

Tactic:
]

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ z * x = 1
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = x⁻¹

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * (b * c⁻¹) = a * (b * c⁻¹)

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a = a

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a * a = a * a

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : a * b = 1
⊢ a = a

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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 ↦ a * x) b = (fun x ↦ a * x) c
⊢ c = c

Tactic:
]

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 = c

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x

Tactic:
classical
  exact Decidable.exists_ne x

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ∃ x, ¬f x = g x
⊢ Nontrivial β

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ∃ x, ¬f x = g x
⊢ Nontrivial β
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
⊢ Nontrivial α ↔ Nontrivial α

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α

Tactic:
]

Goal state after:
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ f y' = f y'

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
⊢ (b = a) = (b = a)

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ (b ↔ a) = (b ↔ a)

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = c ↔ a = c

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ b = a ↔ b = a

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: β : Sort u
b a : β
h : a = cast ⋯ b
⊢ b ≍ b

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Tactic:
]

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x

Tactic:
]

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
q : Prop
p : α → Prop
⊢ (q ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Nonempty α
p : α → Prop
q : Prop
⊢ (∀ (x : α), p x) ∧ q ↔ (∀ (x : α), p x) ∧ q

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b c : α
⊢ P ∧ a = c ∨ ¬P ∧ b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ ¬P ∧ a ≠ b ↔ ¬P ∧ a ≠ b

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ P ∧ a ≠ b ↔ P ∧ a ≠ b

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p default

Tactic:
]

Goal state after:
α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p default
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ default = default

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f default ≍ Function.const α (f default) x✝¹

Tactic:
]

Goal state after:
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f default ≍ Function.const α (f default) x✝¹
Module: Mathlib.Logic.Unique

Goal state before:
pp: α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α default

Tactic:
]

Goal state after:
α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α default
Module: Mathlib.Logic.Unique

Goal state before:
pp: A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f

Tactic:
]

Goal state after:
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
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:
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: