-- Mathlib/Data/DFinsupp/WellFounded.lean
theorem Lex.acc_single (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFounded (s i))
    [DecidableEq ι] {i : ι} (hi : Acc (rᶜ ⊓ (· ≠ ·)) i) :
    ∀ a, Acc (DFinsupp.Lex r s) (single i a)

Proof state:
case pos.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
hj : i ∈ x.support
⊢ Acc (DFinsupp.Lex r s) (single i (x i))

Tactic:
exact ha _ hs

Result:
no goals

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
⊢ (fun x => Acc (DFinsupp.Lex r s) (single i x)) a

Tactic:
refine Acc.intro _ fun x ↦ ?_

Result:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
⊢ DFinsupp.Lex r s x (single i a) → Acc (DFinsupp.Lex r s) x

Proof state:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : i = k
hs : s k (x k) (Eq.recOn hik a)
⊢ Acc (DFinsupp.Lex r s) x

case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : ¬i = k
hs : s k (x k) 0
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
swap

Result:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : ¬i = k
hs : s k (x k) 0
⊢ Acc (DFinsupp.Lex r s) x

case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : i = k
hs : s k (x k) (Eq.recOn hik a)
⊢ Acc (DFinsupp.Lex r s) x

Proof state:
case pos.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : i ≠ j
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
by_cases h : r j i

Result:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : i ≠ j
h : r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : i ≠ j
h : ¬r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : i ≠ j
h : ¬r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
exact ih _ ⟨h, hij.symm⟩ _

Result:
no goals