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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
⊢ v = v'

Tactic:
by
  have := congr_fun h a'
  rwa [update_self, update_self] at this

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
unfold extend

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ gb (f x) (f x) = f x

Tactic:
Std.IdempotentOp.idempotent (op := gb)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f x = f x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
by
  have : SMulCommClass β α β := .symm ..; exact smul_smul_smul_comm a b c d

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
funext x
  simp [Function.extend_def, apply_dite Inv.inv]

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

Goal state before:
pp: b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ b₀.toNat ≤ b₁.toNat

Tactic:
cases b₀

Goal state after:
case false
b₁ : Bool
h : false ≤ b₁
⊢ false.toNat ≤ b₁.toNat

case true
b₁ : Bool
h : true ≤ b₁
⊢ true.toNat ≤ b₁.toNat
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 2 * k ^ 2 = (2 * k) ^ 2

Tactic:
rw [Nat.mul_pow, ← Nat.add_mul]

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:
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:
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:
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:
grind only

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

Goal state before:
pp: f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
⊢ f n = f b

Tactic:
replace key : ∀ k : ℕ, f (m + k) = f (m + k + 1) ∧ f (m + k) = f m := fun k =>
    Nat.rec ⟨hm, rfl⟩ (fun k ih => ⟨hfstab _ ih.1, ih.1.symm.trans ih.2⟩) k

Goal state after:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), f (m + k) = f (m + k + 1) ∧ f (m + k) = f m
⊢ f n = f b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b ⊔ b = b ⊔ b ⊓ (b ⊔ b)

Tactic:
by rw [inf_sup_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ (b ⊔ b ⊓ b) = b

Tactic:
by rw [inf_sup_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
by rw [inf_sup_self]

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

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

Tactic:
by rw [sup_comm, sup_sdiff_right_self]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b ⊔ a \ b) = f a

Tactic:
by rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]

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

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

Tactic:
image_preimage_inter,

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ ↑(fst ⟨(p₁, p₂), he⟩) = ↑(snd ⟨(p₁, p₂), he⟩)

Tactic:
Prod.ext_iff

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔
    (↑(fst ⟨(p₁, p₂), he⟩)).1 = (↑(snd ⟨(p₁, p₂), he⟩)).1 ∧ (↑(fst ⟨(p₁, p₂), he⟩)).2 = (↑(snd ⟨(p₁, p₂), he⟩)).2
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
⊢ f '' s ⊓ g '' t ⊆ ⊥

Tactic:
rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ InjOn f univ ↔ Injective f

Tactic:
by simp [InjOn, Injective]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s

Tactic:
rwa [← hx, h hs]

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

Goal state before:
pp: a b c : ℤ
hbc : c ∣ b
⊢ a ∣ b / c ↔ c * a ∣ b

Tactic:
by
  simp [hbc]

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

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -(↑n + 1) = ↑(m - n.succ)

Tactic:
← Int.natCast_one,

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -(↑n + ↑1) = ↑(m - n.succ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (f₁ x.1, f₂ x.2) = (f₁ y.1, f₂ y.2) → x = y

Tactic:
Prod.ext_iff

Goal state after:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [← one_div_one_div a, h, one_div_one_div]

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

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

Tactic:
by rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * (y * z) = 1

Tactic:
by rwa [← mul_assoc]

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

Goal state before:
pp: F : Type u_1
G : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : FunLike F M N
inst✝³ : FunLike G N M
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ⇑g ⇑f
h : IsUnit (f x)
⊢ IsUnit x

Tactic:
simpa only [hfg x] using h.map g

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

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
simp only [hc, mul_zero, or_true]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Opposite

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝ : Monoid α
⊢ Monoid.toMulAction αᵐᵒᵖ = instMulAction

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: α : Type u_7
β : α → Type u_8
⊢ Function.Injective ⇑(sigmaCongrRightHom β)

Tactic:
by
  intro x y h
  ext a b
  simpa using Equiv.congr_fun h ⟨a, b⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
m : A'
⊢ 0 • m = 0

Tactic:
rcases hf m with ⟨x, rfl⟩

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
x : A
⊢ 0 • f x = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
rw [hx, inv_zero, smul_zero, inv_zero]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
← Int.natCast_one,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑1 = 1
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℤ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
by
  simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]

Goal state after:
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:
simpa using zpow_sub₀ ha m n

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ ↑n • b = n • b

Tactic:
by
  induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

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

Goal state before:
pp: case ofNat
R✝ : Type u_1
S : Type u_2
M✝ : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M
a✝ : ℕ
⊢ (Int.ofNat a✝ • x) • y = Int.ofNat a✝ • x • y

Tactic:
simp [mul_smul, Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))

Tactic:
exact h a⁻¹ bc

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

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
exact h a⁻¹ bc

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)

Tactic:
exact h a⁻¹ bc

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

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
exact h a⁻¹ bc

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

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

Tactic:
by
  rw [← mul_lt_mul_iff_left b, mul_one, mul_inv_cancel_left]

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✝ : MulRightStrictMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
by
  simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

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

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

Tactic:
by
  simpa only [zero_mul] using mul_le_mul_of_nonpos_right ha hb

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 : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ 1 ≤ a ^ n ↔ 0 ≤ n

Tactic:
by
  simp [← zpow_le_zpow_iff_right₀ ha]

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 : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ a ^ n ≤ 1 ↔ n ≤ 0

Tactic:
by
  simp [← zpow_le_zpow_iff_right₀ ha]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ a * b * a⁻¹)

Tactic:
mul_inv_cancel_comm

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ b)
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
az : a = 0
⊢ a.sign = a / |a|

Tactic:
simp [az]

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

Goal state before:
pp: a : ℤ
az : a = 0
⊢ a.sign = |a| / a

Tactic:
simp [az]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : |a|ₘ = |b|ₘ
⊢ a = b ∨ a = b⁻¹

Tactic:
obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h

Goal state after:
case inl
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
b : α
h : |(|b|ₘ)|ₘ = |b|ₘ
⊢ |b|ₘ = b ∨ |b|ₘ = b⁻¹

case inr
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
b : α
h : ||b|ₘ⁻¹|ₘ = |b|ₘ
⊢ |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
simp [mabs_of_one_lt ha, ha, ha.ne']

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

Goal state before:
pp: r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

Tactic:
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ r.succ.xgcdAux s t r' s' t' = (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℤ
hc : x = 0 ∧ y = 0
⊢ x.gcd y = 0

Tactic:
hc.left,

Goal state after:
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ gcd 0 y = 0
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ ↑((m + 1).gcd n) = 1

Tactic:
Nat.gcd_eq_gcd_ab,

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ (↑(m + 1) * (m + 1).gcdA n + ↑n * (m + 1).gcdB n) = 1
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
| b * a = 0

Tactic:
← mul_zero b

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
| b * a = b * 0
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

Tactic:
rintro ⟨ab, ba⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : LT α
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
WithBot.bot_lt_iff_ne_bot,

Goal state after:
α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : LT α
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
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:
rw [neg_neg]; exact Helt

Goal state after:
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 α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
⊢ ∃ n, x ≤ ↑n

Tactic:
by
    obtain ⟨n, hn⟩ := bounded x
    use n
    exact_mod_cast hn

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0

Tactic:
exact (floor_le a).trans ha

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hy : y ≠ 0
⊢ x < y * exp 1 ↔ x ≤ y

Tactic:
lift y to Multiplicative ℤ using hy

Goal state after:
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
⊢ x < ↑y * exp 1 ↔ x ≤ ↑y
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
· rw [floor_of_nonpos ha]
    exact
      iff_of_false (Nat.pos_of_ne_zero hn).not_ge
        (not_le_of_gt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
⊢ 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a

Tactic:
le_floor_iff' Nat.one_ne_zero,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
⊢ ↑1 ≤ a ↔ 1 ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

Tactic:
rw [cast_one.symm, ceil_add_natCast ha 1]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsCodirectedOrder β
⊢ ∃ a b, a < b

Tactic:
rcases exists_pair_ne β with ⟨a, b, hne⟩
  rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
  exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)

Tactic:
hab.one_div_add_one_div ha hb

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ (a + b) / (a * b) = (a + b) / (a * b)
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u).natAbs * (↑u⁻¹).natAbs = 1

Tactic:
by rw [← natAbs_mul, Units.mul_inv]; rfl

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

Goal state before:
pp: u v : ℤ
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩

Goal state after:
case refine_1
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = 1 ∧ v = -1
⊢ u * v = -1

case refine_2
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = -1 ∧ v = 1
⊢ u * v = -1
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
⊢ {b | p (e.symm b)} = ⇑e '' {a | p a}

Tactic:
Equiv.image_eq_preimage_symm,

Goal state after:
α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
⊢ {b | p (e.symm b)} = ⇑e.symm ⁻¹' {a | p a}