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

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ (n + 1))

Tactic:
pow_succ

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ n * y)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)

Tactic:
hg b

Goal state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b✝ c✝ : α
hab : TransGen r a b✝
hbc : r b✝ c✝
h_ih : motive hab
⊢ motive ⋯

Tactic:
| tail hab hbc h_ih =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b : α
h : TransGen r a b
⊢ r a b

Tactic:
by
      induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x.out ≈ y.out ↔ x = y

Tactic:
rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)

Tactic:
simp only [hf'.eq, hf.eq, comp_apply]

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), a / b = a * b⁻¹

Tactic:
by intros; ext; exact div_eq_mul_inv _ _

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
⊢ ¬IsMax a

Tactic:
intro ha'

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝¹ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝¹ a a
le_trans✝¹ : ∀ (a b c : α), le✝¹ a b → le✝¹ b c → le✝¹ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝¹ a b ∧ ¬le✝¹ b a
le✝ B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff }.toLE =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }.toLE →
    { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }

Tactic:
by
    rintro ⟨⟩
    have : A_lt = B_lt := by
      funext a b
      rw [A_iff, B_iff]
    cases this
    congr

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False

Tactic:
rcases hne.2.1.lt_or_gt with h₂ | h₂

Goal state after:
case inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False

case inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False

Tactic:
rcases hne.2.1.lt_or_gt with h₂ | h₂

Goal state after:
case inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False

case inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.gt a b := hab
    rwa [ho.inj (h hab)]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b

Tactic:
rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u
inst✝⁴ : Lattice α
inst✝³ : DecidableEq α
inst✝² : DecidableLE α
inst✝¹ : DecidableLT α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ (a b : α), a ⊔ b = if a ≤ b then b else a

Tactic:
exact congr_fun₂ sup_eq_maxDefault

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

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

Tactic:
rw [inf_sup_right, inf_comm x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]

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

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

Tactic:
insert_sdiff_singleton

Goal state after:
α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ t) = insert a (s \ t)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Tactic:
simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤

Tactic:
rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ (a \ b) \ a ⊔ (b \ a) \ a = b \ a

Tactic:
sdiff_idem,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ (a \ b) \ a ⊔ b \ a = b \ a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b \ c ⊔ (c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)

Tactic:
sup_comm (c ⊓ a ⊓ b),

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b \ c ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ s.piecewise f g x ≠ s.piecewise f g y ↔ f x ≠ g y

Tactic:
piecewise_eq_of_mem s f g hx,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ f x ≠ s.piecewise f g y ↔ f x ≠ g y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ ({x | x i ∈ s} ∩ {i}ᶜ.pi fun j ↦ univ) = eval i ⁻¹' s

Tactic:
pi_univ,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ {x | x i ∈ s} ∩ univ = eval i ⁻¹' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = ⟨y, ⋯⟩
⊢ f ↑x = y

Tactic:
rw [hfg, hx, Subtype.coe_mk]

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

Goal state before:
pp: a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a ≤ c - b ↔ 0 < c - b

Tactic:
le_iff_pos_of_dvd ha hab

Goal state after:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ 0 < c - b ↔ 0 < c - b
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by
  rw [← mul_div_assoc, div_mul_cancel]

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

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

Tactic:
zpow_zero

Goal state after:
case zero
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
⊢ P 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
zpow_zero

Goal state after:
case zero
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
⊢ P 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✝ : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = 1

Tactic:
rw [← npow, pow_zero, ← one]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ a ^ ↑n.succ = a ^ ↑n * a

Tactic:
by simp only [HPow.hPow, Pow.pow]; simp [pow_succ]

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:
by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [inv_mul_cancel₀ h, one_mul]

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

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ 0 = 1

Tactic:
zpow_zero

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x : A
⊢ r • (-x + x) = 0

Tactic:
neg_add_cancel,

Goal state after:
M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x : A
⊢ r • 0 = 0
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
cases e : n - m

Goal state after:
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑(match 0 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑(match n✝ + 1 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n
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 + r) • x = 0

Tactic:
neg_add_cancel,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ 0 • x = 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 s : R
y : M
⊢ (r - s) • y = r • y - s • y

Tactic:
simp [add_smul, sub_eq_add_neg]

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

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ (-a + a) * b = 0

Tactic:
neg_add_cancel,

Goal state after:
α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ 0 * b = 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * (-b + b) = 0

Tactic:
neg_add_cancel,

Goal state after:
α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * 0 = 0
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: n : ℤ
⊢ ↑(n.natAbs * n.natAbs).sqrt = ↑n.natAbs

Tactic:
Nat.sqrt_eq

Goal state after:
n : ℤ
⊢ ↑n.natAbs = ↑n.natAbs
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ n✝ * a ∣ b ^ (n✝ + 1)

Tactic:
pow_succ

Goal state after:
case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ n✝ * a ∣ b ^ n✝ * b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
· exact pow_sub₀ _ ha <| Nat.le_of_lt h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a b : R
h : Commute a b
⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Tactic:
by
  simp [sq, add_mul, mul_add, two_mul, h.eq, add_assoc]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • f 1

Tactic:
rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ (-1 + 1) • a = 0

Tactic:
neg_add_cancel,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ 0 • a = 0
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Module ℕ M
n : ℕ
⊢ ∀ (m : M), n • m = n • m

Tactic:
by convert! nat_smul_eq_nsmul P n

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))

Tactic:
pow_succ

Goal state after:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ n * a)
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 : ℕ
⊢ ↑↑n = ↑n

Tactic:
by rw [← intCast, Int.cast_natCast, natCast]

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

Goal state before:
pp: case succ
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ (n + 1))

Tactic:
pow_succ

Goal state after:
case succ
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ n * a)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case succ
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
hrec : Odd (a ^ n)
⊢ Odd (a ^ (n + 1))

Tactic:
rw [pow_succ]; exact hrec.mul ha

Goal state after:
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 : ℕ
⊢ ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
by
      rw [← intCast, Int.cast_negSucc, neg, natCast]

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

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

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulRightMono α
a b : α
⊢ cmp (a / b) 1 = cmp a b

Tactic:
rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) ≤ a ^ n * 1

Tactic:
pow_succ

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ n * a ≤ a ^ n * 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
pow_succ

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
by
  simpa only [pow_one] using pow_lt_pow_right_of_lt_one₀ h₀ h₁ hn

Goal state after:
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
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Tactic:
mul_inv_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 ≤ a * c ↔ b ≤ c * a
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ 1 ≤ a

Tactic:
suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
    rwa [← inf_eq_right, ← mul_eq_left]
  rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
    inf_assoc, inf_of_le_left ha]

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
rw [← denselyOrdered_orderDual]
  let e : Xᵒᵈ ≃o Y := ⟨OrderDual.ofDual.trans (f : X ≃ Y), ?_⟩
  · exact denselyOrdered_iff_of_orderIsoClass e
  · simp only [Equiv.trans_apply, EquivLike.coe_coe, OrderDual.forall, OrderDual.ofDual_toDual,
      OrderDual.toDual_le_toDual]
    intro a b
    rw [hf.le_iff_ge]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k.succ < 1

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) = a ^ (n + 1) * a

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 1) * a = a ^ (n + 1) * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ (k + 1)

Tactic:
pow_succ

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * b
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:
pow_succ

Goal state after:
β : 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 * f a
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ a < b ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
  apply exists_congr
  intro c
  rw [and_comm, and_congr_left_iff, gt_iff_lt]
  rintro rfl
  constructor
  · rw [one_lt_iff_ne_one]
    apply mt
    rintro rfl
    rw [mul_one]
  · rw [← (self_le_mul_right a c).lt_iff_ne]
    apply lt_mul_of_one_lt_right'

Goal state after: