mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
rw [isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, ← forall_and]

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: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 * a = a * a

Tactic:
pow_one

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a * a = a * a
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
pow_one

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a = a
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
by rw [zpow_ofNat, pow_two]

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

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

Tactic:
by
  rw [mul_comm, inv_mul_cancel_right]

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → α
a : α
⊢ foldl (fun b x ↦ f b) a [] = f^[[].length] a

Tactic:
| nil =>

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
⊢ Sort ?u.25

Tactic:
haveI := comp α g; haveI := comp β g; exact IsScalarTower N α β

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy x (r • a) (r • b)

Tactic:
by
  rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy (r • x) a b

Tactic:
by
  rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i

Tactic:
exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ le_trans a (h h')⟩

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ < a₂
h₂ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
by
  simp [lt_iff, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ ≤ a₂
h₂ : b₁ < b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
by
  simp [lt_iff, *]

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a b : ι
⊢ rangeFactorization f a = rangeFactorization f b ↔ f a = f b

Tactic:
by
  simp [Set.rangeFactorization]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
induction b using WellFoundedLT.induction generalizing a' with | ind b ihb

Goal state after:
case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
by
    suffices h : ∀ a, ∀ a' ≤ a, ∀ b, Acc (· < ·) (a', b) from ⟨fun x => h x.1 x.1 le_rfl x.2⟩
    intro a a' ha b
    induction a using WellFoundedLT.induction generalizing a' b with | ind a iha
    induction b using WellFoundedLT.induction generalizing a' with | ind b ihb
    refine Acc.intro (a', b) fun x hx => ?_
    obtain ⟨ha', hb⟩ | ⟨ha', hb⟩ := Prod.lt_iff.1 hx
    · exact iha x.1 (ha'.trans_le ha) x.1 le_rfl x.2
    · exact ihb x.2 hb x.1 (ha'.trans ha)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Antitone f

Tactic:
antitone_toDual_comp_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Monotone (f ∘ ⇑ofDual) ↔ Antitone f
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
· exact h_anti h₁

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i
Module: Mathlib.Data.Set.Disjoint

Goal state before:
pp: α : Type u
β : Sort u_1
γ : Sort u_2
x : β → α
y : γ → α
⊢ Disjoint (range x) (range y) ↔ ∀ (i : β) (j : γ), x i ≠ y j

Tactic:
by
  simp [Set.disjoint_iff_forall_ne]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a = b ⊓ a

Tactic:
rw [inf_comm, inf_himp, inf_comm]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a s \ t ⊆ insert a (s \ t)

Tactic:
rintro b ⟨rfl | hbs, hbt⟩

Goal state after:
case inl
α : Type u_1
s t : Set α
b : α
hbt : ¬b ∈ t
⊢ b ∈ insert b (s \ t)

case inr
α : Type u_1
s t : Set α
a b : α
hbt : ¬b ∈ t
hbs : b ∈ s
⊢ b ∈ insert a (s \ t)
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ insert a t) = insert a (s \ t)

Tactic:
rw [← union_singleton (s := t), ← sdiff_sdiff, insert_sdiff_singleton]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
by rw [inf_assoc, hd.eq_bot, inf_bot_eq]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
⊢ BiheytingAlgebra α

Tactic:
let heytingAlgebra := e.heytingAlgebra

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ BiheytingAlgebra α
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : OrderTop α
a b : α
⊢ a \ b = a ⊓ ⊤ \ b

Tactic:
rw [← inf_sdiff_assoc, inf_top_eq]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥

Tactic:
← inf_inf_distrib_left,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ (b ⊓ bᶜ) = ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')

Tactic:
grind [eq_def, coe_trans]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
⊢ a ∆ b = b \ a

Tactic:
by
  rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π i

Tactic:
rw [← f.2 i]; exact (f.1 i).2

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a ∆ b ⊔ b

Tactic:
convert! symmDiff_triangle a b ⊥ <;> rw [symmDiff_bot]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a \ ￢a

Tactic:
sup_sdiff_self

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f

Tactic:
· exact ⟨f a, funext fun x ↦ hf _ _⟩

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

Goal state before:
pp: case mp.inl.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]

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

Goal state before:
pp: case mp.inl.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]

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

Goal state before:
pp: case mp.inr.inl
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ s
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]

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

Goal state before:
pp: case mp.inr.inr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h2 : ¬x.1 = x.2
h1 : x.2 ∈ t
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
simp [h0, h1, h2]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = (fun x ↦ (x.1, f x.1)) '' s

Tactic:
EqOn.image_eq_self

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = s

case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ EqOn (fun x ↦ (x.1, f x.1)) id 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 : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)

Tactic:
exact h.injOn_image ha.injOn hf

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✝ : DivisionMonoid 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₁
h : x * y = 1
⊢ (f x)⁻¹ = f y

Tactic:
inv_eq_of_mul_eq_one_right (by rw [← mul, h, one])

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✝ : DivisionMonoid 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₁
h : x * y = 1
⊢ f y = f y
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x /ₚ u * ↑u = y * ↑u ↔ y * ↑u = x

Tactic:
rw [divp_mul_cancel]; exact ⟨Eq.symm, Eq.symm⟩

Goal state after:
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✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ (MonoidHom.mk' (fun u ↦ { val := (↑u).1, inv := (↑u⁻¹).1, val_inv := ⋯, inv_val := ⋯ }) ⋯)
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹), val_inv := ⋯, inv_val := ⋯ } =
      u₁ ∧
    (MonoidHom.mk' (fun u ↦ { val := (↑u).2, inv := (↑u⁻¹).2, val_inv := ⋯, inv_val := ⋯ }) ⋯)
        { val := (↑u₁, ↑u₂), inv := (↑u₁⁻¹, ↑u₂⁻¹), val_inv := ⋯, inv_val := ⋯ } =
      u₂

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

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

Tactic:
apply eq_inv_of_mul_eq_one_right

Goal state after:
case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x * g • x⁻¹ = 1
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a

Tactic:
constructor <;> intro h <;> simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

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

Goal state before:
pp: case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one n with h₂ | h₂

Goal state after:
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one n with h₂ | h₂

Goal state after:
case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case nil
a b : Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) [a, b]
h_last : [].getLastD b → a
⊢ [a, b].TFAE

Tactic:
| nil =>

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1

Tactic:
simp only [Units.ext_iff]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (x * -y) = f (-(x * y))

Tactic:
rw [neg, mul, neg, mul_neg, mul]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd (a + a + (2 * b + 1))

Tactic:
exact ⟨a + b, by rw [mul_add, ← two_mul, add_assoc]⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : IsMulCommutative α
⊢ PosMulReflectLE α ↔ MulPosReflectLE α

Tactic:
simp [posMulReflectLE_iff, mulPosReflectLE_iff, mul_comm']

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
exact mul_lt_mul_right (h.lt_of_ne h') a |>.ne

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulOneClass α
inst✝ : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b

Tactic:
by
  simpa only [one_mul] using id

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 c : α
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
by
    contrapose! h
    exact hmul _ _ _ h

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
ha : 0 < ↑a
⊢ b < c

Tactic:
· exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h

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 : G₀
⊢ 0 ≤ a⁻¹ ↔ 0 ≤ a

Tactic:
by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
⊢ 0 ≤ a⁻¹ ↔ 0 ≤ a

Tactic:
by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 ≤ 0 ∧ 0 ≤ r ^ 2

Tactic:
and_iff_left (sq_nonneg r)

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c

Tactic:
inv_mul_le_iff₀ hc,

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a ≤ c * b / d ↔ a * d ≤ c * b

Tactic:
le_div_iff₀ hd

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a * d ≤ c * b ↔ a * d ≤ c * b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
⊢ ∀ {a b : α}, f.toEmbedding a < f.toEmbedding b ↔ a < b

Tactic:
simp [lt_iff_le_not_ge, f.map_rel_iff]

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

Goal state before:
pp: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|

Tactic:
rw [Int.ediv_neg, abs_neg]; apply this

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a⁻¹

Tactic:
simpa using inv_mabs_le a⁻¹

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (a.xgcdAux s t b s' t')

Tactic:
xgcdAux_rec h

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y ((b % a).xgcdAux (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
by
  refine ⟨fun h => ⟨h.pos, pos_of_ne_zero ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
  rintro rfl
  rw [tsub_zero] at h
  exact h.false

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

Goal state before:
pp: m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ P (findGreatest P n)

Tactic:
by_cases h : Nat.findGreatest P n = 0

Goal state after:
case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ 0 ≤ 1

Tactic:
simpa only [Nat.cast_one] using natCast_nonneg 1

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

Goal state before:
pp: α : Type u_4
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
by
  refine ⟨_, fun n ↦ ⟨?_, (floorAux below above).2.2 _⟩⟩
  rw [← Int.cast_le (R := α)]
  exact le_trans' (floorAux below above).2.1

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

Goal state before:
pp: x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ ∃ k, exp (-↑k) < x

Tactic:
use (-y.log).toNat

Goal state after:
case h
x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ exp (-↑(-y.log).toNat) < x
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
· exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

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

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a ^ 2

Tactic:
rw [sq]; exact mul_pos_of_neg_of_neg ha ha

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅

Tactic:
simp [not_nonempty_iff_eq_empty]

Goal state after: