mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
h : 0 ≤ a / b
⊢ a * 0 / (b * 0) ≤ a / b

Tactic:
simpa

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
h : a / b ≤ 0
⊢ a / b ≤ a * 0 / (b * 0)

Tactic:
simpa

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)

Tactic:
rw [mul_mul_mul_comm, ← pow_two r, two_mul, two_add_two_eq_four]

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 4 * r ^ 2 ≤ (a + b) * (a + b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
h : 0 ≤ a / b
⊢ 0 * a / (0 * b) ≤ a / b

Tactic:
simpa

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
h : a / b ≤ 0
⊢ a / b ≤ 0 * a / (0 * b)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = ⇑e
hg : g = ⇑e.symm
⊢ ∀ {a b : α},
    s ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b) ↔
      r a b

Tactic:
simp [hf, e.map_rel_iff]

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 β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a✝ : α
⊢ a✝ = g (f a✝)

Tactic:
← cmp_eq_eq_iff,

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a✝ : α
⊢ cmp a✝ (g (f a✝)) = Ordering.eq
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 β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ f (g x✝) = x✝

Tactic:
← cmp_eq_eq_iff,

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ cmp (f (g x✝)) x✝ = Ordering.eq
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
f : β → M
hf : StrictMono f
x✝ : 1 ≠ 0
⊢ StrictMono fun x ↦ f x ^ 1

Tactic:
simpa

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

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

Tactic:
simp [mod_one]

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

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → 1 < c

Tactic:
one_lt_iff_ne_one

Goal state after:
case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → c ≠ 1
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
obtain ⟨c, hc, rfl⟩ := exists_mul_of_le hbc
    rw [le_iff_exists_mul]
    exact ⟨c, (mul_assoc _ _ _).symm⟩

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
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b

Tactic:
← 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 * a * a.gcdA c + b * c * a.gcdB c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
hm : a ^ 0 = 1
⊢ a ^ Nat.gcd 0 n = 1

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ -b ≠ ⊤

Tactic:
simpa

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:
by
  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.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
⊢ b - a + a = b

Tactic:
add_comm

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.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 c : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = c + (a - b)

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ c + (a - b) = c + (a - b)
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 c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c
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 c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
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 c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
refine ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩
  rintro rfl
  exact h'.ne' hc.add_tsub_cancel_right

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 c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
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 c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + a

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ b + a = b + a
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = b ↔ a ≤ b

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
| b + ⋯.choose ≤ c + b

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
| ⋯.choose + b ≤ c + b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
by
  refine ⟨fun a b c hbc => ?_⟩
  induction a
  · rwa [zero_add, zero_add]
  induction b
  · rw [add_zero]
    induction c
    · rw [add_zero]
    · rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)
  · rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
    rw [← coe_add, ← coe_add _ c, coe_le_coe]
    gcongr

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c

Tactic:
simp at this

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

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ b < 0

Tactic:
simp at this

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ k, exp (-↑k) < x ∧ exp (-↑k) < y

Tactic:
by
  obtain ⟨z, hz, hzx, hzy⟩ := WithZero.exists_ne_zero_and_le_and_le hx hy
  obtain ⟨k, hk⟩ := exists_exp_neg_natCast_lt hz
  grind

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

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:
Module: Mathlib.Algebra.GroupWithZero.Invertible

Goal state before:
pp: α : Type u
inst✝² : GroupWithZero α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ b / a * (a / b) = 1

Tactic:
simp [← mul_div_assoc]

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

Goal state before:
pp: α : Type u
inst✝² : GroupWithZero α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ a / b * (b / a) = 1

Tactic:
simp [← mul_div_assoc]

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

Goal state before:
pp: α : Type u
inst✝³ : GroupWithZero α
a b : α
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a / b)
⊢ a / b * (b / a) = 1

Tactic:
simp [← mul_div_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟b + ⅟a

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟b + ⅟a = ⅟b + ⅟a
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 = ⅟b * a + ⅟a * b ↔ -1 = ⅟a * b + ⅟b * a

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -1 = ⅟a * b + ⅟b * a ↔ -1 = ⅟a * b + ⅟b * a
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)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
⊢ -(a + b) = b * ⅟a * b

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟b * a + ⅟a * b
h_a_binv_a : -(b + a) = a * ⅟b * a
⊢ -(a + b) = b * ⅟a * b
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)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ -(b + a) = -(a + b)

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ -(a + b) = -(a + b)
Module: Mathlib.Algebra.Field.Basic

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

Tactic:
simpa only [one_div] using (inv_add_inv' ha hb).symm

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ (b * c + a) / c = (a + b * c) / c

pp: case hc
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ c ≠ 0

Tactic:
add_comm

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ (a + b * c) / c = (a + b * c) / c

case hc
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ c ≠ 0
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c
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 : ℕ
⊢ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Tactic:
by
      simp only [← mul_assoc, ← pow_add, ← pow_mul]
      cases n
      · rfl
      · simp [Nat.two_mul]

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

Tactic:
add_comm

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.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:
by
  rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
rw [strictMonoOn_insert_iff]
  have : ∀ b ∈ s, b < a → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
  tauto

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |(-1)| ^ n = 1

Tactic:
abs_neg,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |1| ^ n = 1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
this : a ^ n > -b ^ n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
by simpa [he, not_odd_iff_even.2 he] using this.ne'

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

Goal state before:
pp: a b : ℤ
h₁ : b ≠ 0
h₂ : a ∣ b
⊢ 0 < |b|

Tactic:
simpa

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

Goal state before:
pp: a b : ℤ
h₁ : b ≠ 0
h₂ : a ∣ b
⊢ a ∣ |b|

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2

Tactic:
by
  refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
  · suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
    exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
  · suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
    exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
  · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
  · exact fun q hq =>
      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩

Goal state after:
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:
rw [Equiv.image_eq_preimage_symm, preimage_ofPred_eq]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
⊢ f a = g a

Tactic:
obtain h | rfl | h := lt_trichotomy b a

Goal state after:
case inl
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : b < a
⊢ f a = g a

case inr.inl
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
⊢ f b = g b

case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
⊢ f a = g a
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ Disjoint s {a}

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioi x)
a : α
ha : a ∈ Ioi x
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
by
    rcases exists_between ha with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, hb₁⟩, hb₂⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a ≤ 1 / b
⊢ 0 < 1 / a

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ 0 < 1 / a

Tactic:
simpa

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

Goal state before:
pp: case nil
M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ [] → p x
⊢ p [].prod

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d

Tactic:
by
  rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
simp [zpow', ha]

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
ha : a ≠ 0
⊢ zpow' a n = a ^ n

Tactic:
simp [zpow', ha]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
ha : a ≠ 0
⊢ zpow' a 0 = 1

Tactic:
simp [zpow', ha]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
rw [hn]
    simp [zpow', ha, zpow_ne_zero ]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (0 * n) = zpow' (zpow' a 0) n

Tactic:
simp [zpow', ha]

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

Goal state before:
pp: case cons
α : 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
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
List.map_cons,

Goal state after:
case cons
α : 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
⊢ (f a' :: map f as).prod = f a ^ count a (a' :: as)