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

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

Tactic:
rw [mul_comm, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.Logic.Basic

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

Tactic:
rw [forall_and, forall_const]

Goal state after:
Module: Mathlib.Logic.Basic

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

Tactic:
rw [forall_and, forall_const]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
⊢ Nonempty (Unique α)

Tactic:
inhabit α

Goal state after:
α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty (Unique α)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') g₂
x : α
H : g₁ x = g₂ x
⊢ g₁ x = g₂ x

Tactic:
exact H

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)

Tactic:
iterate_add f m n

Goal state after:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
by rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

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 : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
⊢ b₁ = b₂

Tactic:
inhabit α

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabited_h : Inhabited α
⊢ b₁ = b₂
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ∃ f, StrictMono f

Tactic:
inhabit α

Goal state after:
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ f, StrictMono f
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case ind
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
by_cases heq : f 0 = f 1
    · have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
      exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩
    · have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
      let g (i : ℕ) := f (i + 1)
      have hg_anti : Antitone g := by grind [Antitone]
      obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl
      refine ⟨p + 1, by omega, fun m hm => ?_⟩
      specialize hp' (m - 1) (by lia)
      grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ a ≤ a ⊔ b

Tactic:
rw [← le, map_sup]

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f a ≤ f a ⊔ f b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ b ≤ a ⊔ b

Tactic:
rw [← le, map_sup]

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f b ≤ f a ⊔ f b
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: case mp
α : Type u
s : Set α
⊢ Subsingleton ↑s → s.Subsingleton

pp: case mpr
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton ↑s

Tactic:
· intro h a ha b hb
    exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)

Goal state after:
case mpr
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton ↑s
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
by simp_rw [himp_himp, inf_comm]

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

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

Tactic:
rw [sup_comm, sup_inf_sdiff]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a : α
⊢ ⊥ ≤ a

Tactic:
rw [← inf_inf_sdiff a a, inf_assoc]
    exact inf_le_left

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 ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c

Tactic:
exact sdiff_le_iff

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c

Tactic:
exact sdiff_le_iff

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

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

Tactic:
by rw [inf_idem]

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

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

Tactic:
sdiff_sdiff_right

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
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
f : ℕ → Type u
⊢ RightInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)) fun x ↦
    Sigma.casesOn x fun n ↦
      Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩

Tactic:
rintro (x | ⟨n, x⟩) <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ range m₁ ×ˢ range m₂ ↔ x ∈ range fun p ↦ (m₁ p.1, m₂ p.2)

Tactic:
by simp [range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m₁ : α → γ
⊢ ∀ (x : γ × β), x ∈ range m₁ ×ˢ univ ↔ x ∈ range fun p ↦ (m₁ p.1, p.2)

Tactic:
by simp [range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
m₂ : β → δ
⊢ ∀ (x : α × δ), x ∈ univ ×ˢ range m₂ ↔ x ∈ range fun p ↦ (p.1, m₂ p.2)

Tactic:
by simp [range]

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
· refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)
    grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Prod.snd '' graphOn f s = f '' s

Tactic:
ext x; simp

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
hf : Injective ⇑f
inst✝ : IsDedekindFiniteMonoid N
a✝ b✝ : M
eq : a✝ * b✝ = 1
⊢ f (b✝ * a✝) = f 1

Tactic:
by simpa [mul_eq_one_comm] using congr_arg f eq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
by
  rw [invFunOn, dif_pos h]
  exact Classical.choose_spec h

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

Goal state before:
pp: case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ (k : ℤ) → m ≤ k → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k + 1 → motive k_1

Tactic:
intro _n _ ih l _

Goal state after:
case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝¹ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
a✝ : l < _n + 1
⊢ motive l
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ 1 = 1⁻¹

Tactic:
inv_one

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1⁻¹ = 1

Tactic:
inv_one

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 = 1
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✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ 1⁻¹ = 1

Tactic:
inv_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✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

Tactic:
simp_rw [isDedekindFiniteMonoid_iff, ← opEquiv.forall_congr_right]

Goal state after:
α : Type u_1
inst✝ : MulOne α
⊢ (∀ (a a_1 : α), opEquiv a * opEquiv a_1 = 1 → opEquiv a_1 * opEquiv a = 1) ↔ ∀ {a b : α}, a * b = 1 → b * a = 1
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:
pow_sub a⁻¹ h,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
⊢ f a c = f a b * f b c

Tactic:
have : Std.Symm (p · ∧ p ·) := { symm _ _ := And.symm }

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x * ↑((liftRight f g h) x)⁻¹ = 1

Tactic:
by
  rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]

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

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

Tactic:
rw [divp_mul_cancel, one_mul]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * swap y z = swap z x

Tactic:
nth_rewrite 3 [← swap_inv]
  rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁵ : MulZeroOneClass α
inst✝⁴ : MulZeroOneClass β✝
inst✝³ : MulZeroOneClass γ
inst✝² : MulZeroOneClass δ
inst✝¹ : FunLike F α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ (↑(↑f * ↑g)).toFun 0 = 0

Tactic:
by dsimp; rw [map_zero, zero_mul]

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

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

Tactic:
exact mul_self_div_self a

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:
by
  rw [isRegular_iff, isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1⁻¹ = -1

Tactic:
inv_one

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1 = -1
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ Nontrivial (Option α)

Tactic:
inhabit α

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nontrivial (Option α)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x✝ : IsUnit 0
a : M₀
a0 : 0 * a = 1
inv_val✝ : a * 0 = 1
⊢ 0 = 1

Tactic:
rwa [zero_mul] at a0

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

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

Tactic:
pow_sub₀ _ (inv_ne_zero ha) h,

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
rintro ⟨c, rfl⟩ a; simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a b : M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ 1 ≤ b ^ 1

Tactic:
simpa using hab

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
x✝ : 1 ≠ 0
⊢ a ^ 1 < b ^ 1

Tactic:
simpa using hab

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ a ^ (n + 1) < a ^ n

Tactic:
have : ZeroLEOneClass M₀ := ⟨(h₀.trans h₁).le⟩

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) < a ^ n
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hb : b ≤ 0
h : a ≤ 1
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

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✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hb : b ≤ 0
h : 1 ≤ a
⊢ a * b ≤ b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

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✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
have or_c := le_total 0 c

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
or_c : 0 ≤ c ∨ c ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
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

Tactic:
rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ d * c ≤ max a c * max d b

Tactic:
by simpa [mul_comm, max_comm] using cd

Goal state after:
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✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2
⊢ ∀ {a b : α}, f.toEmbedding a ≤ f.toEmbedding b ↔ a ≤ b

Tactic:
by
      simp [le_iff_lt_or_eq, f.map_rel_iff, f.injective.eq_iff]

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

Goal state before:
pp: case mp
n : ℕ
x : ℤ
h : ↑n = x * x
⊢ IsSquare n

pp: case mpr
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n

Tactic:
· exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩

Goal state after:
case mpr
n x : ℕ
h : n = x * x
⊢ IsSquare ↑n
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑|n|

Tactic:
by
  rw [← natCast_natAbs, Int.cast_natCast]

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

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
let a := a_n % q.succ

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
simp [← sub_self_eq_zero_of_ne_top hb, hb]

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

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

Tactic:
rw [tsub_zero] at h

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a : α
ha : AddLECancellable a
h : a < a
⊢ False
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
⊢ MulLeftReflectLT (WithZero α)

Tactic:
by
  refine ⟨fun a b c h => ?_⟩
  have := h.ne_zero
  induction a
  · simp at this
  induction c
  · simp at this
  induction b
  exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
⊢ 0 < ⌈a⌉₊ ↔ 0 < a

Tactic:
by rw [lt_ceil, cast_zero]

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 < ⌈a⌉ ↔ 0 < a

Tactic:
by rw [lt_ceil, cast_zero]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ (fun a ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ ↑n

Tactic:
by rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
simp [floor_lt, le_floor_iff, hb, ha]

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

Goal state before:
pp: case h₁
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉₊

Tactic:
apply le_ceil

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

Goal state before:
pp: case h₂
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉₊

Tactic:
apply le_ceil

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t

Tactic:
image2_inter_union_subset_union,

Goal state after:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f t s ∪ image2 f s t ⊆ image2 f s t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c

pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}

Tactic:
· have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
    exact
      ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
        eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inl (Subset.antisymm hc ?_)

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s