-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_replicate {n : Nat} {a : α} :
    (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a

Proof state:
case succ.mpr.inr
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : R a a
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a)

Tactic:
exact ⟨fun _ => h, Or.inr h⟩

Result:
no goals

Proof state:
case succ.mp.intro.inr
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : R a a
⊢ n + 1 ≤ 1 ∨ R a a

Tactic:
right

Result:
case succ.mp.intro.inr.h
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : R a a
⊢ R a a

Proof state:
case succ.mp.intro.inr.h
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : R a a
⊢ R a a

Tactic:
exact h'

Result:
no goals

Proof state:
case succ.mp
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a) → n + 1 ≤ 1 ∨ R a a

Tactic:
rintro ⟨h, h' | h'⟩

Result:
case succ.mp.intro.inl
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
⊢ n + 1 ≤ 1 ∨ R a a

case succ.mp.intro.inr
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : R a a
⊢ n + 1 ≤ 1 ∨ R a a

Proof state:
case succ.mpr.inl
α : Type u_1
R : α → α → Prop
a : α
ih : Pairwise R (replicate 0 a) ↔ 0 ≤ 1 ∨ R a a
h : 0 + 1 ≤ 1
⊢ (¬0 = 0 → R a a) ∧ (0 ≤ 1 ∨ R a a)

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : ¬n = 0
⊢ n + 1 ≤ 1 ∨ R a a

Tactic:
right

Result:
case neg.h
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : ¬n = 0
⊢ R a a

Proof state:
case neg.h
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : ¬n = 0
⊢ R a a

Tactic:
exact h w

Result:
no goals

Proof state:
case succ
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ Pairwise R (replicate (n + 1) a) ↔ n + 1 ≤ 1 ∨ R a a

Tactic:
simp only [replicate_succ, pairwise_cons, mem_replicate, ne_eq, and_imp,
  forall_eq_apply_imp_iff, ih]

Result:
case succ
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a) ↔ n + 1 ≤ 1 ∨ R a a

Proof state:
case succ
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a) ↔ n + 1 ≤ 1 ∨ R a a

Tactic:
constructor

Result:
case succ.mp
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a) → n + 1 ≤ 1 ∨ R a a

case succ.mpr
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ n + 1 ≤ 1 ∨ R a a → (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a)

Proof state:
case pos.h
α : Type u_1
R : α → α → Prop
a : α
ih : Pairwise R (replicate 0 a) ↔ 0 ≤ 1 ∨ R a a
h : ¬0 = 0 → R a a
h' : 0 ≤ 1
⊢ 0 + 1 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case succ.mpr
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
⊢ n + 1 ≤ 1 ∨ R a a → (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a)

Tactic:
rintro (h | h)

Result:
case succ.mpr.inl
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : n + 1 ≤ 1
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a)

case succ.mpr.inr
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : R a a
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a)

Proof state:
case succ.mp.intro.inl
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
⊢ n + 1 ≤ 1 ∨ R a a

Tactic:
by_cases w : n = 0

Result:
case pos
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : n = 0
⊢ n + 1 ≤ 1 ∨ R a a

case neg
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : ¬n = 0
⊢ n + 1 ≤ 1 ∨ R a a

Proof state:
case pos
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : n = 0
⊢ n + 1 ≤ 1 ∨ R a a

Tactic:
left

Result:
case pos.h
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : n = 0
⊢ n + 1 ≤ 1

Proof state:
case succ.mpr.inl
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : n + 1 ≤ 1
⊢ (¬n = 0 → R a a) ∧ (n ≤ 1 ∨ R a a)

Tactic:
obtain rfl := eq_zero_of_le_zero (le_of_lt_succ h)

Result:
case succ.mpr.inl
α : Type u_1
R : α → α → Prop
a : α
ih : Pairwise R (replicate 0 a) ↔ 0 ≤ 1 ∨ R a a
h : 0 + 1 ≤ 1
⊢ (¬0 = 0 → R a a) ∧ (0 ≤ 1 ∨ R a a)

Proof state:
case zero
α : Type u_1
R : α → α → Prop
a : α
⊢ Pairwise R (replicate 0 a) ↔ 0 ≤ 1 ∨ R a a

Tactic:
simp

Result:
no goals

Proof state:
case pos.h
α : Type u_1
R : α → α → Prop
a : α
n : Nat
ih : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
h : ¬n = 0 → R a a
h' : n ≤ 1
w : n = 0
⊢ n + 1 ≤ 1

Tactic:
subst w

Result:
case pos.h
α : Type u_1
R : α → α → Prop
a : α
ih : Pairwise R (replicate 0 a) ↔ 0 ≤ 1 ∨ R a a
h : ¬0 = 0 → R a a
h' : 0 ≤ 1
⊢ 0 + 1 ≤ 1