mathlib-initiative/mathlib-tactics huggingface dataset:
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 + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
← Nat.add_assoc,

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 + (n + 1) + 1) a = npowRec m a * npowRec (n + 1 + 1) a
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:
Nat.add_assoc

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ (m + (n + 1))
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
β₂ : α₁ → Sort v
f₂ : (a : α₁) → β₂ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₁ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₁

Tactic:
cases funext fun v => ht v v .rfl

Goal state after:
case refl.refl
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
f₂ : (a : α₁) → β₁ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₁
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Refl r
x y : α
hr : x ≠ y → r x y
⊢ r x y

Tactic:
by
  grind [Std.Refl]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c

Tactic:
by
  induction hbc with
  | single hbc => exact tail' hab hbc
  | tail _ hcd hac => exact hac.tail hcd

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

Goal state before:
pp: case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + k + 1))

Tactic:
Nat.add_assoc

Goal state after:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
⊢ FaithfulSMul R A ↔ Injective fun r ↦ r • 1

Tactic:
by
  refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
  · simp only at hr
    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
  · simpa using hr 1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
by
      inhabit δ
      obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
      exact ⟨a, congr_arg Prod.fst h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
⊢ ∃ a, g a = d

Tactic:
inhabit γ
      obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
      exact ⟨b, congr_arg Prod.snd h⟩

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ compareOfLessAndEq (f x✝¹) (f x✝) = compareOfLessAndEq x✝¹ x✝

Tactic:
compareOfLessAndEq,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ (if f x✝¹ < f x✝ then Ordering.lt else if f x✝¹ = f x✝ then Ordering.eq else Ordering.gt) =
    if x✝¹ < x✝ then Ordering.lt else if x✝¹ = x✝ then Ordering.eq else Ordering.gt
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
⊢ False

Tactic:
obtain ⟨M, hM, hM'⟩ := hind x hx hx'

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
M : α
hM : M > x
hM' : P M
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + (m + 1) ≤ f (n + (m + 1))

Tactic:
← Nat.add_assoc,

Goal state after:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m + 1 ≤ f (n + (m + 1))
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m + 1 ≤ f (n + (m + 1))

Tactic:
← Nat.add_assoc,

Goal state after:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m + 1 ≤ f (n + m + 1)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b ≤ a ⊓ b ↔ a = b

Tactic:
by simp [le_antisymm_iff, and_comm]

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y

Tactic:
by rw [← inf_inf_sdiff, sup_inf_sdiff]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
  rw [symmDiff_eq_sup_sdiff_inf] at h
  exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
ext ⟨x, y⟩
  simp [and_assoc, and_left_comm]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (s.pi fun j ↦ t j (update f i a j)) = ({i} ∪ s \ {i}).pi fun j ↦ t j (update f i a j)

Tactic:
by
        rw [union_sdiff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t

Tactic:
by
  rwa [SurjOn, ← H.image_eq]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * y⁻¹ = x / y

Tactic:
div_eq_mul_inv

Goal state after:
G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * y⁻¹ = x * y⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
simp only [one_div, inv_pow]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f x / f y = f x * (f y)⁻¹

Tactic:
div_eq_mul_inv

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f x * (f y)⁻¹ = f x * (f y)⁻¹
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
div_eq_mul_inv

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]

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

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

Tactic:
simp [Int.add_left_neg]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f (x / y) = f (x * y⁻¹)

Tactic:
div_eq_mul_inv

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f (x * y⁻¹) = f (x * y⁻¹)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case inl
α : 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
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c

Tactic:
exact hmul' rbc pab pbc pac

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)

Tactic:
div_eq_mul_inv

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
by simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Goal state after:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Tactic:
rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : (ofSubtype x) ↑a = (ofSubtype y) ↑a
⊢ x a = y a

Tactic:
ofSubtype_apply_coe,

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : ↑(x a) = (ofSubtype y) ↑a
⊢ x a = y a
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : ↑(x a) = (ofSubtype y) ↑a
⊢ x a = y a

Tactic:
ofSubtype_apply_coe,

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : ↑(x a) = ↑(y a)
⊢ x a = y a
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case pos
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
⊢ lt l hlm = Int.strongRec lt ge l

Tactic:
strongRec_of_lt hlm

Goal state after:
case pos
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
⊢ lt l hlm = lt l hlm
Module: Mathlib.Algebra.Group.Even

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

Tactic:
by simp [IsSquare, pow_two]

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

Goal state before:
pp: 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

Tactic:
isLeftRegular_iff_right_eq_zero_of_mul,

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → IsLeftRegular a, ∀ {a : R}, a ≠ 0 → IsRightRegular a,
      ∀ {a : R}, a ≠ 0 → IsRegular a].TFAE

Tactic:
isLeftRegular_iff_right_eq_zero_of_mul,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → IsRightRegular a,
      ∀ {a : R}, a ≠ 0 → IsRegular a].TFAE
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : 2 = 0 ∨ f (x * y) = f x * f y
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
or_iff_not_imp_left

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : ¬2 = 0 → f (x * y) = f x * f y
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y / y')

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ m * (a ^ n)⁻¹ = a ^ m / a ^ n

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ m * (a ^ n)⁻¹ = a ^ m * (a ^ n)⁻¹
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
⊢ IsUnit 2

Tactic:
obtain ⟨a, ha⟩ := h 1

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = a + a
⊢ IsUnit 2
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
by
  simp [*, parity_simps]

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

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

Tactic:
obtain rfl | h := eq_or_lt_of_le h
    · simp
    · simpa [mul_comm] using (hmul _ _ _ h).le

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ d ≤ c

Tactic:
· grw [hab] at h
    · exact le_of_mul_le_mul_of_pos_left h <| ha.trans_le hab
    · exact hc.le

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₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a / b

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
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₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
simp_rw [← not_le, ← or_iff_not_imp_left]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a / b ≤ 0

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a / c

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c / d

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c * d⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a * b⁻¹ < c / d

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c / d

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a / b ≤ 0

Tactic:
div_eq_mul_inv

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: ⊢ IsCompl {n | Even n} {n | Odd n}

Tactic:
by
  simp [← not_even_iff_odd, ← Set.compl_ofPred, isCompl_compl]

Goal state after: