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

Goal state before:
pp: α✝ : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst✝ : Unique ι
x : α default
i : ι
⊢ α i

Tactic:
rw [Unique.eq_default i]
  exact x

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f

Tactic:
Function.bijective_iff_has_inverse

Goal state after:
A : Sort u_2
B : Sort u_3
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1.tail
α : Type u_1
r : α → α → Prop
a b b✝ : α
hac : ReflTransGen r a b✝
hcb : r b✝ b
⊢ b = a ∨ TransGen r a b

Tactic:
| tail hac hcb =>

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

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ (g ∘ f^[m]) ∘ f = g

Tactic:
iterate_invariant h m

Goal state after:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f = g
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_4
⊢ IsEmpty (PLift α) ↔ IsEmpty α

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_plift]

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)
n✝ : ℕ
a✝ : (i : I) → f i
x✝ : I
⊢ (a✝ ^ Int.negSucc n✝) x✝ = (a✝ ^ ↑n✝.succ)⁻¹ x✝

Tactic:
exact DivInvMonoid.zpow_neg' _ _

Goal state after:
Module: Mathlib.Order.Max

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

Tactic:
simp_rw [le_antisymm_iff, h j, and_true]
  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ le_trans a (h h')⟩

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
rw [Int.lt_iff_le_and_ne, Int.mul_nonneg_iff, ne_comm, Int.mul_ne_zero_iff]
  lia

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ x' ≤ y'

Tactic:
← not_lt

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: ι : Type u_1
α : Type u
β : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (β i)
inst✝ : Preorder α
f : α → (i : ι) → β i
⊢ Antitone f ↔ ∀ (i : ι), Antitone fun x ↦ f x i

Tactic:
by
  simp [Antitone, Pi.le_def, @forall_comm ι]

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

Goal state before:
pp: case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + (m + 1) ≤ f (n + (m + 1))

Tactic:
rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
    exact ih.trans_lt (hf (n + m).lt_succ_self)

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

Goal state before:
pp: α : Type u
h : univ = {∅}
this : univ ∈ univ
⊢ IsEmpty α

Tactic:
by aesop

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

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

Tactic:
himp_inf_distrib,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ (a ⇨ a) ⊓ (a ⇨ b) = b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
himp_inf_distrib,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ (b ⇨ a) ⊓ (b ⇨ b) = a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

Tactic:
rw [le_himp_iff, ← compl_compl_inf_distrib]

Goal state after:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ
Module: Mathlib.Logic.Equiv.Sum

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
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x ↦
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)

Tactic:
by rintro (x | x) <;> simp

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

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
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ RightInverse (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x ↦
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)

Tactic:
by rintro (x | x) <;> simp

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
⊢ LeftInverse (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val)

Tactic:
by
    rintro (⟨x, hx⟩ | ⟨x, hx⟩) <;> dsimp
    · rw [dif_pos]
    · rw [dif_neg]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
        { rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff] }

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b ∆ a = b

Tactic:
rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]

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ᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ

Tactic:
rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
a : Set α
⊢ f ∘ g '' a = f '' g '' a

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (∃ x, x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔ ∃ x, x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
x✝¹ : α × β
p₁ : α
p₂ : β
x✝ : (p₁, p₂) ∈ s
⊢ (p₁, p₂) ∈ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Tactic:
by aesop

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁

Tactic:
rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
g : α → β
f : ι → α
⊢ range (g ∘ f) = g '' range f

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ f x✝ = y

Tactic:
by simp_rw [← h, exists_apply_eq_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
← injOn_univ,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ InjOn (s.piecewise f g) univ ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
h✝ : InjOn g s
hs : range f ⊆ s
h : Injective f
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (g ∘ f) x✝ = (g ∘ f) a₂ → x✝ = a₂

Tactic:
by aesop

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

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

Tactic:
exact fun x hx ↦ h (hf hx) hx rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (f '' range fun a ↦ x ⋯) = t

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a = c ↔ b = d

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a ≠ c ↔ b ≠ d

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ b = 1 / a

Tactic:
rw [eq_inv_of_mul_eq_one_left h, one_div]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * 1 = f x

Tactic:
rw [← one, ← mul, mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b * (b⁻¹ * a⁻¹) = a⁻¹

Tactic:
h.mul_inv_cancel_left

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a⁻¹ = a⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
u.val_inv_eq_inv_val

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a * (↑u)⁻¹ = a * (↑u)⁻¹
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : ¬p x
⊢ p ((ofSubtype f) x) ↔ p x

Tactic:
simp [h, ofSubtype_apply_of_not_mem f h]

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

Goal state before:
pp: case ind.zero
R : Type u_1
inst✝ : AddMonoidWithOne R
hk : ∀ (m : ℕ), m < 0 → m.binCast = ↑m
⊢ Nat.binCast 0 = ↑0

Tactic:
Nat.binCast,

Goal state after:
case ind.zero
R : Type u_1
inst✝ : AddMonoidWithOne R
hk : ∀ (m : ℕ), m < 0 → m.binCast = ↑m
⊢ 0 = ↑0
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝ : CommGroup G
a b c d e : G
ha : IsSquare a
n : ℕ
k : ℤ
hk : Even k
⊢ IsSquare (a * (b * b) / c ^ 2 * d ^ k * e ^ (n + n))

Tactic:
by aesop

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝ : AddCommGroup G
a b c d e : G
ha : Even a
n : ℕ
k : ℤ
hk : Even k
⊢ Even (a + (b + b) - 2 • c + k • d + (n + n) • e)

Tactic:
by aesop

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

Tactic:
← two_mul,

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 * y) + (f (x * y) - 2 * (f x * f y)) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
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 * y) + f (x * y) - 2 * (f x * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
← two_mul,

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 : 2 * f (x * y) - 2 * (f x * f y) = 0
⊢ (↑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 : M₀
a✝ : Nontrivial M₀
⊢ IsUnit x ↔ x * x⁻¹ʳ = 1

Tactic:
refine ⟨mul_inverse_cancel _, ?_⟩

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
a✝ : Nontrivial M₀
⊢ x * x⁻¹ʳ = 1 → IsUnit x
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = b * (d * d⁻¹) * c ↔ d * a = b * c

Tactic:
hd.mul_inv_cancel,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = b * 1 * c ↔ d * a = b * c
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1]) x

Tactic:
simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using
      (n + 1).cast_commute (-x)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)

Tactic:
← two_mul,

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c) = a ^ (2 * c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ ∃ b, a = 2 * b

Tactic:
by simp [even_iff_exists_two_nsmul]

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

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

Tactic:
← two_mul,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a + (2 * b + 1) = 2 * a + 2 * b + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * (a + a)

Tactic:
← two_mul,

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * (2 * a)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = a + a
⊢ IsUnit 2

Tactic:
← two_mul,

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = 2 * a
⊢ IsUnit 2
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id

Tactic:
← two_mul,

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m] = id
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
by rw [h.neg_zpow, one_zpow]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a - c + (b + c)

Tactic:
rw [add_comm a, add_comm (a - c)]
  exact add_le_add_add_tsub

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a - b = c - d

Tactic:
by
  calc a - b = a + d - d - b := by rw [add_tsub_cancel_right]
           _ = c + b - b - d := by rw [h, tsub_right_comm]
           _ = c - d := by rw [add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ min a b < max c d

Tactic:
by
  simp_rw [min_lt_iff, lt_max_iff]; contrapose! h; exact mul_le_mul' h.1.1 h.2.2

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

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

Tactic:
exact @CovariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ d ≤ c

Tactic:
grw [hab] at h
    · exact le_of_mul_le_mul_of_pos_left h <| ha.trans_le hab
    · exact hc.le

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
rw [zero_mul] at hab

Goal state after:
case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
{ cases f; cases g; congr }

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✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Preorder γ
inst✝¹ : Preorder δ
ι : Type u_6
π : ι → Type u_7
inst✝ : (i : ι) → Preorder (π i)
p q : α → Prop
h : ∀ (a : α), p a → q a
⊢ ∀ {a b : { x // p x }}, (Subtype.impEmbedding p q h) a ≤ (Subtype.impEmbedding p q h) b ↔ a ≤ b

Tactic:
by aesop

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

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
mabs_of_le_one ha,

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = a⁻¹ ^ n
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
n : ℕ
⊢ ↑(a / ↑n).natAbs ≤ ↑a.natAbs

Tactic:
exact ofNat_le_ofNat_of_le
    (match a, n with
      | (m : ℕ), n => Nat.div_le_self _ _
      | -[m+1], 0 => Nat.zero_le _
      | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
mabs_of_le_one ha,

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ |b|ₘ
Module: Mathlib.Algebra.Ring.Int.Parity

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

Tactic:
by rw [h.neg_zpow, one_zpow]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ Commute a b

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ Commute b b

Tactic:
by aesop

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ f x = 0 ↔ x = 0

Tactic:
refine ⟨?_, by simp +contextual⟩
  contrapose!
  intro hx H
  lift x to G₀ˣ using isUnit_iff_ne_zero.mpr hx
  apply one_ne_zero (α := M₀)
  rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
⊢ f (1 x) = 1 x

Tactic:
rcases eq_or_ne x 0 with rfl | hx
  · simp
  · rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = min ↑a ↑b

Tactic:
by
  simp_rw [min_def, val_le_val, ← apply_ite]
  rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithTop α
⊢ x ≤ y ↔ y = ⊤ ∨ ∃ a b, a ≤ b ∧ x = ↑a ∧ y = ↑b

Tactic:
by
  grind [WithTop.le_def']

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
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊↑n * a⌋₊ / n = ⌊a⌋₊

Tactic:
rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Invertible 2
⊢ ⅟2 + ⅟2 = 1

Tactic:
← two_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Invertible 2
⊢ 2 * ⅟2 = 1
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
n : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n

Tactic:
rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩
  induction k with
  | zero => simp only [zero_add, pow_one, le_refl]
  | succ k ih =>
    let n := k.succ
    have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
    have h2 := add_nonneg hx hy
    calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (n + n) ≤ 2 ^ (n + n - 1) * (a ^ (n + n) + b ^ (n + n))

Tactic:
← two_mul,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (2 * n) ≤ 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr
⊢ IsUnit (-1)

Tactic:
exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α × β → γ
s : Set α
t : Set β
⊢ image2 (fun a b ↦ f (a, b)) s t = f '' s ×ˢ t

Tactic:
simp [← image_uncurry_prod, uncurry]

Goal state after: