mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set (α × α)
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
⊢ range (if p then f else g) ⊆ range f ∪ range g

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ (range fun x ↦ if p x then f x else g x) ⊆ range f ∪ range g

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
⊢ ∅.pi s = univ

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
t : (i : ι) → Set (α i)
⊢ (univ.pi fun i ↦ if i ∈ s then t i else univ) = s.pi t

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t t₁ : (i : ι) → Set (α i)
⊢ (s.pi fun i ↦ t i ∩ t₁ i) = s.pi t ∩ s.pi t₁

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s₁ = s₂
h' : ∀ (i : ι), i ∈ s₁ → t₁ i = t₂ i
⊢ s₁.pi t₁ = s₂.pi t₂

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
⊢ s.pi t = ∅

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
s : Set ι
t : (i : ι) → Set (α i)
⊢ (insert i s).pi t = eval i ⁻¹' t i ∩ s.pi t

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
t : (i : ι) → Set (α i)
⊢ {i}.pi t = eval i ⁻¹' t i

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t

Tactic:
ext x
  rw [mem_image]
  exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ range val = s

Tactic:
← image_univ

Goal state after:
α : Type u_1
s : Set α
⊢ val '' univ = s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
s : Set ι
⊢ s.pi t ∩ sᶜ.pi t = univ.pi t

Tactic:
by grind

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}

Tactic:
image_singleton,

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {f x} = f '' {x'}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {f x} = f '' {x'}

Tactic:
image_singleton,

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {f x} = {f x'}
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
heq : EqOn f₁ f₂ s
⊢ f₁ '' s = f₂ '' s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Set α
f : α → α
h : EqOn f id s
⊢ f '' s = s

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
⊢ update a i b ∈ s.pi t ↔ a ∈ (s \ {i}).pi t ∧ (i ∈ s → b ∈ t i)

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
x✝ : a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
i : ι
h₁ : a ∈ univ.pi t
h₂ : ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
⊢ a i ∈ t i

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i) → a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
κ : Type u_4
α : Type u_5
s : Set ι
t : Set κ
u : ι × κ → Set α
⊢ uncurry ⁻¹' (s ×ˢ t).pi u = s.pi fun i ↦ t.pi fun j ↦ u (i, j)

Tactic:
by grind

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f a * f b = 1

Tactic:
rw [← map_mul, h, map_one]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a⁻¹ = a ↔ a = 1

Tactic:
rw [eq_comm, self_eq_inv]

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
⊢ (range fun a ↦ x ⋯) ⊆ s

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' f '' s

Tactic:
rw [h x]

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
a₂ : α₂
ha₂ : a₂ ∈ s₂
hx₂ : f₂ a₂ = x.2
⊢ x ∈ (fun x ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Tactic:
exact ⟨(a₁, a₂), ⟨ha₁, ha₂⟩, Prod.ext hx₁ hx₂⟩

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

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

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]

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

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

Tactic:
inv_mul_cancel_left

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

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

Tactic:
inv_mul_cancel_left

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℤ
⊢ P (g ^ n)

Tactic:
induction n with
  | zero => rwa [zpow_zero]
  | succ n ih =>
    rw [Int.add_comm, zpow_add, zpow_one]
    exact h_mul _ ih
  | pred n ih =>
    rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
    exact h_inv _ ih

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

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

Tactic:
inv_mul_cancel_left

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

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

Tactic:
inv_mul_cancel_left

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ b = b
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
inv_mul_cancel_left

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
⊢ IsUnit a

Tactic:
have : IsUnit (a * ↑u * ↑u⁻¹) := by exists v * u⁻¹; rw [← hv, Units.val_mul]
      rwa [mul_assoc, Units.mul_inv, mul_one] at this

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

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

Tactic:
inv_mul_cancel_left

Goal state after:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : ↑b * a = c
⊢ a = a
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
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
⊢ g 1 = 1

Tactic:
ext; rw [h 1]; exact f.map_one

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

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

Tactic:
inv_mul_cancel_left

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ a = a
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑(1 + n) = 1 + ↑n

Tactic:
Nat.cast_add,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑1 + ↑n = 1 + ↑n
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
b : G₀
⊢ 0 ^ 2 * b / 0 = 0 * b

pp: case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a ^ 2 * b / a = a * b

Tactic:
· simp

Goal state after:
case inr
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ a ^ 2 * b / a = a * b
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n - ↑m.succ = -↑(m + 1) + ↑n

Tactic:
sub_eq_iff_eq_add,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n = -↑(m + 1) + ↑n + ↑m.succ
Module: Mathlib.Data.Nat.Sqrt

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

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

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: ⊢ ¬Even 1

Tactic:
by grind

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

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

Tactic:
by grind

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

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

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

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

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

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

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

Tactic:
by grind

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

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

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

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

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

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: case zero
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f 0 = g 0

pp: case succ
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
· simp

Goal state after:
case succ
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)
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
⊢ IsUnit a ∧ ¬IsUnit b ∨ ¬IsUnit a ∧ IsUnit b ∨ IsUnit a ∧ IsUnit b

Tactic:
by grind

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ 0⁻¹ʳ = 0⁻¹

pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹

Tactic:
· simp

Goal state after:
case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ ↑n • b = n • b

Tactic:
induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

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

Goal state before:
pp: n : ℕ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
⊢ ¬Odd n ↔ Even n

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
⊢ ¬Even n ↔ Odd n

Tactic:
by grind

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

Goal state before:
pp: ⊢ ¬Odd 0

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ ¬2 ∣ n

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
⊢ Xor (Even n) (Odd n)

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
hn : Odd n
⊢ m % 2 + (m + n) % 2 = 1

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ Even (m - n)

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
by grind

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

Goal state before:
pp: n e : ℕ
he : e ≠ 0
⊢ Odd (n ^ e) ↔ Odd n

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
hm : Odd m
hn : Even n
⊢ Odd (m - n)

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
hm : Even m
hn : Odd n
⊢ Odd (m - n)

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ 2 * (n / 2) + 1 = n

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ n / 2 * 2 + 1 = n

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ 1 + n / 2 * 2 = n

Tactic:
by grind

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

Goal state before:
pp: case zero
⊢ 2 ∣ 0 * (0 - 1)

pp: case succ
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)

Tactic:
· simp

Goal state after:
case succ
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ ((-a) ^ 2) ^ c = (a ^ 2) ^ c

Tactic:
zpow_two,

Goal state after:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a * -a) ^ c = (a * a) ^ c
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a - b = a + d - d - b

Tactic:
by rw [add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ c + b - b - d = c - d

Tactic:
by rw [add_tsub_cancel_right]

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

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

Tactic:
rw [← inv_lt_inv_iff, inv_inv]

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

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

Tactic:
rw [← inv_lt_inv_iff, inv_inv]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a c : α
h : a ≤ a
⊢ a * c ≤ a * c

pp: case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c

Tactic:
· simp

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ 1 ≤ a * a ↔ 1 ≤ a

Tactic:
exact one_le_mul_self_iff

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (a + a * b) ≤ a * (2 + b)

Tactic:
rw [mul_add, mul_two, add_assoc]

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 : G₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
ha : 0 ≤ a
h : a ≤ b
⊢ b ∈ {a | 0 ≤ a}

Tactic:
by grind

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 : G₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 < n
ha : 0 ≤ a
h : a < b
⊢ b ∈ {a | 0 ≤ a}

Tactic:
by grind

Goal state after: