mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.Basic

Goal state before:
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.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
Module: Mathlib.Data.Fin.Basic

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

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

Tactic:
·

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = (↑↑u - ↑↑v) % ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:
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 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
Module: Mathlib.Data.Fin.Basic

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

Tactic:
·

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i

pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
·

Goal state after:
case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i
Module: Mathlib.Data.Fin.Basic

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

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

Tactic:
·

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

Goal state before:
pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
·

Goal state after:
case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)
Module: Mathlib.Data.Fin.Basic

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

Tactic:
·

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : 2 < n
⊢ n ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #s.attach

pp: case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #t

Tactic:
·

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #s.attach
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : 0 ≠ i ∧ 0 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
·

Goal state after:
case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : 0 ≠ i ∧ 0 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
·

Goal state after:
case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
·

Goal state after:
case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ 1 < n

Tactic:
by lia

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

Goal state before:
pp: case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #t

Tactic:
·

Goal state after:
case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #t
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
·

Goal state after:
case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ 2 < n

Tactic:
by lia

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

Goal state before:
pp: case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ b ∈ t

pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
·

Goal state after:
case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ b ∈ t
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n✝ m n : ℕ
i j : Fin n
hij : i < j
⊢ n - ↑i ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
·

Goal state after:
case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
rwa [Fin.le_iff_val_le_val, Fin.val_one, Nat.one_le_iff_ne_zero, val_ne_zero_iff]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ succ 0 = 1

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
⊢ succ 0 = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ succ 1 = 2

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
⊢ succ 1 = 2
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑(castLE h ((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩)) = ↑i

Tactic:
exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

pp: case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
·

Goal state after:
case zero
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
⊢ n ≤ n + 1

Tactic:
by lia

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
t : Finset β
f : ↥∅ → ↥t
hf : Injective f
⊢ #∅ ≤ #t

pp: case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
t : Finset β
f : ↥∅ → ↥t
hf : Injective f
⊢ #∅ ≤ #t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.hf
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.MapsTo f' ↑s ↑t

pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.InjOn f' ↑s

Tactic:
·

Goal state after:
case inr.hf
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.MapsTo f' ↑s ↑t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.InjOn f' ↑s

Tactic:
·

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.InjOn f' ↑s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

pp: case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
·

Goal state after:
case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
·

Goal state after:
case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_1
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
h : (fun x1 x2 ↦ x1 < x2) i 0
⊢ r (f i) (f 0)

pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x1 x2 ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun x1 x2 ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)

Tactic:
·

Goal state after:
case mpr.refine_1
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
h : (fun x1 x2 ↦ x1 < x2) i 0
⊢ r (f i) (f 0)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x1 x2 ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun x1 x2 ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)

Tactic:
·

Goal state after:
case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x1 x2 ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun x1 x2 ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ i.castPred hi = j

Tactic:
simp_rw [h, castPred_castSucc]

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

Goal state before:
pp: case mpr.refine_2.inl
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i = ↑j.castSucc
⊢ r (f i) (f j.succ)

pp: case mpr.refine_2.inr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i < ↑j.castSucc
⊢ r (f i) (f j.succ)

Tactic:
·

Goal state after:
case mpr.refine_2.inl
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i = ↑j.castSucc
⊢ r (f i) (f j.succ)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2.inr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i < ↑j.castSucc
⊢ r (f i) (f j.succ)

Tactic:
·

Goal state after:
case mpr.refine_2.inr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i < ↑j.castSucc
⊢ r (f i) (f j.succ)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: i : Fin 2
hi : i ≠ 0
⊢ i = 1

Tactic:
by lia

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

Goal state before:
pp: case zero
⊢ ↑(-1) = 0

pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
·

Goal state after:
case zero
⊢ ↑(-1) = 0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case zero
a b : Fin (0 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
·

Goal state after:
case zero
a b : Fin (0 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ castPred 1 ⋯ = 1

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
⊢ castPred 1 ⋯ = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ ↑i + 1 < n

Tactic:
by lia

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

Goal state before:
pp: n m : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero (OfNat.ofNat m)
⊢ m < n + m

Tactic:
simpa using! zero_lt_of_ne_zero (NeZero.ne n)

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case last
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

pp: case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Tactic:
·

Goal state after:
case last
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Tactic:
·

Goal state after:
case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
a : Fin (n + 1)
hb : a ≠ last n
h : a ≤ a
⊢ ↑(a.castPred ⋯ - a.castPred hb) = ↑(a - a) - 1

pp: case inr
n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
h' : a < b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
·

Goal state after:
case inl
n : ℕ
a : Fin (n + 1)
hb : a ≠ last n
h : a ≤ a
⊢ ↑(a.castPred ⋯ - a.castPred hb) = ↑(a - a) - 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i ≠ p

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p

Tactic:
·

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i ≠ p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p

Tactic:
·

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : j.castSucc < p
hij : i.castSucc = j.castSucc
⊢ i = j

pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
·

Goal state after:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : j.castSucc < p
hij : i.castSucc = j.castSucc
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
·

Goal state after:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Tactic:
rw [hij] at hi

Goal state after:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
·

Goal state after:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
·

Goal state after:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0

pp: case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a

Tactic:
·

Goal state after:
case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
·

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
·

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
·

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : #s < #t + #u
⊢ (t ∩ u).Nonempty

Tactic:
contrapose! hstu
  calc
    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, hstu]
    _ ≤ #s := by gcongr; exact union_subset hts hus

Goal state after: