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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ ⅟a * (a * b) = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible a
⊢ a * (⅟a * b) = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible b
⊢ a * ⅟b * b = a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
x✝ : Invertible b
⊢ a * b * ⅟b = a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ a * b = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ b * a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b✝ : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab } =
    { invOf := c, invOf_mul_self := invOf_mul_self✝, mul_invOf_self := hac }

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ si * s = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ s * si = 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : a * c = b * c
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : c * a = c * b
⊢ a = b

Tactic:
by

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

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ ⅟c * a = b ↔ a = c * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ c * a = b ↔ a = ⅟c * b

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌈a⌉₊| ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * ⅟c = b ↔ a = b * c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
⊢ f a = f b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * c = b ↔ a = b * ⅟c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a : α
inst✝ : Invertible a
⊢ a * ⅟a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a : α
inst✝ : Invertible a
⊢ ⅟a * a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ a * ⅟b = ⅟b * (b * a * ⅟b)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ ⅟b * (b * a * ⅟b) = ⅟b * (a * b * ⅟b)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ ⅟b * (a * b * ⅟b) = ⅟b * a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * a = ⅟b * (a * b * ⅟b)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * (a * b * ⅟b) = ⅟b * (b * a * ⅟b)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * (b * a * ⅟b) = a * ⅟b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ ⅟m ^ n * m ^ n = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ m ^ n * ⅟m ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) ↔ DenselyOrdered α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
⊢ DirectedOn (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) (Set.univ.pi d)

Tactic:
by

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

Goal state before:
pp: α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r * f r = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 ↦ r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 ↦ r₂ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x✝¹ z ∧ (fun p q ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x✝ z

Tactic:
by

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

Goal state before:
pp: α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f r * f ⅟r = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (f r)
⊢ f ⅟r = ⅟(f r)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : LinearOrder R
inst✝⁷ : FloorSemiring R
S : Type u_3
inst✝⁶ : Semiring S
inst✝⁵ : LinearOrder S
inst✝⁴ : FloorSemiring S
F : Type u_4
inst✝³ : FunLike F R S
inst✝² : RingHomClass F R S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
F : Type u_4
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℕ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithBot α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
⊢ FloorSemiring.floor = FloorSemiring.floor

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorSemiring R)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : MulZeroOneClass α
a : α
inst✝¹ : Nontrivial α
inst✝ : Invertible a
ha : a = 0
⊢ 0 = ⅟a * a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a * a⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a⁻¹ * a = 1

Tactic:
by

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

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

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

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Std.Trichotomous fun x1 x2 ↦ x1 < x2
x y : WithTop α
⊢ x < y ∨ x = y ∨ y < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : WithBot α
⊢ a < b ↔ ∃ x, ↑x < b ∧ a < ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
a : α
⊢ ⊥ < ↑a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * ↑x + y * x.neg = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * x.neg + y * ↑x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ ↑x * y + x.neg * y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ x.neg * y + ↑x * y = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x) * ↑y = ↑x * ↑(-y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x) * ↑(-y) = ↑x * ↑y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Mul R
inst✝² : One R
inst✝¹ : HasDistribNeg R
a : R
inst✝ : Invertible a
⊢ -⅟a * -a = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Mul R
inst✝² : One R
inst✝¹ : HasDistribNeg R
a : R
inst✝ : Invertible a
⊢ -a * -⅟a = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
inst✝² : HasDistribNeg R
a : R
inst✝¹ : Invertible a
inst✝ : Invertible (-a)
⊢ -a * -⅟a = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 * (1 - ⅟2) = 2 * ⅟2

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Tactic:
by

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

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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
⊢ -a = b + a * ⅟b * a ↔ -a = a * ⅟a * b + a * ⅟b * a

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x

Tactic:
by

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
h : -a = a * (⅟a * b + ⅟b * a)
⊢ -1 = ⅟a * b + ⅟b * a

Tactic:
by

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
h : -1 = ⅟a * b + ⅟b * a
⊢ -a = a * (⅟a * b + ⅟b * a)

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Tactic:
by

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 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b) ↔ 1 = 1 + ⅟b * a + (1 + ⅟a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x < y ↔ WithTop.ofDual y < x

Tactic:
by

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 + ⅟b * a + (1 + ⅟a * b) ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < WithBot.toDual y ↔ y < WithTop.ofDual x

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ WithBot.toDual x < WithBot.toDual y ↔ y < x

Tactic:
by

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)
⊢ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b) ↔ -2 + 1 = ⅟b * a + ⅟a * b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x < y ↔ WithTop.toDual y < x

Tactic:
by

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)
⊢ -2 + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < WithBot.ofDual y ↔ y < WithTop.toDual x

Tactic:
by

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 + 0 = ⅟b * a + ⅟a * b ↔ -1 = ⅟a * b + ⅟b * a

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_sub_invOf]

Goal state after: