mathlib-initiative/mathlib-tactics huggingface dataset:
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:
pow_zero,

Goal state after:
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 1 = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
pow_zero,

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
by rw [not_iff_comm]; simp

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
by rw [not_iff_comm]; simp

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

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
by rw [not_iff_comm]; simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
by ext <;> exact DivInvMonoid.zpow_succ' ..

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

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (x ^ 0 * y) = f x ^ 0 * f y

Tactic:
pow_zero,

Goal state after:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (1 * y) = f x ^ 0 * f y
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (1 * y) = f x ^ 0 * f y

Tactic:
pow_zero,

Goal state after:
case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (1 * y) = 1 * f y
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑ofSubtype

Tactic:
intro x y h
  rw [Perm.ext_iff] at h ⊢
  intro a
  specialize h a
  rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑↑(n + 1) = -↑-[n+1]

Tactic:
cast_natCast

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(n + 1) = -↑-[n+1]
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ ↑m.natAbs ∣ ↑n ↔ (↑m.natAbs).natAbs ∣ n

Tactic:
simp [← natCast_dvd_natCast, Int.neg_dvd]

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

Goal state before:
pp: case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ -↑m.natAbs ∣ ↑n ↔ (-↑m.natAbs).natAbs ∣ n

Tactic:
simp [← natCast_dvd_natCast, Int.neg_dvd]

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

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

Tactic:
by
  rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]

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

Goal state before:
pp: case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ r⁻¹ʳ ^ 0 = (r ^ 0)⁻¹ʳ

Tactic:
pow_zero,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ 1 = (r ^ 0)⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ 1 = (r ^ 0)⁻¹ʳ

Tactic:
pow_zero,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ 1 = 1⁻¹ʳ
Module: Mathlib.Algebra.Ring.Commute

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

Tactic:
by
  rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]

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
z : ℕ
a : M
⊢ ↑z.succ • a = ↑z • a + a

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]; simp [add_comm, add_smul]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (fun x1 x2 ↦ x1 * x2) r ↔ Contravariant N N (fun x1 x2 ↦ x1 * x2) r

Tactic:
by
  refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
    exact h a⁻¹ bc
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
    exact h a⁻¹ bc

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
⊢ c + b - d - b = c + b - b - d

Tactic:
tsub_right_comm

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ c + b - b - d = c + b - b - d
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ c * a ≤ c * b

Tactic:
rw [mul_comm c, mul_comm c]; exact mul_le_mul_left a b h c

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 c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]

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

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

Tactic:
{

Goal state after:
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [le_inv_mul_iff₀ ha, mul_one]

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₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 < n
⊢ StrictMonoOn (fun a ↦ a ^ n) {a | 0 ≤ a}

Tactic:
lift n to ℕ using hn.le

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
hn : 0 < ↑n
⊢ StrictMonoOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case inl
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : 0 ≤ a
⊢ 0 ≤ a ^ 2

pp: case inr
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
⊢ 0 ≤ a ^ 2

Tactic:
· exact pow_succ_nonneg ha _

Goal state after:
case inr
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
⊢ 0 ≤ a ^ 2
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f x) (f y)
⊢ x = y

Tactic:
rw [hxy] at this

Goal state after:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f x)
⊢ x = y

Tactic:
rw [hxy] at this

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ x = y
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = a * b * |b / a|ₘ

Tactic:
← inf_mul_sup a b,

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = a * b / |b / a|ₘ

Tactic:
← inf_mul_sup a b,

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a * |a|ₘ

Tactic:
← mul_inv_cancel a,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a * a⁻¹ ≤ a * |a|ₘ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑n % ↑k * (n.gcdA k % ↑k % ↑k) % ↑k = ↑n * n.gcdA k % ↑k

Tactic:
Int.emod_emod,

Goal state after:
case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑n % ↑k * (n.gcdA k % ↑k) % ↑k = ↑n * n.gcdA k % ↑k
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y

Tactic:
push Not

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
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 ↔ a = 0

Tactic:
conv_lhs => rw [← mul_zero b]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 ≤ a - a

Tactic:
by
  obtain rfl | ha := eq_or_ne a ⊤
  · simp
  · rw [sub_self_eq_zero_of_ne_top ha]

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

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

Tactic:
refine le_antisymm ?_ le_add_tsub

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) ≤ b
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑0 = ↑m - ↑n

Tactic:
cast_zero,

Goal state after:
case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ 0 = ↑m - ↑n
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑↑k

Tactic:
cast_natCast

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
⊢ ∀ ⦃a : Multiplicative αᵒᵈ⦄, 0 < a → ∀ ⦃b c : Multiplicative αᵒᵈ⦄, b < c → a * b < a * c

Tactic:
simpa [← ofAdd_add, ← toDual_add]
      using! fun a ha b c hbc ↦ add_right_strictMono_of_ne_top (by simpa using! ha.ne') hbc

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
push Not

Goal state after:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (Exists fun ⦃n⦄ ↦ 0 < n ∧ n ≤ k ∧ P n) ↔ Exists fun ⦃n⦄ ↦ 0 < n ∧ n ≤ k ∧ P n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ a ≤ ↑(ofAdd b)

Tactic:
rwa [← coe_unzero ha, coe_le_coe, ← ofAdd_toAdd (unzero ha), ofAdd_le]

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

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : toAdd (unzero h) = b
⊢ a = ↑(ofAdd b)

Tactic:
subst k

Goal state after:
α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
⊢ a = ↑(ofAdd (toAdd (unzero h)))
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : a = ↑(ofAdd b)
⊢ toAdd (unzero h) = b

Tactic:
subst k

Goal state after:
α : Type u_3
b : α
h : ↑(ofAdd b) ≠ 0
⊢ toAdd (unzero h) = b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x.log < a ↔ x < exp a

Tactic:
rw [← toAdd_unzero_eq_log hx, ← lt_ofAdd_iff hx, exp]

Goal state after:
Module: Mathlib.Order.Directed

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

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

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + 1 + ⅟b * a + ⅟a * b ↔ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b)

Tactic:
by rw [one_add_one_eq_two, add_right_inj]

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
⊢ (a + b) * ((a + b) * (a + b) ^ 0) = a * (a * a ^ 0) + b * (b * b ^ 0) + (a * b + b * a)

Tactic:
pow_zero,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) * ((a + b) * 1) = a * (a * 1) + b * (b * 1) + (a * b + b * a)
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
⊢ a * (a * a ^ 0) + b * (b * b ^ 0) + (a * a + b * b) = 2 * (a * (a * a ^ 0) + b * (b * b ^ 0))

Tactic:
pow_zero,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a * (a * 1) + b * (b * 1) + (a * a + b * b) = 2 * (a * (a * 1) + b * (b * 1))
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ (fun x ↦ f x.1 x.2) '' s ×ˢ t ↔ x✝ ∈ image2 f s t

Tactic:
by simp [and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ |a| < |b|

Tactic:
← sq_lt_sq

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : t.Nonempty
⊢ image2 (fun x x_1 ↦ x) s t = s

Tactic:
by
  simp [nonempty_def.mp h, Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : s.Nonempty
⊢ image2 (fun x y ↦ y) s t = t

Tactic:
by
  simp [nonempty_def.mp h, Set.ext_iff]

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t

Tactic:
{

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ id ≤ f

Tactic:
rw [Pi.le_def]
  by_contra! H
  obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min {i | f i < i} H
  exact hm' _ (hf hm) hm

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b

Tactic:
rw [← Ico_sdiff_left, sdiff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
c : ℕ
⊢ smul c 0 = 0

Tactic:
simp [smul, nsmul_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a : M
⊢ (replicate 0 a).prod = a ^ 0

Tactic:
pow_zero,

Goal state after:
case zero
M : Type u_2
inst✝ : Monoid M
a : M
⊢ (replicate 0 a).prod = 1
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
simp [zpow', zpow_eq_zero_iff hn]
    tauto

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

Goal state before:
pp: case cons
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha

Goal state after:
case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
· rw [hf a' ha' mem_cons_self, one_mul, add_zero]

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length - 1 < l.length
⊢ l ≠ []

Tactic:
rintro rfl; exact Nat.lt_irrefl 0 h

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

Goal state before:
pp: case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)

Tactic:
apply Function.Injective.comp hf

Goal state after:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective lh
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹ ↔ a * y = x * a

Tactic:
← mul_inv_rev,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ (x * a)⁻¹ = (a * y)⁻¹ ↔ a * y = x * a
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q r : ℚ≥0
⊢ q * r = divNat (q.num * r.num) (q.den * r.den)

Tactic:
by
  ext; simp [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, num_coe, den_coe]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
x y : α
inst✝ : Nontrivial α
h : IsRelPrime x y
⊢ x = 0 → y ≠ 0

Tactic:
rintro rfl rfl

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
h : IsRelPrime 0 0
⊢ False
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = 1

Tactic:
rw [h, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = x * (d * e)

Tactic:
← he,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = x * 1
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ q.num * q.num / ↑1 = q.num * q.num

pp: q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)

Tactic:
Int.ofNat_one,

Goal state after:
q : ℚ
⊢ q.num * q.num / 1 = q.num * q.num

q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)