mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
⊢ a = a

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
⊢ a = cast ⋯ a

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
⊢ cast ⋯ a = a

Tactic:
rfl

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

Goal state before:
pp: case neg
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match -[(b - z - 1).toNat+1] with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
grind

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ succ n hmn
      (Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) n m (fun x ↦ base)
        (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction base succ n hmn)

Tactic:
rfl

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ pred n hnm
      (Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) n m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
        (fun k hle ih x ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
rfl

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

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ - -[m+1] = ↑m + 1

Tactic:
rfl

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

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ invFun f (f a) ∈ s ↔ f a ∈ f '' s

Tactic:
leftInverse_invFun hf,

Goal state after:
case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ a ∈ s ↔ f a ∈ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (range fun a ↦ x ⋯) ⊆ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
x✝ : α
⊢ (x✝ ∈ range fun a ↦ x ⋯) → ∀ ⦃x₂ : α⦄, (x₂ ∈ range fun a ↦ x ⋯) → f x✝ = f x₂ → x✝ = x₂

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : p
⊢ a ^ b h✝ = a ^ b h✝

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : ¬p
⊢ a ^ c h✝ = a ^ c h✝

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : p
⊢ a h✝ ^ c = a h✝ ^ c

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : ¬p
⊢ b h✝ ^ c = b h✝ ^ c

Tactic:
rfl

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

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1

Tactic:
(rintro rfl; simpa using h)

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

Goal state before:
pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1

Tactic:
(rintro rfl; simpa using h)

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * c * d = a * c * b * d

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = a ^ ↑(n + 1)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = a ^ ↑(m * n)

Tactic:
rfl

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

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

Tactic:
Int.ofNat_mul_negSucc,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (-↑(m * n.succ)) = (a ^ (m * (n + 1)))⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m.succ * ↑n.succ) = a ^ ↑((m + 1) * (n + 1))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc : p b✝ c✝
pac : p a c✝
b c : α
rbc : r b c
pab : p a b
⊢ p b c → p a c → f a c = f a b * f b c

Tactic:
pbc

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
⊢ p a c → f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]

Tactic:
rfl

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

Goal state before:
pp: M : Type u
inst✝ : Monoid M
x✝ : Mˣ
⊢ ↑((map (MonoidHom.id M)) x✝) = ↑((MonoidHom.id Mˣ) x✝)

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : CommMonoid M
f g : G →* M
x✝ : G
⊢ ↑((f * g).toHomUnits x✝) = ↑((f.toHomUnits * g.toHomUnits) x✝)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x x✝ : M
⊢ ↑⋯.unit = f x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
rwa [LeftCancelMonoid.eq_one_of_mul_right h, one_mul] at h

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a * a⁻¹ * b⁻¹ = b⁻¹

Tactic:
h.mul_inv_cancel,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ 1 * b⁻¹ = b⁻¹
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h ↦ h f) ∘ Function.comp) <$> x <*> y = (fun x ↦ x ∘ f) <$> x <*> y

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: case id_map.inl
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e
⊢ id <$> inl x✝ = inl x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: case id_map.inr
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : α✝
⊢ id <$> inr x✝ = inr x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: case comp_map.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e
⊢ (h✝ ∘ g✝) <$> inl x✝ = h✝ <$> g✝ <$> inl x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: case comp_map.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr x✝ = h✝ <$> g✝ <$> inr x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
α✝ β✝ : Type u
g✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ pure g✝ <*> x✝ = g✝ <$> x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun a ↦ (fun p ↦ f p.fst p.snd) ∘ fun a_1 ↦ (a_1, a)) <$> b <*> a = (fun b a ↦ f a b) <$> b <*> a

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝ : Monoid α
⊢ Monoid.toMulAction αᵐᵒᵖ = instMulAction

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ x ^ (n.succ * N) = 0

Tactic:
Nat.succ_mul,

Goal state after:
n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ x ^ (n * N + N) = 0
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
⊢ 0⁻¹ = 0

Tactic:
rw [← zero, ← inv, inv_zero]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : P
⊢ ↑m = ↑m

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : ¬P
⊢ ↑n = ↑n

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) = ↑(2 * ((k + 1) / 2))

Tactic:
Nat.succ_mul,

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) = ↑(1 * ((k + 1) / 2) + (k + 1) / 2)
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
inv_zero,

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

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

Tactic:
inv_zero,

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ 0 * 0 * 0 = 0
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑(2 * ((k + 1) / 2) + 1)

Tactic:
Nat.succ_mul,

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑(1 * ((k + 1) / 2) + (k + 1) / 2 + 1)
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
inv_zero,

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ 0 * 0 * 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
inv_zero,

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ 0 * 0 * 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ n = 0

Tactic:
zero_pow

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 = 0

G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ g • 0⁻¹ = (g • 0)⁻¹

Tactic:
inv_zero,

Goal state after:
case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ g • 0 = (g • 0)⁻¹
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : n.sqrt = 1
⊢ n.sqrt < 2

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n

Tactic:
grind

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

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ n * n + a < n.succ * n.succ

Tactic:
grind

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

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ n * n ≤ n * n + a

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : n.sqrt = 0
this : n.sqrt < 1 ↔ n < 1 * 1
⊢ n = 0

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ n = 0 → n.sqrt = 0

Tactic:
grind

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

Goal state before:
pp: m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
⊢ IsSquare a ↔ ∃ r, a = r ^ 2

Tactic:
simp [IsSquare, pow_two]

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

Goal state before:
pp: n : ℕ
h : n % 2 = 0
⊢ n = n / 2 + n / 2

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ n ↔ n % 2 = 1

Tactic:
grind

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

Goal state before:
pp: ⊢ ¬Even 1

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: case zero
m n : ℕ
⊢ Even (m ^ 0) ↔ Even m ∧ 0 ≠ 0

Tactic:
grind

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

Goal state before:
pp: case succ
m n n✝ : ℕ
a✝ : Even (m ^ n✝) ↔ Even m ∧ n✝ ≠ 0
⊢ Even (m ^ (n✝ + 1)) ↔ Even m ∧ n✝ + 1 ≠ 0

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≠ 0
⊢ Even (m ^ n) ↔ Even m

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ Even (n * (n + 1))

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ Even (n * (n - 1))

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
hn : Even n
⊢ 1 < n

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
hn : Even n
hm : Even m
hnm : n < m
⊢ n + 1 < m

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

Tactic:
grind

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

Goal state before:
pp: n : ℤ
h : n % 2 = 0
⊢ n = n / 2 + n / 2

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬2 ∣ n ↔ n % 2 = 1

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even (n - 1) ↔ ¬Even n

Tactic:
grind

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

Goal state before:
pp: case zero
m : ℤ
⊢ Even (m ^ 0) ↔ Even m ∧ 0 ≠ 0

Tactic:
grind

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

Goal state before:
pp: case succ
m : ℤ
n✝ : ℕ
a✝ : Even (m ^ n✝) ↔ Even m ∧ n✝ ≠ 0
⊢ Even (m ^ (n✝ + 1)) ↔ Even m ∧ n✝ + 1 ≠ 0

Tactic:
grind

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

Goal state before:
pp: m : ℤ
n : ℕ
h : n ≠ 0
⊢ Even (m ^ n) ↔ Even m

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even n → 2 * (n / 2) = n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even n → n / 2 * 2 = n

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
⊢ a ↔ a

Tactic:
rfl

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0

Tactic:
isRegular_iff,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
⊢ IsLeftRegular r ∧ IsRightRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
x✝ : α
⊢ (comp 0 f) x✝ = 0 x✝

Tactic:
rfl

Goal state after: