mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mp
α : Type u_1
x y : α
⊢ [x] <:+: [y] → x = y

pp: case mpr
α : Type u_1
x y : α
⊢ x = y → [x] <:+: [y]

Tactic:
·

Goal state after:
case mp
α : Type u_1
x y : α
⊢ [x] <:+: [y] → x = y
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mpr
α : Type u_1
x y : α
⊢ x = y → [x] <:+: [y]

Tactic:
·

Goal state after:
case mpr
α : Type u_1
x y : α
⊢ x = y → [x] <:+: [y]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mp
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] → head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

pp: case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]

Tactic:
·

Goal state after:
case mp
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] → head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]

Tactic:
·

Goal state after:
case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
x✝¹ : α
x✝ : Multiset α
h : x✝.ndunion t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u
⊢ (x✝¹ ::ₘ x✝).ndunion t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u

Tactic:
by simp only [cons_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h,
        and_assoc]

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ s.ndunion t = s.dedup + t

Tactic:
induction s, t using Quot.induction_on₂

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) =
    dedup (Quot.mk (⇑(isSetoid α)) a✝) + Quot.mk (⇑(isSetoid α)) b✝
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndunion t = t

Tactic:
induction s, t using Quot.induction_on₂

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) b✝
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndinter t = s

Tactic:
induction s, t using Quot.induction_on₂

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndinter (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) a✝
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case cons.inl
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs

pp: case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs

Tactic:
·

Goal state after:
case cons.inl
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs

Tactic:
·

Goal state after:
case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x ↦ x ∈ t₁) s ∪ filter (fun x ↦ x ∉ t₁) s = s

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x ↦ x ∈ t₁) s ∪ filter (fun x ↦ x ∉ t₁) s = s
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ = ∅ ↔ IsEmpty α

Tactic:
contrapose!; exact univ_nonempty_iff

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ x ∈ t

pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ x ∈ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
simp [Finset.subset_iff, Set.subset_def]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ s = ↑Finset.univ ↔ s = univ

Tactic:
coe_univ

Goal state after:
α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ s = univ ↔ s = univ
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq γ
g : β → γ
⊢ image g ∘ image f = image (g ∘ f)

Tactic:
by ext s; simp [image_image]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i ↦ f i) (range n)

pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i ↦ f i) (range n) → a ∈ Set.range f

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i ↦ f i) (range n)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i ↦ f i) (range n) → a ∈ Set.range f

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i ↦ f i) (range n) → a ∈ Set.range f
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ c = 0 ∨ 0 < c

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inl
a : Int
ha : 0 ≤ a
b : Int
hc : 0 ≤ 0
⊢ a * (b / 0) ≤ a * b / 0

pp: case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c

Tactic:
·

Goal state after:
case inl
a : Int
ha : 0 ≤ a
b : Int
hc : 0 ≤ 0
⊢ a * (b / 0) ≤ a * b / 0
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c

Tactic:
·

Goal state after:
case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t

pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))

Tactic:
range_add_one,

Goal state after:
case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ insert (k + 1) (range (k + 1)) \ {0} = image Nat.succ (insert k (range k))
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
·

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
·

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
·

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
·

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: n m : ℕ
p : Fin (n + 1)
hmn : n ≤ m
⊢ n + (m - n) = m

Tactic:
by lia

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ

pp: case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s → ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

pp: case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ (∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a) → a ∈ s

Tactic:
·

Goal state after:
case mp
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s → ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)

pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
·

Goal state after:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)

pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
·

Goal state after:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
·

Goal state after:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
·

Goal state after:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯

pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
·

Goal state after:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
·

Goal state after:
case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
·

Goal state after:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
·

Goal state after:
case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v

pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n

Tactic:
·

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h : j ≤ i
⊢ i = j

pp: n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i = j

Tactic:
·

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h : j ≤ i
⊢ i = j
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case inr.inl
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h✝ : j ≤ i
h : j < i
⊢ i = j

pp: case inr.inr
n : ℕ
j : Fin (n + 1)
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
hij : j.predAbove = j.predAbove
h : j ≤ j
⊢ j = j

Tactic:
·

Goal state after:
case inr.inl
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h✝ : j ≤ i
h : j < i
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n

Tactic:
·

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n