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₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0 * (0⁻¹ * b)

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
ha : a ≠ 0
⊢ b ≤ a * (a⁻¹ * b)

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0 * (0⁻¹ * b)

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
ha : a ≠ 0
⊢ b ≤ a * (a⁻¹ * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
ha : a ≠ 0
⊢ a⁻¹ * (a * b) ≤ b

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0⁻¹ * (0 * b) ≤ b

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
ha : a ≠ 0
⊢ a⁻¹ * (a * b) ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
ha : a ≠ 0
⊢ b ≤ a⁻¹ * (a * b)

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : b ≤ 0
⊢ b ≤ 0⁻¹ * (0 * b)

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : b ≤ 0
ha : a ≠ 0
⊢ b ≤ a⁻¹ * (a * b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0 * 0⁻¹ ≤ a

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
hb : b ≠ 0
⊢ a * b * b⁻¹ ≤ a

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0 * 0⁻¹ ≤ a

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
hb : b ≠ 0
⊢ a * b * b⁻¹ ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : a ≤ 0
⊢ a ≤ a * 0 * 0⁻¹

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : a ≤ 0
hb : b ≠ 0
⊢ a ≤ a * b * b⁻¹

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : a ≤ 0
⊢ a ≤ a * 0 * 0⁻¹

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : a ≤ 0
hb : b ≠ 0
⊢ a ≤ a * b * b⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0⁻¹ * 0 ≤ a

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
hb : b ≠ 0
⊢ a * b⁻¹ * b ≤ a

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0⁻¹ * 0 ≤ a

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
hb : b ≠ 0
⊢ a * b⁻¹ * b ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : a ≤ 0
⊢ a ≤ a * 0⁻¹ * 0

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : a ≤ 0
hb : b ≠ 0
⊢ a ≤ a * b⁻¹ * b

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : a ≤ 0
⊢ a ≤ a * 0⁻¹ * 0

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : a ≤ 0
hb : b ≠ 0
⊢ a ≤ a * b⁻¹ * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
⊢ 0 / 0 ≤ 1

pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a / a ≤ 1

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
⊢ 0 / 0 ≤ 1

case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a / a ≤ 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
⊢ 0⁻¹ * 0 ≤ 1

pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ * a ≤ 1

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
⊢ 0⁻¹ * 0 ≤ 1

case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ * a ≤ 1
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : p ↑y
⊢ Sum.inl ⟨↑x, h✝¹⟩ = Sum.inl ⟨↑y, h✝⟩ → x = y

pp: case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : ¬p ↑y
⊢ False → x = y

pp: case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : p ↑y
⊢ False → x = y

pp: case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : ¬p ↑y
⊢ Sum.inr ⟨↑x, ⋯⟩ = Sum.inr ⟨↑y, ⋯⟩ → x = y

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : p ↑y
⊢ Sum.inl ⟨↑x, h✝¹⟩ = Sum.inl ⟨↑y, h✝⟩ → x = y

case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : p ↑x
h✝ : ¬p ↑y
⊢ False → x = y

case pos
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : p ↑y
⊢ False → x = y

case neg
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x y : { x // p x ∨ q x }
h✝¹ : ¬p ↑x
h✝ : ¬p ↑y
⊢ Sum.inr ⟨↑x, ⋯⟩ = Sum.inr ⟨↑y, ⋯⟩ → x = y
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

pp: case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b

Tactic:
<;>

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

Tactic:
apply mul_self_nonneg

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

Goal state before:
pp: case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b

Tactic:
apply mul_self_nonneg

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
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ (Embedding.quotientOut α) ⟦a✝⟧ ≈ a✝

pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ (Embedding.quotientOut α) ⟦b✝⟧ ≈ b✝

Tactic:
<;>

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ (Embedding.quotientOut α) ⟦a✝⟧ ≈ a✝

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ (Embedding.quotientOut α) ⟦b✝⟧ ≈ b✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inl c)

pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inr d)

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inl c)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inr d)

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inl c)

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inr d)

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inl c)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inr d)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inl c)

pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inr d)

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inl c)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inr d)

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inl c)

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inr d)

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inl c)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inr d)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝) b

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝) b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝) b

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝) b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ

Tactic:
apply div_le_iff_le_mul.2
    convert! mabs_mul_le (a / b) b
    rw [div_mul_cancel]

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

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
hb : 1 ≤ a
⊢ |a|ₘ = a

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
b : G
hb : 1 ≤ b
⊢ |b⁻¹|ₘ = b

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
hb : 1 ≤ a
⊢ |a|ₘ = a

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
b : G
hb : 1 ≤ b
⊢ |b⁻¹|ₘ = b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : 1 ≤ a
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : 1 ≤ a
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
ha : 1 ≤ a
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
ha : a ≤ 1
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
ha : 1 ≤ a
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
ha : a ≤ 1
⊢ |a|ₘ = max a 1 * max a⁻¹ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

pp: case inr
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : a = b⁻¹
⊢ |a|ₘ = |b|ₘ

Tactic:
<;>

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

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

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

pp: case inr
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
b : α
h : ||b|ₘ⁻¹|ₘ = |b|ₘ
⊢ |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹

Tactic:
<;>

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

case inr
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
b : α
h : ||b|ₘ⁻¹|ₘ = |b|ₘ
⊢ |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

pp: case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
<;>

Goal state after:
case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case mp
n : ℕ
⊢ IsSquare ↑n → IsSquare n

pp: case mpr
n : ℕ
⊢ IsSquare n → IsSquare ↑n

Tactic:
<;>

Goal state after:
case mp
n : ℕ
⊢ IsSquare ↑n → IsSquare n

case mpr
n : ℕ
⊢ IsSquare n → IsSquare ↑n
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: case e'_3
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 = ↑1

pp: case e'_4
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)

pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ n + 1

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 = ↑1

case e'_4
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)

α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ n + 1
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: case zero
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ 0 < ↑0 ↔ 0 < 0

pp: case succ
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n✝ : ℕ
⊢ 0 < ↑(n✝ + 1) ↔ 0 < n✝ + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ 0 < ↑0 ↔ 0 < 0

case succ
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n✝ : ℕ
⊢ 0 < ↑(n✝ + 1) ↔ 0 < n✝ + 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ x.xgcd y = (x.gcdA y, x.gcdB y)

Tactic:
by
  unfold gcdA gcdB; constructor

Goal state after: