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

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • y • z = x₁ • y • z

Tactic:
]

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

Goal state before:
pp: α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ x • y = x • y

Tactic:
]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • y = x • y

Tactic:
]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ x • y = x • y

Tactic:
]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ x • (y * z) = x • (y * z)

Tactic:
]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ y * (z * x • 1) = y * (z * x • 1)

Tactic:
]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ m • n • q = m • n • q

Tactic:
]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ m • p • q = m • p • q

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ c = c

Tactic:
]

Goal state after:
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ (∃ a, IsEmpty β) ↔ ∃ x, IsEmpty β

Tactic:
]

Goal state after:
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ Nonempty α ∧ IsEmpty β ↔ Nonempty α ∧ IsEmpty β

Tactic:
]

Goal state after:
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ BiTotal R ↔ IsEmpty α

Tactic:
by
  simp only [BiTotal, leftTotal_iff_isEmpty_left, rightTotal_empty, and_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map g₂ (Option.map f₂ (some a)) = Option.map g₂ (Option.map f₂ (some a))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a ⋯)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a ⋯)
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : γ → α → β
x : α → β
i : Option γ
y : α
⊢ i.elim x f y = i.elim x f y

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : Option α
f : α → β
⊢ x = none ↔ x = none

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
⊢ (∃ a, x = some a ∧ f a = b) ↔ ∃ a, x = some a ∧ f a = b

Tactic:
]

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

Goal state before:
pp: I : Type u
α : Type u_4
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ x = x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Defs.PartialOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a = b
⊢ b ≤ b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d

Tactic:
by
      inhabit β
      exact congr_arg Prod.snd (h (default, d))

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (if a ≤ b then a else b)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (if a ≤ b then a else b)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (if a ≤ b then b else a)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (if a ≤ b then b else a)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ if a ≤ b then a else b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ if a ≤ b then a else b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min b (min a c) = min b (min a c)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a < b ↔ a < b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a = b ↔ a = b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b < a ↔ b < a

Tactic:
]

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ ((x : α) → (fun x ↦ β') x) = (α → β')

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Type u_1
a b : ULift α
h : a = b
⊢ b.down = b.down

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Sort u_1
a b : PLift α
h : a = b
⊢ b.down = b.down

Tactic:
]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a ≤ b ∨ b ≤ a ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f (f a b) c

Tactic:
comm.comm _ c,

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f a b)
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then a else b) = if a < b then a else b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then a else b) = if a < b then a else b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then b else a) = if a < b then b else a

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then b else a) = if a < b then b else a
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ (le✝ a b ∧ ¬le✝ b a) = (le✝ a b ∧ ¬le✝ b a)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x < y ∨ x = y ↔ x < y ∨ x = y

Tactic:
]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝² : Preorder β
inst✝¹ : LE α
inst✝ : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x✝¹ x✝ : α
⊢ f x✝¹ ≤ f x✝ ∧ ¬f x✝ ≤ f x✝¹ ↔ f x✝¹ ≤ f x✝ ∧ ¬f x✝ ≤ f x✝¹

Tactic:
]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap.swap < (b, a).swap ↔ x < (a, b)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap.swap < (b, a).swap ↔ x < (a, b)
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < c

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < c
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ c < b i

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ c < b i
Module: Mathlib.Tactic.Push

Goal state before:
pp: p q : Prop
⊢ p ∧ ¬q ∨ ¬p ∧ q ↔ p ∧ ¬q ∨ ¬p ∧ q

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ (∃ b, a < b) ↔ a < ⊤

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ (∃ b, a < b) ↔ a < ⊤
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ↑⊥ ↔ ↑x = ↑⊥

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
]

Goal state after:
a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)

Tactic:
]

Goal state after:
a b : ℤ
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 ↔ ¬(0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b)
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)

Tactic:
]

Goal state after:
a b : ℤ
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ ¬(0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: a b c : ℕ
⊢ a / c / b = a / c / b

Tactic:
]

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

Goal state before:
pp: x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ a / x = x ^ a / x

Tactic:
]

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

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : x = y
⊢ x = y

Tactic:
]

Goal state after:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : x = y
⊢ x = y
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : next (leRecOn hnm (fun {k} ↦ next) x) = next (leRecOn hnm (fun {k} ↦ next) y)
⊢ x = y

Tactic:
]

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : next (leRecOn hnm (fun {k} ↦ next) x) = next (leRecOn hnm (fun {k} ↦ next) y)
⊢ x = y
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
x : C n
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ next (leRecOn ?step.h1 (fun {k} ↦ next) x) = next (leRecOn hnm (fun {k} ↦ next) x)

pp: case step.h1
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ n ≤ m✝

Tactic:
]

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

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)

Tactic:
]

Goal state after:
case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 ≤ 0 ^ (b + 1)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b

Tactic:
]

Goal state after:
case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ (2 + 2) * k ^ 2 = 2 ^ 2 * k ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
⊢ ¬0 = 1

pp: m n : ℕ
⊢ 1 < 2

Tactic:
]

Goal state after:
m n : ℕ
⊢ ¬0 = 1

m n : ℕ
⊢ 1 < 2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n m : ℕ
⊢ ↑m * 2 ≤ ↑n ↔ ↑m * 2 ≤ ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ le_succ_of_le ?h1 refl = le_succ_of_le ⋯ refl

pp: case h1
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ n ≤ n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case refl
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
⊢ leRec refl le_succ_of_le ⋯ = leRec refl (fun x h ↦ le_succ_of_le h) hnm

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case step
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ le_succ_of_le ⋯ (leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk) =
    le_succ_of_le ⋯ (leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ?step.h1)

pp: case step.h1
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ m ≤ m✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
⊢ leRec (le_succ_of_le ⋯ refl) (fun x h ih ↦ le_succ_of_le ⋯ ih) h2 =
    leRec (le_succ_of_le ⋯ refl) (fun x h ↦ le_succ_of_le ⋯) h2

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ self = self

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) ?h1 (fun i hi ↦ of_succ i ⋯)
      (of_succ n ⋯ self) =
    leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) mn (fun x x_1 ↦ of_succ x ⋯)
      (of_succ n ⋯ self)

pp: case h1
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ m ≤ n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ (fun {motive} of_succ self ↦ self) (fun i hi ↦ of_succ i ⋯) (of_succ n ⋯ self) = of_succ n ⋯ self

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case refl
m n k : ℕ
hmn : m ≤ n
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ = decreasingInduction (fun x x_1 ↦ of_succ x ⋯) self hmn

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) hnk)
      hmn =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯)
      (decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) ?step.mn) hmn

pp: case step.mn
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ n ≤ m✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ of_succ m ⋯ (decreasingInduction of_succ self ?hnk) = of_succ m smn (decreasingInduction of_succ self smn)

pp: case hnk
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ m + 1 ≤ n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n✝ ∣ n ↔ n✝ ∣ n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ n✝ ↔ n ∣ n✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P x
⊢ P x

Tactic:
]

Goal state after:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P x
⊢ P x
Module: Mathlib.Order.Compare

Goal state before:
pp: o o' : Ordering
⊢ o = o'.swap ↔ o = o'.swap

Tactic:
]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a < b
hab : lt.Compares a b
⊢ lt.Compares a b

Tactic:
]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a < b
hab : lt.Compares a b
⊢ lt.Compares a b
Module: Mathlib.Data.Set.Operations

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : ↑(range f)
⊢ ↑⟨f a, ⋯⟩ = ↑⟨↑b, ⋯⟩ ↔ f a = ↑⟨↑b, ⋯⟩

Tactic:
]

Goal state after: