mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.single
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a : α} (h : r a b), motive a ⋯

pp: case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
·

Goal state after:
case tail.single
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a : α} (h : r a b), motive a ⋯
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
·

Goal state after:
case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a ⋯
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inl
α : Type u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b

pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y

pp: case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inl
α : Type u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

pp: case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂

Tactic:
·

Goal state after:
case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂

Tactic:
·

Goal state after:
case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : FaithfulSMul G α
a : G
ha : ∀ (a_1 : α), a • a_1 = a_1
⊢ ∀ (a_1 : α), a • a_1 = 1 • a_1

pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂

Tactic:
·

Goal state after:
case refine_1
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : FaithfulSMul G α
a : G
ha : ∀ (a_1 : α), a • a_1 = a_1
⊢ ∀ (a_1 : α), a • a_1 = 1 • a_1
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂

Tactic:
·

Goal state after:
case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

pp: case neg
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c

pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c

Tactic:
·

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c

Tactic:
·

Goal state after:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Tactic:
·

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Tactic:
·

Goal state after:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : α
c : γ
⊢ Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (inl i) c

Tactic:
by
  simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b

pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
·

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
·

Goal state after:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
·

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a

pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a

Tactic:
·

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a

Tactic:
·

Goal state after:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a

Tactic:
·

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
·

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
·

Goal state after:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
·

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : (fun x1 x2 ↦ x1 < x2) a b
⊢ Ordering.lt.Compares a b

pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : (fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : (fun x1 x2 ↦ x1 < x2) a b
⊢ Ordering.lt.Compares a b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : (fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : (fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.gt.Compares a b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b
Module: Mathlib.Tactic.GCongr.Core

Goal state before:
pp: declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
strict forGrw : Bool
cinfo : ConstantInfo
xs : Array Expr
type : Expr
c : Name
us✝ : List Level
i✝ i : Nat
h : i + 1 ≤ xs.size
⊢ i < xs.size

Tactic:
by lia

Goal state after:
Module: Mathlib.Tactic.GCongr.Core

Goal state before:
pp: declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
strict forGrw : Bool
cinfo : ConstantInfo
xs : Array Expr
type : Expr
c : Name
us✝ : List Level
i✝ i : Nat
h : i + 1 ≤ xs.size
⊢ i ≤ xs.size

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
·

Goal state after:
case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
·

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
·

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
·

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd