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

Goal state before:
pp: ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ (if h : ∃ a, f a = x then r • g (Classical.choose ⋯) else r • e x) =
    r • if h : ∃ a, f a = x then g (Classical.choose h) else e x

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ∃ a, f a = x
⊢ r • g (Classical.choose ⋯) = r • g (Classical.choose h✝)

case neg
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ¬∃ a, f a = x
⊢ r • e x = r • e x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (univ.pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j ↦ t j (f j)

Tactic:
compl_eq_univ_sdiff,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (univ.pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ (univ \ {i}).pi fun j ↦ t j (f j)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ p₂ (f a) = g (p₁ a)

Tactic:
by rw [comm a]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a ^ n = 1 ^ n

Tactic:
one_pow

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a ^ n = 1
Module: Mathlib.Data.Int.Init

Goal state before:
pp: ⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Tactic:
by
  lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
⊢ (a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h

Tactic:
split_ifs

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

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
h✝ : ¬p
⊢ a ^ c h✝ = a ^ c h✝
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
⊢ (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c

Tactic:
split_ifs

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

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
h✝ : ¬p
⊢ b h✝ ^ c = b h✝ ^ c
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
one_pow

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]

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

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

Tactic:
h1

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝¹ : f z = x
h✝ : z = f⁻¹ x
⊢ y = f (f⁻¹ y)

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ y = f (f⁻¹ x)

case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ y = f z

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : f z = y
h✝ : z = f⁻¹ x
⊢ x = f (f⁻¹ y)

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ x = f (f⁻¹ x)

case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ x = f z

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : ¬f z = y
h✝ : z = f⁻¹ x
⊢ f z = f (f⁻¹ y)

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ f z = f (f⁻¹ x)

case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ f z = f z
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
⊢ ↑(if P then m else n) = if P then ↑m else ↑n

Tactic:
split_ifs

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

case neg
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : ¬P
⊢ ↑n = ↑n
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
⊢ (a • if p then b else 0) = if p then a • b else 0

Tactic:
split_ifs

Goal state after:
case pos
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : p
⊢ a • b = a • b

case neg
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : ¬p
⊢ a • 0 = 0
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • -x = r • x

Tactic:
rw [neg_smul, smul_neg, neg_neg]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)

Tactic:
by
  aesop (add simp Commute.mul_zpow)

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

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

Tactic:
rcases mod_two_eq_zero_or_one m with h₁ | h₁

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

case inr
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0

Tactic:
by simp [← sub_eq_add_neg, h]

Goal state after:
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 : f x * f x + f (y * x) + (f (x * y) + f (y * y)) = (f x + f y) * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
h y,

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 : f x * f x + f (y * x) + (f (x * y) + f y * f y) = (f x + f y) * (f x + f y)
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * (x⁻¹ʳ * x) = y

Tactic:
inverse_mul_cancel x h,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * 1 = y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ x⁻¹ʳ * x * y = y

Tactic:
inverse_mul_cancel x h,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ 1 * y = y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
h1

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ m = a ^ m
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 - n) = a ^ m / a ^ n

Tactic:
by
  rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
a : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a ^ 2 = 1 ^ 2

Tactic:
one_pow

Goal state after:
R : Type u
inst✝¹ : Ring R
a : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a ^ 2 = 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ 1 ^ n = 1

Tactic:
one_pow

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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
inst✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
Int.cast_negSucc,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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
inst✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f (-↑(n + 1)) = -↑(n + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ -1 ^ n = -1

Tactic:
one_pow

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ -1 = -1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
⊢ f = id

Tactic:
rwa [hf.iterate_even hn, eq_comm] at H

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

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

Tactic:
by
  rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
by
  rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
by
  simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
⊢ ∃ a, 1 < a

Tactic:
by
  obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)
  obtain h | h := hy.lt_or_gt
  · exact ⟨y⁻¹, one_lt_inv'.mpr h⟩
  · exact ⟨y, 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 b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c⁻¹ * b
⊢ c * a ≤ b

Tactic:
by
  obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_inv_mul_iff₀ hc] at h

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
⊢ ((if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) = if h : p ↑y then Sum.inl ⟨↑y, h⟩ else Sum.inr ⟨↑y, ⋯⟩) →
    x = y

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : p ↑y
⊢ Sum.inl ⟨↑x, h✝¹⟩ = Sum.inl ⟨↑y, h✝⟩ → x = y

case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : ¬p ↑y
⊢ False → x = y

case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : p ↑y
⊢ False → x = y

case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : ¬p ↑y
⊢ Sum.inr ⟨↑x, ⋯⟩ = Sum.inr ⟨↑y, ⋯⟩ → x = y
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case ha
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
⊢ 0 ≤ a

pp: case hb
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
⊢ 0 < c

Tactic:
exacts [ha, hc]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

Tactic:
simp only [← not_lt, one_lt_inv_iff₀, not_and_or]

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

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
f : β → M
hf : StrictMono f
n : ℕ
x✝ : n.succ.succ ≠ 0
⊢ StrictMono fun x ↦ f x ^ n.succ.succ

Tactic:
simpa only [pow_succ] using (hf.pow_const n.succ_ne_zero).mul' hf

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

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
⊢ Monotone fun a ↦ f a ^ 0

Tactic:
by simpa using monotone_const

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

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a ↦ f a ^ (n + 1)

Tactic:
by
    simp_rw [pow_succ]
    exact (Monotone.pow_const hf _).mul' hf

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

Goal state before:
pp: z : ℤ
hz : z ≠ 0
⊢ ↑z.sign.natAbs = 1

Tactic:
natAbs_sign_of_ne_zero hz,

Goal state after:
z : ℤ
hz : z ≠ 0
⊢ ↑1 = 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n

Tactic:
by
  obtain ⟨k, rfl⟩ := h
  cases k with
  | ofNat k =>
    rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]
  | negSucc k =>
    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
    norm_cast
    simp [pow_add]

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

Goal state before:
pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c

Tactic:
rw [← (self_le_mul_right a c).lt_iff_ne]
    apply lt_mul_of_one_lt_right'

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

Goal state before:
pp: case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 ^ (m / m.gcd n) = 1

Tactic:
one_pow

Goal state after:
case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 ^ (n / m.gcd n) = 1

Tactic:
one_pow

Goal state after:
case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c

Tactic:
convert! tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)

Tactic:
by
  rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
by
  refine ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩
  rintro rfl
  exact h'.ne' hc.add_tsub_cancel_right

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 α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a - (a - b) = min a b

Tactic:
by
  rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
⊢ ⋯.choose ≤ c ↔ ⋯.choose + b ≤ c + b

Tactic:
rw [add_le_add_iff_right]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]

Tactic:
have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
    simpa [(negSucc_lt_zero n).not_ge, ← sub_eq_add_neg, le_neg] using this.not_ge

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
a : α
⊢ ↑a ≤ ⊥ ↔ ↑a = ⊥

Tactic:
simp [not_coe_le_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ a * c⁻¹ < b

Tactic:
contrapose! h
  simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le zero_le h

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

Goal state before:
pp: case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ if P (m✝ + 1) then m✝ + 1 else findGreatest P m✝

Tactic:
split_ifs

Goal state after:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : P (m✝ + 1)
⊢ findGreatest P m ≤ m✝ + 1

case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
n : { x_1 // x ≤ ↑x_1 } := Classical.indefiniteDescription (fun x_1 ↦ x ≤ ↑x_1) above
m : ℤ
hm : ↑m ≤ x
⊢ m ≤ ↑n

Tactic:
rw [← Int.cast_le (R := α)]

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
n : { x_1 // x ≤ ↑x_1 } := Classical.indefiniteDescription (fun x_1 ↦ x ≤ ↑x_1) above
m : ℤ
hm : ↑m ≤ x
⊢ ↑m ≤ ↑↑n
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
⊢ { n // ↑n ≤ x ∧ ∀ (m : ℤ), ↑m ≤ x → m ≤ n }

Tactic:
by
  let n := Classical.indefiniteDescription _ above
  refine Int.greatestOfBdd (P := (· ≤ x)) n.1 (fun m hm ↦ ?_) below
  rw [← Int.cast_le (R := α)]
  exact hm.trans n.2

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
n : ℤ
⊢ n ≤ ↑(floorAux below above) → ↑n ≤ x

Tactic:
rw [← Int.cast_le (R := α)]

Goal state after:
α : Type u_4
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
n : ℤ
⊢ ↑n ≤ ↑↑(floorAux below above) → ↑n ≤ x
Module: Mathlib.Order.Directed

Goal state before:
pp: β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
⊢ ¬IsMin b

Tactic:
intro hb'
  obtain ⟨a, c, hac⟩ := exists_lt_of_directed_le β
  have := hb.isTop a
  obtain rfl := (hb' <| this).antisymm this
  exact hb'.not_lt hac

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ 1 ^ n = 1

Tactic:
one_pow

Goal state after:
α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
rw [H₁.floor_of_neg, H₂.floor_of_neg]

Goal state after:
case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0

case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b

Tactic:
by
  simpa only [← sub_eq_add_neg] using dvd_add_left (dvd_neg.2 h)

Goal state after: