Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_aux (Arithmetization/ISigmaOne/Bit.lean)

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
haveI : M ⊧ₘ* 𝐈𝚺₁ := mod_iSigma_of_le (show 1 ≤ m from Fact.out)
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : ∃ s < exp a, ∀ i < a, P i → i ∈ s :=
  ⟨under a, pred_lt_self_of_pos (by simp), fun i hi _ ↦ by simpa [mem_under_iff] using hi⟩
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
this : ∃ s < exp a, ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
this : ∃ s < exp a, ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases this with ⟨s, hsn, hs⟩
State after:
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : (Γ.alt, m)-Predicate (fun s : M ↦ ∀ i < a, P i → i ∈ s) := by
  apply Definable.ball_lt₀; simp; apply Definable.imp <;> definability
State after:
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ (t' : M) := by
  simpa using least_number_h (L := ℒₒᵣ) Γ.alt m this hs
State after:
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
this : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
case intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
this : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases this with ⟨t, ht, t_minimal⟩
State after:
case intro.intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
case intro.intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have t_le_s : t ≤ s := not_lt.mp (by
  intro lt
  rcases t_minimal s lt with ⟨i, hin, hi, his⟩
  exact his (hs i hin hi))
State after:
case intro.intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
case intro.intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
have : ∀ i < a, i ∈ t → P i := by
  intro i _ hit
  by_contra Hi
  have : ∃ j < a, P j ∧ (j ∈ t → j = i) := by
    simpa [not_imp_not] using t_minimal (bitRemove i t) (bitRemove_lt_of_mem hit)
  rcases this with ⟨j, hjn, Hj, hm⟩
  rcases hm (ht j hjn Hj); contradiction
State after:
case intro.intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
this : ∀ i < a, i ∈ t → P i
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

State before:
case intro.intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
this : ∀ i < a, i ∈ t → P i
⊢ ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
Tactic:
exact ⟨t, lt_of_le_of_lt t_le_s hsn, fun i hi ↦ ⟨this i hi, ht i hi⟩⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
⊢ 0 < exp a
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
i : M
hi : i < a
x✝ : P i
⊢ i ∈ under a
Tactic:
simpa [mem_under_iff] using hi
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
Tactic:
apply Definable.ball_lt₀
State after:
case hf
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ DefinableBoundedFunction ℒₒᵣ (Γ.alt.coe, m) fun v => a

case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0

State before:
case hf
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ DefinableBoundedFunction ℒₒᵣ (Γ.alt.coe, m) fun v => a

case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0
Tactic:
simp
State after:
case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0

State before:
case h
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
⊢ Definable ℒₒᵣ (Γ.alt.coe, m) fun w => P (w 0) → w 0 ∈ (fun x => w x.succ) 0
Tactic:
apply Definable.imp <;> definability
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
⊢ ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
Tactic:
simpa using least_number_h (L := ℒₒᵣ) Γ.alt m this hs
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
⊢ ¬s < t
Tactic:
intro lt
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
⊢ False

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
⊢ False
Tactic:
rcases t_minimal s lt with ⟨i, hin, hi, his⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
i : M
hin : i < a
hi : P i
his : i ∉ s
⊢ False

State before:
case intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
i : M
hin : i < a
hi : P i
his : i ∉ s
⊢ False
Tactic:
exact his (hs i hin hi)
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
⊢ ∀ i < a, i ∈ t → P i
Tactic:
intro i _ hit
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
⊢ P i

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
⊢ P i
Tactic:
by_contra Hi
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
⊢ False

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
⊢ False
Tactic:
have : ∃ j < a, P j ∧ (j ∈ t → j = i) := by
  simpa [not_imp_not] using t_minimal (bitRemove i t) (bitRemove_lt_of_mem hit)
State after:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
this : ∃ j < a, P j ∧ (j ∈ t → j = i)
⊢ False

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝¹ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this✝ : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
this : ∃ j < a, P j ∧ (j ∈ t → j = i)
⊢ False
Tactic:
rcases this with ⟨j, hjn, Hj, hm⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
j : M
hjn : j < a
Hj : P j
hm : j ∈ t → j = i
⊢ False

State before:
case intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
j : M
hjn : j < a
Hj : P j
hm : j ∈ t → j = i
⊢ False
Tactic:
rcases hm (ht j hjn Hj)
State after:
case intro.intro.intro.refl
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
hjn : i < a
Hj : P i
hm : i ∈ t → i = i
⊢ False

State before:
case intro.intro.intro.refl
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
hjn : i < a
Hj : P i
hm : i ∈ t → i = i
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
t_le_s : t ≤ s
i : M
a✝ : i < a
hit : i ∈ t
Hi : ¬P i
⊢ ∃ j < a, P j ∧ (j ∈ t → j = i)
Tactic:
simpa [not_imp_not] using t_minimal (bitRemove i t) (bitRemove_lt_of_mem hit)
State after:
no goals