mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
x✝ : G₀
⊢ (fun x ↦ x * a) ((fun x ↦ x / a) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
x✝ : G₀
⊢ (fun x ↦ x / a) ((fun x ↦ x * a) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
x✝ : G₀
⊢ (fun x ↦ a / x) ((fun x ↦ a / x) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ ⋯

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (mulRight₀ a ha).symm = mulRight₀ a⁻¹ ⋯

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ (Equiv.divRight₀ a ⋯) b ≤ (Equiv.divRight₀ a ⋯) c ↔ b ≤ c

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulLeft₀ c hc).map_inf a b

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
by

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

Goal state before:
pp: M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h : IsUnit (f a)
⊢ IsUnit a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : Monoid M
inst✝³ : GroupWithZero G₀
inst✝² : FunLike F G₀ M₀
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : Nontrivial M₀
f : F
⊢ f 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
⊢ f a ≠ 0 ↔ a ≠ 0

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
⊢ f a ≠ 0 ↔ a ≠ 0

Tactic:
by
  refine ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩
  intro hx H
  lift a to G₀ˣ using isUnit_iff_ne_zero.mpr hx
  apply one_ne_zero (α := M₀')
  rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
⊢ f a⁻¹ = g a⁻¹

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
x : R
h : IsSquare x
⊢ 0 ≤ x

Tactic:
by

Goal state after:
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
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
by

Goal state after:
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
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)

Tactic:
by

Goal state after:
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
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ (n + 1)

Tactic:
by

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

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 0 ≤ 2 ^ (0 - 1) * (a ^ 0 + b ^ 0)

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 1 ≤ 2 ^ (1 - 1) * (a ^ 1 + b ^ 1)

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hab : a ≤ b
⊢ a ^ (n + 1) ≤ b ^ (n + 1)

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hba : b ≤ a
⊢ b ^ (n + 1) ≤ a ^ (n + 1)

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) ≤
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a : α
b : β
⊢ f a ∣ b ↔ a ∣ (↑f).symm b

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) =
    2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
by

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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 2) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g x✝ : G
⊢ (fun x ↦
        match x with
        | ⟨val, h⟩ => Exists.choose h)
      ((fun a ↦ ⟨g * a, ⋯⟩) x✝) =
    x✝

Tactic:
by

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 : ℕ
⊢ (2 * (a ^ 2 + b ^ 2)) ^ n = 2 ^ n * (a ^ 2 + b ^ 2) ^ n

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g : G
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | ⟨val, h⟩ => Exists.choose h)
    fun a ↦ ⟨g * a, ⋯⟩

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Add α
inst✝¹ : Semigroup α
inst✝ : LeftDistribClass α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
d : α
hd : b = a * d
e : α
he : c = a * e
⊢ a * (d + e) = b + c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b : α
⊢ (∃ b_1, -b = a * (Equiv.symm (Equiv.neg α)) b_1) ↔ a ∣ b

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b : α
⊢ (∃ b_1, b = -a * (Equiv.symm (Equiv.neg α)) b_1) ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c

Tactic:
by

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

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

Tactic:
by

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 : ℕ
⊢ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)

Tactic:
by

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

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

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

Tactic:
by

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
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
⊢ (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Tactic:
by

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:
by

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

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

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

Tactic:
by

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 : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ k ≠ 0

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ (a + a) / 2 = a

Tactic:
by

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 : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
h₀ : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ a / 2 + a / 2 = a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ a / -a = -1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: u : ℤ
hu : IsUnit u
⊢ u = 1 ∨ u = -1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ -a / a = -1

Tactic:
by

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 : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
by

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

Goal state before:
pp: u v : ℤ
hu : IsUnit u
hv : IsUnit v
⊢ u ≠ v ↔ u = -v

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c - b / c = (a - b) / c

Tactic:
by

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

Goal state before:
pp: ⊢ -1 * -1 = 1

Tactic:
by

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

Goal state before:
pp: u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1

Tactic:
by

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 : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Tactic:
by

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:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)

Tactic:
by

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

Goal state before:
pp: u : ℤˣ
⊢ u = 1 ∨ u = -1

Tactic:
by

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

Goal state before:
pp: u v : ℤˣ
⊢ u ≠ v ↔ u = -v

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a - a / 2 = a / 2

Tactic:
by

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:
by

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

Goal state before:
pp: u : ℤ
⊢ IsUnit u ↔ u.natAbs = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ IsUnit ↑n ↔ IsUnit n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a / 2 - a = -(a / 2)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
⊢ a ^ 0 = 1

Tactic:
by

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

Goal state before:
pp: a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℤ
⊢ a ^ (-n) = (a ^ n)⁻¹

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
by

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

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

Tactic:
by

Goal state after: