mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)

Tactic:
;

Goal state after:
α : 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
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
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 + 1) * (a ^ (n + 2) + b ^ (n + 2)) = 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
;

Goal state after:
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 + 1) * (a ^ (n + 2) + b ^ (n + 2)) = 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
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✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ a = EquivLike.inv f a₁ * EquivLike.inv f a₂

Tactic:
← EquivLike.apply_eq_iff_eq f,

Goal state after:
α : 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✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ f a = f (EquivLike.inv f a₁ * EquivLike.inv f a₂)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case h
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ Commute 2 (a ^ 2 + b ^ 2)

Tactic:
;

Goal state after:
case h
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ Commute 2 (a ^ 2 + b ^ 2)
Module: Mathlib.Algebra.Ring.Divisibility.Basic

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ natAbs 1 = 1

Tactic:
;

Goal state after:
u : ℤˣ
⊢ natAbs 1 = 1
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
hn : Odd 0
⊢ False

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False

Tactic:
;

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False
Module: Mathlib.Algebra.Field.Basic

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

pp: case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
;

Goal state after:
case inl
K : Type u_1
inst✝ : DivisionRing K
⊢ 0⁻¹ = 0 ↔ 0 = -1 ∨ 0 = 0 ∨ 0 = 1

case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ ψ x ≤ ψ y

Tactic:
φψs.eq ys,

Goal state after:
case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ φ (ψ x)
⊢ ψ x ≤ ψ y
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
⊢ image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t

Tactic:
← image_uncurry_prod,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
⊢ uncurry f '' (s ∩ s') ×ˢ t = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Tactic:
← image_uncurry_prod,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ uncurry f '' s ×ˢ (t ∩ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
x✝ : δ
⊢ x✝ ∈ image2 f (g '' s) t ↔ x✝ ∈ image2 (fun a b ↦ f (g a) b) s t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
x✝ : δ
⊢ x✝ ∈ image2 f (g '' s) t ↔ x✝ ∈ image2 (fun a b ↦ f (g a) b) s t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
x✝ : δ
⊢ x✝ ∈ image2 f s (g '' t) ↔ x✝ ∈ image2 (fun a b ↦ f a (g b)) s t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
x✝ : δ
⊢ x✝ ∈ image2 f s (g '' t) ↔ x✝ ∈ image2 (fun a b ↦ f a (g b)) s t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image2 (fun a b ↦ f b a) t s = image2 g t s

Tactic:
by simp_rw [h_comm]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 (fun a b ↦ f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
exact image_image2_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * max |a| |b| ^ (0 - 1)

pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)

Tactic:
;

Goal state after:
case zero
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * max |a| |b| ^ (0 - 1)

case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
x✝ : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝ : α × β
⊢ uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
      (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯ (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
x✝ : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝ : α × β
⊢ uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
      (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯ (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
fst✝ : Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2
snd✝ : Antisymmetrization β fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α
a✝ : β
⊢ Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯
      (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
        (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
          Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
      Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
fst✝ : Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2
snd✝ : Antisymmetrization β fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α
a✝ : β
⊢ Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯
      (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
        (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
          Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
      Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝² : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α × β
b✝ : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝ : α × β
⊢ { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
          left_inv := ⋯, right_inv := ⋯ }
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝¹) ≤
      { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
          left_inv := ⋯, right_inv := ⋯ }
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝) ↔
    Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝¹ ≤
      Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝² : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α × β
b✝ : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝ : α × β
⊢ { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
          left_inv := ⋯, right_inv := ⋯ }
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝¹) ≤
      { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
          left_inv := ⋯, right_inv := ⋯ }
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝) ↔
    Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝¹ ≤
      Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
x✝ : α
⊢ x✝ ∈ ⇑e.symm '' s ↔ x✝ ∈ ⇑e ⁻¹' s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
x✝ : α
⊢ x✝ ∈ ⇑e.symm '' s ↔ x✝ ∈ ⇑e ⁻¹' s
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
a : ↑S
left✝ : a ∈ x
⊢ ↑a ∈ S

Tactic:
;

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
a : ↑S
left✝ : a ∈ x
⊢ ↑a ∈ S
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : ↑(𝒫 S)
y : α
⊢ y ∈ ↑((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) ((fun x ↦ Subtype.val ⁻¹' ↑x) x)) ↔ y ∈ ↑x

Tactic:
;

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : ↑(𝒫 S)
y : α
⊢ y ∈ ↑((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) ((fun x ↦ Subtype.val ⁻¹' ↑x) x)) ↔ y ∈ ↑x
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
x✝ : ↑S
⊢ x✝ ∈ (fun x ↦ Subtype.val ⁻¹' ↑x) ((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) x) ↔ x✝ ∈ x

Tactic:
;

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
x✝ : ↑S
⊢ x✝ ∈ (fun x ↦ Subtype.val ⁻¹' ↑x) ((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) x) ↔ x✝ ∈ x
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : β
x : α
h' : Sum.inl x = Sum.inr val✝
⊢ False

Tactic:
;

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : β
x : α
h' : Sum.inl x = Sum.inr val✝
⊢ False
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : α
x : β
h' : Sum.inr x = Sum.inl val✝
⊢ False

Tactic:
;

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : α
x : β
h' : Sum.inr x = Sum.inl val✝
⊢ False
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Iio 1 ↔ x✝ ∈ ∅

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Iio 1 ↔ x✝ ∈ ∅
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Iic a ⊂ Iic b
⊢ a < b

Tactic:
by
    obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h
    exact lt_of_le_not_ge (Iic_subset_Iic.mp ab) (fun h' ↦ ac (cb.trans h'))

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (Icc a b).Nonempty ↔ a ≤ b

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (Icc a b).Nonempty ↔ a ≤ b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (Ico a b).Nonempty ↔ a < b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
a b : α
inst✝ : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
a b : α
inst✝ : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Ici 1 ↔ x✝ ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Ici 1 ↔ x✝ ∈ univ
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x

Tactic:
simp [BddAbove, upperBounds, Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨w, hw, hzw⟩ := hc hz

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
w : α
hw : w ∈ s
hzw : z ≤ w
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ⊆ s ∧ {a} ⊆ s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ⊆ s ∧ {a} ⊆ s
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ ⇑f = ⇑g

Tactic:
← coe_toOrderEmbedding,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ ⇑f.toOrderEmbedding = ⇑g
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ ⇑f.toOrderEmbedding = ⇑g

Tactic:
← coe_toOrderEmbedding,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ ⇑f.toOrderEmbedding = ⇑g.toOrderEmbedding
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc x y)
⊢ x ≤ ↑z ∧ ↑z ≤ y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc x y)
⊢ x ≤ ↑z ∧ ↑z ≤ y
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc (e x) (e y))
⊢ e x ≤ ↑z ∧ ↑z ≤ e y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc (e x) (e y))
⊢ e x ≤ ↑z ∧ ↑z ≤ e y
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t

Tactic:
rcases le_total a b with h | h

Goal state after:
case inl
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : a ≤ b
⊢ min a b ∈ s ∪ t

case inr
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : b ≤ a
⊢ min a b ∈ s ∪ t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
⊢ False
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : ¬a ≤ b
contra : ¬c ≤ d
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : ¬a ≤ b
contra : ¬c ≤ d
⊢ False
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ univ
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : Nonempty ↑s
ht : Nonempty ↑t
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : Nonempty ↑s
ht : Nonempty ↑t
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d

Tactic:
;

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d

Tactic:
;

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x

Tactic:
;

Goal state after:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case hc
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ 0 < 2

Tactic:
;

Goal state after:
case hc
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ 0 < 2