mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
⊢ (a = b) = (b = a)

Tactic:
by rw [@eq_comm _ a b]

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

Goal state before:
pp: α : Sort u_4
β : Sort u_5
⊢ IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_psum, not_or]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂
⊢ b₁ = b₂

Tactic:
simpa only [and_true, eq_self_iff_true, mk_inj] using h

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
· simpa using compare_gt_iff_gt.1 h

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

Goal state before:
pp: a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a * b ≤ a ^ b

Tactic:
cases b with
  | zero => exact Nat.zero_le _
  | succ b =>
      obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
      · rw [Nat.zero_mul]; exact Nat.zero_le _
      · have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
        rw [Nat.pow_succ']; exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f a ≤ f b) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b ≤ a → f b ≤ f a

Tactic:
by grind only

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f b ≤ f a) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b ≤ a → f a ≤ f b

Tactic:
by grind only

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a < f b) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b < a → f b < f a

Tactic:
by grind only

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b < f a) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b < a → f a < f b

Tactic:
by grind only

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s

Tactic:
rw [not_iff_comm, not_bounded_iff]

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

Goal state before:
pp: case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)

Tactic:
exact hg (Nat.lt_succ_self _)

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

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

Tactic:
by
  inhabit α
  rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
  rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
  refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
  rintro (n | _ | n)
  · exact hf n.lt_succ_self
  · change g 1 < f 0
    rw [hf₀, ← hg₀]
    exact hg Nat.zero_lt_one
  · exact hg (Nat.lt_succ_self _)

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

Goal state before:
pp: case h
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∀ (n : ℕ), n ≥ N → f n = c + 1

Tactic:
intro n

Goal state after:
case h
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
n : ℕ
⊢ n ≥ N → f n = c + 1
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ (↑((optionSubtype x).symm e)).symm ↑b = some (e.symm b)

Tactic:
simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
             Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
  exact fun h => False.elim (b.property h)

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

Goal state before:
pp: case none
α✝ : 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.12
p : Option α → Type v
h : ∀ (a : p none), False
⊢ ∀ (a : p none), none.isSome = true

Tactic:
intro n

Goal state after:
case none
α✝ : 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.12
p : Option α → Type v
h : ∀ (a : p none), False
n : p none
⊢ none.isSome = true
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_comm (a ⊓ b ⊓ c),

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ ((prodExtendRight a e) ab).fst = ab.fst

Tactic:
grind [prodExtendRight]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c

Tactic:
congr 1
      · congr 1
        rw [inf_comm, inf_assoc]
      · apply inf_left_right_swap

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Tactic:
image_preimage_inter

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ t ∩ f '' s = t ∩ f '' s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g i = s.piecewise f g i

Tactic:
simp [piecewise, h]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (Prod.map (fun x ↦ ↑x) fun x ↦ ↑x) ⁻¹' diagonal α = diagonal ↑s

Tactic:
by
  ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
  simp [Set.diagonal]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t

Tactic:
rw [mem_image]

Goal state after:
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1, x_1 ∈ {x | ↑x ∈ t} ∧ ↑x_1 = x) ↔ x ∈ t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
Set.ext_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ
e₂ : γ → β
he₂ : ∀ (x : γ × β), x ∈ range (⇑(Equiv.prodComm β γ) ∘ f) ↔ x ∈ graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h
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 = graphOn f (Prod.fst '' s)

Tactic:
rw [graphOn, image_image, 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
⊢ EqOn (fun x ↦ (x.1, f x.1)) id s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ (-a.pred).pred = -a

Tactic:
neg_pred,

Goal state after:
a : ℤ
⊢ (-a).succ.pred = -a
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i : ℕ
⊢ ∀ (n : ℕ), motive (-↑n)

Tactic:
intro n

Goal state after:
case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
⊢ motive (-↑n)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case pos
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

pp: case neg
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
· rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = 0 by lia]
    grind [inductionOn'.pos]

Goal state after:
case neg
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ (a ^ ↑(m * n.succ))⁻¹ = (a ^ (m * (n + 1)))⁻¹

Tactic:
inv_inj,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ ↑(m * n.succ) = a ^ (m * (n + 1))
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ (a ^ ↑(m.succ * n))⁻¹ = (a ^ ((m + 1) * n))⁻¹

Tactic:
inv_inj,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ ↑(m.succ * n) = a ^ ((m + 1) * n)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
mul_pow

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a⁻¹ * b⁻¹) ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)

Tactic:
mul_pow

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

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

Tactic:
by simp [h.symm, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ ↑a⁻¹ * (↑a * b) = b

Tactic:
rw [← mul_assoc, inv_mul, one_mul]

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

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

Tactic:
rw [← a.commute_coe_inv.mul_pow]

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ (↑a * ↑a⁻¹) ^ n = 1
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case ofNat
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ f.subtypePerm hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm ⋯

Tactic:
| ofNat n =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
if_neg h,

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 0 ↔ n = 0

Tactic:
rw [← cast_zero, cast_inj]

Goal state after:
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:
neg_neg

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
⊢ r • x = r • x
Module: Mathlib.Algebra.Group.Even

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

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

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

Goal state before:
pp: A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ ∀ (x : ℕ), f x = g x

Tactic:
intro n

Goal state after:
A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
n : ℕ
⊢ f n = g n
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ - -(a / b) = a / b

Tactic:
neg_neg

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ a / b = a / b
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -a / -b = a / b

Tactic:
rw [div_neg_eq_neg_div, neg_div, neg_neg]

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

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

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by lia), zero_mul]
  · 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✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ - -1 = 1

Tactic:
neg_neg

Goal state after:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ 1 = 1
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℤ
⊢ n • a = a * ↑n

Tactic:
by
  rw [zsmul_eq_mul, (n.cast_commute a).eq]

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

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
calc
    _ = (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) := by
      rw [add_mul, ← pow_add, add_right_comm]; rfl
    _ = _ := by rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLT α
h : a < b
⊢ ∃ c, 1 < c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLT α
c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : b ≤ 1
⊢ a * b ≤ a

Tactic:
by
  simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : 1 ≤ b
⊢ a ≤ a * b

Tactic:
by
  simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
← neg_pos,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
· simp [ha, hb, mabs_of_one_le, one_le_mul ha hb]

Goal state after:
case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
pow_two,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * (a ⊔ a⁻¹)
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' : ℤ
⊢ x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
p

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)
⊢ x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case zero
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
⊢ ∃ a b, a * 0 + b * q = n

pp: case succ
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * q = n

Tactic:
· have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
    exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩

Goal state after:
case succ
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * q = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
⊢ ∃ m, m < k ∧ n * m % k = r % k

Tactic:
obtain rfl | hk : k = 1 ∨ 1 < k := by lia
  · simp [mod_one]
  obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hkn hk
  use (m * r) % k, mod_lt _ (by lia)
  rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]

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

Goal state before:
pp: a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b

Tactic:
have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← Int.mul_add, ← this]

Goal state after:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
ua : IsUnit a
⊢ IsRegular a

Tactic:
rcases ua with ⟨a, rfl⟩
  exact Units.isRegular a

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c

pp: case coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ + b ≤ ↑a✝ + c

Tactic:
· rwa [zero_add, zero_add]

Goal state after:
case coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ + b ≤ ↑a✝ + c
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P (- -elt)

Tactic:
neg_neg

Goal state after:
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ z, P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h : P z
⊢ P (- -z)

Tactic:
neg_neg

Goal state after:
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ z, P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h : P z
⊢ P z
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✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
floor : α → ℤ
gc_coe_floor : GaloisConnection Int.cast floor
a : α
z : ℤ
⊢ (fun a ↦ -floor (-a)) a ≤ z ↔ a ≤ ↑z

Tactic:
by rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
a : α
x✝¹ : 0 < ↑a
c : α
x✝ : 0 < ↑c
⊢ ↑a * 0 < ↑a * ↑c

Tactic:
by simp [← WithZero.coe_mul]

Goal state after: